Golf

SphereEversion/ToMathlib/Topology/Misc.lean

@@ -19,10 +19,7 @@ theorem Function.LeftInverse.mem_preimage_iff (hfg : LeftInverse g f) {s : Set 
 -- TODO: move to Data.Set.Basic
 theorem Function.LeftInverse.image_eq (hfg : LeftInverse g f) (s : Set α) :
     f '' s = range f ∩ g ⁻¹' s := by
-  ext x
-  constructor
-  · rintro ⟨x, hx, rfl⟩; exact ⟨mem_range_self x, hfg.mem_preimage_iff.mpr hx⟩
-  · rintro ⟨⟨x, rfl⟩, b⟩; exact mem_image_of_mem f (hfg.mem_preimage_iff.mp b)
+  rw [inter_comm, ← image_preimage_eq_inter_range, hfg.preimage_preimage]
 
 theorem Function.LeftInverse.isOpenMap {f : α → β} {g : β → α} (hfg : LeftInverse g f)
     (hf : IsOpen (range f)) (hg : ContinuousOn g (range f)) : IsOpenMap f := fun U hU ↦ by