From dca1393efc490921fe8e9289a3130aba52ee11ea Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Fri, 16 Oct 2020 00:56:13 +0000
Subject: [PATCH] feat(data/equiv/basic): add `equiv.set.compl` (#4630)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Given an equivalence between two sets `e₀ : s ≃ t`, the set of
`e : α ≃ β` that agree with `e₀` on `s` is equivalent to `sᶜ ≃ tᶜ`.

Also add a bunch of lemmas to `data/set/function`; some of them are
used in the definition of `equiv.set.compl`.

Co-authored-by: Chris Hughes <chrishughes24@gmail.com>
---
 src/data/equiv/basic.lean  | 68 +++++++++++++++++++++++++++++++++++++-
 src/data/set/function.lean | 58 ++++++++++++++++++++++++++++----
 2 files changed, 119 insertions(+), 7 deletions(-)

diff --git a/src/data/equiv/basic.lean b/src/data/equiv/basic.lean
index 5f5269416287d..9f8148b5fac7b 100644
--- a/src/data/equiv/basic.lean
+++ b/src/data/equiv/basic.lean
@@ -640,6 +640,14 @@ def sigma_preimage_equiv {α β : Type*} (f : α → β) :
 @[simp] lemma sigma_preimage_equiv_symm_apply_snd_fst {α β : Type*} (f : α → β) (a : α) :
   ((sigma_preimage_equiv f).symm a).2.1 = a := rfl
 
+/-- A set `s` in `α × β` is equivalent to the sigma-type `Σ x, {y | (x, y) ∈ s}`. -/
+def set_prod_equiv_sigma {α β : Type*} (s : set (α × β)) :
+  s ≃ Σ x : α, {y | (x, y) ∈ s} :=
+{ to_fun := λ x, ⟨x.1.1, x.1.2, by simp⟩,
+  inv_fun := λ x, ⟨(x.1, x.2.1), x.2.2⟩,
+  left_inv := λ ⟨⟨x, y⟩, h⟩, rfl,
+  right_inv := λ ⟨x, y, h⟩, rfl }
+
 end
 
 section sum_compl
@@ -1029,6 +1037,16 @@ def subtype_congr {p : α → Prop} {q : β → Prop}
  λ ⟨x, h⟩, subtype.ext_val $ by simp,
  λ ⟨y, h⟩, subtype.ext_val $ by simp⟩
 
+@[simp] lemma subtype_congr_apply {p : α → Prop} {q : β → Prop} (e : α ≃ β)
+  (h : ∀ (a : α), p a ↔ q (e a)) (x : {x // p x}) :
+  e.subtype_congr h x = ⟨e x, (h _).1 x.2⟩ :=
+rfl
+
+@[simp] lemma subtype_congr_symm_apply {p : α → Prop} {q : β → Prop} (e : α ≃ β)
+  (h : ∀ (a : α), p a ↔ q (e a)) (y : {y // q y}) :
+  (e.subtype_congr h).symm y = ⟨e.symm y, (h _).2 $ (e.apply_symm_apply y).symm ▸ y.2⟩ :=
+rfl
+
 /-- If two predicates `p` and `q` are pointwise equivalent, then `{x // p x}` is equivalent to
 `{x // q x}`. -/
 def subtype_congr_right {p q : α → Prop} (e : ∀x, p x ↔ q x) : {x // p x} ≃ {x // q x} :=
@@ -1248,6 +1266,14 @@ lemma union_apply_right {α} {s t : set α} [decidable_pred (λ x, x ∈ s)] (H
   {a : (s ∪ t : set α)} (ha : ↑a ∈ t) : equiv.set.union H a = sum.inr ⟨a, ha⟩ :=
 dif_neg $ λ h, H ⟨h, ha⟩
 
+@[simp] lemma union_symm_apply_left {α} {s t : set α} [decidable_pred (λ x, x ∈ s)] (H : s ∩ t ⊆ ∅)
+  (a : s) : (equiv.set.union H).symm (sum.inl a) = ⟨a, subset_union_left _ _ a.2⟩ :=
+rfl
+
+@[simp] lemma union_symm_apply_right {α} {s t : set α} [decidable_pred (λ x, x ∈ s)] (H : s ∩ t ⊆ ∅)
+  (a : t) : (equiv.set.union H).symm (sum.inr a) = ⟨a, subset_union_right _ _ a.2⟩ :=
+rfl
+
 -- TODO: Any reason to use the same universe?
 /-- A singleton set is equivalent to a `punit` type. -/
 protected def singleton {α} (a : α) : ({a} : set α) ≃ punit.{u} :=
@@ -1313,6 +1339,14 @@ lemma sum_compl_symm_apply_of_not_mem {α : Type u} {s : set α} [decidable_pred
 have ↑(⟨x, or.inr hx⟩ : (s ∪ sᶜ : set α)) ∈ sᶜ, from hx,
 by { rw [equiv.set.sum_compl], simpa using set.union_apply_right _ this }
 
+@[simp] lemma sum_compl_symm_apply {α : Type*} {s : set α} [decidable_pred s] {x : s} :
+  (equiv.set.sum_compl s).symm x = sum.inl x :=
+by cases x with x hx; exact set.sum_compl_symm_apply_of_mem hx
+
+@[simp] lemma sum_compl_symm_apply_compl {α : Type*} {s : set α}
+  [decidable_pred s] {x : sᶜ} : (equiv.set.sum_compl s).symm x = sum.inr x :=
+by cases x with x hx; exact set.sum_compl_symm_apply_of_not_mem hx
+
 /-- `sum_diff_subset s t` is the natural equivalence between
 `s ⊕ (t \ s)` and `t`, where `s` and `t` are two sets. -/
 protected def sum_diff_subset {α} {s t : set α} (h : s ⊆ t) [decidable_pred s] :
@@ -1361,6 +1395,38 @@ calc  (s ∪ t : set α) ⊕ (s ∩ t : set α)
   end
 ... ≃ s ⊕ t : by { rw (_ : t \ s ∪ s ∩ t = t), rw [union_comm, inter_comm, inter_union_diff] }
 
+/-- Given an equivalence `e₀` between sets `s : set α` and `t : set β`, the set of equivalences
+`e : α ≃ β` such that `e ↑x = ↑(e₀ x)` for each `x : s` is equivalent to the set of equivalences
+between `sᶜ` and `tᶜ`. -/
+protected def compl {α β : Type*} {s : set α} {t : set β} [decidable_pred s] [decidable_pred t]
+  (e₀ : s ≃ t) : {e : α ≃ β // ∀ x : s, e x = e₀ x} ≃ ((sᶜ : set α) ≃ (tᶜ : set β)) :=
+{ to_fun := λ e, subtype_congr e
+    (λ a, not_congr $ iff.symm $ maps_to.mem_iff
+      (maps_to_iff_exists_map_subtype.2 ⟨e₀, e.2⟩)
+      (surj_on.maps_to_compl (surj_on_iff_exists_map_subtype.2
+        ⟨t, e₀, subset.refl t, e₀.surjective, e.2⟩) e.1.injective)),
+  inv_fun := λ e₁,
+    subtype.mk
+      (calc α ≃ s ⊕ (sᶜ : set α) : (set.sum_compl s).symm
+          ... ≃ t ⊕ (tᶜ : set β) : e₀.sum_congr e₁
+          ... ≃ β : set.sum_compl t)
+      (λ x, by simp only [sum.map_inl, trans_apply, sum_congr_apply,
+        set.sum_compl_apply_inl, set.sum_compl_symm_apply]),
+  left_inv := λ e,
+    begin
+      ext x,
+      by_cases hx : x ∈ s,
+      { simp only [set.sum_compl_symm_apply_of_mem hx, ←e.prop ⟨x, hx⟩,
+          sum.map_inl, sum_congr_apply, trans_apply,
+          subtype.coe_mk, set.sum_compl_apply_inl] },
+      { simp only [set.sum_compl_symm_apply_of_not_mem hx, sum.map_inr,
+          subtype_congr_apply, set.sum_compl_apply_inr, trans_apply,
+          sum_congr_apply, subtype.coe_mk] },
+    end,
+  right_inv := λ e, equiv.ext $ λ x, by simp only [sum.map_inr, subtype_congr_apply,
+    set.sum_compl_apply_inr, function.comp_app, sum_congr_apply, equiv.coe_trans,
+    subtype.coe_eta, subtype.coe_mk, set.sum_compl_symm_apply_compl] }
+
 /-- The set product of two sets is equivalent to the type product of their coercions to types. -/
 protected def prod {α β} (s : set α) (t : set β) :
   s.prod t ≃ s × t :=
@@ -1377,7 +1443,7 @@ protected noncomputable def image_of_inj_on {α β} (f : α → β) (s : set α)
 
 /-- If `f` is an injective function, then `s` is equivalent to `f '' s`. -/
 protected noncomputable def image {α β} (f : α → β) (s : set α) (H : injective f) : s ≃ (f '' s) :=
-equiv.set.image_of_inj_on f s (λ x y hx hy hxy, H hxy)
+equiv.set.image_of_inj_on f s (H.inj_on s)
 
 @[simp] theorem image_apply {α β} (f : α → β) (s : set α) (H : injective f) (a h) :
   set.image f s H ⟨a, h⟩ = ⟨f a, mem_image_of_mem _ h⟩ := rfl
diff --git a/src/data/set/function.lean b/src/data/set/function.lean
index cf368bedab214..4e7d57eb3c017 100644
--- a/src/data/set/function.lean
+++ b/src/data/set/function.lean
@@ -106,6 +106,10 @@ subtype.map f h
 @[simp] lemma maps_to.coe_restrict_apply (h : maps_to f s t) (x : s) :
   (h.restrict f s t x : β) = f x := rfl
 
+lemma maps_to_iff_exists_map_subtype : maps_to f s t ↔ ∃ g : s → t, ∀ x : s, f x = g x :=
+⟨λ h, ⟨h.restrict f s t, λ _, rfl⟩,
+  λ ⟨g, hg⟩ x hx, by { erw [hg ⟨x, hx⟩], apply subtype.coe_prop }⟩
+
 theorem maps_to' : maps_to f s t ↔ f '' s ⊆ t :=
 image_subset_iff.symm
 
@@ -165,9 +169,16 @@ theorem maps_to_image (f : α → β) (s : set α) : maps_to f s (f '' s) := by
 
 theorem maps_to_preimage (f : α → β) (t : set β) : maps_to f (f ⁻¹' t) t := subset.refl _
 
-theorem maps_to_range (f : set α) (s : set α) : maps_to f s (range f) :=
+theorem maps_to_range (f : α → β) (s : set α) : maps_to f s (range f) :=
 (maps_to_image f s).mono (subset.refl s) (image_subset_range _ _)
 
+theorem surjective_maps_to_image_restrict (f : α → β) (s : set α) :
+  surjective ((maps_to_image f s).restrict f s (f '' s)) :=
+λ ⟨y, x, hs, hxy⟩, ⟨⟨x, hs⟩, subtype.ext hxy⟩
+
+theorem maps_to.mem_iff (h : maps_to f s t) (hc : maps_to f sᶜ tᶜ) {x} : f x ∈ t ↔ x ∈ s :=
+⟨λ ht, by_contra $ λ hs, hc hs ht, λ hx, h hx⟩
+
 /-! ### Injectivity on a set -/
 
 /-- `f` is injective on `a` if the restriction of `f` to `a` is injective. -/
@@ -202,6 +213,11 @@ theorem inj_on_insert {f : α → β} {s : set α} {a : α} (has : a ∉ s) :
 lemma injective_iff_inj_on_univ : injective f ↔ inj_on f univ :=
 ⟨λ h x hx y hy hxy, h hxy, λ h _ _ heq, h trivial trivial heq⟩
 
+lemma inj_on_of_injective (h : injective f) (s : set α) : inj_on f s :=
+λ x hx y hy hxy, h hxy
+
+alias inj_on_of_injective ← function.injective.inj_on
+
 theorem inj_on.comp (hg : inj_on g t) (hf: inj_on f s) (h : maps_to f s t) :
   inj_on (g ∘ f) s :=
 λ x hx y hy heq, hf hx hy $ hg (h hx) (h hy) heq
@@ -229,6 +245,12 @@ lemma inj_on_preimage {B : set (set β)} (hB : B ⊆ powerset (range f)) :
 theorem surj_on.subset_range (h : surj_on f s t) : t ⊆ range f :=
 subset.trans h $ image_subset_range f s
 
+lemma surj_on_iff_exists_map_subtype :
+  surj_on f s t ↔ ∃ (t' : set β) (g : s → t'), t ⊆ t' ∧ surjective g ∧ ∀ x : s, f x = g x :=
+⟨λ h, ⟨_, (maps_to_image f s).restrict f s _, h, surjective_maps_to_image_restrict _ _, λ _, rfl⟩,
+  λ ⟨t', g, htt', hg, hfg⟩ y hy, let ⟨x, hx⟩ := hg ⟨y, htt' hy⟩ in
+    ⟨x, x.2, by rw [hfg, hx, subtype.coe_mk]⟩⟩
+
 theorem surj_on_empty (f : α → β) (s : set α) : surj_on f s ∅ := empty_subset _
 
 theorem surj_on.comap_nonempty (h : surj_on f s t) (ht : t.nonempty) : s.nonempty :=
@@ -280,6 +302,12 @@ lemma surj_on.image_eq_of_maps_to (h₁ : surj_on f s t) (h₂ : maps_to f s t)
   f '' s = t :=
 eq_of_subset_of_subset h₂.image_subset h₁
 
+lemma surj_on.maps_to_compl (h : surj_on f s t) (h' : injective f) : maps_to f sᶜ tᶜ :=
+λ x hs ht, let ⟨x', hx', heq⟩ := h ht in hs $ h' heq ▸ hx'
+
+lemma maps_to.surj_on_compl (h : maps_to f s t) (h' : surjective f) : surj_on f sᶜ tᶜ :=
+h'.forall.2 $ λ x ht, mem_image_of_mem _ $ λ hs, ht (h hs)
+
 /-! ### Bijectivity -/
 
 /-- `f` is bijective from `s` to `t` if `f` is injective on `s` and `f '' s = t`. -/
@@ -332,10 +360,13 @@ bij_on.mk (hg.maps_to.comp hf.maps_to) (hg.inj_on.comp hf.inj_on hf.maps_to)
 lemma bijective_iff_bij_on_univ : bijective f ↔ bij_on f univ univ :=
 iff.intro
 (λ h, let ⟨inj, surj⟩ := h in
-⟨maps_to_univ f _, iff.mp injective_iff_inj_on_univ inj, iff.mp surjective_iff_surj_on_univ surj⟩)
+⟨maps_to_univ f _, inj.inj_on _, iff.mp surjective_iff_surj_on_univ surj⟩)
 (λ h, let ⟨map, inj, surj⟩ := h in
 ⟨iff.mpr injective_iff_inj_on_univ inj, iff.mpr surjective_iff_surj_on_univ surj⟩)
 
+lemma bij_on.compl (hst : bij_on f s t) (hf : bijective f) : bij_on f sᶜ tᶜ :=
+⟨hst.surj_on.maps_to_compl hf.1, hf.1.inj_on _, hst.maps_to.surj_on_compl hf.2⟩
+
 /-! ### left inverse -/
 
 /-- `g` is a left inverse to `f` on `a` means that `g (f x) = x` for all `x ∈ a`. -/
@@ -361,9 +392,12 @@ calc
   ...   = f₁' (f x₂) : congr_arg f₁' heq
   ...   = x₂       : h h₂
 
-theorem left_inv_on.surj_on (h : left_inv_on f₁' f s) (hf : maps_to f s t) : surj_on f₁' t s :=
+theorem left_inv_on.surj_on (h : left_inv_on f' f s) (hf : maps_to f s t) : surj_on f' t s :=
 λ x hx, ⟨f x, hf hx, h hx⟩
 
+theorem left_inv_on.maps_to (h : left_inv_on f' f s) (hf : surj_on f s t) : maps_to f' t s :=
+λ y hy, let ⟨x, hs, hx⟩ := hf hy in by rwa [← hx, h hs]
+
 theorem left_inv_on.comp (hf' : left_inv_on f' f s) (hg' : left_inv_on g' g t) (hf : maps_to f s t) :
   left_inv_on (f' ∘ g') (g ∘ f) s :=
 λ x h,
@@ -371,6 +405,9 @@ calc
   (f' ∘ g') ((g ∘ f) x) = f' (f x) : congr_arg f' (hg' (hf h))
   ...                   = x        : hf' h
 
+theorem left_inv_on.mono (hf : left_inv_on f' f s) (ht : s₁ ⊆ s) : left_inv_on f' f s₁ :=
+λ x hx, hf (ht hx)
+
 /-! ### Right inverse -/
 
 /-- `g` is a right inverse to `f` on `b` if `f (g x) = x` for all `x ∈ b`. -/
@@ -393,10 +430,16 @@ theorem right_inv_on.surj_on (hf : right_inv_on f' f t) (hf' : maps_to f' t s) :
   surj_on f s t :=
 hf.surj_on hf'
 
+theorem right_inv_on.maps_to (h : right_inv_on f' f t) (hf : surj_on f' t s) : maps_to f s t :=
+h.maps_to hf
+
 theorem right_inv_on.comp (hf : right_inv_on f' f t) (hg : right_inv_on g' g p)
   (g'pt : maps_to g' p t) : right_inv_on (f' ∘ g') (g ∘ f) p :=
 hg.comp hf g'pt
 
+theorem right_inv_on.mono (hf : right_inv_on f' f t) (ht : t₁ ⊆ t) : right_inv_on f' f t₁ :=
+hf.mono ht
+
 theorem inj_on.right_inv_on_of_left_inv_on (hf : inj_on f s) (hf' : left_inv_on f f' t)
     (h₁ : maps_to f s t) (h₂ : maps_to f' t s) :
   right_inv_on f f' s :=
@@ -420,6 +463,12 @@ left_inv_on g f s ∧ right_inv_on g f t
 
 lemma inv_on.symm (h : inv_on f' f s t) : inv_on f f' t s := ⟨h.right, h.left⟩
 
+lemma inv_on.mono (h : inv_on f' f s t) (hs : s₁ ⊆ s) (ht : t₁ ⊆ t) : inv_on f' f s₁ t₁ :=
+⟨h.1.mono hs, h.2.mono ht⟩
+
+/-- If functions `f'` and `f` are inverse on `s` and `t`, `f` maps `s` into `t`, and `f'` maps `t`
+into `s`, then `f` is a bijection between `s` and `t`. The `maps_to` arguments can be deduced from
+`surj_on` statements using `left_inv_on.maps_to` and `right_inv_on.maps_to`. -/
 theorem inv_on.bij_on (h : inv_on f' f s t) (hf : maps_to f s t) (hf' : maps_to f' t s) :
   bij_on f s t :=
 ⟨hf, h.left.inj_on, h.right.surj_on hf'⟩
@@ -567,9 +616,6 @@ open set
 
 variables {fa : α → α} {fb : β → β} {f : α → β} {g : β → γ} {s t : set α}
 
-lemma injective.inj_on (h : injective f) (s : set α) : s.inj_on f :=
-λ _ _ _ _ heq, h heq
-
 lemma injective.comp_inj_on (hg : injective g) (hf : s.inj_on f) : s.inj_on (g ∘ f) :=
 (hg.inj_on univ).comp hf (maps_to_univ _ _)