awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.TensorProduct (goal)
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 : AddCommMonoid A
inst_3 : AddCommMonoid B
inst_4 : Algebra R S
inst_5 : Module R A
inst_6 : Module S A
inst_7 : Module R B
inst_8 : IsScalarTower R S A
inst_9 : Coalgebra R B
inst_10 : Coalgebra S A
inst_11 : IsCocomm S A
inst_12 : IsCocomm R B
⊢ Eq (α := A ⊗[R] B →ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B))
    ((↑(TensorProduct.comm S (A ⊗[R] B) (A ⊗[R] B)) : A ⊗[R] B ⊗[S] (A ⊗[R] B) →ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B)) ∘ₗ comul)
    comul
have a : ∀ (x : A) (y : B),
  Eq (α := A ⊗[R] B ⊗[S] (A ⊗[R] B))
    (((((AlgebraTensorModule.curry
                    ((↑(TensorProduct.comm S (A ⊗[R] B) (A ⊗[R] B)) :
                        A ⊗[R] B ⊗[S] (A ⊗[R] B) →ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B)) ∘ₗ
                      comul) :
                  A →ₗ[S] B →ₗ[R] A ⊗[R] B ⊗[S] (A ⊗[R] B)) :
                (a : A) → B →ₗ[R] A ⊗[R] B ⊗[S] (A ⊗[R] B))
              x :
            B →ₗ[R] A ⊗[R] B ⊗[S] (A ⊗[R] B)) :
          (a : B) → A ⊗[R] B ⊗[S] (A ⊗[R] B))
        y :
      A ⊗[R] B ⊗[S] (A ⊗[R] B))
    (((((AlgebraTensorModule.curry comul : A →ₗ[S] B →ₗ[R] A ⊗[R] B ⊗[S] (A ⊗[R] B)) :
                (a : A) → B →ₗ[R] A ⊗[R] B ⊗[S] (A ⊗[R] B))
              x :
            B →ₗ[R] A ⊗[R] B ⊗[S] (A ⊗[R] B)) :
          (a : B) → A ⊗[R] B ⊗[S] (A ⊗[R] B))
        y :
      A ⊗[R] B ⊗[S] (A ⊗[R] B))
Tactic: ext x y
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.TensorProduct (goal)
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
f : M →ₗc[S] N
g : P →ₗc[R] Q
⊢ Eq (α := M ⊗[R] P →ₗ[S] S)
    ((counit : N ⊗[R] Q →ₗ[S] S) ∘ₗ (AlgebraTensorModule.map f.toLinearMap g.toLinearMap : M ⊗[R] P →ₗ[S] N ⊗[R] Q) :
      M ⊗[R] P →ₗ[S] S)
    (counit : M ⊗[R] P →ₗ[S] S)
have a : ∀ (x : M) (x_1 : P),
  Eq.{u_6 + 1} (α := S)
    (((((AlgebraTensorModule.curry
                    ((counit : N ⊗[R] Q →ₗ[S] S) ∘ₗ
                      (AlgebraTensorModule.map f.toLinearMap g.toLinearMap : M ⊗[R] P →ₗ[S] N ⊗[R] Q)) :
                  M →ₗ[S] P →ₗ[R] S) :
                (a : M) → P →ₗ[R] S)
              x :
            P →ₗ[R] S) :
          (a : P) → S)
        x_1 :
      S)
    (((((AlgebraTensorModule.curry counit : M →ₗ[S] P →ₗ[R] S) : (a : M) → P →ₗ[R] S) x : P →ₗ[R] S) : (a : P) → S)
        x_1 :
      S)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.TensorProduct (goal)
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
f : M →ₗc[S] N
g : P →ₗc[R] Q
⊢ Eq (α := M ⊗[R] P →ₗ[S] N ⊗[R] Q ⊗[S] (N ⊗[R] Q))
    ((_root_.TensorProduct.map (AlgebraTensorModule.map f.toLinearMap g.toLinearMap)
            (AlgebraTensorModule.map f.toLinearMap g.toLinearMap) :
          M ⊗[R] P ⊗[S] (M ⊗[R] P) →ₗ[S] N ⊗[R] Q ⊗[S] (N ⊗[R] Q)) ∘ₗ
        (comul : M ⊗[R] P →ₗ[S] M ⊗[R] P ⊗[S] (M ⊗[R] P)) :
      M ⊗[R] P →ₗ[S] N ⊗[R] Q ⊗[S] (N ⊗[R] Q))
    (comul ∘ₗ AlgebraTensorModule.map f.toLinearMap g.toLinearMap : M ⊗[R] P →ₗ[S] N ⊗[R] Q ⊗[S] (N ⊗[R] Q))
have a : ∀ (x : M) (y : P),
  Eq (α := N ⊗[R] Q ⊗[S] (N ⊗[R] Q))
    (((((AlgebraTensorModule.curry
                    ((_root_.TensorProduct.map (AlgebraTensorModule.map f.toLinearMap g.toLinearMap)
                          (AlgebraTensorModule.map f.toLinearMap g.toLinearMap) :
                        M ⊗[R] P ⊗[S] (M ⊗[R] P) →ₗ[S] N ⊗[R] Q ⊗[S] (N ⊗[R] Q)) ∘ₗ
                      (comul : M ⊗[R] P →ₗ[S] M ⊗[R] P ⊗[S] (M ⊗[R] P))) :
                  M →ₗ[S] P →ₗ[R] N ⊗[R] Q ⊗[S] (N ⊗[R] Q)) :
                (a : M) → P →ₗ[R] N ⊗[R] Q ⊗[S] (N ⊗[R] Q))
              x :
            P →ₗ[R] N ⊗[R] Q ⊗[S] (N ⊗[R] Q)) :
          (a : P) → N ⊗[R] Q ⊗[S] (N ⊗[R] Q))
        y :
      N ⊗[R] Q ⊗[S] (N ⊗[R] Q))
    (((((AlgebraTensorModule.curry (comul ∘ₗ AlgebraTensorModule.map f.toLinearMap g.toLinearMap) :
                  M →ₗ[S] P →ₗ[R] N ⊗[R] Q ⊗[S] (N ⊗[R] Q)) :
                (a : M) → P →ₗ[R] N ⊗[R] Q ⊗[S] (N ⊗[R] Q))
              x :
            P →ₗ[R] N ⊗[R] Q ⊗[S] (N ⊗[R] Q)) :
          (a : P) → N ⊗[R] Q ⊗[S] (N ⊗[R] Q))
        y :
      N ⊗[R] Q ⊗[S] (N ⊗[R] Q))
Tactic: ext x y
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.TensorProduct (goal)
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
⊢ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.TensorProduct (goal)
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
⊢ Eq (α := R ⊗[R] P →ₗ[R] R) (counit ∘ₗ (↑(_root_.TensorProduct.lid R P) : R ⊗[R] P →ₗ[R] P)) counit
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.TensorProduct (goal)
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
⊢ 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))
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.TensorProduct (goal)
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 (α := 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)
have 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)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.TensorProduct (goal)
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_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)
have 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)
Tactic: simp only [one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.TensorProduct (goal)
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_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)
have 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)
Tactic: hopf_tensor_induction comul (R := R) x with x₁ x₂
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.TensorProduct (goal)
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
⊢ Eq (α := M ⊗[R] R →ₗ[S] S) (counit ∘ₗ (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M) : M ⊗[R] R →ₗ[S] S)
    (counit : M ⊗[R] R →ₗ[S] S)
have a : ∀ (x : M),
  Eq.{u_6 + 1} (α := S)
    (((((AlgebraTensorModule.curry (counit ∘ₗ (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M)) :
                  M →ₗ[S] R →ₗ[R] S) :
                (a : M) → R →ₗ[R] S)
              x :
            R →ₗ[R] S) :
          (a : R) → S)
        1 :
      S)
    (((((AlgebraTensorModule.curry counit : M →ₗ[S] R →ₗ[R] S) : (a : M) → R →ₗ[R] S) x : R →ₗ[R] S) : (a : R) → S) 1 :
      S)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.TensorProduct (goal)
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
⊢ Eq (α := M ⊗[R] R →ₗ[S] M ⊗[S] M)
    ((_root_.TensorProduct.map (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M)
            (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M) :
          M ⊗[R] R ⊗[S] (M ⊗[R] R) →ₗ[S] M ⊗[S] M) ∘ₗ
        (comul : M ⊗[R] R →ₗ[S] M ⊗[R] R ⊗[S] (M ⊗[R] R)) :
      M ⊗[R] R →ₗ[S] M ⊗[S] M)
    (comul ∘ₗ (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M) : M ⊗[R] R →ₗ[S] M ⊗[S] M)
have a : ∀ (x : M),
  Eq.{u_7 + 1} (α := M ⊗[S] M)
    (((((AlgebraTensorModule.curry
                  ((_root_.TensorProduct.map (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M)
                        (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M) :
                      M ⊗[R] R ⊗[S] (M ⊗[R] R) →ₗ[S] M ⊗[S] M) ∘ₗ
                    (comul : M ⊗[R] R →ₗ[S] M ⊗[R] R ⊗[S] (M ⊗[R] R))) :
                M →ₗ[S] LinearMap.{u_5, u_5, u_5, u_7} (RingHom.id R) R (M ⊗[S] M)) :
              (a : M) → R →ₗ[R] M ⊗[S] M)
            x :
          LinearMap.{u_5, u_5, u_5, u_7} (RingHom.id R) R (M ⊗[S] M)) :
        (a : R) → M ⊗[S] M)
      1)
    (((((AlgebraTensorModule.curry (comul ∘ₗ (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M)) :
                M →ₗ[S] LinearMap.{u_5, u_5, u_5, u_7} (RingHom.id R) R (M ⊗[S] M)) :
              (a : M) → R →ₗ[R] M ⊗[S] M)
            x :
          LinearMap.{u_5, u_5, u_5, u_7} (RingHom.id R) R (M ⊗[S] M)) :
        (a : R) → M ⊗[S] M)
      1)
Tactic: ext x