From 5558fe8be03aeca1fc0fc050890d1c9f145a1a75 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sun, 29 Aug 2021 13:34:36 +0100
Subject: [PATCH] Add ext lemmas

---
 src/algebra/direct_sum/algebra.lean               |  9 +++++++++
 src/algebra/direct_sum/module.lean                | 13 ++++++++++---
 src/algebra/direct_sum/ring.lean                  |  9 +++++++++
 src/linear_algebra/direct_sum/tensor_product.lean |  6 +-----
 4 files changed, 29 insertions(+), 8 deletions(-)

diff --git a/src/algebra/direct_sum/algebra.lean b/src/algebra/direct_sum/algebra.lean
index 34e582fd8c43e..18d8b700e3807 100644
--- a/src/algebra/direct_sum/algebra.lean
+++ b/src/algebra/direct_sum/algebra.lean
@@ -131,6 +131,15 @@ def to_algebra
   commutes' := λ r, (direct_sum.to_semiring_of _ _ _ _ _).trans (hcommutes r),
   .. to_semiring (λ i, (f i).to_add_monoid_hom) hone @hmul}
 
+/-- Two `alg_hom`s out of a direct sum are equal if they agree on the generators.
+
+See note [partially-applied ext lemmas]. -/
+@[ext]
+lemma alg_hom_ext ⦃f g : (⨁ i, A i) →ₐ[R] B⦄
+  (h : ∀ i, f.to_linear_map.comp (lof _ _ A i) = g.to_linear_map.comp (lof _ _ A i)) : f = g :=
+alg_hom.coe_ring_hom_injective $
+  direct_sum.ring_hom_ext $ λ i, add_monoid_hom.ext $ linear_map.congr_fun (h i)
+
 end direct_sum
 
 /-! ### Concrete instances -/
diff --git a/src/algebra/direct_sum/module.lean b/src/algebra/direct_sum/module.lean
index 907a85750284c..5ac2e5d844a0b 100644
--- a/src/algebra/direct_sum/module.lean
+++ b/src/algebra/direct_sum/module.lean
@@ -56,6 +56,9 @@ dfinsupp.lmk
 /-- Inclusion of each component into the direct sum. -/
 def lof : Π i : ι, M i →ₗ[R] (⨁ i, M i) :=
 dfinsupp.lsingle
+
+lemma lof_eq_of (i : ι) (b : M i) : lof R ι M i b = of M i b := rfl
+
 variables {ι M}
 
 lemma single_eq_lof (i : ι) (b : M i) :
@@ -103,9 +106,13 @@ to_add_monoid.unique ψ.to_add_monoid_hom f
 
 variables {ψ} {ψ' : (⨁ i, M i) →ₗ[R] N}
 
-theorem to_module.ext (H : ∀ i, ψ.comp (lof R ι M i) = ψ'.comp (lof R ι M i)) (f : ⨁ i, M i) :
-  ψ f = ψ' f :=
-by rw dfinsupp.lhom_ext' H
+/-- Two `linear_map`s out of a direct sum are equal if they agree on the generators.
+
+See note [partially-applied ext lemmas]. -/
+@[ext]
+theorem linear_map_ext ⦃ψ ψ' : (⨁ i, M i) →ₗ[R] N⦄
+  (H : ∀ i, ψ.comp (lof R ι M i) = ψ'.comp (lof R ι M i)) : ψ = ψ' :=
+dfinsupp.lhom_ext' H
 
 /--
 The inclusion of a subset of the direct summands
diff --git a/src/algebra/direct_sum/ring.lean b/src/algebra/direct_sum/ring.lean
index a248669f8a9c4..e4097dcbdf8eb 100644
--- a/src/algebra/direct_sum/ring.lean
+++ b/src/algebra/direct_sum/ring.lean
@@ -634,6 +634,15 @@ def lift_ring_hom :
       add_monoid_hom.comp_apply, to_semiring_coe_add_monoid_hom],
   end}
 
+/-- Two `ring_hom`s out of a direct sum are equal if they agree on the generators.
+
+See note [partially-applied ext lemmas]. -/
+@[ext]
+lemma ring_hom_ext ⦃f g : (⨁ i, A i) →+* R⦄
+  (h : ∀ i, (↑f : (⨁ i, A i) →+ R).comp (of A i) = (↑g : (⨁ i, A i) →+ R).comp (of A i)) :
+  f = g :=
+direct_sum.lift_ring_hom.symm.injective $ subtype.ext $ funext h
+
 end to_semiring
 
 end direct_sum
diff --git a/src/linear_algebra/direct_sum/tensor_product.lean b/src/linear_algebra/direct_sum/tensor_product.lean
index 6d816ccb96428..f026b481bb433 100644
--- a/src/linear_algebra/direct_sum/tensor_product.lean
+++ b/src/linear_algebra/direct_sum/tensor_product.lean
@@ -37,14 +37,10 @@ begin
     (lift $ direct_sum.to_module R _ _ $ λ i₁, flip $ direct_sum.to_module R _ _ $ λ i₂,
       flip $ curry $ direct_sum.lof R (ι₁ × ι₂) (λ i, M₁ i.1 ⊗[R] M₂ i.2) (i₁, i₂))
     (direct_sum.to_module R _ _ $ λ i, map (direct_sum.lof R _ _ _) (direct_sum.lof R _ _ _))
-    (linear_map.ext $ direct_sum.to_module.ext _ $ λ i, mk_compr₂_inj $
-      linear_map.ext $ λ x₁, linear_map.ext $ λ x₂, _)
-    (mk_compr₂_inj $ linear_map.ext $ direct_sum.to_module.ext _ $ λ i₁, linear_map.ext $ λ x₁,
-      linear_map.ext $ direct_sum.to_module.ext _ $ λ i₂, linear_map.ext $ λ x₂, _),
+    _ _; [ext ⟨i₁, i₂⟩ x₁ x₂ : 4, ext i₁ i₂ x₁ x₂ : 5],
   repeat { rw compr₂_apply <|> rw comp_apply <|> rw id_apply <|> rw mk_apply <|>
     rw direct_sum.to_module_lof <|> rw map_tmul <|> rw lift.tmul <|> rw flip_apply <|>
     rw curry_apply },
-  cases i; refl
 end
 
 @[simp] theorem direct_sum_lof_tmul_lof (i₁ : ι₁) (m₁ : M₁ i₁) (i₂ : ι₂) (m₂ : M₂ i₂) :