feat: make Set.mem_image_equiv a simp lemma (#5644)

Not certain about this one. It's useful for me (experimenting with `UnivLE`), and arguably this is a better simp normal form since `''` is relatively hard to reason about, but I'm not certain how it interacts with everything else. Let's see what CI says. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · Jul 1, 2023 · b856949 · b856949
1 parent a9b3aae
commit b856949
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/Mathlib/CategoryTheory/Subobject/Lattice.lean b/Mathlib/CategoryTheory/Subobject/Lattice.lean
@@ -707,7 +707,7 @@ theorem sSup_le {A : C} (s : Set (Subobject A)) (f : Subobject A) (k : ∀ g ∈
     · refine' Sigma.desc _
       rintro ⟨g, m⟩
       refine' underlying.map (homOfLE (k _ _))
-      simpa [symm_apply_mem_iff_mem_image] using m
+      simpa using m
     · ext
       dsimp [smallCoproductDesc]
       simp

diff --git a/Mathlib/Logic/Equiv/Set.lean b/Mathlib/Logic/Equiv/Set.lean
@@ -44,6 +44,7 @@ protected theorem image_eq_preimage {α β} (e : α ≃ β) (s : Set α) : e ''
   Set.ext fun _ => mem_image_iff_of_inverse e.left_inv e.right_inv
 #align equiv.image_eq_preimage Equiv.image_eq_preimage
 
+@[simp 1001]
 theorem _root_.Set.mem_image_equiv {α β} {S : Set α} {f : α ≃ β} {x : β} :
     x ∈ f '' S ↔ f.symm x ∈ S :=
   Set.ext_iff.mp (f.image_eq_preimage S) x