Commit 2020-09-24 08:37 ba8fa0f1

View on Github →

feat(logic/embedding): use simps (#4169) Some lemmas are slightly reformulated, and have a worse name. But they are (almost) never typed explicitly, since they are simp lemmas (even the occurrences in other files probably came from squeeze_simp).

Estimated changes

Modified src/algebra/big_operators/basic.lean

Modified src/algebra/big_operators/nat_antidiagonal.lean

Modified src/data/finset/nat_antidiagonal.lean

Modified src/logic/embedding.lean

modified theorem equiv.refl_to_embedding

deleted theorem equiv.to_embedding_coe_fn

deleted theorem function.embedding.coe_image

deleted theorem function.embedding.coe_sigma_map

deleted theorem function.embedding.coe_sigma_mk

deleted theorem function.embedding.refl_apply

modified def function.embedding.sigma_map

modified def function.embedding.sigma_mk

deleted theorem function.embedding.trans_apply

deleted theorem mul_left_embedding_apply

deleted theorem mul_right_embedding_apply

deleted theorem set.coe_embedding_of_subset_apply

modified def set.embedding_of_subset

deleted theorem set.embedding_of_subset_apply_mk

Modified src/measure_theory/haar_measure.lean