From 99b70d9eb8cb3d88184f37754368833b128453de Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Wed, 8 Sep 2021 14:01:03 +0000
Subject: [PATCH] feat(data/(fin)set/basic): `image` and `mem` lemmas (#9031)

I rename `set.mem_image_of_injective` to `function.injective.mem_set_image_iff` to allow dot notation and fit the new  `function.injective.mem_finset_image_iff`.
---
 src/data/finset/basic.lean                      |  9 +++++++++
 src/data/set/basic.lean                         | 17 +++++++++++++----
 src/data/set/function.lean                      |  4 ++--
 src/data/set/lattice.lean                       |  8 ++++++++
 .../affine_space/independent.lean               |  2 +-
 5 files changed, 33 insertions(+), 7 deletions(-)

diff --git a/src/data/finset/basic.lean b/src/data/finset/basic.lean
index 1f8a5239871a1..d173b567add4a 100644
--- a/src/data/finset/basic.lean
+++ b/src/data/finset/basic.lean
@@ -1906,6 +1906,15 @@ by simp only [mem_def, image_val, mem_erase_dup, multiset.mem_map, exists_prop]
 theorem mem_image_of_mem (f : α → β) {a} {s : finset α} (h : a ∈ s) : f a ∈ s.image f :=
 mem_image.2 ⟨_, h, rfl⟩
 
+lemma _root_.function.injective.mem_finset_image {f : α → β} (hf : function.injective f)
+  {s : finset α} {x : α} :
+  f x ∈ s.image f ↔ x ∈ s :=
+begin
+  refine ⟨λ h, _, finset.mem_image_of_mem f⟩,
+  obtain ⟨y, hy, heq⟩ := mem_image.1 h,
+  exact hf heq ▸ hy,
+end
+
 lemma filter_mem_image_eq_image (f : α → β) (s : finset α) (t : finset β) (h : ∀ x ∈ s, f x ∈ t) :
   t.filter (λ y, y ∈ s.image f) = s.image f :=
 by { ext, rw [mem_filter, mem_image],
diff --git a/src/data/set/basic.lean b/src/data/set/basic.lean
index 69a76cd0a3dd5..354ef6371b4ac 100644
--- a/src/data/set/basic.lean
+++ b/src/data/set/basic.lean
@@ -1272,11 +1272,9 @@ lemma image_eta (f : α → β) : f '' s = (λ x, f x) '' s := rfl
 theorem mem_image_of_mem (f : α → β) {x : α} {a : set α} (h : x ∈ a) : f x ∈ f '' a :=
 ⟨_, h, rfl⟩
 
-theorem mem_image_of_injective {f : α → β} {a : α} {s : set α} (hf : injective f) :
+theorem _root_.function.injective.mem_set_image {f : α → β} (hf : injective f) {s : set α} {a : α} :
   f a ∈ f '' s ↔ a ∈ s :=
-iff.intro
-  (assume ⟨b, hb, eq⟩, (hf eq) ▸ hb)
-  (assume h, mem_image_of_mem _ h)
+⟨λ ⟨b, hb, eq⟩, (hf eq) ▸ hb, mem_image_of_mem f⟩
 
 theorem ball_image_iff {f : α → β} {s : set α} {p : β → Prop} :
   (∀ y ∈ f '' s, p y) ↔ (∀ x ∈ s, p (f x)) :=
@@ -2072,6 +2070,13 @@ set.ext $ assume a,
 ⟨assume ⟨⟨a', ha'⟩, in_s, h_eq⟩, h_eq ▸ ⟨ha', in_s⟩,
   assume ⟨ha, in_s⟩, ⟨⟨a, ha⟩, in_s, rfl⟩⟩
 
+@[simp] lemma coe_image_of_subset {s t : set α} (h : t ⊆ s) : coe '' {x : ↥s | ↑x ∈ t} = t :=
+begin
+  ext x,
+  rw set.mem_image,
+  exact ⟨λ ⟨x', hx', hx⟩, hx ▸ hx', λ hx, ⟨⟨x, h hx⟩, hx, rfl⟩⟩,
+end
+
 lemma range_coe {s : set α} :
   range (coe : s → α) = s :=
 by { rw ← set.image_univ, simp [-set.image_univ, coe_image] }
@@ -2809,4 +2814,8 @@ lemma eq_univ_of_nonempty {s : set α} : s.nonempty → s = univ :=
 lemma set_cases {p : set α → Prop} (h0 : p ∅) (h1 : p univ) (s) : p s :=
 s.eq_empty_or_nonempty.elim (λ h, h.symm ▸ h0) $ λ h, (eq_univ_of_nonempty h).symm ▸ h1
 
+lemma mem_iff_nonempty {α : Type*} [subsingleton α] {s : set α} {x : α} :
+  x ∈ s ↔ s.nonempty :=
+⟨λ hx, ⟨x, hx⟩, λ ⟨y, hy⟩, subsingleton.elim y x ▸ hy⟩
+
 end subsingleton
diff --git a/src/data/set/function.lean b/src/data/set/function.lean
index fba2409c4e0aa..98d57403328fa 100644
--- a/src/data/set/function.lean
+++ b/src/data/set/function.lean
@@ -603,7 +603,7 @@ lemma preimage_inv_fun_of_mem [n : nonempty α] {f : α → β} (hf : injective
 begin
   ext x,
   rcases em (x ∈ range f) with ⟨a, rfl⟩|hx,
-  { simp [left_inverse_inv_fun hf _, mem_image_of_injective hf] },
+  { simp [left_inverse_inv_fun hf _, hf.mem_set_image] },
   { simp [mem_preimage, inv_fun_neg hx, h, hx] }
 end
 
@@ -612,7 +612,7 @@ lemma preimage_inv_fun_of_not_mem [n : nonempty α] {f : α → β} (hf : inject
 begin
   ext x,
   rcases em (x ∈ range f) with ⟨a, rfl⟩|hx,
-  { rw [mem_preimage, left_inverse_inv_fun hf, mem_image_of_injective hf] },
+  { rw [mem_preimage, left_inverse_inv_fun hf, hf.mem_set_image] },
   { have : x ∉ f '' s, from λ h', hx (image_subset_range _ _ h'),
     simp only [mem_preimage, inv_fun_neg hx, h, this] },
 end
diff --git a/src/data/set/lattice.lean b/src/data/set/lattice.lean
index d13a1a684e7e0..a4c564b1fda63 100644
--- a/src/data/set/lattice.lean
+++ b/src/data/set/lattice.lean
@@ -1478,6 +1478,14 @@ lemma preimage_eq_empty_iff {f : α → β} {s : set β} : disjoint s (range f)
 ⟨preimage_eq_empty,
   λ h, by { simp [eq_empty_iff_forall_not_mem, set.disjoint_iff_inter_eq_empty] at h ⊢, finish }⟩
 
+lemma disjoint_iff_subset_compl_right :
+  disjoint s t ↔ s ⊆ tᶜ :=
+disjoint_left
+
+lemma disjoint_iff_subset_compl_left :
+  disjoint s t ↔ t ⊆ sᶜ :=
+disjoint_right
+
 end set
 
 end disjoint
diff --git a/src/linear_algebra/affine_space/independent.lean b/src/linear_algebra/affine_space/independent.lean
index bd9df333f6fa0..1122cceb6c31b 100644
--- a/src/linear_algebra/affine_space/independent.lean
+++ b/src/linear_algebra/affine_space/independent.lean
@@ -137,7 +137,7 @@ begin
   split,
   { intro h,
     have hv : ∀ v : (λ p, (p -ᵥ p₁ : V)) '' (s \ {p₁}), (v : V) +ᵥ p₁ ∈ s \ {p₁} :=
-      λ v, (set.mem_image_of_injective (vsub_left_injective p₁)).1
+      λ v, (vsub_left_injective p₁).mem_set_image.1
              ((vadd_vsub (v : V) p₁).symm ▸ v.property),
     let f : (λ p : P, (p -ᵥ p₁ : V)) '' (s \ {p₁}) → {x : s // x ≠ ⟨p₁, hp₁⟩} :=
       λ x, ⟨⟨(x : V) +ᵥ p₁, set.mem_of_mem_diff (hv x)⟩,