Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-19 02:29 5993b90e

View on Github →

feat(tactic/simps): use new options in library (#7095)

Estimated changes

Modified src/data/equiv/local_equiv.lean

modified def equiv.to_local_equiv

added def mfld_cfg

Modified src/geometry/manifold/charted_space.lean

Modified src/geometry/manifold/smooth_manifold_with_corners.lean

Modified src/order/order_iso_nat.lean

Modified src/order/rel_iso.lean

deleted theorem order_embedding.coe_subtype

modified def order_embedding.subtype

modified theorem rel_embedding.coe_trans

deleted theorem rel_embedding.refl_apply

added def rel_embedding.simps.apply

deleted theorem rel_hom.comp_apply

deleted theorem rel_hom.id_apply

deleted theorem rel_iso.of_surjective_coe

deleted theorem rel_iso.refl_apply

added def rel_iso.simps.apply

added def rel_iso.simps.symm_apply

deleted theorem rel_iso.trans_apply

Modified src/topology/homeomorph.lean

deleted theorem homeomorph.coe_prod_punit

deleted theorem homeomorph.coe_refl

added def homeomorph.simps.apply

added def homeomorph.simps.symm_apply

Modified src/topology/local_homeomorph.lean

deleted theorem homeomorph.to_local_homeomorph_coe

deleted theorem homeomorph.to_local_homeomorph_source

deleted theorem homeomorph.to_local_homeomorph_target

deleted theorem local_homeomorph.of_set_coe

deleted theorem local_homeomorph.of_set_source

deleted theorem local_homeomorph.of_set_target

deleted theorem local_homeomorph.piecewise_coe

deleted theorem local_homeomorph.piecewise_to_local_equiv

deleted theorem local_homeomorph.prod_coe

deleted theorem local_homeomorph.prod_coe_symm

deleted theorem local_homeomorph.prod_source

deleted theorem local_homeomorph.prod_target

deleted theorem local_homeomorph.prod_to_local_equiv

deleted theorem local_homeomorph.refl_coe

deleted theorem local_homeomorph.refl_source

deleted theorem local_homeomorph.refl_target

deleted theorem local_homeomorph.restr_coe

deleted theorem local_homeomorph.restr_coe_symm

deleted theorem local_homeomorph.restr_source

deleted theorem local_homeomorph.restr_target

added def local_homeomorph.simps.apply

added def local_homeomorph.simps.symm_apply

deleted theorem local_homeomorph.to_homeomorph_coe

deleted theorem local_homeomorph.to_homeomorph_symm_coe

deleted theorem open_embedding.source

deleted theorem open_embedding.target

deleted theorem open_embedding.to_local_homeomorph_coe