Module: Mathlib.RingTheory.Bialgebra.TensorProduct

Goal state before:
pp: 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✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Bialgebra S A
inst✝³ : Bialgebra R B
inst✝² : Algebra R A
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S A
hcounit :
  ⇑counit =
    ⇑((↑(Algebra.TensorProduct.rid R S S)).comp
          (Algebra.TensorProduct.map (counitAlgHom S A) (counitAlgHom R B))).toLinearMap
hcomul :
  ⇑comul =
    ⇑((↑(Algebra.TensorProduct.tensorTensorTensorComm R S R S A A B B)).comp
          (Algebra.TensorProduct.map (comulAlgHom S A) (comulAlgHom R B))).toLinearMap
⊢ Bialgebra S (A ⊗[R] B)

Tactic:
refine Bialgebra.mk' S (A ⊗[R] B) ?_ (fun {x y} => ?_) ?_ (fun {x y} => ?_)

Goal state after:
case refine_1
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✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Bialgebra S A
inst✝³ : Bialgebra R B
inst✝² : Algebra R A
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S A
hcounit :
  ⇑counit =
    ⇑((↑(Algebra.TensorProduct.rid R S S)).comp
          (Algebra.TensorProduct.map (counitAlgHom S A) (counitAlgHom R B))).toLinearMap
hcomul :
  ⇑comul =
    ⇑((↑(Algebra.TensorProduct.tensorTensorTensorComm R S R S A A B B)).comp
          (Algebra.TensorProduct.map (comulAlgHom S A) (comulAlgHom R B))).toLinearMap
⊢ counit 1 = 1

case refine_2
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✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Bialgebra S A
inst✝³ : Bialgebra R B
inst✝² : Algebra R A
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S A
hcounit :
  ⇑counit =
    ⇑((↑(Algebra.TensorProduct.rid R S S)).comp
          (Algebra.TensorProduct.map (counitAlgHom S A) (counitAlgHom R B))).toLinearMap
hcomul :
  ⇑comul =
    ⇑((↑(Algebra.TensorProduct.tensorTensorTensorComm R S R S A A B B)).comp
          (Algebra.TensorProduct.map (comulAlgHom S A) (comulAlgHom R B))).toLinearMap
x y : A ⊗[R] B
⊢ counit (x * y) = counit x * counit y

case refine_3
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✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Bialgebra S A
inst✝³ : Bialgebra R B
inst✝² : Algebra R A
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S A
hcounit :
  ⇑counit =
    ⇑((↑(Algebra.TensorProduct.rid R S S)).comp
          (Algebra.TensorProduct.map (counitAlgHom S A) (counitAlgHom R B))).toLinearMap
hcomul :
  ⇑comul =
    ⇑((↑(Algebra.TensorProduct.tensorTensorTensorComm R S R S A A B B)).comp
          (Algebra.TensorProduct.map (comulAlgHom S A) (comulAlgHom R B))).toLinearMap
⊢ comul 1 = 1

case refine_4
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✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Bialgebra S A
inst✝³ : Bialgebra R B
inst✝² : Algebra R A
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S A
hcounit :
  ⇑counit =
    ⇑((↑(Algebra.TensorProduct.rid R S S)).comp
          (Algebra.TensorProduct.map (counitAlgHom S A) (counitAlgHom R B))).toLinearMap
hcomul :
  ⇑comul =
    ⇑((↑(Algebra.TensorProduct.tensorTensorTensorComm R S R S A A B B)).comp
          (Algebra.TensorProduct.map (comulAlgHom S A) (comulAlgHom R B))).toLinearMap
x y : A ⊗[R] B
⊢ comul (x * y) = comul x * comul y