awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Coalgebra.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 : 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 (α := A ⊗[R] B ⊗[S] S)
    ((LinearMap.lTensor (A ⊗[R] B) counit : (a : A ⊗[R] B ⊗[S] (A ⊗[R] B)) → A ⊗[R] B ⊗[S] S)
        (((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)) :
      A ⊗[R] B ⊗[S] S)
    ((TensorProduct.rid S A : (a : A ⊗[S] S) → A)
            ((LinearMap.lTensor A counit : (a : A ⊗[S] A) → A ⊗[S] S) ((comul : (a : A) → A ⊗[S] A) x) : A ⊗[S] S) ⊗ₜ[R]
          (TensorProduct.rid R B : (a : B ⊗[R] R) → B)
            ((LinearMap.lTensor B counit : (a : B ⊗[R] B) → B ⊗[R] R) ((comul : (a : B) → B ⊗[R] B) y) : B ⊗[R] R) ⊗ₜ[S]
        1 :
      A ⊗[R] B ⊗[S] S)
⊢ 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)
    ((LinearEquiv.symm (TensorProduct.rid S (A ⊗[R] B)) : (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] S)
        ((TensorProduct.rid S A : (a : A ⊗[S] S) → A)
            ((LinearMap.lTensor A counit : (a : A ⊗[S] A) → A ⊗[S] S) ((comul : (a : A) → A ⊗[S] A) x) : A ⊗[S] S) ⊗ₜ[R]
          (TensorProduct.rid R B : (a : B ⊗[R] R) → B)
            ((LinearMap.lTensor B counit : (a : B ⊗[R] B) → B ⊗[R] R) ((comul : (a : B) → B ⊗[R] B) y) : B ⊗[R] R)) :
      A ⊗[R] B ⊗[S] S)

Tactic:
dsimp
-- Module: Mathlib.RingTheory.Coalgebra.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 : 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 :
  ∀ (x₁ x₂ : A),
    Eq (α := A ⊗[R] B ⊗[S] S)
      ((LinearMap.lTensor (A ⊗[R] B) counit : (a : A ⊗[R] B ⊗[S] (A ⊗[R] B)) → A ⊗[R] B ⊗[S] S)
          (((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)) :
        A ⊗[R] B ⊗[S] S)
      ((TensorProduct.rid S A : (a : A ⊗[S] S) → A)
              ((LinearMap.lTensor A counit : (a : A ⊗[S] A) → A ⊗[S] S) (x₁ ⊗ₜ[S] x₂) : A ⊗[S] S) ⊗ₜ[R]
            (TensorProduct.rid R B : (a : B ⊗[R] R) → B)
              ((LinearMap.lTensor B counit : (a : B ⊗[R] B) → B ⊗[R] R) ((comul : (a : B) → B ⊗[R] B) y) :
                B ⊗[R] R) ⊗ₜ[S]
          1 :
        A ⊗[R] B ⊗[S] S)
⊢ Eq (α := A ⊗[R] B ⊗[S] S)
    ((LinearMap.lTensor (A ⊗[R] B) counit : (a : A ⊗[R] B ⊗[S] (A ⊗[R] B)) → A ⊗[R] B ⊗[S] S)
        (((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)) :
      A ⊗[R] B ⊗[S] S)
    ((TensorProduct.rid S A : (a : A ⊗[S] S) → A)
            ((LinearMap.lTensor A counit : (a : A ⊗[S] A) → A ⊗[S] S) ((comul : (a : A) → A ⊗[S] A) x) : A ⊗[S] S) ⊗ₜ[R]
          (TensorProduct.rid R B : (a : B ⊗[R] R) → B)
            ((LinearMap.lTensor B counit : (a : B ⊗[R] B) → B ⊗[R] R) ((comul : (a : B) → B ⊗[R] B) y) : B ⊗[R] R) ⊗ₜ[S]
        1 :
      A ⊗[R] B ⊗[S] S)

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

Premises used: CoalgebraStruct.comul, DFunLike.coe
-- Module: Mathlib.RingTheory.Coalgebra.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 : 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
h :
  ∀ (y₁ y₂ : B),
    Eq (α := A ⊗[R] B ⊗[S] S)
      ((LinearMap.lTensor (A ⊗[R] B) counit : (a : A ⊗[R] B ⊗[S] (A ⊗[R] B)) → A ⊗[R] B ⊗[S] S)
          (((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 ⊗[S] S)
      ((TensorProduct.rid S A : (a : A ⊗[S] S) → A)
              ((LinearMap.lTensor A counit : (a : A ⊗[S] A) → A ⊗[S] S) (x₁ ⊗ₜ[S] x₂) : A ⊗[S] S) ⊗ₜ[R]
            (TensorProduct.rid R B : (a : B ⊗[R] R) → B)
              ((LinearMap.lTensor B counit : (a : B ⊗[R] B) → B ⊗[R] R) (y₁ ⊗ₜ[R] y₂) : B ⊗[R] R) ⊗ₜ[S]
          1 :
        A ⊗[R] B ⊗[S] S)
⊢ Eq (α := A ⊗[R] B ⊗[S] S)
    ((LinearMap.lTensor (A ⊗[R] B) counit : (a : A ⊗[R] B ⊗[S] (A ⊗[R] B)) → A ⊗[R] B ⊗[S] S)
        (((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)) :
      A ⊗[R] B ⊗[S] S)
    ((TensorProduct.rid S A : (a : A ⊗[S] S) → A)
            ((LinearMap.lTensor A counit : (a : A ⊗[S] A) → A ⊗[S] S) (x₁ ⊗ₜ[S] x₂) : A ⊗[S] S) ⊗ₜ[R]
          (TensorProduct.rid R B : (a : B ⊗[R] R) → B)
            ((LinearMap.lTensor B counit : (a : B ⊗[R] B) → B ⊗[R] R) ((comul : (a : B) → B ⊗[R] B) y) : B ⊗[R] R) ⊗ₜ[S]
        1 :
      A ⊗[R] B ⊗[S] S)

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

Premises used: CoalgebraStruct.comul, DFunLike.coe
-- Module: Mathlib.RingTheory.Coalgebra.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 : 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 :
  Eq (α := A ⊗[R] B)
    ((TensorProduct.rid S (A ⊗[R] B) : (a : A ⊗[R] B ⊗[S] S) → A ⊗[R] B)
        ((LinearMap.lTensor (A ⊗[R] B) counit : (a : A ⊗[R] B ⊗[S] (A ⊗[R] B)) → A ⊗[R] B ⊗[S] S)
          (((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.rid S (A ⊗[R] B) : (a : A ⊗[R] B ⊗[S] S) → A ⊗[R] B)
        ((TensorProduct.rid S A : (a : A ⊗[S] S) → A)
              ((LinearMap.lTensor A counit : (a : A ⊗[S] A) → A ⊗[S] S) (x₁ ⊗ₜ[S] x₂) : A ⊗[S] S) ⊗ₜ[R]
            (TensorProduct.rid R B : (a : B ⊗[R] R) → B)
              ((LinearMap.lTensor B counit : (a : B ⊗[R] B) → B ⊗[R] R) (y₁ ⊗ₜ[R] y₂) : B ⊗[R] R) ⊗ₜ[S]
          1) :
      A ⊗[R] B)
⊢ Eq (α := A ⊗[R] B ⊗[S] S)
    ((LinearMap.lTensor (A ⊗[R] B) counit : (a : A ⊗[R] B ⊗[S] (A ⊗[R] B)) → A ⊗[R] B ⊗[S] S)
        (((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 ⊗[S] S)
    ((TensorProduct.rid S A : (a : A ⊗[S] S) → A)
            ((LinearMap.lTensor A counit : (a : A ⊗[S] A) → A ⊗[S] S) (x₁ ⊗ₜ[S] x₂) : A ⊗[S] S) ⊗ₜ[R]
          (TensorProduct.rid R B : (a : B ⊗[R] R) → B)
            ((LinearMap.lTensor B counit : (a : B ⊗[R] B) → B ⊗[R] R) (y₁ ⊗ₜ[R] y₂) : B ⊗[R] R) ⊗ₜ[S]
        1 :
      A ⊗[R] B ⊗[S] S)

Tactic:
apply (TensorProduct.rid S _).injective

Premises used: TensorProduct.rid, LinearEquiv.injective
-- Module: Mathlib.RingTheory.Coalgebra.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 : 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) (β := 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₁)
⊢ Eq (α := A ⊗[R] B)
    ((TensorProduct.rid S (A ⊗[R] B) : (a : A ⊗[R] B ⊗[S] S) → A ⊗[R] B)
        ((LinearMap.lTensor (A ⊗[R] B) counit : (a : A ⊗[R] B ⊗[S] (A ⊗[R] B)) → A ⊗[R] B ⊗[S] S)
          (((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.rid S (A ⊗[R] B) : (a : A ⊗[R] B ⊗[S] S) → A ⊗[R] B)
        ((TensorProduct.rid S A : (a : A ⊗[S] S) → A)
              ((LinearMap.lTensor A counit : (a : A ⊗[S] A) → A ⊗[S] S) (x₁ ⊗ₜ[S] x₂) : A ⊗[S] S) ⊗ₜ[R]
            (TensorProduct.rid R B : (a : B ⊗[R] R) → B)
              ((LinearMap.lTensor B counit : (a : B ⊗[R] B) → B ⊗[R] R) (y₁ ⊗ₜ[R] y₂) : B ⊗[R] R) ⊗ₜ[S]
          1) :
      A ⊗[R] B)

Tactic:
dsimp
-- Module: Mathlib.RingTheory.Coalgebra.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 : 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₁)
h₃ 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₁)
⊢ 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:
rw [tmul_smul, smul_assoc, one_smul, smul_tmul']

Premises used: smul_assoc, TensorProduct.tmul_smul, one_smul, TensorProduct.smul_tmul'
-- Module: Mathlib.RingTheory.Coalgebra.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 : 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 (α := A ⊗[R] B ⊗[S] S) (x ⊗ₜ[R] y ⊗ₜ[S] 1)
    (HSMul.hSMul.{u_2, u_3, u_3} (α := S) 1 x ⊗ₜ[R] HSMul.hSMul.{u_1, u_4, u_4} (α := R) 1 y ⊗ₜ[S] 1)
⊢ Eq (α := 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)
    ((LinearEquiv.symm (TensorProduct.rid S (A ⊗[R] B)) : (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] S)
        ((TensorProduct.rid S A : (a : A ⊗[S] S) → A) (x ⊗ₜ[S] 1) ⊗ₜ[R]
          (TensorProduct.rid R B : (a : B ⊗[R] R) → B) (y ⊗ₜ[R] 1)) :
      A ⊗[R] B ⊗[S] S)

Tactic:
dsimp
-- Module: Mathlib.RingTheory.Coalgebra.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 : 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 (α := A ⊗[R] B ⊗[S] S) (x ⊗ₜ[R] y ⊗ₜ[S] 1)
    (HSMul.hSMul.{u_2, u_3, u_3} (α := S) 1 x ⊗ₜ[R] HSMul.hSMul.{u_1, u_4, u_4} (α := R) 1 y ⊗ₜ[S] 1)

Tactic:
simp only [one_smul]

Premises used: one_smul
-- Module: Mathlib.RingTheory.Coalgebra.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 : 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
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))
⊢ 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

Tactic:
ext x y
-- 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
f : M →ₗc[S] N
g : P →ₗc[R] Q
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)
⊢ 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)

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
f : M →ₗc[S] N
g : P →ₗc[R] Q
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:
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
f : M →ₗc[S] N
g : P →ₗc[R] Q
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))
⊢ 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))

Tactic:
ext x y
-- 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
Q : Type u_10
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 : AddCommMonoid Q
inst_7 : Module R M
inst_8 : Module R N
inst_9 : Module R P
inst_10 : Module R Q
inst_11 : Module S M
inst_12 : IsScalarTower R S M
inst_13 : Coalgebra S M
inst_14 : Module S N
inst_15 : IsScalarTower R S N
inst_16 : Coalgebra S N
inst_17 : Coalgebra R P
inst_18 : Coalgebra R Q
f : M →ₗc[S] N
g : P →ₗc[R] Q
x : M
y : P
⊢ Eq (α := N ⊗[R] Q) ((map f g : (a : M ⊗[R] P) → N ⊗[R] Q) (x ⊗ₜ[R] y) : N ⊗[R] Q)
    ((f : (a : M) → N) x ⊗ₜ[R] (g : (a : P) → Q) y : N ⊗[R] Q)

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
Q : Type u_10
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 : AddCommMonoid Q
inst_7 : Module R M
inst_8 : Module R N
inst_9 : Module R P
inst_10 : Module R Q
inst_11 : Module S M
inst_12 : IsScalarTower R S M
inst_13 : Coalgebra S M
inst_14 : Module S N
inst_15 : IsScalarTower R S N
inst_16 : Coalgebra S N
inst_17 : Coalgebra R P
inst_18 : Coalgebra R Q
f : M →ₗc[S] N
g : P →ₗc[R] Q
⊢ Eq (α := M ⊗[R] P →ₗ[S] N ⊗[R] Q)
    ((↑(map f g) :
        [inst_19 : FunLike (M ⊗[R] P →ₗc[S] N ⊗[R] Q) (M ⊗[R] P) (N ⊗[R] Q)] →
          [SemilinearMapClass (M ⊗[R] P →ₗc[S] N ⊗[R] Q) (RingHom.id S) (M ⊗[R] P) (N ⊗[R] Q)] →
            M ⊗[R] P →ₗ[S] N ⊗[R] Q) :
      M ⊗[R] P →ₗ[S] N ⊗[R] Q)
    (AlgebraTensorModule.map
        (↑f : [inst : FunLike (M →ₗc[S] N) M N] → [SemilinearMapClass (M →ₗc[S] N) (RingHom.id S) M N] → M →ₗ[S] N)
        (↑g : [inst_19 : FunLike (P →ₗc[R] Q) P Q] → [SemilinearMapClass (P →ₗc[R] Q) (RingHom.id R) P Q] → P →ₗ[R] Q) :
      M ⊗[R] P →ₗ[S] N ⊗[R] Q)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, SemilinearMapClass.semilinearMap, TensorProduct, TensorProduct.AlgebraTensorModule.map, rfl, TensorProduct.AlgebraTensorModule.lift