Commit 2022-09-07 12:54 fff99b92

View on Github →

feat(Mathlib/Logic/Equiv/LocalEquiv): add the mfld_set_tac tactic (#331) This PR adds the mfld_set_tac tactic. This tactic relies on a custom simp set which mostly contain lemmas about advanced math that is not yet in mathlib4. In the test file, we have created stubs of a random subset of the various definitions and lemmas it needs; this will need to be revisited during the port.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Init/Set.lean

added theorem Set.ext

Created Mathlib/Logic/Equiv/LocalEquiv.lean

Created Mathlib/Logic/Equiv/MfldSimpsAttr.lean

Modified Mathlib/Mathport/Syntax.lean

Created test/MfldSetTac.lean

added theorem LocalEquiv.coe_trans

added theorem LocalEquiv.coe_trans_symm

added theorem LocalEquiv.left_inv

added theorem LocalEquiv.map_source

added def LocalEquiv.symm

added theorem LocalEquiv.symm_source

added def LocalEquiv.trans

added theorem LocalEquiv.trans_source

added structure LocalEquiv

added theorem LocalHomeomorph.coe_coe

added theorem LocalHomeomorph.coe_coe_symm

added theorem LocalHomeomorph.left_inv

added def LocalHomeomorph.symm

added theorem LocalHomeomorph.symm_to_LocalEquiv

added structure LocalHomeomorph

added theorem ModelWithCorners.left_inv

added def ModelWithCorners.symm

added theorem ModelWithCorners.to_local_equiv_coe

added theorem ModelWithCorners.to_local_equiv_coe_symm

added structure ModelWithCorners

added theorem Set.inter_univ

added theorem Set.mem_inter_eq

added theorem Set.mem_preimage

added theorem Set.mem_set_of_eq

added def Set.preimage

added theorem Set.preimage_inter

added theorem Set.preimage_univ