chore(RingTheory/Coalgebra/TensorProduct): generalize (leanprover-community#29157)

Defining `comul` and `counit` for tensor products should only require `CoalgebraStruct` and not `Coalgebra`.

Author: themathqueen

Mathlib/RingTheory/Coalgebra/TensorProduct.lean

@@ -25,13 +25,15 @@ the base change `S ⊗[R] B` as an `S`-coalgebra.
 open TensorProduct
 
 variable {R S A B : Type*} [CommSemiring R] [CommSemiring S] [AddCommMonoid A] [AddCommMonoid B]
-    [Algebra R S] [Module R A] [Module S A] [Module R B] [Coalgebra R B]
-    [Coalgebra S A] [IsScalarTower R S A]
+    [Algebra R S] [Module R A] [Module S A] [Module R B] [IsScalarTower R S A]
 
 namespace TensorProduct
 
 open Coalgebra
 
+section CoalgebraStruct
+variable [CoalgebraStruct R B] [CoalgebraStruct S A]
+
 noncomputable
 instance instCoalgebraStruct : CoalgebraStruct S (A ⊗[R] B) where
   comul :=
@@ -63,6 +65,10 @@ lemma comul_tmul (x : A) (y : B) :
 lemma counit_tmul (x : A) (y : B) :
     counit (R := S) (x ⊗ₜ[R] y) = counit (R := R) y • counit (R := S) x := rfl
 
+end CoalgebraStruct
+
+variable [Coalgebra R B] [Coalgebra S A]
+
 open Lean.Parser.Tactic in
 /-- `hopf_tensor_induction x with x₁ x₂` attempts to replace `x` by
 `x₁ ⊗ₜ x₂` via linearity. This is an implementation detail that is used to set up tensor products