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
x : A
y : B
⊢ Eq (α := S ⊗[S] (A ⊗[R] B))
    (((((AlgebraTensorModule.curry (LinearMap.rTensor (A ⊗[R] B) counit ∘ₗ comul) : A →ₗ[S] B →ₗ[R] S ⊗[S] (A ⊗[R] B)) :
                (a : A) → B →ₗ[R] S ⊗[S] (A ⊗[R] B))
              x :
            B →ₗ[R] S ⊗[S] (A ⊗[R] B)) :
          (a : B) → S ⊗[S] (A ⊗[R] B))
        y :
      S ⊗[S] (A ⊗[R] B))
    (((((AlgebraTensorModule.curry ((mk S S (A ⊗[R] B) : (a : S) → A ⊗[R] B →ₗ[S] S ⊗[S] (A ⊗[R] B)) 1) :
                  A →ₗ[S] B →ₗ[R] S ⊗[S] (A ⊗[R] B)) :
                (a : A) → B →ₗ[R] S ⊗[S] (A ⊗[R] B))
              x :
            B →ₗ[R] S ⊗[S] (A ⊗[R] B)) :
          (a : B) → S ⊗[S] (A ⊗[R] B))
        y :
      S ⊗[S] (A ⊗[R] B))
have h : Eq (α := S ⊗[S] (A ⊗[R] B))
  (((((AlgebraTensorModule.curry (LinearMap.rTensor (A ⊗[R] B) counit ∘ₗ comul) : A →ₗ[S] B →ₗ[R] S ⊗[S] (A ⊗[R] B)) :
              (a : A) → B →ₗ[R] S ⊗[S] (A ⊗[R] B))
            x :
          B →ₗ[R] S ⊗[S] (A ⊗[R] B)) :
        (a : B) → S ⊗[S] (A ⊗[R] B))
      y :
    S ⊗[S] (A ⊗[R] B))
  ((LinearEquiv.symm (TensorProduct.lid S (A ⊗[R] B)) : (a : A ⊗[R] B) → S ⊗[S] (A ⊗[R] B))
      ((TensorProduct.lid S A : (a : S ⊗[S] A) → A)
          ((LinearMap.rTensor A counit : (a : A ⊗[S] A) → S ⊗[S] A) ((comul : (a : A) → A ⊗[S] A) x) : S ⊗[S] A) ⊗ₜ[R]
        (TensorProduct.lid R B : (a : R ⊗[R] B) → B)
          ((LinearMap.rTensor B counit : (a : B ⊗[R] B) → R ⊗[R] B) ((comul : (a : B) → B ⊗[R] B) y) : R ⊗[R] B)) :
    S ⊗[S] (A ⊗[R] B))
Tactic: convert!
      congr((TensorProduct.lid S _).symm
        (TensorProduct.lid _ _ $(rTensor_counit_comul (R := S) x) ⊗ₜ[R]
          TensorProduct.lid _ _ $(rTensor_counit_comul (R := R) y)))
-- 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
x : A
y : B
h :
  Eq (α := S ⊗[S] (A ⊗[R] B))
    (((((AlgebraTensorModule.curry (LinearMap.rTensor (A ⊗[R] B) counit ∘ₗ comul) : A →ₗ[S] B →ₗ[R] S ⊗[S] (A ⊗[R] B)) :
                (a : A) → B →ₗ[R] S ⊗[S] (A ⊗[R] B))
              x :
            B →ₗ[R] S ⊗[S] (A ⊗[R] B)) :
          (a : B) → S ⊗[S] (A ⊗[R] B))
        y :
      S ⊗[S] (A ⊗[R] B))
    ((LinearEquiv.symm (TensorProduct.lid S (A ⊗[R] B)) : (a : A ⊗[R] B) → S ⊗[S] (A ⊗[R] B))
        ((TensorProduct.lid S A : (a : S ⊗[S] A) → A)
            ((LinearMap.rTensor A counit : (a : A ⊗[S] A) → S ⊗[S] A) ((comul : (a : A) → A ⊗[S] A) x) : S ⊗[S] A) ⊗ₜ[R]
          (TensorProduct.lid R B : (a : R ⊗[R] B) → B)
            ((LinearMap.rTensor B counit : (a : B ⊗[R] B) → R ⊗[R] B) ((comul : (a : B) → B ⊗[R] B) y) : R ⊗[R] B)) :
      S ⊗[S] (A ⊗[R] B))
⊢ Eq (α := S ⊗[S] (A ⊗[R] B))
    (((((AlgebraTensorModule.curry (LinearMap.rTensor (A ⊗[R] B) counit ∘ₗ comul) : A →ₗ[S] B →ₗ[R] S ⊗[S] (A ⊗[R] B)) :
                (a : A) → B →ₗ[R] S ⊗[S] (A ⊗[R] B))
              x :
            B →ₗ[R] S ⊗[S] (A ⊗[R] B)) :
          (a : B) → S ⊗[S] (A ⊗[R] B))
        y :
      S ⊗[S] (A ⊗[R] B))
    (((((AlgebraTensorModule.curry ((mk S S (A ⊗[R] B) : (a : S) → A ⊗[R] B →ₗ[S] S ⊗[S] (A ⊗[R] B)) 1) :
                  A →ₗ[S] B →ₗ[R] S ⊗[S] (A ⊗[R] B)) :
                (a : A) → B →ₗ[R] S ⊗[S] (A ⊗[R] B))
              x :
            B →ₗ[R] S ⊗[S] (A ⊗[R] B)) :
          (a : B) → S ⊗[S] (A ⊗[R] B))
        y :
      S ⊗[S] (A ⊗[R] B))
have h₁ : Eq (α := S ⊗[S] (A ⊗[R] B))
  (((((AlgebraTensorModule.curry ((mk S S (A ⊗[R] B) : (a : S) → A ⊗[R] B →ₗ[S] S ⊗[S] (A ⊗[R] B)) 1) :
                A →ₗ[S] B →ₗ[R] S ⊗[S] (A ⊗[R] B)) :
              (a : A) → B →ₗ[R] S ⊗[S] (A ⊗[R] B))
            x :
          B →ₗ[R] S ⊗[S] (A ⊗[R] B)) :
        (a : B) → S ⊗[S] (A ⊗[R] B))
      y :
    S ⊗[S] (A ⊗[R] B))
  ((LinearEquiv.symm (TensorProduct.lid S (A ⊗[R] B)) : (a : A ⊗[R] B) → S ⊗[S] (A ⊗[R] B))
      ((TensorProduct.lid S A : (a : S ⊗[S] A) → A) (1 ⊗ₜ[S] x) ⊗ₜ[R]
        (TensorProduct.lid R B : (a : R ⊗[R] B) → B) (1 ⊗ₜ[R] y)) :
    S ⊗[S] (A ⊗[R] B))
Tactic: convert!
      congr((TensorProduct.lid S _).symm
        (TensorProduct.lid _ _ $(rTensor_counit_comul (R := S) x) ⊗ₜ[R]
          TensorProduct.lid _ _ $(rTensor_counit_comul (R := R) y)))
-- 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
x : A
y : B
⊢ Eq (α := S ⊗[S] (A ⊗[R] B))
    (((((AlgebraTensorModule.curry (LinearMap.rTensor (A ⊗[R] B) counit ∘ₗ comul) : A →ₗ[S] B →ₗ[R] S ⊗[S] (A ⊗[R] B)) :
                (a : A) → B →ₗ[R] S ⊗[S] (A ⊗[R] B))
              x :
            B →ₗ[R] S ⊗[S] (A ⊗[R] B)) :
          (a : B) → S ⊗[S] (A ⊗[R] B))
        y :
      S ⊗[S] (A ⊗[R] B))
    ((LinearEquiv.symm (TensorProduct.lid S (A ⊗[R] B)) : (a : A ⊗[R] B) → S ⊗[S] (A ⊗[R] B))
        ((TensorProduct.lid S A : (a : S ⊗[S] A) → A)
            ((LinearMap.rTensor A counit : (a : A ⊗[S] A) → S ⊗[S] A) ((comul : (a : A) → A ⊗[S] A) x) : S ⊗[S] A) ⊗ₜ[R]
          (TensorProduct.lid R B : (a : R ⊗[R] B) → B)
            ((LinearMap.rTensor B counit : (a : B ⊗[R] B) → R ⊗[R] B) ((comul : (a : B) → B ⊗[R] B) y) : R ⊗[R] B)) :
      S ⊗[S] (A ⊗[R] B))
have h : Eq (α := S ⊗[S] (A ⊗[R] B))
  ((LinearMap.rTensor (A ⊗[R] B) counit : (a : A ⊗[R] B ⊗[S] (A ⊗[R] B)) → S ⊗[S] (A ⊗[R] B))
      (((AlgebraTensorModule.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)) :
          (a : A ⊗[S] A ⊗[R] (B ⊗[R] B)) → A ⊗[R] B ⊗[S] (A ⊗[R] B))
        ((comul : (a : A) → A ⊗[S] A) x ⊗ₜ[R] (comul : (a : B) → B ⊗[R] B) y)) :
    S ⊗[S] (A ⊗[R] B))
  (1 ⊗ₜ[S]
      ((TensorProduct.lid S A : (a : S ⊗[S] A) → A)
          ((LinearMap.rTensor A counit : (a : A ⊗[S] A) → S ⊗[S] A) ((comul : (a : A) → A ⊗[S] A) x) : S ⊗[S] A) ⊗ₜ[R]
        (TensorProduct.lid R B : (a : R ⊗[R] B) → B)
          ((LinearMap.rTensor B counit : (a : B ⊗[R] B) → R ⊗[R] B) ((comul : (a : B) → B ⊗[R] B) y) : R ⊗[R] B)) :
    S ⊗[S] (A ⊗[R] B))
Tactic: dsimp
-- 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
x : A
y : B
⊢ Eq (α := S ⊗[S] (A ⊗[R] B))
    ((LinearMap.rTensor (A ⊗[R] B) counit : (a : A ⊗[R] B ⊗[S] (A ⊗[R] B)) → S ⊗[S] (A ⊗[R] B))
        (((AlgebraTensorModule.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)) :
            (a : A ⊗[S] A ⊗[R] (B ⊗[R] B)) → A ⊗[R] B ⊗[S] (A ⊗[R] B))
          ((comul : (a : A) → A ⊗[S] A) x ⊗ₜ[R] (comul : (a : B) → B ⊗[R] B) y)) :
      S ⊗[S] (A ⊗[R] B))
    (1 ⊗ₜ[S]
        ((TensorProduct.lid S A : (a : S ⊗[S] A) → A)
            ((LinearMap.rTensor A counit : (a : A ⊗[S] A) → S ⊗[S] A) ((comul : (a : A) → A ⊗[S] A) x) : S ⊗[S] A) ⊗ₜ[R]
          (TensorProduct.lid R B : (a : R ⊗[R] B) → B)
            ((LinearMap.rTensor B counit : (a : B ⊗[R] B) → R ⊗[R] B) ((comul : (a : B) → B ⊗[R] B) y) : R ⊗[R] B)) :
      S ⊗[S] (A ⊗[R] B))
have h : ∀ (x₁ x₂ : A),
  Eq (α := S ⊗[S] (A ⊗[R] B))
    ((LinearMap.rTensor (A ⊗[R] B) counit : (a : A ⊗[R] B ⊗[S] (A ⊗[R] B)) → S ⊗[S] (A ⊗[R] B))
        (((AlgebraTensorModule.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)) :
            (a : A ⊗[S] A ⊗[R] (B ⊗[R] B)) → A ⊗[R] B ⊗[S] (A ⊗[R] B))
          (x₁ ⊗ₜ[S] x₂ ⊗ₜ[R] (comul : (a : B) → B ⊗[R] B) y)) :
      S ⊗[S] (A ⊗[R] B))
    (1 ⊗ₜ[S]
        ((TensorProduct.lid S A : (a : S ⊗[S] A) → A)
            ((LinearMap.rTensor A counit : (a : A ⊗[S] A) → S ⊗[S] A) (x₁ ⊗ₜ[S] x₂) : S ⊗[S] A) ⊗ₜ[R]
          (TensorProduct.lid R B : (a : R ⊗[R] B) → B)
            ((LinearMap.rTensor B counit : (a : B ⊗[R] B) → R ⊗[R] B) ((comul : (a : B) → B ⊗[R] B) y) : R ⊗[R] B)) :
      S ⊗[S] (A ⊗[R] B))
Tactic: hopf_tensor_induction comul (R := S) x with x₁ x₂
-- 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
x : A
y : B
x₁ x₂ : A
⊢ Eq (α := S ⊗[S] (A ⊗[R] B))
    ((LinearMap.rTensor (A ⊗[R] B) counit : (a : A ⊗[R] B ⊗[S] (A ⊗[R] B)) → S ⊗[S] (A ⊗[R] B))
        (((AlgebraTensorModule.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)) :
            (a : A ⊗[S] A ⊗[R] (B ⊗[R] B)) → A ⊗[R] B ⊗[S] (A ⊗[R] B))
          (x₁ ⊗ₜ[S] x₂ ⊗ₜ[R] (comul : (a : B) → B ⊗[R] B) y)) :
      S ⊗[S] (A ⊗[R] B))
    (1 ⊗ₜ[S]
        ((TensorProduct.lid S A : (a : S ⊗[S] A) → A)
            ((LinearMap.rTensor A counit : (a : A ⊗[S] A) → S ⊗[S] A) (x₁ ⊗ₜ[S] x₂) : S ⊗[S] A) ⊗ₜ[R]
          (TensorProduct.lid R B : (a : R ⊗[R] B) → B)
            ((LinearMap.rTensor B counit : (a : B ⊗[R] B) → R ⊗[R] B) ((comul : (a : B) → B ⊗[R] B) y) : R ⊗[R] B)) :
      S ⊗[S] (A ⊗[R] B))
have h : ∀ (y₁ y₂ : B),
  Eq (α := S ⊗[S] (A ⊗[R] B))
    ((LinearMap.rTensor (A ⊗[R] B) counit : (a : A ⊗[R] B ⊗[S] (A ⊗[R] B)) → S ⊗[S] (A ⊗[R] B))
        (((AlgebraTensorModule.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)) :
            (a : A ⊗[S] A ⊗[R] (B ⊗[R] B)) → A ⊗[R] B ⊗[S] (A ⊗[R] B))
          (x₁ ⊗ₜ[S] x₂ ⊗ₜ[R] (y₁ ⊗ₜ[R] y₂))) :
      S ⊗[S] (A ⊗[R] B))
    (1 ⊗ₜ[S]
        ((TensorProduct.lid S A : (a : S ⊗[S] A) → A)
            ((LinearMap.rTensor A counit : (a : A ⊗[S] A) → S ⊗[S] A) (x₁ ⊗ₜ[S] x₂) : S ⊗[S] A) ⊗ₜ[R]
          (TensorProduct.lid R B : (a : R ⊗[R] B) → B)
            ((LinearMap.rTensor B counit : (a : B ⊗[R] B) → R ⊗[R] B) (y₁ ⊗ₜ[R] y₂) : R ⊗[R] B)) :
      S ⊗[S] (A ⊗[R] B))
Tactic: hopf_tensor_induction comul (R := R) y with y₁ y₂
-- 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
x : A
y : B
x₁ x₂ : A
y₁ y₂ : B
⊢ Eq (α := S ⊗[S] (A ⊗[R] B))
    ((LinearMap.rTensor (A ⊗[R] B) counit : (a : A ⊗[R] B ⊗[S] (A ⊗[R] B)) → S ⊗[S] (A ⊗[R] B))
        (((AlgebraTensorModule.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)) :
            (a : A ⊗[S] A ⊗[R] (B ⊗[R] B)) → A ⊗[R] B ⊗[S] (A ⊗[R] B))
          (x₁ ⊗ₜ[S] x₂ ⊗ₜ[R] (y₁ ⊗ₜ[R] y₂))) :
      S ⊗[S] (A ⊗[R] B))
    (1 ⊗ₜ[S]
        ((TensorProduct.lid S A : (a : S ⊗[S] A) → A)
            ((LinearMap.rTensor A counit : (a : A ⊗[S] A) → S ⊗[S] A) (x₁ ⊗ₜ[S] x₂) : S ⊗[S] A) ⊗ₜ[R]
          (TensorProduct.lid R B : (a : R ⊗[R] B) → B)
            ((LinearMap.rTensor B counit : (a : B ⊗[R] B) → R ⊗[R] B) (y₁ ⊗ₜ[R] y₂) : R ⊗[R] B)) :
      S ⊗[S] (A ⊗[R] B))
have h : Eq (α := A ⊗[R] B)
  ((TensorProduct.lid S (A ⊗[R] B) : (a : S ⊗[S] (A ⊗[R] B)) → A ⊗[R] B)
      ((LinearMap.rTensor (A ⊗[R] B) counit : (a : A ⊗[R] B ⊗[S] (A ⊗[R] B)) → S ⊗[S] (A ⊗[R] B))
        (((AlgebraTensorModule.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)) :
            (a : A ⊗[S] A ⊗[R] (B ⊗[R] B)) → A ⊗[R] B ⊗[S] (A ⊗[R] B))
          (x₁ ⊗ₜ[S] x₂ ⊗ₜ[R] (y₁ ⊗ₜ[R] y₂)))) :
    A ⊗[R] B)
  ((TensorProduct.lid S (A ⊗[R] B) : (a : S ⊗[S] (A ⊗[R] B)) → A ⊗[R] B)
      (1 ⊗ₜ[S]
        ((TensorProduct.lid S A : (a : S ⊗[S] A) → A)
            ((LinearMap.rTensor A counit : (a : A ⊗[S] A) → S ⊗[S] A) (x₁ ⊗ₜ[S] x₂) : S ⊗[S] A) ⊗ₜ[R]
          (TensorProduct.lid R B : (a : R ⊗[R] B) → B)
            ((LinearMap.rTensor B counit : (a : B ⊗[R] B) → R ⊗[R] B) (y₁ ⊗ₜ[R] y₂) : R ⊗[R] B))) :
    A ⊗[R] B)
Tactic: apply (TensorProduct.lid S _).injective
-- 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
x : A
y : B
x₁ x₂ : A
y₁ y₂ : B
⊢ Eq (α := A ⊗[R] B)
    ((TensorProduct.lid S (A ⊗[R] B) : (a : S ⊗[S] (A ⊗[R] B)) → A ⊗[R] B)
        ((LinearMap.rTensor (A ⊗[R] B) counit : (a : A ⊗[R] B ⊗[S] (A ⊗[R] B)) → S ⊗[S] (A ⊗[R] B))
          (((AlgebraTensorModule.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)) :
              (a : A ⊗[S] A ⊗[R] (B ⊗[R] B)) → A ⊗[R] B ⊗[S] (A ⊗[R] B))
            (x₁ ⊗ₜ[S] x₂ ⊗ₜ[R] (y₁ ⊗ₜ[R] y₂)))) :
      A ⊗[R] B)
    ((TensorProduct.lid S (A ⊗[R] B) : (a : S ⊗[S] (A ⊗[R] B)) → A ⊗[R] B)
        (1 ⊗ₜ[S]
          ((TensorProduct.lid S A : (a : S ⊗[S] A) → A)
              ((LinearMap.rTensor A counit : (a : A ⊗[S] A) → S ⊗[S] A) (x₁ ⊗ₜ[S] x₂) : S ⊗[S] A) ⊗ₜ[R]
            (TensorProduct.lid R B : (a : R ⊗[R] B) → B)
              ((LinearMap.rTensor B counit : (a : B ⊗[R] B) → R ⊗[R] B) (y₁ ⊗ₜ[R] y₂) : R ⊗[R] B))) :
      A ⊗[R] B)
have h : HSMul.hSMul (β := A ⊗[R] B)
    (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((counit : (a : B) → R) y₁ : R) ((counit : (a : A) → S) x₁ : S))
    (x₂ ⊗ₜ[R] y₂) =
  HSMul.hSMul (α := S) (β := A ⊗[R] B) 1
    (HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((counit : (a : A) → S) x₁ : S) x₂ ⊗ₜ[R]
      HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((counit : (a : B) → R) y₁ : R) y₂)
Tactic: dsimp
-- 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
x : A
y : B
x₁ x₂ : A
y₁ y₂ : B
⊢ HSMul.hSMul (β := A ⊗[R] B)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((counit : (a : B) → R) y₁ : R) ((counit : (a : A) → S) x₁ : S))
      (x₂ ⊗ₜ[R] y₂) =
    HSMul.hSMul (α := S) (β := A ⊗[R] B) 1
      (HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((counit : (a : A) → S) x₁ : S) x₂ ⊗ₜ[R]
        HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((counit : (a : B) → R) y₁ : R) y₂)
have h : HSMul.hSMul (β := A ⊗[R] B)
    (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((counit : (a : B) → R) y₁ : R) ((counit : (a : A) → S) x₁ : S))
    (x₂ ⊗ₜ[R] y₂) =
  HSMul.hSMul (α := S) 1
    (HSMul.hSMul (α := R) (β := A ⊗[R] B) ((counit : (a : B) → R) y₁ : R)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((counit : (a : A) → S) x₁ : S) x₂ ⊗ₜ[R] y₂))
Tactic: rw [tmul_smul, smul_assoc, one_smul, smul_tmul']
-- 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
x : A
y : B
x₁ x₂ : A
y₁ y₂ : B
h :
  HSMul.hSMul (β := A ⊗[R] B)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((counit : (a : B) → R) y₁ : R) ((counit : (a : A) → S) x₁ : S))
      (x₂ ⊗ₜ[R] y₂) =
    HSMul.hSMul (α := S) 1
      (HSMul.hSMul (α := R) (β := A ⊗[R] B) ((counit : (a : B) → R) y₁ : R)
        (HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((counit : (a : A) → S) x₁ : S) x₂ ⊗ₜ[R] y₂))
⊢ HSMul.hSMul (β := A ⊗[R] B)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((counit : (a : B) → R) y₁ : R) ((counit : (a : A) → S) x₁ : S))
      (x₂ ⊗ₜ[R] y₂) =
    HSMul.hSMul (α := S) (β := A ⊗[R] B) 1
      (HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((counit : (a : A) → S) x₁ : S) x₂ ⊗ₜ[R]
        HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((counit : (a : B) → R) y₁ : R) y₂)
have h₁ : HSMul.hSMul (α := R) ((counit : (a : B) → R) y₁ : R)
    (HSMul.hSMul (α := S) (β := A ⊗[R] B) ((counit : (a : A) → S) x₁ : S) (x₂ ⊗ₜ[R] y₂)) =
  HSMul.hSMul (α := S) 1
    (HSMul.hSMul (α := R) (β := A ⊗[R] B) ((counit : (a : B) → R) y₁ : R)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((counit : (a : A) → S) x₁ : S) x₂ ⊗ₜ[R] y₂))
Tactic: rw [tmul_smul, smul_assoc, one_smul, smul_tmul']
-- 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
x : A
y : B
x₁ x₂ : A
y₁ y₂ : B
h :
  HSMul.hSMul (β := A ⊗[R] B)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((counit : (a : B) → R) y₁ : R) ((counit : (a : A) → S) x₁ : S))
      (x₂ ⊗ₜ[R] y₂) =
    HSMul.hSMul (α := S) 1
      (HSMul.hSMul (α := R) (β := A ⊗[R] B) ((counit : (a : B) → R) y₁ : R)
        (HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((counit : (a : A) → S) x₁ : S) x₂ ⊗ₜ[R] y₂))
h₁ :
  HSMul.hSMul (α := R) ((counit : (a : B) → R) y₁ : R)
      (HSMul.hSMul (α := S) (β := A ⊗[R] B) ((counit : (a : A) → S) x₁ : S) (x₂ ⊗ₜ[R] y₂)) =
    HSMul.hSMul (α := S) 1
      (HSMul.hSMul (α := R) (β := A ⊗[R] B) ((counit : (a : B) → R) y₁ : R)
        (HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((counit : (a : A) → S) x₁ : S) x₂ ⊗ₜ[R] y₂))
⊢ HSMul.hSMul (β := A ⊗[R] B)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((counit : (a : B) → R) y₁ : R) ((counit : (a : A) → S) x₁ : S))
      (x₂ ⊗ₜ[R] y₂) =
    HSMul.hSMul (α := S) (β := A ⊗[R] B) 1
      (HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((counit : (a : A) → S) x₁ : S) x₂ ⊗ₜ[R]
        HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((counit : (a : B) → R) y₁ : R) y₂)
have h₂ : HSMul.hSMul (α := R) ((counit : (a : B) → R) y₁ : R)
    (HSMul.hSMul (α := S) (β := A ⊗[R] B) ((counit : (a : A) → S) x₁ : S) (x₂ ⊗ₜ[R] y₂)) =
  HSMul.hSMul (α := R) (β := A ⊗[R] B) ((counit : (a : B) → R) y₁ : R)
    (HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((counit : (a : A) → S) x₁ : S) x₂ ⊗ₜ[R] y₂)
Tactic: rw [tmul_smul, smul_assoc, one_smul, smul_tmul']
-- 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
x : A
y : B
x₁ x₂ : A
y₁ y₂ : B
h :
  HSMul.hSMul (β := A ⊗[R] B)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((counit : (a : B) → R) y₁ : R) ((counit : (a : A) → S) x₁ : S))
      (x₂ ⊗ₜ[R] y₂) =
    HSMul.hSMul (α := S) 1
      (HSMul.hSMul (α := R) (β := A ⊗[R] B) ((counit : (a : B) → R) y₁ : R)
        (HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((counit : (a : A) → S) x₁ : S) x₂ ⊗ₜ[R] y₂))
h₁ :
  HSMul.hSMul (α := R) ((counit : (a : B) → R) y₁ : R)
      (HSMul.hSMul (α := S) (β := A ⊗[R] B) ((counit : (a : A) → S) x₁ : S) (x₂ ⊗ₜ[R] y₂)) =
    HSMul.hSMul (α := S) 1
      (HSMul.hSMul (α := R) (β := A ⊗[R] B) ((counit : (a : B) → R) y₁ : R)
        (HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((counit : (a : A) → S) x₁ : S) x₂ ⊗ₜ[R] y₂))
h₂ :
  HSMul.hSMul (α := R) ((counit : (a : B) → R) y₁ : R)
      (HSMul.hSMul (α := S) (β := A ⊗[R] B) ((counit : (a : A) → S) x₁ : S) (x₂ ⊗ₜ[R] y₂)) =
    HSMul.hSMul (α := R) (β := A ⊗[R] B) ((counit : (a : B) → R) y₁ : R)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((counit : (a : A) → S) x₁ : S) x₂ ⊗ₜ[R] y₂)
⊢ HSMul.hSMul (β := A ⊗[R] B)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((counit : (a : B) → R) y₁ : R) ((counit : (a : A) → S) x₁ : S))
      (x₂ ⊗ₜ[R] y₂) =
    HSMul.hSMul (α := S) (β := A ⊗[R] B) 1
      (HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((counit : (a : A) → S) x₁ : S) x₂ ⊗ₜ[R]
        HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((counit : (a : B) → R) y₁ : R) y₂)
have h₃ : HSMul.hSMul (α := R) (β := A ⊗[R] B) ((counit : (a : B) → R) y₁ : R)
    (HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((counit : (a : A) → S) x₁ : S) x₂ ⊗ₜ[R] y₂) =
  HSMul.hSMul (α := R) (β := A ⊗[R] B) ((counit : (a : B) → R) y₁ : R)
    (HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((counit : (a : A) → S) x₁ : S) x₂ ⊗ₜ[R] y₂)
Tactic: rw [tmul_smul, smul_assoc, one_smul, smul_tmul']
-- 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
x : A
y : B
⊢ Eq (α := S ⊗[S] (A ⊗[R] B))
    (((((AlgebraTensorModule.curry ((mk S S (A ⊗[R] B) : (a : S) → A ⊗[R] B →ₗ[S] S ⊗[S] (A ⊗[R] B)) 1) :
                  A →ₗ[S] B →ₗ[R] S ⊗[S] (A ⊗[R] B)) :
                (a : A) → B →ₗ[R] S ⊗[S] (A ⊗[R] B))
              x :
            B →ₗ[R] S ⊗[S] (A ⊗[R] B)) :
          (a : B) → S ⊗[S] (A ⊗[R] B))
        y :
      S ⊗[S] (A ⊗[R] B))
    ((LinearEquiv.symm (TensorProduct.lid S (A ⊗[R] B)) : (a : A ⊗[R] B) → S ⊗[S] (A ⊗[R] B))
        ((TensorProduct.lid S A : (a : S ⊗[S] A) → A) (1 ⊗ₜ[S] x) ⊗ₜ[R]
          (TensorProduct.lid R B : (a : R ⊗[R] B) → B) (1 ⊗ₜ[R] y)) :
      S ⊗[S] (A ⊗[R] B))
have h : Eq (α := S ⊗[S] (A ⊗[R] B)) (1 ⊗ₜ[S] (x ⊗ₜ[R] y))
  (1 ⊗ₜ[S] (HSMul.hSMul.{u_2, u_3, u_3} (α := S) 1 x ⊗ₜ[R] HSMul.hSMul.{u_1, u_4, u_4} (α := R) 1 y))
Tactic: dsimp
-- 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
⊢ Eq (α := A ⊗[R] B →ₗ[S] A ⊗[R] B ⊗[S] S) (LinearMap.lTensor (A ⊗[R] B) counit ∘ₗ comul)
    ((LinearMap.flip (mk S (A ⊗[R] B) S) : (a : S) → A ⊗[R] B →ₗ[S] A ⊗[R] B ⊗[S] S) 1)
have a : ∀ (x : A) (y : B),
  Eq (α := A ⊗[R] B ⊗[S] S)
    (((((AlgebraTensorModule.curry (LinearMap.lTensor (A ⊗[R] B) counit ∘ₗ comul) : A →ₗ[S] B →ₗ[R] A ⊗[R] B ⊗[S] S) :
                (a : A) → B →ₗ[R] A ⊗[R] B ⊗[S] S)
              x :
            B →ₗ[R] A ⊗[R] B ⊗[S] S) :
          (a : B) → A ⊗[R] B ⊗[S] S)
        y :
      A ⊗[R] B ⊗[S] S)
    (((((AlgebraTensorModule.curry ((LinearMap.flip (mk S (A ⊗[R] B) S) : (a : S) → A ⊗[R] B →ₗ[S] A ⊗[R] B ⊗[S] S) 1) :
                  A →ₗ[S] B →ₗ[R] A ⊗[R] B ⊗[S] S) :
                (a : A) → B →ₗ[R] A ⊗[R] B ⊗[S] S)
              x :
            B →ₗ[R] A ⊗[R] B ⊗[S] S) :
          (a : B) → A ⊗[R] B ⊗[S] S)
        y :
      A ⊗[R] B ⊗[S] S)
Tactic: ext x y