awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Bialgebra.SymmetricAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
h :
  ∀ (x : M),
    Eq (α := SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
      (((↑(AlgHom.comp
                    (↑(Algebra.TensorProduct.comm R (SymmetricAlgebra R M) (SymmetricAlgebra R M)) :
                      SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M →ₐ[R]
                        SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                    (Bialgebra.comulAlgHom R (SymmetricAlgebra R M))) :
                [inst_3 :
                    FunLike (SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                      (SymmetricAlgebra R M) (SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)] →
                  [SemilinearMapClass (SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                        (RingHom.id R) (SymmetricAlgebra R M) (SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)] →
                    SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) ∘ₗ
              ι R M :
            (a : M) → SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
          x :
        SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
      (((↑(Bialgebra.comulAlgHom R (SymmetricAlgebra R M)) :
                [inst_3 :
                    FunLike (SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                      (SymmetricAlgebra R M) (SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)] →
                  [SemilinearMapClass (SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                        (RingHom.id R) (SymmetricAlgebra R M) (SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)] →
                    SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) ∘ₗ
              ι R M :
            (a : M) → SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
          x :
        SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
⊢ Eq (α := SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
    (AlgHom.comp
      (↑(Algebra.TensorProduct.comm R (SymmetricAlgebra R M) (SymmetricAlgebra R M)) :
        SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
      (Bialgebra.comulAlgHom R (SymmetricAlgebra R M)))
    (Bialgebra.comulAlgHom R (SymmetricAlgebra R M))

Tactic:
ext x
-- Module: Mathlib.RingTheory.Bialgebra.SymmetricAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
h :
  HAdd.hAdd (α := SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) (β := SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
      (1 ⊗ₜ[R] (ι R M : (a : M) → SymmetricAlgebra R M) x : SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
      ((ι R M : (a : M) → SymmetricAlgebra R M) x ⊗ₜ[R] 1 : SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) =
    HAdd.hAdd (α := SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) (β :=
      SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
      ((ι R M : (a : M) → SymmetricAlgebra R M) x ⊗ₜ[R] 1 : SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
      (1 ⊗ₜ[R] (ι R M : (a : M) → SymmetricAlgebra R M) x : SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
⊢ Eq (α := SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
    (((↑(AlgHom.comp
                  (↑(Algebra.TensorProduct.comm R (SymmetricAlgebra R M) (SymmetricAlgebra R M)) :
                    SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                  (Bialgebra.comulAlgHom R (SymmetricAlgebra R M))) :
              [inst_3 :
                  FunLike (SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                    (SymmetricAlgebra R M) (SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)] →
                [SemilinearMapClass (SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                      (RingHom.id R) (SymmetricAlgebra R M) (SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)] →
                  SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) ∘ₗ
            ι R M :
          (a : M) → SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
        x :
      SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
    (((↑(Bialgebra.comulAlgHom R (SymmetricAlgebra R M)) :
              [inst_3 :
                  FunLike (SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                    (SymmetricAlgebra R M) (SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)] →
                [SemilinearMapClass (SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                      (RingHom.id R) (SymmetricAlgebra R M) (SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)] →
                  SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) ∘ₗ
            ι R M :
          (a : M) → SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
        x :
      SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)

Tactic:
simp
-- Module: Mathlib.RingTheory.Bialgebra.SymmetricAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
⊢ HAdd.hAdd (α := SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) (β := SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
      (1 ⊗ₜ[R] (ι R M : (a : M) → SymmetricAlgebra R M) x : SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
      ((ι R M : (a : M) → SymmetricAlgebra R M) x ⊗ₜ[R] 1 : SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) =
    HAdd.hAdd (α := SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) (β :=
      SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
      ((ι R M : (a : M) → SymmetricAlgebra R M) x ⊗ₜ[R] 1 : SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
      (1 ⊗ₜ[R] (ι R M : (a : M) → SymmetricAlgebra R M) x : SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)

Tactic:
abel
-- Module: Mathlib.RingTheory.Bialgebra.SymmetricAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
    (AlgHom.comp
      (↑(Algebra.TensorProduct.comm R (SymmetricAlgebra R M) (SymmetricAlgebra R M)) :
        SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
      (Bialgebra.comulAlgHom R (SymmetricAlgebra R M)))
    (Bialgebra.comulAlgHom R (SymmetricAlgebra R M))

Tactic:
have h : (Algebra.TensorProduct.comm R (SymmetricAlgebra R M)
          (SymmetricAlgebra R M)).toAlgHom.comp (Bialgebra.comulAlgHom R _) =
        Bialgebra.comulAlgHom R (SymmetricAlgebra R M) := by
      ext x
      simp
      abel
-- Module: Mathlib.RingTheory.Bialgebra.SymmetricAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
h :
  Eq (α := SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
    (AlgHom.comp
      (↑(Algebra.TensorProduct.comm R (SymmetricAlgebra R M) (SymmetricAlgebra R M)) :
        SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
      (Bialgebra.comulAlgHom R (SymmetricAlgebra R M)))
    (Bialgebra.comulAlgHom R (SymmetricAlgebra R M))
⊢ Eq (α := SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
    ((↑(TensorProduct.comm R (SymmetricAlgebra R M) (SymmetricAlgebra R M)) :
        SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) ∘ₗ
      CoalgebraStruct.comul)
    CoalgebraStruct.comul

Tactic:
congr(($h).toLinearMap)

Premises used: AlgHom.toLinearMap, congrArg, id
-- Module: Mathlib.RingTheory.Bialgebra.SymmetricAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
h :
  Eq (α := SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
    (AlgHom.comp
      (↑(Algebra.TensorProduct.comm R (SymmetricAlgebra R M) (SymmetricAlgebra R M)) :
        SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
      (Bialgebra.comulAlgHom R (SymmetricAlgebra R M)))
    (Bialgebra.comulAlgHom R (SymmetricAlgebra R M))
⊢ Eq (α := SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
    ((↑(TensorProduct.comm R (SymmetricAlgebra R M) (SymmetricAlgebra R M)) :
        SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) ∘ₗ
      CoalgebraStruct.comul)
    CoalgebraStruct.comul

Tactic:
exact congr(($h).toLinearMap)
-- Module: Mathlib.RingTheory.Bialgebra.SymmetricAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := SymmetricAlgebra R M →ₐ[R] R) (Bialgebra.counitAlgHom R (SymmetricAlgebra R M)) algebraMapInv

Tactic:
rfl

Premises used: SymmetricAlgebra.algebraMapInv, AlgHom.ofLinearMap, Bialgebra.counitAlgHom, rfl
-- Module: Mathlib.RingTheory.Bialgebra.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
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
⊢ Eq (α := A ⊗[R] B →ₗ[S] S) (counit : A ⊗[R] B →ₗ[S] 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)

Tactic:
rfl

Premises used: AlgHom.toLinearMap, Quotient.liftOn', AddCon.liftOn, rfl
-- Module: Mathlib.RingTheory.Bialgebra.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
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
⊢ Eq (α := A ⊗[R] B →ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B)) comul
    (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))))

Tactic:
rfl

Premises used: AlgHom.toLinearMap, Quotient.liftOn', AddCon.liftOn, rfl
-- 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
⊢ 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)

Tactic:
have hcounit := congr(DFunLike.coe $(counit_eq_algHom_toLinearMap R S A B))
-- 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)
⊢ 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))

Tactic:
have hcomul := congr(DFunLike.coe $(comul_eq_algHom_toLinearMap R S A B))
-- 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))
refine_1 : Eq.{u_2 + 1} (α := S) ((counit : (a : A ⊗[R] B) → S) 1 : S) (1 : S)
refine_2 :
  ∀ {x y : A ⊗[R] B},
    (counit : (a : A ⊗[R] B) → S) (x * y) =
      HMul.hMul (α := S) (β := S) ((counit : (a : A ⊗[R] B) → S) x : S) ((counit : (a : A ⊗[R] B) → S) y : S)
refine_3 : Eq (α := A ⊗[R] B ⊗[S] (A ⊗[R] B)) ((comul : (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B)) 1) 1
refine_4 :
  ∀ {x y : A ⊗[R] B},
    (comul : (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))
        ((comul : (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B)) x : A ⊗[R] B ⊗[S] (A ⊗[R] B))
        ((comul : (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B)) y : A ⊗[R] B ⊗[S] (A ⊗[R] B))
⊢ Bialgebra S (A ⊗[R] B)

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

Premises used: Bialgebra.mk', TensorProduct
-- 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))
refine_1 :
  Eq.{u_2 + 1} (α := S)
    (((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)
        1 :
      S)
    (1 : S)
⊢ Eq.{u_2 + 1} (α := S) ((counit : (a : A ⊗[R] B) → S) 1 : S) (1 : S)

Tactic:
simp_all only [AlgHom.toLinearMap_apply]

Premises used: AlgHom.toLinearMap_apply
-- 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
refine_2 :
  ((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)
      (x * y) =
    HMul.hMul (α := S) (β := S)
      (((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)
          x :
        S)
      (((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)
          y :
        S)
⊢ (counit : (a : A ⊗[R] B) → S) (x * y) =
    HMul.hMul (α := S) (β := S) ((counit : (a : A ⊗[R] B) → S) x : S) ((counit : (a : A ⊗[R] B) → S) y : S)

Tactic:
simp_all only [AlgHom.toLinearMap_apply]

Premises used: AlgHom.toLinearMap_apply
-- 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))
refine_3 :
  Eq (α := 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))
      1)
    1
⊢ Eq (α := A ⊗[R] B ⊗[S] (A ⊗[R] B)) ((comul : (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B)) 1) 1

Tactic:
simp_all only [AlgHom.toLinearMap_apply]

Premises used: AlgHom.toLinearMap_apply