From 92978fbb76a7366cafef059c8c49e7a17ca3a7d4 Mon Sep 17 00:00:00 2001
From: Monica Omar <23701951+themathqueen@users.noreply.github.com>
Date: Fri, 22 May 2026 12:22:40 +0000
Subject: [PATCH 01/13] some api

---
 Mathlib/LinearAlgebra/TensorProduct/Tower.lean |  3 +++
 Mathlib/RingTheory/TensorProduct/Basic.lean    | 18 ++++++++++--------
 2 files changed, 13 insertions(+), 8 deletions(-)

diff --git a/Mathlib/LinearAlgebra/TensorProduct/Tower.lean b/Mathlib/LinearAlgebra/TensorProduct/Tower.lean
index 7607ff2d6e0b81..c71de9452136f5 100644
--- a/Mathlib/LinearAlgebra/TensorProduct/Tower.lean
+++ b/Mathlib/LinearAlgebra/TensorProduct/Tower.lean
@@ -176,6 +176,9 @@ nonrec def mk (A M N : Type*) [Semiring A]
 
 variable {R A B M N P Q}
 
+/-- The heterobasic version of `mk` coincides with the regular version. -/
+lemma mk_eq : mk R R M N = TensorProduct.mk R M N := rfl
+
 /-- Heterobasic version of `TensorProduct.map` -/
 def map (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : M ⊗[R] N →ₗ[A] P ⊗[R] Q :=
   lift <|
diff --git a/Mathlib/RingTheory/TensorProduct/Basic.lean b/Mathlib/RingTheory/TensorProduct/Basic.lean
index e7ec44de33ee7f..0f1d5cc41adee0 100644
--- a/Mathlib/RingTheory/TensorProduct/Basic.lean
+++ b/Mathlib/RingTheory/TensorProduct/Basic.lean
@@ -269,11 +269,9 @@ theorem tmul_pow (a : A) (b : B) (k : ℕ) : a ⊗ₜ[R] b ^ k = (a ^ k) ⊗ₜ[
   | succ k ih => simp [pow_succ, ih]
 
 /-- The ring morphism `A →+* A ⊗[R] B` sending `a` to `a ⊗ₜ 1`. -/
-@[simps]
+@[simps!]
 def includeLeftRingHom : A →+* A ⊗[R] B where
-  toFun a := a ⊗ₜ 1
-  map_zero' := by simp
-  map_add' := by simp [add_tmul]
+  __ := (AlgebraTensorModule.mk R R A B).flip 1 |>.toAddMonoidHom
   map_one' := rfl
   map_mul' := by simp
 
@@ -317,19 +315,23 @@ theorem includeLeft_apply [SMulCommClass R S A] (a : A) :
     (includeLeft : A →ₐ[S] A ⊗[R] B) a = a ⊗ₜ 1 :=
   rfl
 
+@[simp] theorem toLinearMap_includeLeft [SMulCommClass R S A] :
+    (includeLeft : A →ₐ[S] A ⊗[R] B).toLinearMap = (AlgebraTensorModule.mk R S A B).flip 1 := rfl
+
 /-- The algebra morphism `B →ₐ[R] A ⊗[R] B` sending `b` to `1 ⊗ₜ b`. -/
 def includeRight : B →ₐ[R] A ⊗[R] B where
-  toFun b := 1 ⊗ₜ b
-  map_zero' := by simp
-  map_add' := by simp [tmul_add]
+  __ := AlgebraTensorModule.mk R R A B 1 |>.toAddMonoidHom
   map_one' := rfl
   map_mul' := by simp
-  commutes' r := by simp only [algebraMap_apply']
+  commutes' r := by simp [algebraMap_eq_smul_one', smul_tmul]
 
 @[simp]
 theorem includeRight_apply (b : B) : (includeRight : B →ₐ[R] A ⊗[R] B) b = 1 ⊗ₜ b :=
   rfl
 
+@[simp] theorem toLinearMap_includeRight :
+    (includeRight : B →ₐ[R] A ⊗[R] B).toLinearMap = AlgebraTensorModule.mk R R A B 1 := rfl
+
 theorem includeLeftRingHom_comp_algebraMap :
     (includeLeftRingHom.comp (algebraMap R A) : R →+* A ⊗[R] B) =
       includeRight.toRingHom.comp (algebraMap R B) := by

From d7ba9e39d486a396a961e76b6ada1f8cbb02762c Mon Sep 17 00:00:00 2001
From: Monica Omar <23701951+themathqueen@users.noreply.github.com>
Date: Fri, 22 May 2026 13:51:51 +0000
Subject: [PATCH 02/13] fix

---
 Mathlib/RingTheory/TensorProduct/IncludeLeftSubRight.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/RingTheory/TensorProduct/IncludeLeftSubRight.lean b/Mathlib/RingTheory/TensorProduct/IncludeLeftSubRight.lean
index a4ca029c1952f5..26e9a4cdaf9855 100644
--- a/Mathlib/RingTheory/TensorProduct/IncludeLeftSubRight.lean
+++ b/Mathlib/RingTheory/TensorProduct/IncludeLeftSubRight.lean
@@ -54,7 +54,7 @@ lemma includeLeftSubRight_apply (s : S) : includeLeftSubRight R S s = s ⊗ₜ[R
 lemma includeLeftSubRight_zero_of_mem_range {s : S} (hs : s ∈ Set.range ⇑(algebraMap R S)) :
     includeLeftSubRight R S s = 0 := by
   obtain ⟨_, hr⟩ := Set.mem_range.mp hs
-  simp [includeLeftSubRight, ← hr]
+  simp [includeLeftSubRight, ← hr, algebraMap_eq_smul_one]
 
 /-- `includeLeftSubRight R S` vanishes at `algebraMap R S r`. -/
 lemma includeLeftSubRight_algebraMap_zero (r : R) :

From 9033d8a9e84232e1bccee0964d9a0b6a05ffee12 Mon Sep 17 00:00:00 2001
From: Monica Omar <23701951+themathqueen@users.noreply.github.com>
Date: Fri, 22 May 2026 13:58:47 +0000
Subject: [PATCH 03/13] tiny change

---
 Mathlib/RingTheory/TensorProduct/IncludeLeftSubRight.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/RingTheory/TensorProduct/IncludeLeftSubRight.lean b/Mathlib/RingTheory/TensorProduct/IncludeLeftSubRight.lean
index 26e9a4cdaf9855..781cd5e014c7d1 100644
--- a/Mathlib/RingTheory/TensorProduct/IncludeLeftSubRight.lean
+++ b/Mathlib/RingTheory/TensorProduct/IncludeLeftSubRight.lean
@@ -54,7 +54,7 @@ lemma includeLeftSubRight_apply (s : S) : includeLeftSubRight R S s = s ⊗ₜ[R
 lemma includeLeftSubRight_zero_of_mem_range {s : S} (hs : s ∈ Set.range ⇑(algebraMap R S)) :
     includeLeftSubRight R S s = 0 := by
   obtain ⟨_, hr⟩ := Set.mem_range.mp hs
-  simp [includeLeftSubRight, ← hr, algebraMap_eq_smul_one]
+  simp [← hr, algebraMap_eq_smul_one]
 
 /-- `includeLeftSubRight R S` vanishes at `algebraMap R S r`. -/
 lemma includeLeftSubRight_algebraMap_zero (r : R) :

From d31c93463660c51dec4a78e66edb3dd9a2976141 Mon Sep 17 00:00:00 2001
From: Robin Langer <langer.robin@gmail.com>
Date: Fri, 15 May 2026 21:51:35 +1000
Subject: [PATCH 04/13] feat(RingTheory/HopfAlgebra): Hopf algebra structure on
 polynomials (G_a)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Add the Coalgebra, Bialgebra, and HopfAlgebra instances on `R[X]` with
additive comultiplication `Δ(X) = X ⊗ 1 + 1 ⊗ X`, counit `ε(p) = p(0)`,
and antipode `S(X) = -X`. This is the coordinate ring of the additive
group scheme 𝔾_a, dual to the multiplicative 𝔾_m already formalized via
Laurent polynomials.
---
 Mathlib.lean                                  |   1 +
 .../RingTheory/HopfAlgebra/Polynomial.lean    | 260 ++++++++++++++++++
 2 files changed, 261 insertions(+)
 create mode 100644 Mathlib/RingTheory/HopfAlgebra/Polynomial.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index bb572a5a061e4f..f67491bd0bb6b4 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -6517,6 +6517,7 @@ public import Mathlib.RingTheory.Henselian
 public import Mathlib.RingTheory.HopfAlgebra.Basic
 public import Mathlib.RingTheory.HopfAlgebra.GroupLike
 public import Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra
+public import Mathlib.RingTheory.HopfAlgebra.Polynomial
 public import Mathlib.RingTheory.HopfAlgebra.TensorProduct
 public import Mathlib.RingTheory.HopkinsLevitzki
 public import Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
diff --git a/Mathlib/RingTheory/HopfAlgebra/Polynomial.lean b/Mathlib/RingTheory/HopfAlgebra/Polynomial.lean
new file mode 100644
index 00000000000000..c6c927c3f10664
--- /dev/null
+++ b/Mathlib/RingTheory/HopfAlgebra/Polynomial.lean
@@ -0,0 +1,260 @@
+/-
+Copyright (c) 2025 Robin Langer. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Robin Langer
+-/
+import Mathlib.RingTheory.HopfAlgebra.Basic
+import Mathlib.Algebra.Polynomial.AlgebraMap
+import Mathlib.Algebra.Polynomial.Eval.SMul
+import Mathlib.RingTheory.TensorProduct.Maps
+
+/-!
+# The Hopf algebra structure on polynomials (additive group scheme 𝔾ₐ)
+
+The polynomial ring `R[X]` carries a natural Hopf algebra structure encoding the
+additive group scheme `𝔾ₐ`:
+* comultiplication: `Δ(X) = X ⊗ 1 + 1 ⊗ X` (encoding `p(x) ↦ p(x + x')`)
+* counit: `ε(p) = p(0)` (evaluation at zero)
+* antipode: `S(X) = -X` (requires `CommRing R`)
+
+This is dual to the multiplicative group scheme `𝔾ₘ` formalized via Laurent polynomials
+in `Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra`.
+
+## Main definitions
+
+* `Polynomial.instCoalgebra`: the `R`-coalgebra structure on `R[X]` with additive
+  comultiplication.
+* `Polynomial.instBialgebra`: the `R`-bialgebra structure on `R[X]`.
+* `Polynomial.instHopfAlgebra`: the `R`-Hopf algebra structure on `R[X]` when `R` is a
+  commutative ring.
+
+## Implementation notes
+
+The coalgebra axioms are equalities of linear maps, but both sides factor through
+algebra homomorphisms out of `R[X]`. Since `R[X]` is free on `X`, algebra hom equality
+reduces to checking on `X` alone (`Polynomial.algHom_ext`). The proofs convert between the
+linear map API (`rTensor`, `lTensor`, `TensorProduct.assoc`) and the algebra hom API
+(`Algebra.TensorProduct.map`, `includeRight`, `Algebra.TensorProduct.assoc`) via
+auxiliary lemmas, then apply `algHom_ext`.
+
+## References
+
+* Langer, R., *Determinantal bases and the symmetric group*, arXiv:0907.3950, §1.2
+-/
+
+noncomputable section
+
+open Polynomial TensorProduct
+
+open scoped Polynomial TensorProduct
+
+namespace Polynomial
+
+variable (R : Type*) [CommSemiring R]
+
+/-! ### Comultiplication and counit -/
+
+/-- The comultiplication on `R[X]` for the additive group scheme `𝔾ₐ`:
+the unique `R`-algebra homomorphism sending `X ↦ X ⊗ 1 + 1 ⊗ X`.
+As a linear map, this encodes `Δ(p(x)) = p(x + x')`. -/
+def comulAdditiveAlgHom : R[X] →ₐ[R] R[X] ⊗[R] R[X] :=
+  Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]))
+
+/-- The counit on `R[X]` for the additive group scheme `𝔾ₐ`:
+evaluation at `0`, as an `R`-algebra homomorphism. This is `ε(p) = p(0)`. -/
+def counitAdditiveAlgHom : R[X] →ₐ[R] R :=
+  Polynomial.aeval (0 : R)
+
+@[simp]
+theorem comulAdditiveAlgHom_X :
+    comulAdditiveAlgHom R (X : R[X]) = (X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]) := by
+  simp [comulAdditiveAlgHom]
+
+@[simp]
+theorem comulAdditiveAlgHom_C (r : R) :
+    comulAdditiveAlgHom R (C r) = (C r) ⊗ₜ 1 := by
+  simp [comulAdditiveAlgHom]
+
+@[simp]
+theorem counitAdditiveAlgHom_X :
+    counitAdditiveAlgHom R (X : R[X]) = 0 := by
+  simp [counitAdditiveAlgHom]
+
+@[simp]
+theorem counitAdditiveAlgHom_C (r : R) :
+    counitAdditiveAlgHom R (C r) = r := by
+  simp [counitAdditiveAlgHom]
+
+/-! ### Coalgebra instance
+
+The three coalgebra axioms (coassociativity, left counitality, right counitality)
+reduce to checking equality of `R`-algebra hom compositions on the generator `X`.
+-/
+
+/-- The `𝔾ₐ` coalgebra structure on `R[X]`. -/
+instance instCoalgebraStruct : CoalgebraStruct R R[X] where
+  comul := (comulAdditiveAlgHom R).toLinearMap
+  counit := (counitAdditiveAlgHom R).toLinearMap
+
+-- Auxiliary equations for unfolding the CoalgebraStruct fields
+theorem comul_eq : (CoalgebraStruct.comul : R[X] →ₗ[R] _) =
+    (comulAdditiveAlgHom R).toLinearMap := rfl
+
+theorem counit_eq : (CoalgebraStruct.counit : R[X] →ₗ[R] _) =
+    (counitAdditiveAlgHom R).toLinearMap := rfl
+
+-- Glue lemmas connecting rTensor/lTensor to Algebra.TensorProduct.map
+theorem rTensor_counit_eq :
+    (counitAdditiveAlgHom R).toLinearMap.rTensor R[X] =
+    (Algebra.TensorProduct.map (counitAdditiveAlgHom R)
+     (AlgHom.id R R[X])).toLinearMap := by
+  ext x y; simp [LinearMap.rTensor_tmul]
+
+theorem lTensor_counit_eq :
+    (counitAdditiveAlgHom R).toLinearMap.lTensor R[X] =
+    (Algebra.TensorProduct.map (AlgHom.id R R[X])
+     (counitAdditiveAlgHom R)).toLinearMap := by
+  ext x y; simp [LinearMap.lTensor_tmul]
+
+theorem mk_one_eq_includeRight :
+    TensorProduct.mk R R R[X] 1 =
+    (Algebra.TensorProduct.includeRight : R[X] →ₐ[R] R ⊗[R] R[X]).toLinearMap := by
+  ext y; simp [Algebra.TensorProduct.includeRight_apply]
+
+theorem mk_flip_one_eq_includeLeft :
+    (TensorProduct.mk R R[X] R).flip 1 =
+    (Algebra.TensorProduct.includeLeft : R[X] →ₐ[R] R[X] ⊗[R] R).toLinearMap := by
+  ext y; simp [Algebra.TensorProduct.includeLeft_apply, LinearMap.flip_apply]
+
+theorem rTensor_comul_eq :
+    (comulAdditiveAlgHom R).toLinearMap.rTensor R[X] =
+    (Algebra.TensorProduct.map (comulAdditiveAlgHom R)
+     (AlgHom.id R R[X])).toLinearMap := by
+  ext x y; simp [LinearMap.rTensor_tmul]
+
+theorem lTensor_comul_eq :
+    (comulAdditiveAlgHom R).toLinearMap.lTensor R[X] =
+    (Algebra.TensorProduct.map (AlgHom.id R R[X])
+     (comulAdditiveAlgHom R)).toLinearMap := by
+  ext x y; simp [LinearMap.lTensor_tmul]
+
+/-- The `𝔾ₐ` coalgebra instance on `R[X]`: coassociativity holds because both
+`(Δ ⊗ id) ∘ Δ` and `(id ⊗ Δ) ∘ Δ` send `X` to `X⊗1⊗1 + 1⊗X⊗1 + 1⊗1⊗X`. -/
+instance instCoalgebra : Coalgebra R R[X] :=
+  { instCoalgebraStruct R with
+    rTensor_counit_comp_comul := by
+      rw [counit_eq, comul_eq, rTensor_counit_eq, mk_one_eq_includeRight]
+      change ((Algebra.TensorProduct.map (counitAdditiveAlgHom R)
+               (AlgHom.id R R[X])).comp (comulAdditiveAlgHom R)).toLinearMap = _
+      congr 1
+      apply Polynomial.algHom_ext
+      simp [comulAdditiveAlgHom, counitAdditiveAlgHom,
+            Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.includeRight_apply]
+    lTensor_counit_comp_comul := by
+      rw [counit_eq, comul_eq, lTensor_counit_eq, mk_flip_one_eq_includeLeft]
+      change ((Algebra.TensorProduct.map (AlgHom.id R R[X])
+               (counitAdditiveAlgHom R)).comp (comulAdditiveAlgHom R)).toLinearMap = _
+      congr 1
+      apply Polynomial.algHom_ext
+      simp [comulAdditiveAlgHom, counitAdditiveAlgHom,
+            Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.includeLeft_apply]
+    coassoc := by
+      rw [comul_eq, rTensor_comul_eq, lTensor_comul_eq]
+      change ((Algebra.TensorProduct.assoc R R R R[X] R[X] R[X]).toAlgHom.comp
+              ((Algebra.TensorProduct.map (comulAdditiveAlgHom R)
+                (AlgHom.id R R[X])).comp
+               (comulAdditiveAlgHom R))).toLinearMap =
+             ((Algebra.TensorProduct.map (AlgHom.id R R[X])
+               (comulAdditiveAlgHom R)).comp
+              (comulAdditiveAlgHom R)).toLinearMap
+      congr 1
+      apply Polynomial.algHom_ext
+      simp only [comulAdditiveAlgHom, AlgHom.comp_apply, AlgEquiv.toAlgHom_eq_coe,
+            AlgHom.coe_coe, Algebra.TensorProduct.map_tmul, AlgHom.id_apply, aeval_X,
+            map_add, map_one, Algebra.TensorProduct.one_def,
+            Algebra.TensorProduct.assoc_tmul,
+            TensorProduct.add_tmul, TensorProduct.tmul_add]
+      abel }
+
+/-! ### Bialgebra instance -/
+
+/-- The `𝔾ₐ` bialgebra instance on `R[X]`: the comultiplication and counit are algebra
+homomorphisms by construction. -/
+instance instBialgebra : Bialgebra R R[X] :=
+  Bialgebra.mk' R R[X]
+    (by simp [counit_eq])
+    (by intro a b; simp [counit_eq, map_mul])
+    (by simp [comul_eq])
+    (by intro a b; simp [comul_eq, map_mul])
+
+end Polynomial
+
+end -- end CommSemiring section
+
+/-! ### Hopf algebra instance -/
+
+noncomputable section
+
+open Polynomial TensorProduct
+
+open scoped Polynomial TensorProduct
+
+namespace Polynomial
+
+variable (R : Type*) [CommRing R]
+
+/-- The antipode on `R[X]` for the additive group scheme `𝔾ₐ`:
+the unique `R`-algebra homomorphism sending `X ↦ -X`.
+This is "inversion" on `𝔾ₐ`: if `Δ` encodes addition (`x ↦ x + x'`),
+then `S` encodes negation (`x ↦ -x`). -/
+def antipodeAdditiveAlgHom : R[X] →ₐ[R] R[X] :=
+  Polynomial.aeval (-X : R[X])
+
+@[simp]
+theorem antipodeAdditiveAlgHom_X :
+    antipodeAdditiveAlgHom R (X : R[X]) = -X := by
+  simp [antipodeAdditiveAlgHom]
+
+@[simp]
+theorem antipodeAdditiveAlgHom_C (r : R) :
+    antipodeAdditiveAlgHom R (C r) = C r := by
+  simp [antipodeAdditiveAlgHom]
+
+/-- The `𝔾ₐ` Hopf algebra instance on `R[X]` (requires `CommRing R` for the antipode
+`S(X) = -X`). The antipode axiom `m ∘ (S ⊗ id) ∘ Δ = η ∘ ε` holds because both sides
+send `X` to `0`: `S(X) · 1 + 1 · X = -X + X = 0 = C(ε(X))`. -/
+instance instHopfAlgebra : HopfAlgebra R R[X] where
+  antipode := (antipodeAdditiveAlgHom R).toLinearMap
+  mul_antipode_rTensor_comul := by
+    have rTensor_eq : (antipodeAdditiveAlgHom R).toLinearMap.rTensor R[X] =
+        (Algebra.TensorProduct.map (antipodeAdditiveAlgHom R)
+         (AlgHom.id R R[X])).toLinearMap := by
+      ext x y; simp [LinearMap.rTensor_tmul]
+    rw [comul_eq, counit_eq, rTensor_eq, ← Algebra.TensorProduct.lmul'_toLinearMap]
+    -- Both sides are toLinearMap of algebra hom compositions. Convert and check on X.
+    change ((Algebra.TensorProduct.lmul' R : R[X] ⊗[R] R[X] →ₐ[R] R[X]).comp
+            ((Algebra.TensorProduct.map (antipodeAdditiveAlgHom R)
+              (AlgHom.id R R[X])).comp (comulAdditiveAlgHom R))).toLinearMap =
+           ((Algebra.ofId R R[X]).comp (counitAdditiveAlgHom R)).toLinearMap
+    congr 1; apply Polynomial.algHom_ext
+    simp [comulAdditiveAlgHom, antipodeAdditiveAlgHom, counitAdditiveAlgHom,
+          Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.lmul'_apply_tmul,
+          Algebra.ofId_apply]
+  mul_antipode_lTensor_comul := by
+    have lTensor_eq : (antipodeAdditiveAlgHom R).toLinearMap.lTensor R[X] =
+        (Algebra.TensorProduct.map (AlgHom.id R R[X])
+         (antipodeAdditiveAlgHom R)).toLinearMap := by
+      ext x y; simp [LinearMap.lTensor_tmul]
+    rw [comul_eq, counit_eq, lTensor_eq, ← Algebra.TensorProduct.lmul'_toLinearMap]
+    change ((Algebra.TensorProduct.lmul' R : R[X] ⊗[R] R[X] →ₐ[R] R[X]).comp
+            ((Algebra.TensorProduct.map (AlgHom.id R R[X])
+              (antipodeAdditiveAlgHom R)).comp (comulAdditiveAlgHom R))).toLinearMap =
+           ((Algebra.ofId R R[X]).comp (counitAdditiveAlgHom R)).toLinearMap
+    congr 1; apply Polynomial.algHom_ext
+    simp [comulAdditiveAlgHom, antipodeAdditiveAlgHom, counitAdditiveAlgHom,
+          Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.lmul'_apply_tmul,
+          Algebra.ofId_apply]
+
+end Polynomial
+
+end

From 76dc8a3e23bbfc89a81c2595da576b75a9f3bd6b Mon Sep 17 00:00:00 2001
From: Robin Langer <langer.robin@gmail.com>
Date: Fri, 15 May 2026 22:01:21 +1000
Subject: [PATCH 05/13] fix: add module declaration for Lean 4.30.0
 compatibility

Adds `module` keyword and changes `import` to `public import` to match
the module system introduced in Lean 4.30.0-rc2, which Mathlib master
now requires.
---
 Mathlib/RingTheory/HopfAlgebra/Polynomial.lean | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/Mathlib/RingTheory/HopfAlgebra/Polynomial.lean b/Mathlib/RingTheory/HopfAlgebra/Polynomial.lean
index c6c927c3f10664..0c7bf77004d1fa 100644
--- a/Mathlib/RingTheory/HopfAlgebra/Polynomial.lean
+++ b/Mathlib/RingTheory/HopfAlgebra/Polynomial.lean
@@ -3,10 +3,12 @@ Copyright (c) 2025 Robin Langer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robin Langer
 -/
-import Mathlib.RingTheory.HopfAlgebra.Basic
-import Mathlib.Algebra.Polynomial.AlgebraMap
-import Mathlib.Algebra.Polynomial.Eval.SMul
-import Mathlib.RingTheory.TensorProduct.Maps
+module
+
+public import Mathlib.RingTheory.HopfAlgebra.Basic
+public import Mathlib.Algebra.Polynomial.AlgebraMap
+public import Mathlib.Algebra.Polynomial.Eval.SMul
+public import Mathlib.RingTheory.TensorProduct.Maps
 
 /-!
 # The Hopf algebra structure on polynomials (additive group scheme 𝔾ₐ)

From 8f2bf586dcb502114f468337f25ac559d6f1aef1 Mon Sep 17 00:00:00 2001
From: Robin Langer <langer.robin@gmail.com>
Date: Fri, 15 May 2026 23:36:17 +1000
Subject: [PATCH 06/13] fix: add public section and remove unused simp args

Add `public section` for Lean 4.30.0 module visibility and remove
deprecated/unused simp lemmas (`AlgEquiv.toAlgHom_eq_coe`,
`AlgHom.coe_coe`, `Algebra.TensorProduct.assoc_tmul`) flagged by linters.
---
 Mathlib/RingTheory/HopfAlgebra/Polynomial.lean | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/Mathlib/RingTheory/HopfAlgebra/Polynomial.lean b/Mathlib/RingTheory/HopfAlgebra/Polynomial.lean
index 0c7bf77004d1fa..2f5de8ad6e9077 100644
--- a/Mathlib/RingTheory/HopfAlgebra/Polynomial.lean
+++ b/Mathlib/RingTheory/HopfAlgebra/Polynomial.lean
@@ -44,6 +44,8 @@ auxiliary lemmas, then apply `algHom_ext`.
 * Langer, R., *Determinantal bases and the symmetric group*, arXiv:0907.3950, §1.2
 -/
 
+public section
+
 noncomputable section
 
 open Polynomial TensorProduct
@@ -171,10 +173,9 @@ instance instCoalgebra : Coalgebra R R[X] :=
               (comulAdditiveAlgHom R)).toLinearMap
       congr 1
       apply Polynomial.algHom_ext
-      simp only [comulAdditiveAlgHom, AlgHom.comp_apply, AlgEquiv.toAlgHom_eq_coe,
-            AlgHom.coe_coe, Algebra.TensorProduct.map_tmul, AlgHom.id_apply, aeval_X,
+      simp only [comulAdditiveAlgHom, AlgHom.comp_apply,
+            Algebra.TensorProduct.map_tmul, AlgHom.id_apply, aeval_X,
             map_add, map_one, Algebra.TensorProduct.one_def,
-            Algebra.TensorProduct.assoc_tmul,
             TensorProduct.add_tmul, TensorProduct.tmul_add]
       abel }
 

From 7498f72bd9f58eb60a6afe1fe9b5057b4227cfab Mon Sep 17 00:00:00 2001
From: Robin Langer <langer.robin@gmail.com>
Date: Fri, 22 May 2026 08:46:59 +1000
Subject: [PATCH 07/13] refactor: inline comul/counit AlgHom defs, fix where
 style, add toLinearMap lemmas

Address review feedback:
- Remove comulAdditiveAlgHom/counitAdditiveAlgHom as standalone defs,
  inline aeval expressions directly in the Coalgebra instance
- Use where style for instCoalgebra instead of { ... with }
- Add Algebra.TensorProduct.toLinearMap_includeRight/Left as rfl lemmas
  in TensorProduct/Basic.lean, replacing the reversed mk_one_eq lemmas
- State simp lemmas in terms of Coalgebra.comul/counit after the instance
---
 .../RingTheory/HopfAlgebra/Polynomial.lean    | 203 +++++++-----------
 1 file changed, 82 insertions(+), 121 deletions(-)

diff --git a/Mathlib/RingTheory/HopfAlgebra/Polynomial.lean b/Mathlib/RingTheory/HopfAlgebra/Polynomial.lean
index 2f5de8ad6e9077..04d440204a4080 100644
--- a/Mathlib/RingTheory/HopfAlgebra/Polynomial.lean
+++ b/Mathlib/RingTheory/HopfAlgebra/Polynomial.lean
@@ -56,128 +56,86 @@ namespace Polynomial
 
 variable (R : Type*) [CommSemiring R]
 
-/-! ### Comultiplication and counit -/
-
-/-- The comultiplication on `R[X]` for the additive group scheme `𝔾ₐ`:
-the unique `R`-algebra homomorphism sending `X ↦ X ⊗ 1 + 1 ⊗ X`.
-As a linear map, this encodes `Δ(p(x)) = p(x + x')`. -/
-def comulAdditiveAlgHom : R[X] →ₐ[R] R[X] ⊗[R] R[X] :=
-  Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]))
-
-/-- The counit on `R[X]` for the additive group scheme `𝔾ₐ`:
-evaluation at `0`, as an `R`-algebra homomorphism. This is `ε(p) = p(0)`. -/
-def counitAdditiveAlgHom : R[X] →ₐ[R] R :=
-  Polynomial.aeval (0 : R)
-
-@[simp]
-theorem comulAdditiveAlgHom_X :
-    comulAdditiveAlgHom R (X : R[X]) = (X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]) := by
-  simp [comulAdditiveAlgHom]
-
-@[simp]
-theorem comulAdditiveAlgHom_C (r : R) :
-    comulAdditiveAlgHom R (C r) = (C r) ⊗ₜ 1 := by
-  simp [comulAdditiveAlgHom]
-
-@[simp]
-theorem counitAdditiveAlgHom_X :
-    counitAdditiveAlgHom R (X : R[X]) = 0 := by
-  simp [counitAdditiveAlgHom]
-
-@[simp]
-theorem counitAdditiveAlgHom_C (r : R) :
-    counitAdditiveAlgHom R (C r) = r := by
-  simp [counitAdditiveAlgHom]
-
 /-! ### Coalgebra instance
 
 The three coalgebra axioms (coassociativity, left counitality, right counitality)
 reduce to checking equality of `R`-algebra hom compositions on the generator `X`.
 -/
 
-/-- The `𝔾ₐ` coalgebra structure on `R[X]`. -/
-instance instCoalgebraStruct : CoalgebraStruct R R[X] where
-  comul := (comulAdditiveAlgHom R).toLinearMap
-  counit := (counitAdditiveAlgHom R).toLinearMap
-
--- Auxiliary equations for unfolding the CoalgebraStruct fields
-theorem comul_eq : (CoalgebraStruct.comul : R[X] →ₗ[R] _) =
-    (comulAdditiveAlgHom R).toLinearMap := rfl
-
-theorem counit_eq : (CoalgebraStruct.counit : R[X] →ₗ[R] _) =
-    (counitAdditiveAlgHom R).toLinearMap := rfl
-
--- Glue lemmas connecting rTensor/lTensor to Algebra.TensorProduct.map
-theorem rTensor_counit_eq :
-    (counitAdditiveAlgHom R).toLinearMap.rTensor R[X] =
-    (Algebra.TensorProduct.map (counitAdditiveAlgHom R)
-     (AlgHom.id R R[X])).toLinearMap := by
+-- Glue lemmas connecting rTensor/lTensor of AlgHom.toLinearMap to Algebra.TensorProduct.map
+private theorem rTensor_toLinearMap_eq (f : R[X] →ₐ[R] A) :
+    f.toLinearMap.rTensor R[X] =
+    (Algebra.TensorProduct.map f (AlgHom.id R R[X])).toLinearMap := by
   ext x y; simp [LinearMap.rTensor_tmul]
 
-theorem lTensor_counit_eq :
-    (counitAdditiveAlgHom R).toLinearMap.lTensor R[X] =
-    (Algebra.TensorProduct.map (AlgHom.id R R[X])
-     (counitAdditiveAlgHom R)).toLinearMap := by
+private theorem lTensor_toLinearMap_eq (f : R[X] →ₐ[R] A) :
+    f.toLinearMap.lTensor R[X] =
+    (Algebra.TensorProduct.map (AlgHom.id R R[X]) f).toLinearMap := by
   ext x y; simp [LinearMap.lTensor_tmul]
 
-theorem mk_one_eq_includeRight :
-    TensorProduct.mk R R R[X] 1 =
-    (Algebra.TensorProduct.includeRight : R[X] →ₐ[R] R ⊗[R] R[X]).toLinearMap := by
-  ext y; simp [Algebra.TensorProduct.includeRight_apply]
+/-- The `𝔾ₐ` coalgebra instance on `R[X]`: coassociativity holds because both
+`(Δ ⊗ id) ∘ Δ` and `(id ⊗ Δ) ∘ Δ` send `X` to `X⊗1⊗1 + 1⊗X⊗1 + 1⊗1⊗X`. -/
+instance instCoalgebra : Coalgebra R R[X] where
+  comul := (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]))).toLinearMap
+  counit := (Polynomial.aeval (0 : R)).toLinearMap
+  rTensor_counit_comp_comul := by
+    rw [rTensor_toLinearMap_eq, Algebra.TensorProduct.toLinearMap_includeRight]
+    change ((Algebra.TensorProduct.map (Polynomial.aeval (0 : R))
+             (AlgHom.id R R[X])).comp
+            (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X])))).toLinearMap = _
+    congr 1
+    apply Polynomial.algHom_ext
+    simp [Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.includeRight_apply]
+  lTensor_counit_comp_comul := by
+    rw [lTensor_toLinearMap_eq, Algebra.TensorProduct.toLinearMap_includeLeft]
+    change ((Algebra.TensorProduct.map (AlgHom.id R R[X])
+             (Polynomial.aeval (0 : R))).comp
+            (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X])))).toLinearMap = _
+    congr 1
+    apply Polynomial.algHom_ext
+    simp [Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.includeLeft_apply]
+  coassoc := by
+    rw [rTensor_toLinearMap_eq, lTensor_toLinearMap_eq]
+    change ((Algebra.TensorProduct.assoc R R R R[X] R[X] R[X]).toAlgHom.comp
+            ((Algebra.TensorProduct.map
+              (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X])))
+              (AlgHom.id R R[X])).comp
+             (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]))))).toLinearMap =
+           ((Algebra.TensorProduct.map (AlgHom.id R R[X])
+             (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X])))).comp
+            (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X])))).toLinearMap
+    congr 1
+    apply Polynomial.algHom_ext
+    simp only [AlgHom.comp_apply, AlgEquiv.toAlgHom_eq_coe,
+          AlgHom.coe_coe, Algebra.TensorProduct.map_tmul, AlgHom.id_apply, aeval_X,
+          map_add, map_one, Algebra.TensorProduct.one_def,
+          Algebra.TensorProduct.assoc_tmul,
+          TensorProduct.add_tmul, TensorProduct.tmul_add]
+    abel
 
-theorem mk_flip_one_eq_includeLeft :
-    (TensorProduct.mk R R[X] R).flip 1 =
-    (Algebra.TensorProduct.includeLeft : R[X] →ₐ[R] R[X] ⊗[R] R).toLinearMap := by
-  ext y; simp [Algebra.TensorProduct.includeLeft_apply, LinearMap.flip_apply]
+@[simp]
+theorem comul_X :
+    Coalgebra.comul (R := R) (X : R[X]) = (X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]) := by
+  change (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]))) X = _
+  simp
 
-theorem rTensor_comul_eq :
-    (comulAdditiveAlgHom R).toLinearMap.rTensor R[X] =
-    (Algebra.TensorProduct.map (comulAdditiveAlgHom R)
-     (AlgHom.id R R[X])).toLinearMap := by
-  ext x y; simp [LinearMap.rTensor_tmul]
+@[simp]
+theorem comul_C (r : R) :
+    Coalgebra.comul (R := R) (C r : R[X]) = (C r) ⊗ₜ 1 := by
+  change (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]))) (C r) = _
+  simp
 
-theorem lTensor_comul_eq :
-    (comulAdditiveAlgHom R).toLinearMap.lTensor R[X] =
-    (Algebra.TensorProduct.map (AlgHom.id R R[X])
-     (comulAdditiveAlgHom R)).toLinearMap := by
-  ext x y; simp [LinearMap.lTensor_tmul]
+@[simp]
+theorem counit_X :
+    Coalgebra.counit (R := R) (X : R[X]) = 0 := by
+  change (Polynomial.aeval (0 : R)) X = _
+  simp
 
-/-- The `𝔾ₐ` coalgebra instance on `R[X]`: coassociativity holds because both
-`(Δ ⊗ id) ∘ Δ` and `(id ⊗ Δ) ∘ Δ` send `X` to `X⊗1⊗1 + 1⊗X⊗1 + 1⊗1⊗X`. -/
-instance instCoalgebra : Coalgebra R R[X] :=
-  { instCoalgebraStruct R with
-    rTensor_counit_comp_comul := by
-      rw [counit_eq, comul_eq, rTensor_counit_eq, mk_one_eq_includeRight]
-      change ((Algebra.TensorProduct.map (counitAdditiveAlgHom R)
-               (AlgHom.id R R[X])).comp (comulAdditiveAlgHom R)).toLinearMap = _
-      congr 1
-      apply Polynomial.algHom_ext
-      simp [comulAdditiveAlgHom, counitAdditiveAlgHom,
-            Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.includeRight_apply]
-    lTensor_counit_comp_comul := by
-      rw [counit_eq, comul_eq, lTensor_counit_eq, mk_flip_one_eq_includeLeft]
-      change ((Algebra.TensorProduct.map (AlgHom.id R R[X])
-               (counitAdditiveAlgHom R)).comp (comulAdditiveAlgHom R)).toLinearMap = _
-      congr 1
-      apply Polynomial.algHom_ext
-      simp [comulAdditiveAlgHom, counitAdditiveAlgHom,
-            Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.includeLeft_apply]
-    coassoc := by
-      rw [comul_eq, rTensor_comul_eq, lTensor_comul_eq]
-      change ((Algebra.TensorProduct.assoc R R R R[X] R[X] R[X]).toAlgHom.comp
-              ((Algebra.TensorProduct.map (comulAdditiveAlgHom R)
-                (AlgHom.id R R[X])).comp
-               (comulAdditiveAlgHom R))).toLinearMap =
-             ((Algebra.TensorProduct.map (AlgHom.id R R[X])
-               (comulAdditiveAlgHom R)).comp
-              (comulAdditiveAlgHom R)).toLinearMap
-      congr 1
-      apply Polynomial.algHom_ext
-      simp only [comulAdditiveAlgHom, AlgHom.comp_apply,
-            Algebra.TensorProduct.map_tmul, AlgHom.id_apply, aeval_X,
-            map_add, map_one, Algebra.TensorProduct.one_def,
-            TensorProduct.add_tmul, TensorProduct.tmul_add]
-      abel }
+@[simp]
+theorem counit_C (r : R) :
+    Coalgebra.counit (R := R) (C r : R[X]) = r := by
+  change (Polynomial.aeval (0 : R)) (C r) = _
+  simp
 
 /-! ### Bialgebra instance -/
 
@@ -185,10 +143,12 @@ instance instCoalgebra : Coalgebra R R[X] :=
 homomorphisms by construction. -/
 instance instBialgebra : Bialgebra R R[X] :=
   Bialgebra.mk' R R[X]
-    (by simp [counit_eq])
-    (by intro a b; simp [counit_eq, map_mul])
-    (by simp [comul_eq])
-    (by intro a b; simp [comul_eq, map_mul])
+    (by change (Polynomial.aeval (0 : R)) 1 = 1; simp)
+    (fun {a b} => by change (Polynomial.aeval (0 : R)) (a * b) = _; simp [map_mul])
+    (by change (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]))) 1 = 1; simp)
+    (fun {a b} => by
+      change (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]))) (a * b) = _
+      simp [map_mul])
 
 end Polynomial
 
@@ -233,14 +193,14 @@ instance instHopfAlgebra : HopfAlgebra R R[X] where
         (Algebra.TensorProduct.map (antipodeAdditiveAlgHom R)
          (AlgHom.id R R[X])).toLinearMap := by
       ext x y; simp [LinearMap.rTensor_tmul]
-    rw [comul_eq, counit_eq, rTensor_eq, ← Algebra.TensorProduct.lmul'_toLinearMap]
-    -- Both sides are toLinearMap of algebra hom compositions. Convert and check on X.
+    rw [rTensor_eq, ← Algebra.TensorProduct.lmul'_toLinearMap]
     change ((Algebra.TensorProduct.lmul' R : R[X] ⊗[R] R[X] →ₐ[R] R[X]).comp
             ((Algebra.TensorProduct.map (antipodeAdditiveAlgHom R)
-              (AlgHom.id R R[X])).comp (comulAdditiveAlgHom R))).toLinearMap =
-           ((Algebra.ofId R R[X]).comp (counitAdditiveAlgHom R)).toLinearMap
+              (AlgHom.id R R[X])).comp
+             (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]))))).toLinearMap =
+           ((Algebra.ofId R R[X]).comp (Polynomial.aeval (0 : R))).toLinearMap
     congr 1; apply Polynomial.algHom_ext
-    simp [comulAdditiveAlgHom, antipodeAdditiveAlgHom, counitAdditiveAlgHom,
+    simp [antipodeAdditiveAlgHom,
           Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.lmul'_apply_tmul,
           Algebra.ofId_apply]
   mul_antipode_lTensor_comul := by
@@ -248,13 +208,14 @@ instance instHopfAlgebra : HopfAlgebra R R[X] where
         (Algebra.TensorProduct.map (AlgHom.id R R[X])
          (antipodeAdditiveAlgHom R)).toLinearMap := by
       ext x y; simp [LinearMap.lTensor_tmul]
-    rw [comul_eq, counit_eq, lTensor_eq, ← Algebra.TensorProduct.lmul'_toLinearMap]
+    rw [lTensor_eq, ← Algebra.TensorProduct.lmul'_toLinearMap]
     change ((Algebra.TensorProduct.lmul' R : R[X] ⊗[R] R[X] →ₐ[R] R[X]).comp
             ((Algebra.TensorProduct.map (AlgHom.id R R[X])
-              (antipodeAdditiveAlgHom R)).comp (comulAdditiveAlgHom R))).toLinearMap =
-           ((Algebra.ofId R R[X]).comp (counitAdditiveAlgHom R)).toLinearMap
+              (antipodeAdditiveAlgHom R)).comp
+             (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]))))).toLinearMap =
+           ((Algebra.ofId R R[X]).comp (Polynomial.aeval (0 : R))).toLinearMap
     congr 1; apply Polynomial.algHom_ext
-    simp [comulAdditiveAlgHom, antipodeAdditiveAlgHom, counitAdditiveAlgHom,
+    simp [antipodeAdditiveAlgHom,
           Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.lmul'_apply_tmul,
           Algebra.ofId_apply]
 

From 8796ae32eb74c1a0d9b8cb03f2e9f1036f92d945 Mon Sep 17 00:00:00 2001
From: Robin Langer <langer.robin@gmail.com>
Date: Sun, 24 May 2026 17:39:34 +1000
Subject: [PATCH 08/13] refactor: add CoalgebraStruct instance, comul/counit
 def/apply lemmas

Separate CoalgebraStruct from Coalgebra instance and add comul_def,
counit_def, comul_apply, counit_apply lemmas. This eliminates all
`change` tactics in favour of `rw`/`simp` with the new API lemmas.
---
 .../RingTheory/HopfAlgebra/Polynomial.lean    | 118 ++++++++----------
 1 file changed, 55 insertions(+), 63 deletions(-)

diff --git a/Mathlib/RingTheory/HopfAlgebra/Polynomial.lean b/Mathlib/RingTheory/HopfAlgebra/Polynomial.lean
index 04d440204a4080..27a92fa95d11f6 100644
--- a/Mathlib/RingTheory/HopfAlgebra/Polynomial.lean
+++ b/Mathlib/RingTheory/HopfAlgebra/Polynomial.lean
@@ -24,7 +24,8 @@ in `Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra`.
 
 ## Main definitions
 
-* `Polynomial.instCoalgebra`: the `R`-coalgebra structure on `R[X]` with additive
+* `Polynomial.instCoalgebraStruct`: the `R`-coalgebra structure data on `R[X]`.
+* `Polynomial.instCoalgebra`: the `R`-coalgebra instance on `R[X]` with additive
   comultiplication.
 * `Polynomial.instBialgebra`: the `R`-bialgebra structure on `R[X]`.
 * `Polynomial.instHopfAlgebra`: the `R`-Hopf algebra structure on `R[X]` when `R` is a
@@ -56,12 +57,53 @@ namespace Polynomial
 
 variable (R : Type*) [CommSemiring R]
 
-/-! ### Coalgebra instance
+/-! ### Coalgebra structure and instance
 
 The three coalgebra axioms (coassociativity, left counitality, right counitality)
 reduce to checking equality of `R`-algebra hom compositions on the generator `X`.
 -/
 
+/-- The `𝔾ₐ` coalgebra structure on `R[X]`: comultiplication sends `X` to `X ⊗ 1 + 1 ⊗ X`
+and counit evaluates at zero. -/
+instance instCoalgebraStruct : CoalgebraStruct R R[X] where
+  comul := (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]))).toLinearMap
+  counit := (Polynomial.aeval (0 : R)).toLinearMap
+
+theorem comul_def :
+    (Coalgebra.comul : R[X] →ₗ[R] R[X] ⊗[R] R[X]) =
+    (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]))).toLinearMap := rfl
+
+theorem counit_def :
+    (Coalgebra.counit : R[X] →ₗ[R] R) =
+    (Polynomial.aeval (0 : R)).toLinearMap := rfl
+
+theorem comul_apply (p : R[X]) :
+    Coalgebra.comul (R := R) p =
+    Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X])) p := rfl
+
+theorem counit_apply (p : R[X]) :
+    Coalgebra.counit (R := R) p = Polynomial.aeval (0 : R) p := rfl
+
+@[simp]
+theorem comul_X :
+    Coalgebra.comul (R := R) (X : R[X]) = (X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]) := by
+  simp [comul_apply]
+
+@[simp]
+theorem comul_C (r : R) :
+    Coalgebra.comul (R := R) (C r : R[X]) = (C r) ⊗ₜ 1 := by
+  simp [comul_apply]
+
+@[simp]
+theorem counit_X :
+    Coalgebra.counit (R := R) (X : R[X]) = 0 := by
+  simp [counit_apply]
+
+@[simp]
+theorem counit_C (r : R) :
+    Coalgebra.counit (R := R) (C r : R[X]) = r := by
+  simp [counit_apply]
+
 -- Glue lemmas connecting rTensor/lTensor of AlgHom.toLinearMap to Algebra.TensorProduct.map
 private theorem rTensor_toLinearMap_eq (f : R[X] →ₐ[R] A) :
     f.toLinearMap.rTensor R[X] =
@@ -76,34 +118,20 @@ private theorem lTensor_toLinearMap_eq (f : R[X] →ₐ[R] A) :
 /-- The `𝔾ₐ` coalgebra instance on `R[X]`: coassociativity holds because both
 `(Δ ⊗ id) ∘ Δ` and `(id ⊗ Δ) ∘ Δ` send `X` to `X⊗1⊗1 + 1⊗X⊗1 + 1⊗1⊗X`. -/
 instance instCoalgebra : Coalgebra R R[X] where
-  comul := (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]))).toLinearMap
-  counit := (Polynomial.aeval (0 : R)).toLinearMap
   rTensor_counit_comp_comul := by
-    rw [rTensor_toLinearMap_eq, Algebra.TensorProduct.toLinearMap_includeRight]
-    change ((Algebra.TensorProduct.map (Polynomial.aeval (0 : R))
-             (AlgHom.id R R[X])).comp
-            (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X])))).toLinearMap = _
+    rw [counit_def, comul_def, rTensor_toLinearMap_eq,
+        Algebra.TensorProduct.toLinearMap_includeRight]
     congr 1
     apply Polynomial.algHom_ext
     simp [Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.includeRight_apply]
   lTensor_counit_comp_comul := by
-    rw [lTensor_toLinearMap_eq, Algebra.TensorProduct.toLinearMap_includeLeft]
-    change ((Algebra.TensorProduct.map (AlgHom.id R R[X])
-             (Polynomial.aeval (0 : R))).comp
-            (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X])))).toLinearMap = _
+    rw [counit_def, comul_def, lTensor_toLinearMap_eq,
+        Algebra.TensorProduct.toLinearMap_includeLeft]
     congr 1
     apply Polynomial.algHom_ext
     simp [Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.includeLeft_apply]
   coassoc := by
-    rw [rTensor_toLinearMap_eq, lTensor_toLinearMap_eq]
-    change ((Algebra.TensorProduct.assoc R R R R[X] R[X] R[X]).toAlgHom.comp
-            ((Algebra.TensorProduct.map
-              (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X])))
-              (AlgHom.id R R[X])).comp
-             (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]))))).toLinearMap =
-           ((Algebra.TensorProduct.map (AlgHom.id R R[X])
-             (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X])))).comp
-            (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X])))).toLinearMap
+    rw [comul_def, rTensor_toLinearMap_eq, lTensor_toLinearMap_eq]
     congr 1
     apply Polynomial.algHom_ext
     simp only [AlgHom.comp_apply, AlgEquiv.toAlgHom_eq_coe,
@@ -113,42 +141,16 @@ instance instCoalgebra : Coalgebra R R[X] where
           TensorProduct.add_tmul, TensorProduct.tmul_add]
     abel
 
-@[simp]
-theorem comul_X :
-    Coalgebra.comul (R := R) (X : R[X]) = (X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]) := by
-  change (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]))) X = _
-  simp
-
-@[simp]
-theorem comul_C (r : R) :
-    Coalgebra.comul (R := R) (C r : R[X]) = (C r) ⊗ₜ 1 := by
-  change (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]))) (C r) = _
-  simp
-
-@[simp]
-theorem counit_X :
-    Coalgebra.counit (R := R) (X : R[X]) = 0 := by
-  change (Polynomial.aeval (0 : R)) X = _
-  simp
-
-@[simp]
-theorem counit_C (r : R) :
-    Coalgebra.counit (R := R) (C r : R[X]) = r := by
-  change (Polynomial.aeval (0 : R)) (C r) = _
-  simp
-
 /-! ### Bialgebra instance -/
 
 /-- The `𝔾ₐ` bialgebra instance on `R[X]`: the comultiplication and counit are algebra
 homomorphisms by construction. -/
 instance instBialgebra : Bialgebra R R[X] :=
   Bialgebra.mk' R R[X]
-    (by change (Polynomial.aeval (0 : R)) 1 = 1; simp)
-    (fun {a b} => by change (Polynomial.aeval (0 : R)) (a * b) = _; simp [map_mul])
-    (by change (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]))) 1 = 1; simp)
-    (fun {a b} => by
-      change (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]))) (a * b) = _
-      simp [map_mul])
+    (by simp [counit_apply])
+    (fun {a b} => by simp [counit_apply, map_mul])
+    (by simp [comul_apply])
+    (fun {a b} => by simp [comul_apply, map_mul])
 
 end Polynomial
 
@@ -193,12 +195,7 @@ instance instHopfAlgebra : HopfAlgebra R R[X] where
         (Algebra.TensorProduct.map (antipodeAdditiveAlgHom R)
          (AlgHom.id R R[X])).toLinearMap := by
       ext x y; simp [LinearMap.rTensor_tmul]
-    rw [rTensor_eq, ← Algebra.TensorProduct.lmul'_toLinearMap]
-    change ((Algebra.TensorProduct.lmul' R : R[X] ⊗[R] R[X] →ₐ[R] R[X]).comp
-            ((Algebra.TensorProduct.map (antipodeAdditiveAlgHom R)
-              (AlgHom.id R R[X])).comp
-             (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]))))).toLinearMap =
-           ((Algebra.ofId R R[X]).comp (Polynomial.aeval (0 : R))).toLinearMap
+    rw [comul_def, counit_def, rTensor_eq, ← Algebra.TensorProduct.lmul'_toLinearMap]
     congr 1; apply Polynomial.algHom_ext
     simp [antipodeAdditiveAlgHom,
           Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.lmul'_apply_tmul,
@@ -208,12 +205,7 @@ instance instHopfAlgebra : HopfAlgebra R R[X] where
         (Algebra.TensorProduct.map (AlgHom.id R R[X])
          (antipodeAdditiveAlgHom R)).toLinearMap := by
       ext x y; simp [LinearMap.lTensor_tmul]
-    rw [lTensor_eq, ← Algebra.TensorProduct.lmul'_toLinearMap]
-    change ((Algebra.TensorProduct.lmul' R : R[X] ⊗[R] R[X] →ₐ[R] R[X]).comp
-            ((Algebra.TensorProduct.map (AlgHom.id R R[X])
-              (antipodeAdditiveAlgHom R)).comp
-             (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]))))).toLinearMap =
-           ((Algebra.ofId R R[X]).comp (Polynomial.aeval (0 : R))).toLinearMap
+    rw [comul_def, counit_def, lTensor_eq, ← Algebra.TensorProduct.lmul'_toLinearMap]
     congr 1; apply Polynomial.algHom_ext
     simp [antipodeAdditiveAlgHom,
           Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.lmul'_apply_tmul,

From be9776d0acf448053a3edb73e2456bccbeeea034 Mon Sep 17 00:00:00 2001
From: Robin Langer <langer.robin@gmail.com>
Date: Mon, 25 May 2026 10:16:12 +1000
Subject: [PATCH 09/13] fix: add explicit type variables to glue lemmas

The private rTensor_toLinearMap_eq and lTensor_toLinearMap_eq lemmas
need explicit {A : Type*} [CommSemiring A] [Algebra R A] parameters
since they are no longer under a variable block that provides these.
---
 Mathlib/RingTheory/HopfAlgebra/Polynomial.lean | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/Mathlib/RingTheory/HopfAlgebra/Polynomial.lean b/Mathlib/RingTheory/HopfAlgebra/Polynomial.lean
index 27a92fa95d11f6..ddf1d0fee54d39 100644
--- a/Mathlib/RingTheory/HopfAlgebra/Polynomial.lean
+++ b/Mathlib/RingTheory/HopfAlgebra/Polynomial.lean
@@ -105,12 +105,14 @@ theorem counit_C (r : R) :
   simp [counit_apply]
 
 -- Glue lemmas connecting rTensor/lTensor of AlgHom.toLinearMap to Algebra.TensorProduct.map
-private theorem rTensor_toLinearMap_eq (f : R[X] →ₐ[R] A) :
+private theorem rTensor_toLinearMap_eq {A : Type*} [CommSemiring A] [Algebra R A]
+    (f : R[X] →ₐ[R] A) :
     f.toLinearMap.rTensor R[X] =
     (Algebra.TensorProduct.map f (AlgHom.id R R[X])).toLinearMap := by
   ext x y; simp [LinearMap.rTensor_tmul]
 
-private theorem lTensor_toLinearMap_eq (f : R[X] →ₐ[R] A) :
+private theorem lTensor_toLinearMap_eq {A : Type*} [CommSemiring A] [Algebra R A]
+    (f : R[X] →ₐ[R] A) :
     f.toLinearMap.lTensor R[X] =
     (Algebra.TensorProduct.map (AlgHom.id R R[X]) f).toLinearMap := by
   ext x y; simp [LinearMap.lTensor_tmul]

From 2572d75c4ef8d1c9cae403021d17aa3b1d228595 Mon Sep 17 00:00:00 2001
From: Robin Langer <langer.robin@gmail.com>
Date: Mon, 25 May 2026 13:10:10 +1000
Subject: [PATCH 10/13] refactor: CoalgebraStruct with named AlgHom defs, fix
 all proofs

Separate CoalgebraStruct from Coalgebra, add comulAlgHom/counitAlgHom
as named definitions, and provide comul_def/counit_def/comul_apply/
counit_apply API lemmas. All proofs verified with lake build.
---
 .../RingTheory/HopfAlgebra/Polynomial.lean    | 177 ++++++++++--------
 1 file changed, 100 insertions(+), 77 deletions(-)

diff --git a/Mathlib/RingTheory/HopfAlgebra/Polynomial.lean b/Mathlib/RingTheory/HopfAlgebra/Polynomial.lean
index ddf1d0fee54d39..4005e3c8949ce6 100644
--- a/Mathlib/RingTheory/HopfAlgebra/Polynomial.lean
+++ b/Mathlib/RingTheory/HopfAlgebra/Polynomial.lean
@@ -33,12 +33,9 @@ in `Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra`.
 
 ## Implementation notes
 
-The coalgebra axioms are equalities of linear maps, but both sides factor through
-algebra homomorphisms out of `R[X]`. Since `R[X]` is free on `X`, algebra hom equality
-reduces to checking on `X` alone (`Polynomial.algHom_ext`). The proofs convert between the
-linear map API (`rTensor`, `lTensor`, `TensorProduct.assoc`) and the algebra hom API
-(`Algebra.TensorProduct.map`, `includeRight`, `Algebra.TensorProduct.assoc`) via
-auxiliary lemmas, then apply `algHom_ext`.
+The coalgebra axioms are equalities of linear maps out of `R[X]`. Since comultiplication
+and counit are defined via `Polynomial.aeval`, each axiom reduces to checking on the
+generator `X`, exploiting the universal property of the polynomial ring.
 
 ## References
 
@@ -57,52 +54,52 @@ namespace Polynomial
 
 variable (R : Type*) [CommSemiring R]
 
-/-! ### Coalgebra structure and instance
+/-! ### Coalgebra structure and instance -/
 
-The three coalgebra axioms (coassociativity, left counitality, right counitality)
-reduce to checking equality of `R`-algebra hom compositions on the generator `X`.
--/
+/-- The comultiplication algebra homomorphism for `𝔾ₐ`, sending `X ↦ X ⊗ 1 + 1 ⊗ X`. -/
+def comulAlgHom : R[X] →ₐ[R] R[X] ⊗[R] R[X] :=
+  Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]))
+
+/-- The counit algebra homomorphism for `𝔾ₐ`, sending `X ↦ 0` (evaluation at zero). -/
+def counitAlgHom : R[X] →ₐ[R] R :=
+  Polynomial.aeval (0 : R)
 
-/-- The `𝔾ₐ` coalgebra structure on `R[X]`: comultiplication sends `X` to `X ⊗ 1 + 1 ⊗ X`
-and counit evaluates at zero. -/
+/-- The `𝔾ₐ` coalgebra structure on `R[X]`. -/
 instance instCoalgebraStruct : CoalgebraStruct R R[X] where
-  comul := (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]))).toLinearMap
-  counit := (Polynomial.aeval (0 : R)).toLinearMap
+  comul := (comulAlgHom R).toLinearMap
+  counit := (counitAlgHom R).toLinearMap
 
 theorem comul_def :
-    (Coalgebra.comul : R[X] →ₗ[R] R[X] ⊗[R] R[X]) =
-    (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]))).toLinearMap := rfl
+    (Coalgebra.comul : R[X] →ₗ[R] R[X] ⊗[R] R[X]) = (comulAlgHom R).toLinearMap := rfl
 
 theorem counit_def :
-    (Coalgebra.counit : R[X] →ₗ[R] R) =
-    (Polynomial.aeval (0 : R)).toLinearMap := rfl
+    (Coalgebra.counit : R[X] →ₗ[R] R) = (counitAlgHom R).toLinearMap := rfl
 
 theorem comul_apply (p : R[X]) :
-    Coalgebra.comul (R := R) p =
-    Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X])) p := rfl
+    Coalgebra.comul (R := R) p = comulAlgHom R p := rfl
 
 theorem counit_apply (p : R[X]) :
-    Coalgebra.counit (R := R) p = Polynomial.aeval (0 : R) p := rfl
+    Coalgebra.counit (R := R) p = counitAlgHom R p := rfl
 
 @[simp]
 theorem comul_X :
     Coalgebra.comul (R := R) (X : R[X]) = (X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]) := by
-  simp [comul_apply]
+  simp [comul_apply, comulAlgHom]
 
 @[simp]
 theorem comul_C (r : R) :
     Coalgebra.comul (R := R) (C r : R[X]) = (C r) ⊗ₜ 1 := by
-  simp [comul_apply]
+  simp [comul_apply, comulAlgHom]
 
 @[simp]
 theorem counit_X :
     Coalgebra.counit (R := R) (X : R[X]) = 0 := by
-  simp [counit_apply]
+  simp [counit_apply, counitAlgHom]
 
 @[simp]
 theorem counit_C (r : R) :
     Coalgebra.counit (R := R) (C r : R[X]) = r := by
-  simp [counit_apply]
+  simp [counit_apply, counitAlgHom]
 
 -- Glue lemmas connecting rTensor/lTensor of AlgHom.toLinearMap to Algebra.TensorProduct.map
 private theorem rTensor_toLinearMap_eq {A : Type*} [CommSemiring A] [Algebra R A]
@@ -117,42 +114,52 @@ private theorem lTensor_toLinearMap_eq {A : Type*} [CommSemiring A] [Algebra R A
     (Algebra.TensorProduct.map (AlgHom.id R R[X]) f).toLinearMap := by
   ext x y; simp [LinearMap.lTensor_tmul]
 
-/-- The `𝔾ₐ` coalgebra instance on `R[X]`: coassociativity holds because both
-`(Δ ⊗ id) ∘ Δ` and `(id ⊗ Δ) ∘ Δ` send `X` to `X⊗1⊗1 + 1⊗X⊗1 + 1⊗1⊗X`. -/
+/-- The `𝔾ₐ` coalgebra instance on `R[X]`. -/
 instance instCoalgebra : Coalgebra R R[X] where
   rTensor_counit_comp_comul := by
-    rw [counit_def, comul_def, rTensor_toLinearMap_eq,
-        Algebra.TensorProduct.toLinearMap_includeRight]
-    congr 1
-    apply Polynomial.algHom_ext
-    simp [Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.includeRight_apply]
+    dsimp only [Coalgebra.counit, Coalgebra.comul, CoalgebraStruct.counit, CoalgebraStruct.comul]
+    rw [rTensor_toLinearMap_eq, ← AlgHom.comp_toLinearMap,
+        ← AlgebraTensorModule.mk_eq, ← Algebra.TensorProduct.toLinearMap_includeRight]
+    congr 1; apply Polynomial.algHom_ext
+    simp [comulAlgHom, counitAlgHom,
+          Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.includeRight_apply]
   lTensor_counit_comp_comul := by
-    rw [counit_def, comul_def, lTensor_toLinearMap_eq,
-        Algebra.TensorProduct.toLinearMap_includeLeft]
-    congr 1
-    apply Polynomial.algHom_ext
-    simp [Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.includeLeft_apply]
+    dsimp only [Coalgebra.counit, Coalgebra.comul, CoalgebraStruct.counit, CoalgebraStruct.comul]
+    rw [lTensor_toLinearMap_eq, ← AlgHom.comp_toLinearMap,
+        ← AlgebraTensorModule.mk_eq, ← Algebra.TensorProduct.toLinearMap_includeLeft]
+    congr 1; apply Polynomial.algHom_ext
+    simp [comulAlgHom, counitAlgHom,
+          Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.includeLeft_apply]
   coassoc := by
-    rw [comul_def, rTensor_toLinearMap_eq, lTensor_toLinearMap_eq]
-    congr 1
-    apply Polynomial.algHom_ext
-    simp only [AlgHom.comp_apply, AlgEquiv.toAlgHom_eq_coe,
-          AlgHom.coe_coe, Algebra.TensorProduct.map_tmul, AlgHom.id_apply, aeval_X,
-          map_add, map_one, Algebra.TensorProduct.one_def,
-          Algebra.TensorProduct.assoc_tmul,
-          TensorProduct.add_tmul, TensorProduct.tmul_add]
-    abel
+    dsimp only [Coalgebra.comul, CoalgebraStruct.comul]
+    rw [rTensor_toLinearMap_eq, lTensor_toLinearMap_eq]
+    apply LinearMap.ext; intro p
+    simp only [LinearMap.comp_apply, AlgHom.toLinearMap_apply, LinearEquiv.coe_coe]
+    induction p using Polynomial.induction_on' with
+    | add p q hp hq => simp only [map_add] at hp hq ⊢; rw [hp, hq]
+    | monomial n r =>
+      simp only [← C_mul_X_pow_eq_monomial, comulAlgHom, map_mul, map_pow, aeval_X, aeval_C]
+      have hassoc : ∀ x, (TensorProduct.assoc R R[X] R[X] R[X]) x =
+          (Algebra.TensorProduct.assoc R R R[X] R[X] R[X] R[X]) x := fun _ => rfl
+      simp only [hassoc, map_mul, map_pow]
+      congr 1
+      · simp [Algebra.TensorProduct.one_def,
+              Algebra.algebraMap_eq_smul_one, TensorProduct.smul_tmul']
+      · congr 1
+        simp only [aeval_X, map_add, Algebra.TensorProduct.map_tmul, AlgHom.id_apply,
+              map_one, Algebra.TensorProduct.assoc_tmul,
+              Algebra.TensorProduct.one_def, TensorProduct.add_tmul, TensorProduct.tmul_add]
+        abel
 
 /-! ### Bialgebra instance -/
 
-/-- The `𝔾ₐ` bialgebra instance on `R[X]`: the comultiplication and counit are algebra
-homomorphisms by construction. -/
+/-- The `𝔾ₐ` bialgebra instance on `R[X]`. -/
 instance instBialgebra : Bialgebra R R[X] :=
   Bialgebra.mk' R R[X]
-    (by simp [counit_apply])
-    (fun {a b} => by simp [counit_apply, map_mul])
-    (by simp [comul_apply])
-    (fun {a b} => by simp [comul_apply, map_mul])
+    (by simp [counit_apply, counitAlgHom])
+    (fun {a b} => by simp [counit_apply, counitAlgHom, map_mul])
+    (by simp [comul_apply, comulAlgHom])
+    (fun {a b} => by simp [comul_apply, comulAlgHom, map_mul])
 
 end Polynomial
 
@@ -171,47 +178,63 @@ namespace Polynomial
 variable (R : Type*) [CommRing R]
 
 /-- The antipode on `R[X]` for the additive group scheme `𝔾ₐ`:
-the unique `R`-algebra homomorphism sending `X ↦ -X`.
-This is "inversion" on `𝔾ₐ`: if `Δ` encodes addition (`x ↦ x + x'`),
-then `S` encodes negation (`x ↦ -x`). -/
-def antipodeAdditiveAlgHom : R[X] →ₐ[R] R[X] :=
+the unique `R`-algebra homomorphism sending `X ↦ -X`. -/
+def antipodeAlgHom : R[X] →ₐ[R] R[X] :=
   Polynomial.aeval (-X : R[X])
 
 @[simp]
-theorem antipodeAdditiveAlgHom_X :
-    antipodeAdditiveAlgHom R (X : R[X]) = -X := by
-  simp [antipodeAdditiveAlgHom]
+theorem antipodeAlgHom_X :
+    antipodeAlgHom R (X : R[X]) = -X := by
+  simp [antipodeAlgHom]
 
 @[simp]
-theorem antipodeAdditiveAlgHom_C (r : R) :
-    antipodeAdditiveAlgHom R (C r) = C r := by
-  simp [antipodeAdditiveAlgHom]
+theorem antipodeAlgHom_C (r : R) :
+    antipodeAlgHom R (C r) = C r := by
+  simp [antipodeAlgHom]
 
 /-- The `𝔾ₐ` Hopf algebra instance on `R[X]` (requires `CommRing R` for the antipode
 `S(X) = -X`). The antipode axiom `m ∘ (S ⊗ id) ∘ Δ = η ∘ ε` holds because both sides
 send `X` to `0`: `S(X) · 1 + 1 · X = -X + X = 0 = C(ε(X))`. -/
 instance instHopfAlgebra : HopfAlgebra R R[X] where
-  antipode := (antipodeAdditiveAlgHom R).toLinearMap
+  antipode := (antipodeAlgHom R).toLinearMap
   mul_antipode_rTensor_comul := by
-    have rTensor_eq : (antipodeAdditiveAlgHom R).toLinearMap.rTensor R[X] =
-        (Algebra.TensorProduct.map (antipodeAdditiveAlgHom R)
+    have rTensor_eq : (antipodeAlgHom R).toLinearMap.rTensor R[X] =
+        (Algebra.TensorProduct.map (antipodeAlgHom R)
          (AlgHom.id R R[X])).toLinearMap := by
       ext x y; simp [LinearMap.rTensor_tmul]
-    rw [comul_def, counit_def, rTensor_eq, ← Algebra.TensorProduct.lmul'_toLinearMap]
-    congr 1; apply Polynomial.algHom_ext
-    simp [antipodeAdditiveAlgHom,
-          Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.lmul'_apply_tmul,
-          Algebra.ofId_apply]
+    dsimp only [Coalgebra.comul, Coalgebra.counit, CoalgebraStruct.comul,
+          CoalgebraStruct.counit, Polynomial.instCoalgebraStruct]
+    rw [rTensor_eq, ← Algebra.TensorProduct.lmul'_toLinearMap,
+        ← AlgHom.comp_toLinearMap, ← AlgHom.comp_toLinearMap]
+    have key : (Algebra.TensorProduct.lmul' R).comp
+          ((Algebra.TensorProduct.map (antipodeAlgHom R) (AlgHom.id R R[X])).comp
+           (comulAlgHom R)) =
+        (Algebra.ofId R R[X]).comp (counitAlgHom R) :=
+      Polynomial.algHom_ext (by
+        simp [antipodeAlgHom, comulAlgHom, counitAlgHom,
+              Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.lmul'_apply_tmul,
+              Algebra.ofId_apply])
+    rw [key, AlgHom.comp_toLinearMap]
+    ext p; simp [counitAlgHom, Algebra.linearMap_apply, Algebra.ofId_apply]
   mul_antipode_lTensor_comul := by
-    have lTensor_eq : (antipodeAdditiveAlgHom R).toLinearMap.lTensor R[X] =
+    have lTensor_eq : (antipodeAlgHom R).toLinearMap.lTensor R[X] =
         (Algebra.TensorProduct.map (AlgHom.id R R[X])
-         (antipodeAdditiveAlgHom R)).toLinearMap := by
+         (antipodeAlgHom R)).toLinearMap := by
       ext x y; simp [LinearMap.lTensor_tmul]
-    rw [comul_def, counit_def, lTensor_eq, ← Algebra.TensorProduct.lmul'_toLinearMap]
-    congr 1; apply Polynomial.algHom_ext
-    simp [antipodeAdditiveAlgHom,
-          Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.lmul'_apply_tmul,
-          Algebra.ofId_apply]
+    dsimp only [Coalgebra.comul, Coalgebra.counit, CoalgebraStruct.comul,
+          CoalgebraStruct.counit, Polynomial.instCoalgebraStruct]
+    rw [lTensor_eq, ← Algebra.TensorProduct.lmul'_toLinearMap,
+        ← AlgHom.comp_toLinearMap, ← AlgHom.comp_toLinearMap]
+    have key : (Algebra.TensorProduct.lmul' R).comp
+          ((Algebra.TensorProduct.map (AlgHom.id R R[X]) (antipodeAlgHom R)).comp
+           (comulAlgHom R)) =
+        (Algebra.ofId R R[X]).comp (counitAlgHom R) :=
+      Polynomial.algHom_ext (by
+        simp [antipodeAlgHom, comulAlgHom, counitAlgHom,
+              Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.lmul'_apply_tmul,
+              Algebra.ofId_apply])
+    rw [key, AlgHom.comp_toLinearMap]
+    ext p; simp [counitAlgHom, Algebra.linearMap_apply, Algebra.ofId_apply]
 
 end Polynomial
 

From d363bbc8720988ea416bf9670cb94db7075de604 Mon Sep 17 00:00:00 2001
From: Robin Langer <langer.robin@gmail.com>
Date: Fri, 5 Jun 2026 12:21:08 +1000
Subject: [PATCH 11/13] refactor: inline comul/counit in CoalgebraStruct
 instance

---
 Mathlib/RingTheory/HopfAlgebra/Polynomial.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/RingTheory/HopfAlgebra/Polynomial.lean b/Mathlib/RingTheory/HopfAlgebra/Polynomial.lean
index 4005e3c8949ce6..ab1a7f77c868e7 100644
--- a/Mathlib/RingTheory/HopfAlgebra/Polynomial.lean
+++ b/Mathlib/RingTheory/HopfAlgebra/Polynomial.lean
@@ -66,8 +66,8 @@ def counitAlgHom : R[X] →ₐ[R] R :=
 
 /-- The `𝔾ₐ` coalgebra structure on `R[X]`. -/
 instance instCoalgebraStruct : CoalgebraStruct R R[X] where
-  comul := (comulAlgHom R).toLinearMap
-  counit := (counitAlgHom R).toLinearMap
+  comul := (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]))).toLinearMap
+  counit := (Polynomial.aeval (0 : R)).toLinearMap
 
 theorem comul_def :
     (Coalgebra.comul : R[X] →ₗ[R] R[X] ⊗[R] R[X]) = (comulAlgHom R).toLinearMap := rfl

From a0825d5480f3a0c6fe31784363ec484f88447e33 Mon Sep 17 00:00:00 2001
From: Robin Langer <langer.robin@gmail.com>
Date: Fri, 5 Jun 2026 12:33:13 +1000
Subject: [PATCH 12/13] refactor: remove comulAlgHom/counitAlgHom, inline aeval
 expressions

---
 .../RingTheory/HopfAlgebra/Polynomial.lean    | 58 ++++++++-----------
 1 file changed, 25 insertions(+), 33 deletions(-)

diff --git a/Mathlib/RingTheory/HopfAlgebra/Polynomial.lean b/Mathlib/RingTheory/HopfAlgebra/Polynomial.lean
index ab1a7f77c868e7..79cea22efc8077 100644
--- a/Mathlib/RingTheory/HopfAlgebra/Polynomial.lean
+++ b/Mathlib/RingTheory/HopfAlgebra/Polynomial.lean
@@ -56,50 +56,44 @@ variable (R : Type*) [CommSemiring R]
 
 /-! ### Coalgebra structure and instance -/
 
-/-- The comultiplication algebra homomorphism for `𝔾ₐ`, sending `X ↦ X ⊗ 1 + 1 ⊗ X`. -/
-def comulAlgHom : R[X] →ₐ[R] R[X] ⊗[R] R[X] :=
-  Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]))
-
-/-- The counit algebra homomorphism for `𝔾ₐ`, sending `X ↦ 0` (evaluation at zero). -/
-def counitAlgHom : R[X] →ₐ[R] R :=
-  Polynomial.aeval (0 : R)
-
 /-- The `𝔾ₐ` coalgebra structure on `R[X]`. -/
 instance instCoalgebraStruct : CoalgebraStruct R R[X] where
   comul := (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]))).toLinearMap
   counit := (Polynomial.aeval (0 : R)).toLinearMap
 
 theorem comul_def :
-    (Coalgebra.comul : R[X] →ₗ[R] R[X] ⊗[R] R[X]) = (comulAlgHom R).toLinearMap := rfl
+    (Coalgebra.comul : R[X] →ₗ[R] R[X] ⊗[R] R[X]) =
+    (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]))).toLinearMap := rfl
 
 theorem counit_def :
-    (Coalgebra.counit : R[X] →ₗ[R] R) = (counitAlgHom R).toLinearMap := rfl
+    (Coalgebra.counit : R[X] →ₗ[R] R) = (Polynomial.aeval (0 : R)).toLinearMap := rfl
 
 theorem comul_apply (p : R[X]) :
-    Coalgebra.comul (R := R) p = comulAlgHom R p := rfl
+    Coalgebra.comul (R := R) p =
+    Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X])) p := rfl
 
 theorem counit_apply (p : R[X]) :
-    Coalgebra.counit (R := R) p = counitAlgHom R p := rfl
+    Coalgebra.counit (R := R) p = Polynomial.aeval (0 : R) p := rfl
 
 @[simp]
 theorem comul_X :
     Coalgebra.comul (R := R) (X : R[X]) = (X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]) := by
-  simp [comul_apply, comulAlgHom]
+  simp [comul_apply]
 
 @[simp]
 theorem comul_C (r : R) :
     Coalgebra.comul (R := R) (C r : R[X]) = (C r) ⊗ₜ 1 := by
-  simp [comul_apply, comulAlgHom]
+  simp [comul_apply]
 
 @[simp]
 theorem counit_X :
     Coalgebra.counit (R := R) (X : R[X]) = 0 := by
-  simp [counit_apply, counitAlgHom]
+  simp [counit_apply]
 
 @[simp]
 theorem counit_C (r : R) :
     Coalgebra.counit (R := R) (C r : R[X]) = r := by
-  simp [counit_apply, counitAlgHom]
+  simp [counit_apply]
 
 -- Glue lemmas connecting rTensor/lTensor of AlgHom.toLinearMap to Algebra.TensorProduct.map
 private theorem rTensor_toLinearMap_eq {A : Type*} [CommSemiring A] [Algebra R A]
@@ -121,15 +115,13 @@ instance instCoalgebra : Coalgebra R R[X] where
     rw [rTensor_toLinearMap_eq, ← AlgHom.comp_toLinearMap,
         ← AlgebraTensorModule.mk_eq, ← Algebra.TensorProduct.toLinearMap_includeRight]
     congr 1; apply Polynomial.algHom_ext
-    simp [comulAlgHom, counitAlgHom,
-          Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.includeRight_apply]
+    simp [Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.includeRight_apply]
   lTensor_counit_comp_comul := by
     dsimp only [Coalgebra.counit, Coalgebra.comul, CoalgebraStruct.counit, CoalgebraStruct.comul]
     rw [lTensor_toLinearMap_eq, ← AlgHom.comp_toLinearMap,
         ← AlgebraTensorModule.mk_eq, ← Algebra.TensorProduct.toLinearMap_includeLeft]
     congr 1; apply Polynomial.algHom_ext
-    simp [comulAlgHom, counitAlgHom,
-          Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.includeLeft_apply]
+    simp [Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.includeLeft_apply]
   coassoc := by
     dsimp only [Coalgebra.comul, CoalgebraStruct.comul]
     rw [rTensor_toLinearMap_eq, lTensor_toLinearMap_eq]
@@ -138,7 +130,7 @@ instance instCoalgebra : Coalgebra R R[X] where
     induction p using Polynomial.induction_on' with
     | add p q hp hq => simp only [map_add] at hp hq ⊢; rw [hp, hq]
     | monomial n r =>
-      simp only [← C_mul_X_pow_eq_monomial, comulAlgHom, map_mul, map_pow, aeval_X, aeval_C]
+      simp only [← C_mul_X_pow_eq_monomial, map_mul, map_pow, aeval_X, aeval_C]
       have hassoc : ∀ x, (TensorProduct.assoc R R[X] R[X] R[X]) x =
           (Algebra.TensorProduct.assoc R R R[X] R[X] R[X] R[X]) x := fun _ => rfl
       simp only [hassoc, map_mul, map_pow]
@@ -156,10 +148,10 @@ instance instCoalgebra : Coalgebra R R[X] where
 /-- The `𝔾ₐ` bialgebra instance on `R[X]`. -/
 instance instBialgebra : Bialgebra R R[X] :=
   Bialgebra.mk' R R[X]
-    (by simp [counit_apply, counitAlgHom])
-    (fun {a b} => by simp [counit_apply, counitAlgHom, map_mul])
-    (by simp [comul_apply, comulAlgHom])
-    (fun {a b} => by simp [comul_apply, comulAlgHom, map_mul])
+    (by simp [counit_apply])
+    (fun {a b} => by simp [counit_apply, map_mul])
+    (by simp [comul_apply])
+    (fun {a b} => by simp [comul_apply, map_mul])
 
 end Polynomial
 
@@ -208,14 +200,14 @@ instance instHopfAlgebra : HopfAlgebra R R[X] where
         ← AlgHom.comp_toLinearMap, ← AlgHom.comp_toLinearMap]
     have key : (Algebra.TensorProduct.lmul' R).comp
           ((Algebra.TensorProduct.map (antipodeAlgHom R) (AlgHom.id R R[X])).comp
-           (comulAlgHom R)) =
-        (Algebra.ofId R R[X]).comp (counitAlgHom R) :=
+           (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X])))) =
+        (Algebra.ofId R R[X]).comp (Polynomial.aeval (0 : R)) :=
       Polynomial.algHom_ext (by
-        simp [antipodeAlgHom, comulAlgHom, counitAlgHom,
+        simp [antipodeAlgHom,
               Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.lmul'_apply_tmul,
               Algebra.ofId_apply])
     rw [key, AlgHom.comp_toLinearMap]
-    ext p; simp [counitAlgHom, Algebra.linearMap_apply, Algebra.ofId_apply]
+    ext p; simp [Algebra.linearMap_apply, Algebra.ofId_apply]
   mul_antipode_lTensor_comul := by
     have lTensor_eq : (antipodeAlgHom R).toLinearMap.lTensor R[X] =
         (Algebra.TensorProduct.map (AlgHom.id R R[X])
@@ -227,14 +219,14 @@ instance instHopfAlgebra : HopfAlgebra R R[X] where
         ← AlgHom.comp_toLinearMap, ← AlgHom.comp_toLinearMap]
     have key : (Algebra.TensorProduct.lmul' R).comp
           ((Algebra.TensorProduct.map (AlgHom.id R R[X]) (antipodeAlgHom R)).comp
-           (comulAlgHom R)) =
-        (Algebra.ofId R R[X]).comp (counitAlgHom R) :=
+           (Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X])))) =
+        (Algebra.ofId R R[X]).comp (Polynomial.aeval (0 : R)) :=
       Polynomial.algHom_ext (by
-        simp [antipodeAlgHom, comulAlgHom, counitAlgHom,
+        simp [antipodeAlgHom,
               Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.lmul'_apply_tmul,
               Algebra.ofId_apply])
     rw [key, AlgHom.comp_toLinearMap]
-    ext p; simp [counitAlgHom, Algebra.linearMap_apply, Algebra.ofId_apply]
+    ext p; simp [Algebra.linearMap_apply, Algebra.ofId_apply]
 
 end Polynomial
 

From 02512ac5cb2305f79e522b1da7b43506a6113962 Mon Sep 17 00:00:00 2001
From: Robin Langer <langer.robin@gmail.com>
Date: Fri, 19 Jun 2026 00:33:13 +1000
Subject: [PATCH 13/13] =?UTF-8?q?refactor:=20apply=20review=20suggestions?=
 =?UTF-8?q?=20=E2=80=94=20simp=20lemmas,=20proof=20cleanup?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Make comul_apply and counit_apply @[simp], removing the now-redundant
comul_X, comul_C, counit_X, counit_C lemmas. Simplify coalgebra proofs
to use comul_def/counit_def and bare simp. Consolidate the coassoc
monomial case.
---
 .../RingTheory/HopfAlgebra/Polynomial.lean    | 47 ++++---------------
 1 file changed, 9 insertions(+), 38 deletions(-)

diff --git a/Mathlib/RingTheory/HopfAlgebra/Polynomial.lean b/Mathlib/RingTheory/HopfAlgebra/Polynomial.lean
index 79cea22efc8077..90d95486d76cf7 100644
--- a/Mathlib/RingTheory/HopfAlgebra/Polynomial.lean
+++ b/Mathlib/RingTheory/HopfAlgebra/Polynomial.lean
@@ -68,33 +68,15 @@ theorem comul_def :
 theorem counit_def :
     (Coalgebra.counit : R[X] →ₗ[R] R) = (Polynomial.aeval (0 : R)).toLinearMap := rfl
 
+@[simp]
 theorem comul_apply (p : R[X]) :
     Coalgebra.comul (R := R) p =
     Polynomial.aeval ((X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X])) p := rfl
 
+@[simp]
 theorem counit_apply (p : R[X]) :
     Coalgebra.counit (R := R) p = Polynomial.aeval (0 : R) p := rfl
 
-@[simp]
-theorem comul_X :
-    Coalgebra.comul (R := R) (X : R[X]) = (X : R[X]) ⊗ₜ 1 + 1 ⊗ₜ (X : R[X]) := by
-  simp [comul_apply]
-
-@[simp]
-theorem comul_C (r : R) :
-    Coalgebra.comul (R := R) (C r : R[X]) = (C r) ⊗ₜ 1 := by
-  simp [comul_apply]
-
-@[simp]
-theorem counit_X :
-    Coalgebra.counit (R := R) (X : R[X]) = 0 := by
-  simp [counit_apply]
-
-@[simp]
-theorem counit_C (r : R) :
-    Coalgebra.counit (R := R) (C r : R[X]) = r := by
-  simp [counit_apply]
-
 -- Glue lemmas connecting rTensor/lTensor of AlgHom.toLinearMap to Algebra.TensorProduct.map
 private theorem rTensor_toLinearMap_eq {A : Type*} [CommSemiring A] [Algebra R A]
     (f : R[X] →ₐ[R] A) :
@@ -111,37 +93,26 @@ private theorem lTensor_toLinearMap_eq {A : Type*} [CommSemiring A] [Algebra R A
 /-- The `𝔾ₐ` coalgebra instance on `R[X]`. -/
 instance instCoalgebra : Coalgebra R R[X] where
   rTensor_counit_comp_comul := by
-    dsimp only [Coalgebra.counit, Coalgebra.comul, CoalgebraStruct.counit, CoalgebraStruct.comul]
-    rw [rTensor_toLinearMap_eq, ← AlgHom.comp_toLinearMap,
+    rw [counit_def, comul_def, rTensor_toLinearMap_eq, ← AlgHom.comp_toLinearMap,
         ← AlgebraTensorModule.mk_eq, ← Algebra.TensorProduct.toLinearMap_includeRight]
     congr 1; apply Polynomial.algHom_ext
-    simp [Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.includeRight_apply]
+    simp
   lTensor_counit_comp_comul := by
-    dsimp only [Coalgebra.counit, Coalgebra.comul, CoalgebraStruct.counit, CoalgebraStruct.comul]
-    rw [lTensor_toLinearMap_eq, ← AlgHom.comp_toLinearMap,
+    rw [counit_def, comul_def, lTensor_toLinearMap_eq, ← AlgHom.comp_toLinearMap,
         ← AlgebraTensorModule.mk_eq, ← Algebra.TensorProduct.toLinearMap_includeLeft]
     congr 1; apply Polynomial.algHom_ext
-    simp [Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.includeLeft_apply]
+    simp
   coassoc := by
-    dsimp only [Coalgebra.comul, CoalgebraStruct.comul]
-    rw [rTensor_toLinearMap_eq, lTensor_toLinearMap_eq]
+    rw [comul_def, rTensor_toLinearMap_eq, lTensor_toLinearMap_eq]
     apply LinearMap.ext; intro p
     simp only [LinearMap.comp_apply, AlgHom.toLinearMap_apply, LinearEquiv.coe_coe]
     induction p using Polynomial.induction_on' with
     | add p q hp hq => simp only [map_add] at hp hq ⊢; rw [hp, hq]
     | monomial n r =>
-      simp only [← C_mul_X_pow_eq_monomial, map_mul, map_pow, aeval_X, aeval_C]
       have hassoc : ∀ x, (TensorProduct.assoc R R[X] R[X] R[X]) x =
           (Algebra.TensorProduct.assoc R R R[X] R[X] R[X] R[X]) x := fun _ => rfl
-      simp only [hassoc, map_mul, map_pow]
-      congr 1
-      · simp [Algebra.TensorProduct.one_def,
-              Algebra.algebraMap_eq_smul_one, TensorProduct.smul_tmul']
-      · congr 1
-        simp only [aeval_X, map_add, Algebra.TensorProduct.map_tmul, AlgHom.id_apply,
-              map_one, Algebra.TensorProduct.assoc_tmul,
-              Algebra.TensorProduct.one_def, TensorProduct.add_tmul, TensorProduct.tmul_add]
-        abel
+      simp [← C_mul_X_pow_eq_monomial, hassoc, Algebra.TensorProduct.one_def,
+        TensorProduct.add_tmul, TensorProduct.tmul_add, add_assoc]
 
 /-! ### Bialgebra instance -/