awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
Goal:
R_1 : Type u_1
S_1 : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : AddCommMonoid A
inst_3 : AddCommMonoid B
inst_4 : Algebra R_1 S_1
inst_5 : Module R_1 A
inst_6 : Module S_1 A
inst_7 : Module R_1 B
inst_8 : IsScalarTower R_1 S_1 A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst_9 : CommSemiring R
inst_10 : CommSemiring S
inst_11 : Algebra R S
inst_12 : AddCommMonoid M
inst_13 : AddCommMonoid N
inst_14 : AddCommMonoid P
inst_15 : AddCommMonoid Q
inst_16 : Module R M
inst_17 : Module R N
inst_18 : Module R P
inst_19 : Module R Q
inst_20 : Module S M
inst_21 : IsScalarTower R S M
inst_22 : Coalgebra S M
inst_23 : Module S N
inst_24 : IsScalarTower R S N
inst_25 : Coalgebra S N
inst_26 : Coalgebra R P
inst_27 : Coalgebra R Q
a :
  ∀ (x : M) (x_1 : N) (x_2 : P),
    Eq.{u_6 + 1} (α := S)
      (((((((AlgebraTensorModule.curry
                            (AlgebraTensorModule.curry
                              ((counit : M ⊗[S] (N ⊗[R] P) →ₗ[S] S) ∘ₗ
                                  ((↑(AlgebraTensorModule.assoc R S S M N P) :
                                      M ⊗[S] N ⊗[R] P →ₗ[S] M ⊗[S] (N ⊗[R] P)) :
                                    M ⊗[S] N ⊗[R] P →ₗ[S] M ⊗[S] (N ⊗[R] P)) :
                                M ⊗[S] N ⊗[R] P →ₗ[S] S)) :
                          M →ₗ[S] N →ₗ[S] P →ₗ[R] S) :
                        (a : M) → N →ₗ[S] P →ₗ[R] S)
                      x :
                    N →ₗ[S] P →ₗ[R] S) :
                  (a : N) → P →ₗ[R] S)
                x_1 :
              P →ₗ[R] S) :
            (a : P) → S)
          x_2 :
        S)
      (((((((AlgebraTensorModule.curry (AlgebraTensorModule.curry counit) : M →ₗ[S] N →ₗ[S] P →ₗ[R] S) :
                        (a : M) → N →ₗ[S] P →ₗ[R] S)
                      x :
                    N →ₗ[S] P →ₗ[R] S) :
                  (a : N) → P →ₗ[R] S)
                x_1 :
              P →ₗ[R] S) :
            (a : P) → S)
          x_2 :
        S)
⊢ Eq (α := M ⊗[S] N ⊗[R] P →ₗ[S] S)
    ((counit : M ⊗[S] (N ⊗[R] P) →ₗ[S] S) ∘ₗ
        ((↑(AlgebraTensorModule.assoc R S S M N P) : M ⊗[S] N ⊗[R] P →ₗ[S] M ⊗[S] (N ⊗[R] P)) :
          M ⊗[S] N ⊗[R] P →ₗ[S] M ⊗[S] (N ⊗[R] P)) :
      M ⊗[S] N ⊗[R] P →ₗ[S] S)
    (counit : M ⊗[S] N ⊗[R] P →ₗ[S] S)

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
Goal:
R_1 : Type u_1
S_1 : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : AddCommMonoid A
inst_3 : AddCommMonoid B
inst_4 : Algebra R_1 S_1
inst_5 : Module R_1 A
inst_6 : Module S_1 A
inst_7 : Module R_1 B
inst_8 : IsScalarTower R_1 S_1 A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst_9 : CommSemiring R
inst_10 : CommSemiring S
inst_11 : Algebra R S
inst_12 : AddCommMonoid M
inst_13 : AddCommMonoid N
inst_14 : AddCommMonoid P
inst_15 : AddCommMonoid Q
inst_16 : Module R M
inst_17 : Module R N
inst_18 : Module R P
inst_19 : Module R Q
inst_20 : Module S M
inst_21 : IsScalarTower R S M
inst_22 : Coalgebra S M
inst_23 : Module S N
inst_24 : IsScalarTower R S N
inst_25 : Coalgebra S N
inst_26 : Coalgebra R P
inst_27 : Coalgebra R Q
x : M
x_1 : N
x_2 : P
⊢ Eq.{u_6 + 1} (α := S)
    (((((((AlgebraTensorModule.curry
                          (AlgebraTensorModule.curry
                            ((counit : M ⊗[S] (N ⊗[R] P) →ₗ[S] S) ∘ₗ
                                ((↑(AlgebraTensorModule.assoc R S S M N P) : M ⊗[S] N ⊗[R] P →ₗ[S] M ⊗[S] (N ⊗[R] P)) :
                                  M ⊗[S] N ⊗[R] P →ₗ[S] M ⊗[S] (N ⊗[R] P)) :
                              M ⊗[S] N ⊗[R] P →ₗ[S] S)) :
                        M →ₗ[S] N →ₗ[S] P →ₗ[R] S) :
                      (a : M) → N →ₗ[S] P →ₗ[R] S)
                    x :
                  N →ₗ[S] P →ₗ[R] S) :
                (a : N) → P →ₗ[R] S)
              x_1 :
            P →ₗ[R] S) :
          (a : P) → S)
        x_2 :
      S)
    (((((((AlgebraTensorModule.curry (AlgebraTensorModule.curry counit) : M →ₗ[S] N →ₗ[S] P →ₗ[R] S) :
                      (a : M) → N →ₗ[S] P →ₗ[R] S)
                    x :
                  N →ₗ[S] P →ₗ[R] S) :
                (a : N) → P →ₗ[R] S)
              x_1 :
            P →ₗ[R] S) :
          (a : P) → S)
        x_2 :
      S)

Tactic:
simp
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
Goal:
R_1 : Type u_1
S_1 : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : AddCommMonoid A
inst_3 : AddCommMonoid B
inst_4 : Algebra R_1 S_1
inst_5 : Module R_1 A
inst_6 : Module S_1 A
inst_7 : Module R_1 B
inst_8 : IsScalarTower R_1 S_1 A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst_9 : CommSemiring R
inst_10 : CommSemiring S
inst_11 : Algebra R S
inst_12 : AddCommMonoid M
inst_13 : AddCommMonoid N
inst_14 : AddCommMonoid P
inst_15 : AddCommMonoid Q
inst_16 : Module R M
inst_17 : Module R N
inst_18 : Module R P
inst_19 : Module R Q
inst_20 : Module S M
inst_21 : IsScalarTower R S M
inst_22 : Coalgebra S M
inst_23 : Module S N
inst_24 : IsScalarTower R S N
inst_25 : Coalgebra S N
inst_26 : Coalgebra R P
inst_27 : Coalgebra R Q
x : M
y : N
z : P
x₁ x₂ : M
y₁ y₂ : N
z₁ z₂ : P
⊢ Eq (α := M ⊗[S] (N ⊗[R] P) ⊗[S] (M ⊗[S] (N ⊗[R] P)))
    (((_root_.TensorProduct.map (↑(AlgebraTensorModule.assoc R S S M N P) : M ⊗[S] N ⊗[R] P →ₗ[S] M ⊗[S] (N ⊗[R] P))
              (↑(AlgebraTensorModule.assoc R S S M N P) : M ⊗[S] N ⊗[R] P →ₗ[S] M ⊗[S] (N ⊗[R] P)) :
            M ⊗[S] N ⊗[R] P ⊗[S] (M ⊗[S] N ⊗[R] P) →ₗ[S] M ⊗[S] (N ⊗[R] P) ⊗[S] (M ⊗[S] (N ⊗[R] P))) :
          (a : M ⊗[S] N ⊗[R] P ⊗[S] (M ⊗[S] N ⊗[R] P)) → M ⊗[S] (N ⊗[R] P) ⊗[S] (M ⊗[S] (N ⊗[R] P)))
        (((AlgebraTensorModule.tensorTensorTensorComm R S R S (M ⊗[S] N) (M ⊗[S] N) P P :
              M ⊗[S] N ⊗[S] (M ⊗[S] N) ⊗[R] (P ⊗[R] P) ≃ₗ[S] M ⊗[S] N ⊗[R] P ⊗[S] (M ⊗[S] N ⊗[R] P)) :
            (a : M ⊗[S] N ⊗[S] (M ⊗[S] N) ⊗[R] (P ⊗[R] P)) → M ⊗[S] N ⊗[R] P ⊗[S] (M ⊗[S] N ⊗[R] P))
          (((AlgebraTensorModule.tensorTensorTensorComm S S S S M M N N :
                  TensorProduct.{u_6, u_7, u_8} S (M ⊗[S] M) (N ⊗[S] N) ≃ₗ[S] M ⊗[S] N ⊗[S] (M ⊗[S] N)) :
                (a : M ⊗[S] M ⊗[S] (N ⊗[S] N)) → M ⊗[S] N ⊗[S] (M ⊗[S] N))
              (x₁ ⊗ₜ[S] x₂ ⊗ₜ[S] (y₁ ⊗ₜ[S] y₂)) ⊗ₜ[R]
            (z₁ ⊗ₜ[R] z₂))) :
      M ⊗[S] (N ⊗[R] P) ⊗[S] (M ⊗[S] (N ⊗[R] P)))
    (((AlgebraTensorModule.tensorTensorTensorComm S S S S M M (N ⊗[R] P) (N ⊗[R] P) :
            M ⊗[S] M ⊗[S] (N ⊗[R] P ⊗[S] (N ⊗[R] P)) ≃ₗ[S] M ⊗[S] (N ⊗[R] P) ⊗[S] (M ⊗[S] (N ⊗[R] P))) :
          (a : M ⊗[S] M ⊗[S] (N ⊗[R] P ⊗[S] (N ⊗[R] P))) → M ⊗[S] (N ⊗[R] P) ⊗[S] (M ⊗[S] (N ⊗[R] P)))
        (x₁ ⊗ₜ[S] x₂ ⊗ₜ[S]
          ((AlgebraTensorModule.tensorTensorTensorComm R S R S N N P P :
                TensorProduct.{u_5, u_8, u_9} R (N ⊗[S] N) (P ⊗[R] P) ≃ₗ[S] N ⊗[R] P ⊗[S] (N ⊗[R] P)) :
              (a : N ⊗[S] N ⊗[R] (P ⊗[R] P)) → N ⊗[R] P ⊗[S] (N ⊗[R] P))
            (y₁ ⊗ₜ[S] y₂ ⊗ₜ[R] (z₁ ⊗ₜ[R] z₂))) :
      M ⊗[S] (N ⊗[R] P) ⊗[S] (M ⊗[S] (N ⊗[R] P)))

Tactic:
simp
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
Goal:
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : AddCommMonoid P
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R P
inst_9 : Module S M
inst_10 : IsScalarTower R S M
inst_11 : Coalgebra S M
inst_12 : Module S N
inst_13 : IsScalarTower R S N
inst_14 : Coalgebra S N
inst_15 : Coalgebra R P
x : M
y : N
z : P
⊢ Eq (α := M ⊗[S] (N ⊗[R] P))
    (((TensorProduct.assoc R S M N P : M ⊗[S] N ⊗[R] P ≃ₗc[S] M ⊗[S] (N ⊗[R] P)) :
          (a : M ⊗[S] N ⊗[R] P) → M ⊗[S] (N ⊗[R] P))
        (x ⊗ₜ[S] y ⊗ₜ[R] z) :
      M ⊗[S] (N ⊗[R] P))
    (x ⊗ₜ[S] (y ⊗ₜ[R] z) : M ⊗[S] (N ⊗[R] P))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
Goal:
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : AddCommMonoid P
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R P
inst_9 : Module S M
inst_10 : IsScalarTower R S M
inst_11 : Coalgebra S M
inst_12 : Module S N
inst_13 : IsScalarTower R S N
inst_14 : Coalgebra S N
inst_15 : Coalgebra R P
x : M
y : N
z : P
⊢ Eq (α := M ⊗[S] N ⊗[R] P)
    (((CoalgEquiv.symm (TensorProduct.assoc R S M N P) : M ⊗[S] (N ⊗[R] P) ≃ₗc[S] M ⊗[S] N ⊗[R] P) :
          (a : M ⊗[S] (N ⊗[R] P)) → M ⊗[S] N ⊗[R] P)
        (x ⊗ₜ[S] (y ⊗ₜ[R] z)) :
      M ⊗[S] N ⊗[R] P)
    (x ⊗ₜ[S] y ⊗ₜ[R] z : M ⊗[S] N ⊗[R] P)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
Goal:
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : AddCommMonoid P
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R P
inst_9 : Module S M
inst_10 : IsScalarTower R S M
inst_11 : Coalgebra S M
inst_12 : Module S N
inst_13 : IsScalarTower R S N
inst_14 : Coalgebra S N
inst_15 : Coalgebra R P
⊢ Eq (α := M ⊗[S] N ⊗[R] P ≃ₗ[S] M ⊗[S] (N ⊗[R] P))
    (CoalgEquiv.toLinearEquiv (TensorProduct.assoc R S M N P : M ⊗[S] N ⊗[R] P ≃ₗc[S] M ⊗[S] (N ⊗[R] P)) :
      M ⊗[S] N ⊗[R] P ≃ₗ[S] M ⊗[S] (N ⊗[R] P))
    (AlgebraTensorModule.assoc R S S M N P : M ⊗[S] N ⊗[R] P ≃ₗ[S] M ⊗[S] (N ⊗[R] P))

Tactic:
rfl

Premises used: LinearEquiv.ofLinear, rfl, TensorProduct.AlgebraTensorModule.assoc, TensorProduct.AlgebraTensorModule.lift
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
Goal:
R_1 : Type u_1
S_1 : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : AddCommMonoid A
inst_3 : AddCommMonoid B
inst_4 : Algebra R_1 S_1
inst_5 : Module R_1 A
inst_6 : Module S_1 A
inst_7 : Module R_1 B
inst_8 : IsScalarTower R_1 S_1 A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst_9 : CommSemiring R
inst_10 : CommSemiring S
inst_11 : Algebra R S
inst_12 : AddCommMonoid M
inst_13 : AddCommMonoid N
inst_14 : AddCommMonoid P
inst_15 : AddCommMonoid Q
inst_16 : Module R M
inst_17 : Module R N
inst_18 : Module R P
inst_19 : Module R Q
inst_20 : Module S M
inst_21 : IsScalarTower R S M
inst_22 : Coalgebra S M
inst_23 : Module S N
inst_24 : IsScalarTower R S N
inst_25 : Coalgebra S N
inst_26 : Coalgebra R P
inst_27 : Coalgebra R Q
a :
  ∀ (x : P),
    Eq.{u_5 + 1} (α := R)
      ((((AlgebraTensorModule.curry (counit ∘ₗ (↑(_root_.TensorProduct.lid R P) : R ⊗[R] P →ₗ[R] P)) :
                  R →ₗ[R] P →ₗ[R] R) :
                (a : R) → P →ₗ[R] R)
              1 :
            (a : P) → R)
          x :
        R)
      ((((AlgebraTensorModule.curry counit : R →ₗ[R] P →ₗ[R] R) : (a : R) → P →ₗ[R] R) 1 : (a : P) → R) x : R)
⊢ Eq (α := R ⊗[R] P →ₗ[R] R) (counit ∘ₗ (↑(_root_.TensorProduct.lid R P) : R ⊗[R] P →ₗ[R] P)) counit

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
Goal:
R_1 : Type u_1
S_1 : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : AddCommMonoid A
inst_3 : AddCommMonoid B
inst_4 : Algebra R_1 S_1
inst_5 : Module R_1 A
inst_6 : Module S_1 A
inst_7 : Module R_1 B
inst_8 : IsScalarTower R_1 S_1 A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst_9 : CommSemiring R
inst_10 : CommSemiring S
inst_11 : Algebra R S
inst_12 : AddCommMonoid M
inst_13 : AddCommMonoid N
inst_14 : AddCommMonoid P
inst_15 : AddCommMonoid Q
inst_16 : Module R M
inst_17 : Module R N
inst_18 : Module R P
inst_19 : Module R Q
inst_20 : Module S M
inst_21 : IsScalarTower R S M
inst_22 : Coalgebra S M
inst_23 : Module S N
inst_24 : IsScalarTower R S N
inst_25 : Coalgebra S N
inst_26 : Coalgebra R P
inst_27 : Coalgebra R Q
x : P
⊢ Eq.{u_5 + 1} (α := R)
    ((((AlgebraTensorModule.curry (counit ∘ₗ (↑(_root_.TensorProduct.lid R P) : R ⊗[R] P →ₗ[R] P)) :
                R →ₗ[R] P →ₗ[R] R) :
              (a : R) → P →ₗ[R] R)
            1 :
          (a : P) → R)
        x :
      R)
    ((((AlgebraTensorModule.curry counit : R →ₗ[R] P →ₗ[R] R) : (a : R) → P →ₗ[R] R) 1 : (a : P) → R) x : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
Goal:
R_1 : Type u_1
S_1 : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : AddCommMonoid A
inst_3 : AddCommMonoid B
inst_4 : Algebra R_1 S_1
inst_5 : Module R_1 A
inst_6 : Module S_1 A
inst_7 : Module R_1 B
inst_8 : IsScalarTower R_1 S_1 A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst_9 : CommSemiring R
inst_10 : CommSemiring S
inst_11 : Algebra R S
inst_12 : AddCommMonoid M
inst_13 : AddCommMonoid N
inst_14 : AddCommMonoid P
inst_15 : AddCommMonoid Q
inst_16 : Module R M
inst_17 : Module R N
inst_18 : Module R P
inst_19 : Module R Q
inst_20 : Module S M
inst_21 : IsScalarTower R S M
inst_22 : Coalgebra S M
inst_23 : Module S N
inst_24 : IsScalarTower R S N
inst_25 : Coalgebra S N
inst_26 : Coalgebra R P
inst_27 : Coalgebra R Q
a :
  ∀ (x : P),
    Eq (α := P ⊗[R] P)
      ((((AlgebraTensorModule.curry
                    (_root_.TensorProduct.map (↑(_root_.TensorProduct.lid R P) : R ⊗[R] P →ₗ[R] P)
                        (↑(_root_.TensorProduct.lid R P) : R ⊗[R] P →ₗ[R] P) ∘ₗ
                      comul) :
                  LinearMap.{u_5, u_5, u_5, u_9} (RingHom.id R) R (P →ₗ[R] P ⊗[R] P)) :
                (a : R) → P →ₗ[R] P ⊗[R] P)
              1 :
            (a : P) → P ⊗[R] P)
          x :
        P ⊗[R] P)
      ((((AlgebraTensorModule.curry (comul ∘ₗ (↑(_root_.TensorProduct.lid R P) : R ⊗[R] P →ₗ[R] P)) :
                  LinearMap.{u_5, u_5, u_5, u_9} (RingHom.id R) R (P →ₗ[R] P ⊗[R] P)) :
                (a : R) → P →ₗ[R] P ⊗[R] P)
              1 :
            (a : P) → P ⊗[R] P)
          x :
        P ⊗[R] P)
⊢ Eq (α := R ⊗[R] P →ₗ[R] P ⊗[R] P)
    (_root_.TensorProduct.map (↑(_root_.TensorProduct.lid R P) : R ⊗[R] P →ₗ[R] P)
        (↑(_root_.TensorProduct.lid R P) : R ⊗[R] P →ₗ[R] P) ∘ₗ
      comul)
    (comul ∘ₗ (↑(_root_.TensorProduct.lid R P) : R ⊗[R] P →ₗ[R] P))

Tactic:
ext x
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
Goal:
R_1 : Type u_1
S_1 : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : AddCommMonoid A
inst_3 : AddCommMonoid B
inst_4 : Algebra R_1 S_1
inst_5 : Module R_1 A
inst_6 : Module S_1 A
inst_7 : Module R_1 B
inst_8 : IsScalarTower R_1 S_1 A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst_9 : CommSemiring R
inst_10 : CommSemiring S
inst_11 : Algebra R S
inst_12 : AddCommMonoid M
inst_13 : AddCommMonoid N
inst_14 : AddCommMonoid P
inst_15 : AddCommMonoid Q
inst_16 : Module R M
inst_17 : Module R N
inst_18 : Module R P
inst_19 : Module R Q
inst_20 : Module S M
inst_21 : IsScalarTower R S M
inst_22 : Coalgebra S M
inst_23 : Module S N
inst_24 : IsScalarTower R S N
inst_25 : Coalgebra S N
inst_26 : Coalgebra R P
inst_27 : Coalgebra R Q
x : P
a :
  Eq.{u_9 + 1} (α := P ⊗[R] P)
    ((_root_.TensorProduct.map (↑(_root_.TensorProduct.lid R P) : R ⊗[R] P →ₗ[R] P)
            (↑(_root_.TensorProduct.lid R P) : R ⊗[R] P →ₗ[R] P) :
          (a : R ⊗[R] P ⊗[R] (R ⊗[R] P)) → P ⊗[R] P)
        (((AlgebraTensorModule.tensorTensorTensorComm R R R R R R P P :
              TensorProduct.{u_5, u_5, u_9} R (R ⊗[R] R) (P ⊗[R] P) ≃ₗ[R] R ⊗[R] P ⊗[R] (R ⊗[R] P)) :
            (a : R ⊗[R] R ⊗[R] (P ⊗[R] P)) → R ⊗[R] P ⊗[R] (R ⊗[R] P))
          (1 ⊗ₜ[R] 1 ⊗ₜ[R] (comul : (a : P) → P ⊗[R] P) x)) :
      P ⊗[R] P)
    ((comul : (a : P) → P ⊗[R] P) (HSMul.hSMul.{u_5, u_9, u_9} (α := R) 1 x) : P ⊗[R] P)
⊢ Eq (α := P ⊗[R] P)
    ((((AlgebraTensorModule.curry
                  (_root_.TensorProduct.map (↑(_root_.TensorProduct.lid R P) : R ⊗[R] P →ₗ[R] P)
                      (↑(_root_.TensorProduct.lid R P) : R ⊗[R] P →ₗ[R] P) ∘ₗ
                    comul) :
                LinearMap.{u_5, u_5, u_5, u_9} (RingHom.id R) R (P →ₗ[R] P ⊗[R] P)) :
              (a : R) → P →ₗ[R] P ⊗[R] P)
            1 :
          (a : P) → P ⊗[R] P)
        x :
      P ⊗[R] P)
    ((((AlgebraTensorModule.curry (comul ∘ₗ (↑(_root_.TensorProduct.lid R P) : R ⊗[R] P →ₗ[R] P)) :
                LinearMap.{u_5, u_5, u_5, u_9} (RingHom.id R) R (P →ₗ[R] P ⊗[R] P)) :
              (a : R) → P →ₗ[R] P ⊗[R] P)
            1 :
          (a : P) → P ⊗[R] P)
        x :
      P ⊗[R] P)

Tactic:
dsimp
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
Goal:
R_1 : Type u_1
S_1 : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : AddCommMonoid A
inst_3 : AddCommMonoid B
inst_4 : Algebra R_1 S_1
inst_5 : Module R_1 A
inst_6 : Module S_1 A
inst_7 : Module R_1 B
inst_8 : IsScalarTower R_1 S_1 A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst_9 : CommSemiring R
inst_10 : CommSemiring S
inst_11 : Algebra R S
inst_12 : AddCommMonoid M
inst_13 : AddCommMonoid N
inst_14 : AddCommMonoid P
inst_15 : AddCommMonoid Q
inst_16 : Module R M
inst_17 : Module R N
inst_18 : Module R P
inst_19 : Module R Q
inst_20 : Module S M
inst_21 : IsScalarTower R S M
inst_22 : Coalgebra S M
inst_23 : Module S N
inst_24 : IsScalarTower R S N
inst_25 : Coalgebra S N
inst_26 : Coalgebra R P
inst_27 : Coalgebra R Q
x : P
a :
  Eq.{u_9 + 1} (α := P ⊗[R] P)
    ((_root_.TensorProduct.map (↑(_root_.TensorProduct.lid R P) : R ⊗[R] P →ₗ[R] P)
            (↑(_root_.TensorProduct.lid R P) : R ⊗[R] P →ₗ[R] P) :
          (a : R ⊗[R] P ⊗[R] (R ⊗[R] P)) → P ⊗[R] P)
        (((AlgebraTensorModule.tensorTensorTensorComm R R R R R R P P :
              TensorProduct.{u_5, u_5, u_9} R (R ⊗[R] R) (P ⊗[R] P) ≃ₗ[R] R ⊗[R] P ⊗[R] (R ⊗[R] P)) :
            (a : R ⊗[R] R ⊗[R] (P ⊗[R] P)) → R ⊗[R] P ⊗[R] (R ⊗[R] P))
          (1 ⊗ₜ[R] 1 ⊗ₜ[R] (comul : (a : P) → P ⊗[R] P) x)) :
      P ⊗[R] P)
    ((comul : (a : P) → P ⊗[R] P) x : P ⊗[R] P)
⊢ Eq.{u_9 + 1} (α := P ⊗[R] P)
    ((_root_.TensorProduct.map (↑(_root_.TensorProduct.lid R P) : R ⊗[R] P →ₗ[R] P)
            (↑(_root_.TensorProduct.lid R P) : R ⊗[R] P →ₗ[R] P) :
          (a : R ⊗[R] P ⊗[R] (R ⊗[R] P)) → P ⊗[R] P)
        (((AlgebraTensorModule.tensorTensorTensorComm R R R R R R P P :
              TensorProduct.{u_5, u_5, u_9} R (R ⊗[R] R) (P ⊗[R] P) ≃ₗ[R] R ⊗[R] P ⊗[R] (R ⊗[R] P)) :
            (a : R ⊗[R] R ⊗[R] (P ⊗[R] P)) → R ⊗[R] P ⊗[R] (R ⊗[R] P))
          (1 ⊗ₜ[R] 1 ⊗ₜ[R] (comul : (a : P) → P ⊗[R] P) x)) :
      P ⊗[R] P)
    ((comul : (a : P) → P ⊗[R] P) (HSMul.hSMul.{u_5, u_9, u_9} (α := R) 1 x) : P ⊗[R] P)

Tactic:
simp only [one_smul]

Premises used: one_smul
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
Goal:
R_1 : Type u_1
S_1 : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : AddCommMonoid A
inst_3 : AddCommMonoid B
inst_4 : Algebra R_1 S_1
inst_5 : Module R_1 A
inst_6 : Module S_1 A
inst_7 : Module R_1 B
inst_8 : IsScalarTower R_1 S_1 A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst_9 : CommSemiring R
inst_10 : CommSemiring S
inst_11 : Algebra R S
inst_12 : AddCommMonoid M
inst_13 : AddCommMonoid N
inst_14 : AddCommMonoid P
inst_15 : AddCommMonoid Q
inst_16 : Module R M
inst_17 : Module R N
inst_18 : Module R P
inst_19 : Module R Q
inst_20 : Module S M
inst_21 : IsScalarTower R S M
inst_22 : Coalgebra S M
inst_23 : Module S N
inst_24 : IsScalarTower R S N
inst_25 : Coalgebra S N
inst_26 : Coalgebra R P
inst_27 : Coalgebra R Q
x : P
a :
  ∀ (x₁ x₂ : P),
    Eq.{u_9 + 1} (α := P ⊗[R] P)
      ((_root_.TensorProduct.map (↑(_root_.TensorProduct.lid R P) : R ⊗[R] P →ₗ[R] P)
              (↑(_root_.TensorProduct.lid R P) : R ⊗[R] P →ₗ[R] P) :
            (a : R ⊗[R] P ⊗[R] (R ⊗[R] P)) → P ⊗[R] P)
          (((AlgebraTensorModule.tensorTensorTensorComm R R R R R R P P :
                TensorProduct.{u_5, u_5, u_9} R (R ⊗[R] R) (P ⊗[R] P) ≃ₗ[R] R ⊗[R] P ⊗[R] (R ⊗[R] P)) :
              (a : R ⊗[R] R ⊗[R] (P ⊗[R] P)) → R ⊗[R] P ⊗[R] (R ⊗[R] P))
            (1 ⊗ₜ[R] 1 ⊗ₜ[R] (x₁ ⊗ₜ[R] x₂))) :
        P ⊗[R] P)
      (x₁ ⊗ₜ[R] x₂ : P ⊗[R] P)
⊢ Eq.{u_9 + 1} (α := P ⊗[R] P)
    ((_root_.TensorProduct.map (↑(_root_.TensorProduct.lid R P) : R ⊗[R] P →ₗ[R] P)
            (↑(_root_.TensorProduct.lid R P) : R ⊗[R] P →ₗ[R] P) :
          (a : R ⊗[R] P ⊗[R] (R ⊗[R] P)) → P ⊗[R] P)
        (((AlgebraTensorModule.tensorTensorTensorComm R R R R R R P P :
              TensorProduct.{u_5, u_5, u_9} R (R ⊗[R] R) (P ⊗[R] P) ≃ₗ[R] R ⊗[R] P ⊗[R] (R ⊗[R] P)) :
            (a : R ⊗[R] R ⊗[R] (P ⊗[R] P)) → R ⊗[R] P ⊗[R] (R ⊗[R] P))
          (1 ⊗ₜ[R] 1 ⊗ₜ[R] (comul : (a : P) → P ⊗[R] P) x)) :
      P ⊗[R] P)
    ((comul : (a : P) → P ⊗[R] P) x : P ⊗[R] P)

Tactic:
hopf_tensor_induction comul (R := R) x with x₁ x₂

Premises used: CoalgebraStruct.comul, DFunLike.coe
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
Goal:
R_1 : Type u_1
S_1 : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : AddCommMonoid A
inst_3 : AddCommMonoid B
inst_4 : Algebra R_1 S_1
inst_5 : Module R_1 A
inst_6 : Module S_1 A
inst_7 : Module R_1 B
inst_8 : IsScalarTower R_1 S_1 A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst_9 : CommSemiring R
inst_10 : CommSemiring S
inst_11 : Algebra R S
inst_12 : AddCommMonoid M
inst_13 : AddCommMonoid N
inst_14 : AddCommMonoid P
inst_15 : AddCommMonoid Q
inst_16 : Module R M
inst_17 : Module R N
inst_18 : Module R P
inst_19 : Module R Q
inst_20 : Module S M
inst_21 : IsScalarTower R S M
inst_22 : Coalgebra S M
inst_23 : Module S N
inst_24 : IsScalarTower R S N
inst_25 : Coalgebra S N
inst_26 : Coalgebra R P
inst_27 : Coalgebra R Q
x x₁ x₂ : P
⊢ Eq.{u_9 + 1} (α := P ⊗[R] P)
    ((_root_.TensorProduct.map (↑(_root_.TensorProduct.lid R P) : R ⊗[R] P →ₗ[R] P)
            (↑(_root_.TensorProduct.lid R P) : R ⊗[R] P →ₗ[R] P) :
          (a : R ⊗[R] P ⊗[R] (R ⊗[R] P)) → P ⊗[R] P)
        (((AlgebraTensorModule.tensorTensorTensorComm R R R R R R P P :
              TensorProduct.{u_5, u_5, u_9} R (R ⊗[R] R) (P ⊗[R] P) ≃ₗ[R] R ⊗[R] P ⊗[R] (R ⊗[R] P)) :
            (a : R ⊗[R] R ⊗[R] (P ⊗[R] P)) → R ⊗[R] P ⊗[R] (R ⊗[R] P))
          (1 ⊗ₜ[R] 1 ⊗ₜ[R] (x₁ ⊗ₜ[R] x₂))) :
      P ⊗[R] P)
    (x₁ ⊗ₜ[R] x₂ : P ⊗[R] P)

Tactic:
simp
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
Goal:
R : Type u_5
P : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid P
inst_2 : Module R P
inst_3 : Coalgebra R P
⊢ Eq (α := R ⊗[R] P ≃ₗ[R] P) (CoalgEquiv.toLinearEquiv (TensorProduct.lid R P)) (_root_.TensorProduct.lid R P)

Tactic:
rfl

Premises used: LinearEquiv.ofLinear, TensorProduct.lid, TensorProduct.lift, rfl
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
Goal:
R : Type u_5
P : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid P
inst_2 : Module R P
inst_3 : Coalgebra R P
r : R
a : P
⊢ (TensorProduct.lid R P : (a : R ⊗[R] P) → P) (r ⊗ₜ[R] a) = r • a

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
Goal:
R : Type u_5
P : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid P
inst_2 : Module R P
inst_3 : Coalgebra R P
a : P
⊢ Eq (α := R ⊗[R] P) ((CoalgEquiv.symm (TensorProduct.lid R P) : (a : P) → R ⊗[R] P) a : R ⊗[R] P)
    (1 ⊗ₜ[R] a : R ⊗[R] P)

Tactic:
rfl

Premises used: TensorProduct.tmul, AddCon.toQuotient, rfl