From ca5987fa8b58c8860990f8a95acd88fb958ca3c2 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Sun, 15 Aug 2021 19:29:26 +0000
Subject: [PATCH] chore(data/set/basic): add `image_image` and
 `preimage_preimage` to `function.left_inverse` (#8688)

---
 src/data/equiv/basic.lean | 13 ++++---------
 src/data/set/basic.lean   |  8 ++++++++
 2 files changed, 12 insertions(+), 9 deletions(-)

diff --git a/src/data/equiv/basic.lean b/src/data/equiv/basic.lean
index c015591ad7212..9c6d6a987065a 100644
--- a/src/data/equiv/basic.lean
+++ b/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
diff --git a/src/data/set/basic.lean b/src/data/set/basic.lean
index 1e20c0ca4a5fd..9c63cbd9216dc 100644
--- a/src/data/set/basic.lean
+++ b/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