From e5ba338e9ae4e7feae5027fd5198850971f0fa6a Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Wed, 8 Dec 2021 05:53:31 +0000
Subject: [PATCH] fix(algebra/direct_sum): change `ring_hom_ext` to not
 duplicate `ring_hom_ext'` (#10640)

These two lemmas differed only in the explicitness of their binders.
The statement of the unprimed version has been changed to be fully applied.

This also renames `alg_hom_ext` to `alg_hom_ext'` to make way for the fully applied version. This is consistent with `direct_sum.add_hom_ext` vs `direct_sum.add_hom_ext'`.
---
 src/algebra/direct_sum/algebra.lean |  8 +++++---
 src/algebra/direct_sum/ring.lean    | 18 +++++++-----------
 2 files changed, 12 insertions(+), 14 deletions(-)

diff --git a/src/algebra/direct_sum/algebra.lean b/src/algebra/direct_sum/algebra.lean
index d03143bd3c3b1..1e58cc310470a 100644
--- a/src/algebra/direct_sum/algebra.lean
+++ b/src/algebra/direct_sum/algebra.lean
@@ -110,10 +110,12 @@ def to_algebra
 
 See note [partially-applied ext lemmas]. -/
 @[ext]
-lemma alg_hom_ext ⦃f g : (⨁ i, A i) →ₐ[R] B⦄
+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)
+alg_hom.to_linear_map_injective $ direct_sum.linear_map_ext _ h
+
+lemma alg_hom_ext ⦃f g : (⨁ i, A i) →ₐ[R] B⦄ (h : ∀ i x, f (of A i x) = g (of A i x)) : f = g :=
+alg_hom_ext' R A $ λ i, linear_map.ext $ h i
 
 end direct_sum
 
diff --git a/src/algebra/direct_sum/ring.lean b/src/algebra/direct_sum/ring.lean
index fdd0412d7d44b..3fd02774bfc13 100644
--- a/src/algebra/direct_sum/ring.lean
+++ b/src/algebra/direct_sum/ring.lean
@@ -404,10 +404,15 @@ then they are equal.
 
 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 _ i) = (G : (⨁ i, A i) →+ R).comp (of _ i)) : F = G :=
+lemma ring_hom_ext' ⦃F G : (⨁ i, A i) →+* R⦄
+  (h : ∀ i, (↑F : _ →+ R).comp (of A i) = (↑G : _ →+ R).comp (of A i)) : F = G :=
 ring_hom.coe_add_monoid_hom_injective $ direct_sum.add_hom_ext' h
 
+/-- Two `ring_hom`s out of a direct sum are equal if they agree on the generators. -/
+lemma ring_hom_ext ⦃f g : (⨁ i, A i) →+* R⦄ (h : ∀ i x, f (of A i x) = g (of A i x)) :
+  f = g :=
+ring_hom_ext' $ λ i, add_monoid_hom.ext $ h i
+
 /-- A family of `add_monoid_hom`s preserving `direct_sum.ghas_one.one` and `direct_sum.ghas_mul.mul`
 describes a `ring_hom`s on `⨁ i, A i`. This is a stronger version of `direct_sum.to_monoid`.
 
@@ -475,15 +480,6 @@ 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