@@ -124,7 +124,7 @@ instance instHopfAlgebra : HopfAlgebra R T[M] where
124124 simp only [coe_coe, comul_apply, map_add, map_tmul, antipode_ι_apply, id_coe, id_eq,
125125 mul'_apply, mul_one, ← map_one (algebraMap R T[M]), antipode_algebraMap_apply]
126126 simp only [map_one, mul_one, one_mul, neg_add_cancel]
127- | mul u v hu hv =>
127+ | mul u v hu hv =>
128128 conv =>
129129 rhs
130130 rw [convOne_apply, counit_mul, map_mul, ← convOne_apply, ← convOne_apply]
@@ -156,7 +156,7 @@ instance instHopfAlgebra : HopfAlgebra R T[M] where
156156 rw [LinearMap.lTensor, ← LinearMap.convMul_def, ← convOne_def]
157157 ext x
158158 induction x using induction with
159- | algebraMap r =>
159+ | algebraMap r =>
160160 simp only [convMul_apply, comul_algebraMap, TensorProduct.algebraMap_apply, map_tmul,
161161 id_coe, id_eq, mul'_apply, convOne_apply, counit_algebraMap, ← map_one (algebraMap R
162162 T[M]), antipode_algebraMap_apply]
@@ -175,7 +175,7 @@ instance instHopfAlgebra : HopfAlgebra R T[M] where
175175 mul'_apply, mul_one, ← map_one (algebraMap R T[M]), antipode_algebraMap_apply]
176176 simp only [map_one, mul_one, one_mul, neg_add_cancel]
177177 abel_nf
178- | mul u v hu hv =>
178+ | mul u v hu hv =>
179179 conv =>
180180 rhs
181181 rw [convOne_apply, counit_mul, map_mul, Algebra.commutes, ← convOne_apply,
0 commit comments