From 84582d2872fb47c0c17eec7382dc097c9ec7137a Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Fri, 25 Nov 2022 02:14:15 +0000
Subject: [PATCH] feat(data/quot,data/set/basic): add lemmas about `lift`
 (#17699)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* Add `quot.surjective_lift`, `quotient.surjective_lift_on'`.
* Mark `quot.lift_mk` as `simp`.
* Add `set.range_quot_lift`, `set.range_quotient_lift`, `set.range_quotient_mk'`, and `set.range_quotient_lift_on'`.
* The `mathlib4` version: leanprover-community/mathlib4#701.
* Prove `matrix.to_linear_map₂_apply` by `rfl`.
---
 src/data/quot.lean                            | 21 +++++++++++++------
 src/data/set/basic.lean                       | 21 ++++++++++++++++---
 .../matrix/sesquilinear_form.lean             |  7 +------
 3 files changed, 34 insertions(+), 15 deletions(-)

diff --git a/src/data/quot.lean b/src/data/quot.lean
index b082163abe85a..b2132e6cbeb0c 100644
--- a/src/data/quot.lean
+++ b/src/data/quot.lean
@@ -21,6 +21,8 @@ quotient
 
 variables {α : Sort*} {β : Sort*}
 
+open function
+
 namespace setoid
 
 lemma ext {α : Sort*} :
@@ -73,12 +75,16 @@ variables {γ : Sort*} {r : α → α → Prop} {s : β → β → Prop}
 
 /-- **Alias** of `quot.lift_beta`. -/
 lemma lift_mk (f : α → γ) (h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a₂) (a : α) :
-  quot.lift f h (quot.mk r a) = f a := quot.lift_beta f h a
+  quot.lift f h (quot.mk r a) = f a := rfl
 
 @[simp]
 lemma lift_on_mk (a : α) (f : α → γ) (h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a₂) :
   quot.lift_on (quot.mk r a) f h = f a := rfl
 
+@[simp] lemma surjective_lift {f : α → γ} (h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a₂) :
+  surjective (lift f h) ↔ surjective f :=
+⟨λ hf, hf.comp quot.exists_rep, λ hf y, let ⟨x, hx⟩ := hf y in ⟨quot.mk _ x, hx⟩⟩
+
 /-- Descends a function `f : α → β → γ` to quotients of `α` and `β`. -/
 attribute [reducible, elab_as_eliminator]
 protected def lift₂
@@ -272,12 +278,11 @@ rfl
   quotient.lift_on₂ (quotient.mk x) (quotient.mk y) f h = f x y := rfl
 
 /-- `quot.mk r` is a surjective function. -/
-lemma surjective_quot_mk (r : α → α → Prop) : function.surjective (quot.mk r) :=
-quot.exists_rep
+lemma surjective_quot_mk (r : α → α → Prop) : surjective (quot.mk r) := quot.exists_rep
 
 /-- `quotient.mk` is a surjective function. -/
 lemma surjective_quotient_mk (α : Sort*) [s : setoid α] :
-  function.surjective (quotient.mk : α → quotient s) :=
+  surjective (quotient.mk : α → quotient s) :=
 quot.exists_rep
 
 /-- Choose an element of the equivalence class using the axiom of choice.
@@ -319,7 +324,7 @@ end
   x.out ≈ y.out ↔ x = y :=
 by rw [← quotient.eq_mk_iff_out, quotient.out_eq]
 
-lemma quotient.out_injective {s : setoid α} : function.injective (@quotient.out α s) :=
+lemma quotient.out_injective {s : setoid α} : injective (@quotient.out α s) :=
 λ a b h, quotient.out_equiv_out.1 $ h ▸ setoid.refl _
 
 @[simp] lemma quotient.out_inj {s : setoid α} {x y : quotient s} :
@@ -469,7 +474,7 @@ instance argument. -/
 protected def mk' (a : α) : quotient s₁ := quot.mk s₁.1 a
 
 /-- `quotient.mk'` is a surjective function. -/
-lemma surjective_quotient_mk' : function.surjective (quotient.mk' : α → quotient s₁) :=
+lemma surjective_quotient_mk' : surjective (quotient.mk' : α → quotient s₁) :=
 quot.exists_rep
 
 /-- A version of `quotient.lift_on` taking `{s : setoid α}` as an implicit argument instead of an
@@ -482,6 +487,10 @@ protected def lift_on' (q : quotient s₁) (f : α → φ)
 protected lemma lift_on'_mk' (f : α → φ) (h) (x : α) :
   quotient.lift_on' (@quotient.mk' _ s₁ x) f h = f x := rfl
 
+@[simp] lemma surjective_lift_on' {f : α → φ} (h : ∀ a b, @setoid.r α s₁ a b → f a = f b) :
+  surjective (λ x, quotient.lift_on' x f h) ↔ surjective f :=
+quot.surjective_lift _
+
 /-- A version of `quotient.lift_on₂` taking `{s₁ : setoid α} {s₂ : setoid β}` as implicit arguments
 instead of instance arguments. -/
 @[elab_as_eliminator, reducible]
diff --git a/src/data/set/basic.lean b/src/data/set/basic.lean
index 65eab1507f17d..fbc848343a423 100644
--- a/src/data/set/basic.lean
+++ b/src/data/set/basic.lean
@@ -2284,13 +2284,28 @@ by rw [image_preimage_eq_inter_range, image_preimage_eq_inter_range, ← inter_d
 @[simp] theorem range_quot_mk (r : α → α → Prop) : range (quot.mk r) = univ :=
 (surjective_quot_mk r).range_eq
 
-instance can_lift (c) (p) [can_lift α β c p] :
-  can_lift (set α) (set β) (('') c) (λ s, ∀ x ∈ s, p x) :=
-{ prf := λ s hs, subset_range_iff_exists_image_eq.mp (λ x hx, can_lift.prf _ (hs x hx)) }
+@[simp] theorem range_quot_lift {r : ι → ι → Prop} (hf : ∀ x y, r x y → f x = f y) :
+  range (quot.lift f hf) = range f :=
+ext $ λ y, (surjective_quot_mk _).exists
 
 @[simp] theorem range_quotient_mk [setoid α] : range (λx : α, ⟦x⟧) = univ :=
 range_quot_mk _
 
+@[simp] theorem range_quotient_lift [s : setoid ι] (hf) :
+  range (quotient.lift f hf : quotient s → α) = range f :=
+range_quot_lift _
+
+@[simp] theorem range_quotient_mk' {s : setoid α} : range (quotient.mk' : α → quotient s) = univ :=
+range_quot_mk _
+
+@[simp] theorem range_quotient_lift_on' {s : setoid ι} (hf) :
+  range (λ x : quotient s, quotient.lift_on' x f hf) = range f :=
+range_quot_lift _
+
+instance can_lift (c) (p) [can_lift α β c p] :
+  can_lift (set α) (set β) (('') c) (λ s, ∀ x ∈ s, p x) :=
+{ prf := λ s hs, subset_range_iff_exists_image_eq.mp (λ x hx, can_lift.prf _ (hs x hx)) }
+
 lemma range_const_subset {c : α} : range (λ x : ι, c) ⊆ {c} :=
 range_subset_iff.2 $ λ x, rfl
 
diff --git a/src/linear_algebra/matrix/sesquilinear_form.lean b/src/linear_algebra/matrix/sesquilinear_form.lean
index 8e9f4140be6bb..53f690ff9cb04 100644
--- a/src/linear_algebra/matrix/sesquilinear_form.lean
+++ b/src/linear_algebra/matrix/sesquilinear_form.lean
@@ -315,12 +315,7 @@ by simp only [linear_map.to_matrix₂, linear_equiv.trans_apply, linear_map.to_m
 
 @[simp] lemma matrix.to_linear_map₂_apply (M : matrix n m R) (x : M₁) (y : M₂) :
   matrix.to_linear_map₂ b₁ b₂ M x y = ∑ i j, b₁.repr x i * M i j * b₂.repr y j :=
-begin
-  rw [matrix.to_linear_map₂, linear_map.to_matrix₂, linear_equiv.symm_trans_apply,
-    ←matrix.to_linear_map₂'],
-  simp only [matrix.to_linear_map₂'_apply, linear_equiv.arrow_congr_symm_apply,
-    basis.equiv_fun_apply, linear_equiv.refl_symm, linear_equiv.refl_apply],
-end
+rfl
 
 -- Not a `simp` lemma since `linear_map.to_matrix₂` needs an extra argument
 lemma linear_map.to_matrix₂_aux_eq (B : M₁ →ₗ[R] M₂ →ₗ[R] R) :