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} => ?_) <;>
  simp_all only [AlgHom.toLinearMap_apply]

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
⊢ ((↑(Algebra.TensorProduct.rid R S S)).comp (Algebra.TensorProduct.map (counitAlgHom S A) (counitAlgHom R B))) 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
⊢ ((↑(Algebra.TensorProduct.rid R S S)).comp (Algebra.TensorProduct.map (counitAlgHom S A) (counitAlgHom R B)))
      (x * y) =
    ((↑(Algebra.TensorProduct.rid R S S)).comp (Algebra.TensorProduct.map (counitAlgHom S A) (counitAlgHom R B))) x *
      ((↑(Algebra.TensorProduct.rid R S S)).comp (Algebra.TensorProduct.map (counitAlgHom S A) (counitAlgHom R B))) 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
⊢ ((↑(Algebra.TensorProduct.tensorTensorTensorComm R S R S A A B B)).comp
        (Algebra.TensorProduct.map (comulAlgHom S A) (comulAlgHom R B)))
      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
⊢ ((↑(Algebra.TensorProduct.tensorTensorTensorComm R S R S A A B B)).comp
        (Algebra.TensorProduct.map (comulAlgHom S A) (comulAlgHom R B)))
      (x * y) =
    ((↑(Algebra.TensorProduct.tensorTensorTensorComm R S R S A A B B)).comp
          (Algebra.TensorProduct.map (comulAlgHom S A) (comulAlgHom R B)))
        x *
      ((↑(Algebra.TensorProduct.tensorTensorTensorComm R S R S A A B B)).comp
          (Algebra.TensorProduct.map (comulAlgHom S A) (comulAlgHom R B)))
        y