From 420374b3e812036458cedfb8b91d546270db15e6 Mon Sep 17 00:00:00 2001
From: Jujian Zhang <jujian.zhang1998@outlook.com>
Date: Sun, 10 Mar 2024 04:08:37 +0000
Subject: [PATCH] missing lemma

---
 FLT/for_mathlib/Coalgebra/Monoid.lean  | 12 ++++++++++++
 FLT/for_mathlib/HopfAlgebra/Basic.lean | 15 +++------------
 2 files changed, 15 insertions(+), 12 deletions(-)

diff --git a/FLT/for_mathlib/Coalgebra/Monoid.lean b/FLT/for_mathlib/Coalgebra/Monoid.lean
index 29d4834d..74aad359 100644
--- a/FLT/for_mathlib/Coalgebra/Monoid.lean
+++ b/FLT/for_mathlib/Coalgebra/Monoid.lean
@@ -203,4 +203,16 @@ lemma mul_repr {ι : Type* } (a : A) (ℐ : Finset ι) (Δ₁ Δ₂ : ι → A)
 
 attribute [deprecated] mul_assoc' mul_one' one_mul'
 
+section commutative_bialgebra
+
+variable {A' : Type*} [CommSemiring A'] [Bialgebra R A']
+
+lemma comp_one {A' : Type*} [CommSemiring A'] [Bialgebra R A']
+    (f : AlgHomPoint R A' L) :
+    f.comp (1 : AlgHomPoint R A' A') = 1 := by
+  ext
+  simp [one_def, Algebra.ofId_apply, Algebra.algebraMap_eq_smul_one, f.map_smul, f.map_one]
+
+end commutative_bialgebra
+
 end AlgHomPoint
diff --git a/FLT/for_mathlib/HopfAlgebra/Basic.lean b/FLT/for_mathlib/HopfAlgebra/Basic.lean
index cd08a846..3be9ca67 100644
--- a/FLT/for_mathlib/HopfAlgebra/Basic.lean
+++ b/FLT/for_mathlib/HopfAlgebra/Basic.lean
@@ -148,25 +148,16 @@ noncomputable instance instGroup : Group (AlgHomPoint R A L) where
 end AlgHomPoint
 
 lemma antipodeAlgHom_inv : antipodeAlgHom⁻¹ = AlgHom.id R A :=
-  inv_eq_iff_mul_eq_one.mpr <| AlgHom.ext fun x ↦ congr($(antipode_mul_id) x)
+  inv_eq_iff_mul_eq_one.mpr <| mul_eq_one_iff_eq_inv.mpr rfl
 
 lemma antipodeAlgHom_mul_id : antipodeAlgHom * AlgHom.id R A = 1 :=
   AlgHom.ext fun _ ↦ congr($(antipode_mul_id) _)
 
-
 lemma id_mul_antipodeAlgHom : AlgHom.id R A * antipodeAlgHom = 1 :=
   AlgHom.ext fun _ ↦ congr($(id_mul_antipode) _)
 
-lemma antipodeAlgHom_square : antipodeAlgHom.comp antipodeAlgHom = AlgHom.id R A := by
-  suffices antipodeAlgHom * (antipodeAlgHom.comp antipodeAlgHom) = (1 : AlgHomPoint R A A) by
-    conv_rhs at this => rw [← antipodeAlgHom_mul_id]
-    simpa only [mul_right_inj] using this
-  ext a
-  simp_rw [AlgHomPoint.mul_repr (repr := Coalgebra.comul_repr a),
-    AlgHom.coe_comp, Function.comp_apply, ← antipodeAlgHom.map_mul, ← map_sum,
-    antipodeAlgHom_apply, antipode_repr_eq_smul' (repr := Coalgebra.comul_repr a), map_smul,
-    antipode_one, Algebra.smul_def, mul_one]
-  rfl
+lemma antipodeAlgHom_square : antipodeAlgHom.comp antipodeAlgHom = AlgHom.id R A :=
+  antipodeAlgHom_inv
 
 /--
 Then antipode map is an algebra equivalence.