From 7e1937fc319acaefe2235b47a58547f47b05bd0c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Wed, 16 Jul 2025 12:03:22 +0000
Subject: [PATCH 1/3] feat: coercing to an `AlgHom` then `RingHom` From Toric

---
 Mathlib/Algebra/Algebra/Hom.lean | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/Mathlib/Algebra/Algebra/Hom.lean b/Mathlib/Algebra/Algebra/Hom.lean
index 7ed4b6bb66c21e..24c13c87a3dba6 100644
--- a/Mathlib/Algebra/Algebra/Hom.lean
+++ b/Mathlib/Algebra/Algebra/Hom.lean
@@ -78,6 +78,11 @@ def toAlgHom {F : Type*} [FunLike F A B] [AlgHomClass F R A B] (f : F) : A →
 instance coeTC {F : Type*} [FunLike F A B] [AlgHomClass F R A B] : CoeTC F (A →ₐ[R] B) :=
   ⟨AlgHomClass.toAlgHom⟩
 
+@[simp]
+lemma toRingHom_toAlgHom {R A B : Type*} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A]
+    [Algebra R B] {F : Type*} [FunLike F A B] [AlgHomClass F R A B] (f : F) :
+    RingHomClass.toRingHom (AlgHomClass.toAlgHom f) = RingHomClass.toRingHom f := rfl
+
 end AlgHomClass
 
 namespace AlgHom

From 610be8b2525640141ebd9d02dcff9d5c146b01a1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Wed, 16 Jul 2025 13:18:20 +0000
Subject: [PATCH 2/3] fix

---
 Mathlib/Algebra/Algebra/Hom.lean | 14 +++++++++-----
 1 file changed, 9 insertions(+), 5 deletions(-)

diff --git a/Mathlib/Algebra/Algebra/Hom.lean b/Mathlib/Algebra/Algebra/Hom.lean
index 24c13c87a3dba6..f6ee4c800c18c1 100644
--- a/Mathlib/Algebra/Algebra/Hom.lean
+++ b/Mathlib/Algebra/Algebra/Hom.lean
@@ -78,11 +78,6 @@ def toAlgHom {F : Type*} [FunLike F A B] [AlgHomClass F R A B] (f : F) : A →
 instance coeTC {F : Type*} [FunLike F A B] [AlgHomClass F R A B] : CoeTC F (A →ₐ[R] B) :=
   ⟨AlgHomClass.toAlgHom⟩
 
-@[simp]
-lemma toRingHom_toAlgHom {R A B : Type*} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A]
-    [Algebra R B] {F : Type*} [FunLike F A B] [AlgHomClass F R A B] (f : F) :
-    RingHomClass.toRingHom (AlgHomClass.toAlgHom f) = RingHomClass.toRingHom f := rfl
-
 end AlgHomClass
 
 namespace AlgHom
@@ -367,6 +362,15 @@ lemma cancel_left {g₁ g₂ : A →ₐ[R] B} {f : B →ₐ[R] C} (hf : Function
 end Semiring
 end AlgHom
 
+namespace AlgHomClass
+
+@[simp]
+lemma toRingHom_toAlgHom {R A B : Type*} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A]
+    [Algebra R B] {F : Type*} [FunLike F A B] [AlgHomClass F R A B] (f : F) :
+    RingHomClass.toRingHom (AlgHomClass.toAlgHom f) = RingHomClass.toRingHom f := rfl
+
+end AlgHomClass
+
 namespace RingHom
 
 variable {R S : Type*}

From 97a2d4595b53bcd9c89a00342725dbaafd5f7549 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Wed, 16 Jul 2025 14:17:34 +0000
Subject: [PATCH 3/3] simp nf

---
 Mathlib/Topology/Algebra/Algebra.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Mathlib/Topology/Algebra/Algebra.lean b/Mathlib/Topology/Algebra/Algebra.lean
index 223d657084cee6..416bd81466b301 100644
--- a/Mathlib/Topology/Algebra/Algebra.lean
+++ b/Mathlib/Topology/Algebra/Algebra.lean
@@ -482,8 +482,7 @@ def _root_.Subalgebra.valA (p : Subalgebra R A) : p →A[R] A where
   toAlgHom := p.val
 
 @[simp, norm_cast]
-theorem _root_.Subalgebra.coe_valA (p : Subalgebra R A) :
-    (p.valA : p →ₐ[R] A) = p.subtype :=
+theorem _root_.Subalgebra.coe_valA (p : Subalgebra R A) : p.valA = p.subtype :=
   rfl
 
 @[simp]