chore(data/set/basic): add image_image and preimage_preimage to `…

…function.left_inverse` (#8688)

src/data/equiv/basic.lean

@@ -373,16 +373,11 @@ protected lemma subset_image {α β} (e : α ≃ β) (s : set α) (t : set β) :
 by rw [set.image_subset_iff, e.image_eq_preimage]
 
 @[simp] lemma symm_image_image {α β} (e : α ≃ β) (s : set α) : e.symm '' (e '' s) = s :=
-by { rw [← set.image_comp], simp }
+e.left_inverse_symm.image_image s
 
 lemma eq_image_iff_symm_image_eq {α β} (e : α ≃ β) (s : set α) (t : set β) :
   t = e '' s ↔ e.symm '' t = s :=
-begin
-  refine (injective.eq_iff' _ _).symm,
-  { rw set.image_injective,
-    exact (equiv.symm e).injective },
-  { exact equiv.symm_image_image _ _ }
-end
+(e.symm.injective.image_injective.eq_iff' (e.symm_image_image s)).symm
 
 @[simp] lemma image_symm_image {α β} (e : α ≃ β) (s : set β) : e '' (e.symm '' s) = s :=
 e.symm.symm_image_image s
@@ -399,11 +394,11 @@ set.image_compl_eq f.bijective
 
 @[simp] lemma symm_preimage_preimage {α β} (e : α ≃ β) (s : set β) :
   e.symm ⁻¹' (e ⁻¹' s) = s :=
-by ext; simp
+e.right_inverse_symm.preimage_preimage s
 
 @[simp] lemma preimage_symm_preimage {α β} (e : α ≃ β) (s : set α) :
   e ⁻¹' (e.symm ⁻¹' s) = s :=
-by ext; simp
+e.left_inverse_symm.preimage_preimage s
 
 @[simp] lemma preimage_subset {α β} (e : α ≃ β) (s t : set β) : e ⁻¹' s ⊆ e ⁻¹' t ↔ s ⊆ t :=
 e.surjective.preimage_subset_preimage_iff

src/data/set/basic.lean

@@ -2013,6 +2013,14 @@ lemma injective.exists_unique_of_mem_range (hf : injective f) {b : β} (hb : b 
   ∃! a, f a = b :=
 hf.mem_range_iff_exists_unique.mp hb
 
+lemma left_inverse.image_image {g : β → α} (h : left_inverse g f) (s : set α) :
+  g '' (f '' s) = s :=
+by rw [← image_comp, h.comp_eq_id, image_id]
+
+lemma left_inverse.preimage_preimage {g : β → α} (h : left_inverse g f) (s : set α) :
+  f ⁻¹' (g ⁻¹' s) = s :=
+by rw [← preimage_comp, h.comp_eq_id, preimage_id]
+
 end function
 open function