-- Module: Mathlib.RingTheory.Bialgebra.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Bialgebra S A
inst_5 : Bialgebra R B
inst_6 : Algebra R A
inst_7 : Algebra R S
inst_8 : IsScalarTower R S A
hcounit :
  Eq (α := (a : A ⊗[R] B) → S) (⇑counit : (a : A ⊗[R] B) → S)
    (⇑(AlgHom.toLinearMap
            (AlgHom.comp (B := S ⊗[R] R) ((↑(Algebra.TensorProduct.rid R S S) : S ⊗[R] R →ₐ[S] S) : S ⊗[R] R →ₐ[S] S)
              (Algebra.TensorProduct.map (counitAlgHom S A) (counitAlgHom R B) : A ⊗[R] B →ₐ[S] S ⊗[R] R)) :
          A ⊗[R] B →ₗ[S] S) :
      (a : A ⊗[R] B) → S)
hcomul :
  Eq (α := (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B)) (⇑comul : (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B))
    (⇑(AlgHom.toLinearMap
            (AlgHom.comp (B := TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B))
              ((↑(Algebra.TensorProduct.tensorTensorTensorComm R S R S A A B B) :
                  TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B) →ₐ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B)) :
                TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B) →ₐ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B))
              (Algebra.TensorProduct.map (comulAlgHom S A) (comulAlgHom R B) :
                A ⊗[R] B →ₐ[S] TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B))) :
          A ⊗[R] B →ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B)) :
      (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B))
x y : A ⊗[R] B
⊢ ((AlgHom.comp (B := TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B))
            ((↑(Algebra.TensorProduct.tensorTensorTensorComm R S R S A A B B) :
                TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B) →ₐ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B)) :
              TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B) →ₐ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B))
            (Algebra.TensorProduct.map (comulAlgHom S A) (comulAlgHom R B) :
              A ⊗[R] B →ₐ[S] TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B)) :
          A ⊗[R] B →ₐ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B)) :
        (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B))
      (x * y) =
    HMul.hMul (α := A ⊗[R] B ⊗[S] (A ⊗[R] B)) (β := A ⊗[R] B ⊗[S] (A ⊗[R] B))
      (((AlgHom.comp (B := TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B))
                ((↑(Algebra.TensorProduct.tensorTensorTensorComm R S R S A A B B) :
                    TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B) →ₐ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B)) :
                  TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B) →ₐ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B))
                (Algebra.TensorProduct.map (comulAlgHom S A) (comulAlgHom R B) :
                  A ⊗[R] B →ₐ[S] TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B)) :
              A ⊗[R] B →ₐ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B)) :
            (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B))
          x :
        A ⊗[R] B ⊗[S] (A ⊗[R] B))
      (((AlgHom.comp (B := TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B))
                ((↑(Algebra.TensorProduct.tensorTensorTensorComm R S R S A A B B) :
                    TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B) →ₐ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B)) :
                  TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B) →ₐ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B))
                (Algebra.TensorProduct.map (comulAlgHom S A) (comulAlgHom R B) :
                  A ⊗[R] B →ₐ[S] TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B)) :
              A ⊗[R] B →ₐ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B)) :
            (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B))
          y :
        A ⊗[R] B ⊗[S] (A ⊗[R] B))

Tactic:
simp only [map_one, map_mul]

Premises used: map_mul, map_one