awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
Q : Type uQ
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : Module A M
inst_8 : Module B M
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
inst_12 : AddCommMonoid N
inst_13 : Module R N
inst_14 : AddCommMonoid Q
inst_15 : Module R Q
inst_16 : Algebra A B
inst_17 : IsScalarTower A B M
f : N →ₗ[R] Q
a :
  ∀ (x : M) (x_1 : N),
    Eq (α := M ⊗[R] Q)
      ((((curry
                    (((curry
                            ((((lTensor B M : (N →ₗ[R] Q) →ₗ[R] M ⊗[R] N →ₗ[B] M ⊗[R] Q) :
                                    (a : N →ₗ[R] Q) → M ⊗[R] N →ₗ[B] M ⊗[R] Q)
                                  f :
                                M ⊗[R] N →ₗ[B] M ⊗[R] Q) ∘ₗ
                              ((↑(cancelBaseChange R A B M N) : M ⊗[A] (A ⊗[R] N) →ₗ[B] M ⊗[R] N) :
                                M ⊗[A] (A ⊗[R] N) →ₗ[B] M ⊗[R] N)) :
                          M →ₗ[B] A ⊗[R] N →ₗ[A] M ⊗[R] Q) :
                        (a : M) → A ⊗[R] N →ₗ[A] M ⊗[R] Q)
                      x) :
                  A →ₗ[A] N →ₗ[R] M ⊗[R] Q) :
                (a : A) → N →ₗ[R] M ⊗[R] Q)
              1 :
            (a : N) → M ⊗[R] Q)
          x_1 :
        M ⊗[R] Q)
      ((((curry
                    (((curry
                            ((↑(cancelBaseChange R A B M Q) : M ⊗[A] (A ⊗[R] Q) →ₗ[B] M ⊗[R] Q) ∘ₗ
                              ((lTensor B M :
                                    (A ⊗[R] N →ₗ[A] A ⊗[R] Q) →ₗ[A] M ⊗[A] (A ⊗[R] N) →ₗ[B] M ⊗[A] (A ⊗[R] Q)) :
                                  (a : A ⊗[R] N →ₗ[A] A ⊗[R] Q) → M ⊗[A] (A ⊗[R] N) →ₗ[B] M ⊗[A] (A ⊗[R] Q))
                                (((lTensor A A : (N →ₗ[R] Q) →ₗ[R] A ⊗[R] N →ₗ[A] A ⊗[R] Q) :
                                    (a : N →ₗ[R] Q) → A ⊗[R] N →ₗ[A] A ⊗[R] Q)
                                  f)) :
                          M →ₗ[B] A ⊗[R] N →ₗ[A] M ⊗[R] Q) :
                        (a : M) → A ⊗[R] N →ₗ[A] M ⊗[R] Q)
                      x) :
                  A →ₗ[A] N →ₗ[R] M ⊗[R] Q) :
                (a : A) → N →ₗ[R] M ⊗[R] Q)
              1 :
            (a : N) → M ⊗[R] Q)
          x_1 :
        M ⊗[R] Q)
⊢ Eq (α := M ⊗[A] (A ⊗[R] N) →ₗ[B] M ⊗[R] Q)
    ((((lTensor B M : (N →ₗ[R] Q) →ₗ[R] M ⊗[R] N →ₗ[B] M ⊗[R] Q) : (a : N →ₗ[R] Q) → M ⊗[R] N →ₗ[B] M ⊗[R] Q) f :
          M ⊗[R] N →ₗ[B] M ⊗[R] Q) ∘ₗ
        ((↑(cancelBaseChange R A B M N) : M ⊗[A] (A ⊗[R] N) →ₗ[B] M ⊗[R] N) : M ⊗[A] (A ⊗[R] N) →ₗ[B] M ⊗[R] N) :
      M ⊗[A] (A ⊗[R] N) →ₗ[B] M ⊗[R] Q)
    ((↑(cancelBaseChange R A B M Q) : M ⊗[A] (A ⊗[R] Q) →ₗ[B] M ⊗[R] Q) ∘ₗ
        ((lTensor B M : (A ⊗[R] N →ₗ[A] A ⊗[R] Q) →ₗ[A] M ⊗[A] (A ⊗[R] N) →ₗ[B] M ⊗[A] (A ⊗[R] Q)) :
            (a : A ⊗[R] N →ₗ[A] A ⊗[R] Q) → M ⊗[A] (A ⊗[R] N) →ₗ[B] M ⊗[A] (A ⊗[R] Q))
          (((lTensor A A : (N →ₗ[R] Q) →ₗ[R] A ⊗[R] N →ₗ[A] A ⊗[R] Q) : (a : N →ₗ[R] Q) → A ⊗[R] N →ₗ[A] A ⊗[R] Q) f) :
      M ⊗[A] (A ⊗[R] N) →ₗ[B] M ⊗[R] Q)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
Q : Type uQ
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : Module A M
inst_8 : Module B M
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
inst_12 : AddCommMonoid N
inst_13 : Module R N
inst_14 : AddCommMonoid Q
inst_15 : Module R Q
inst_16 : Algebra A B
inst_17 : IsScalarTower A B M
f : N →ₗ[R] Q
x : M
x_1 : N
⊢ Eq (α := M ⊗[R] Q)
    ((((curry
                  (((curry
                          ((((lTensor B M : (N →ₗ[R] Q) →ₗ[R] M ⊗[R] N →ₗ[B] M ⊗[R] Q) :
                                  (a : N →ₗ[R] Q) → M ⊗[R] N →ₗ[B] M ⊗[R] Q)
                                f :
                              M ⊗[R] N →ₗ[B] M ⊗[R] Q) ∘ₗ
                            ((↑(cancelBaseChange R A B M N) : M ⊗[A] (A ⊗[R] N) →ₗ[B] M ⊗[R] N) :
                              M ⊗[A] (A ⊗[R] N) →ₗ[B] M ⊗[R] N)) :
                        M →ₗ[B] A ⊗[R] N →ₗ[A] M ⊗[R] Q) :
                      (a : M) → A ⊗[R] N →ₗ[A] M ⊗[R] Q)
                    x) :
                A →ₗ[A] N →ₗ[R] M ⊗[R] Q) :
              (a : A) → N →ₗ[R] M ⊗[R] Q)
            1 :
          (a : N) → M ⊗[R] Q)
        x_1 :
      M ⊗[R] Q)
    ((((curry
                  (((curry
                          ((↑(cancelBaseChange R A B M Q) : M ⊗[A] (A ⊗[R] Q) →ₗ[B] M ⊗[R] Q) ∘ₗ
                            ((lTensor B M : (A ⊗[R] N →ₗ[A] A ⊗[R] Q) →ₗ[A] M ⊗[A] (A ⊗[R] N) →ₗ[B] M ⊗[A] (A ⊗[R] Q)) :
                                (a : A ⊗[R] N →ₗ[A] A ⊗[R] Q) → M ⊗[A] (A ⊗[R] N) →ₗ[B] M ⊗[A] (A ⊗[R] Q))
                              (((lTensor A A : (N →ₗ[R] Q) →ₗ[R] A ⊗[R] N →ₗ[A] A ⊗[R] Q) :
                                  (a : N →ₗ[R] Q) → A ⊗[R] N →ₗ[A] A ⊗[R] Q)
                                f)) :
                        M →ₗ[B] A ⊗[R] N →ₗ[A] M ⊗[R] Q) :
                      (a : M) → A ⊗[R] N →ₗ[A] M ⊗[R] Q)
                    x) :
                A →ₗ[A] N →ₗ[R] M ⊗[R] Q) :
              (a : A) → N →ₗ[R] M ⊗[R] Q)
            1 :
          (a : N) → M ⊗[R] Q)
        x_1 :
      M ⊗[R] Q)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
N : Type uN
Q : Type uQ
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid Q
inst_6 : Module R Q
n : N
q : Q
a : A
⊢ Eq (α := A ⊗[R] N ⊗[A] (A ⊗[R] Q))
    ((distribBaseChange R A N Q : (a : A ⊗[R] (N ⊗[R] Q)) → A ⊗[R] N ⊗[A] (A ⊗[R] Q)) (a ⊗ₜ[R] (n ⊗ₜ[R] q)) :
      A ⊗[R] N ⊗[A] (A ⊗[R] Q))
    (a ⊗ₜ[R] n ⊗ₜ[A] (1 ⊗ₜ[R] q) : A ⊗[R] N ⊗[A] (A ⊗[R] Q))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
N : Type uN
Q : Type uQ
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid Q
inst_6 : Module R Q
n : N
q : Q
a b : A
apply :
  Eq (α := A ⊗[R] N ⊗[A] (A ⊗[R] Q))
    ((LinearEquiv.toAddEquiv (distribBaseChange R A N Q) : (a : A ⊗[R] (N ⊗[R] Q)) → A ⊗[R] N ⊗[A] (A ⊗[R] Q))
        ((a * b) ⊗ₜ[R] (n ⊗ₜ[R] q)) :
      A ⊗[R] N ⊗[A] (A ⊗[R] Q))
    (a ⊗ₜ[R] n ⊗ₜ[A] (b ⊗ₜ[R] q) : A ⊗[R] N ⊗[A] (A ⊗[R] Q))
⊢ Eq (α := A ⊗[R] (N ⊗[R] Q))
    ((LinearEquiv.symm (distribBaseChange R A N Q) : (a : A ⊗[R] N ⊗[A] (A ⊗[R] Q)) → A ⊗[R] (N ⊗[R] Q))
        (a ⊗ₜ[R] n ⊗ₜ[A] (b ⊗ₜ[R] q)) :
      A ⊗[R] (N ⊗[R] Q))
    ((a * b) ⊗ₜ[R] (n ⊗ₜ[R] q) : A ⊗[R] (N ⊗[R] Q))

Tactic:
apply ((distribBaseChange R A N Q).apply_eq_iff_symm_apply.mp ?_).symm

Premises used: TensorProduct.AlgebraTensorModule.distribBaseChange, LinearEquiv.toAddEquiv, Iff.mp, Eq.symm, AddEquiv.apply_eq_iff_symm_apply
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
N : Type uN
Q : Type uQ
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid Q
inst_6 : Module R Q
n : N
q : Q
a b : A
rw :
  Eq (α := A ⊗[R] N ⊗[A] (A ⊗[R] Q))
    ((LinearEquiv.toAddEquiv (distribBaseChange R A N Q) : (a : A ⊗[R] (N ⊗[R] Q)) → A ⊗[R] N ⊗[A] (A ⊗[R] Q))
        ((b * a) ⊗ₜ[R] (n ⊗ₜ[R] q)) :
      A ⊗[R] N ⊗[A] (A ⊗[R] Q))
    ((b • a) ⊗ₜ[R] n ⊗ₜ[A] (1 ⊗ₜ[R] q) : A ⊗[R] N ⊗[A] (A ⊗[R] Q))
⊢ Eq (α := A ⊗[R] N ⊗[A] (A ⊗[R] Q))
    ((LinearEquiv.toAddEquiv (distribBaseChange R A N Q) : (a : A ⊗[R] (N ⊗[R] Q)) → A ⊗[R] N ⊗[A] (A ⊗[R] Q))
        ((a * b) ⊗ₜ[R] (n ⊗ₜ[R] q)) :
      A ⊗[R] N ⊗[A] (A ⊗[R] Q))
    (a ⊗ₜ[R] n ⊗ₜ[A] (b ⊗ₜ[R] q) : A ⊗[R] N ⊗[A] (A ⊗[R] Q))

Tactic:
rw [tmul_eq_smul_one_tmul b, ← smul_tmul, smul_tmul', mul_comm]

Premises used: TensorProduct.smul_tmul, TensorProduct.tmul_eq_smul_one_tmul, TensorProduct.smul_tmul', mul_comm
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
N : Type uN
Q : Type uQ
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid Q
inst_6 : Module R Q
n : N
q : Q
a b : A
⊢ Eq (α := A ⊗[R] N ⊗[A] (A ⊗[R] Q))
    ((LinearEquiv.toAddEquiv (distribBaseChange R A N Q) : (a : A ⊗[R] (N ⊗[R] Q)) → A ⊗[R] N ⊗[A] (A ⊗[R] Q))
        ((b * a) ⊗ₜ[R] (n ⊗ₜ[R] q)) :
      A ⊗[R] N ⊗[A] (A ⊗[R] Q))
    ((b • a) ⊗ₜ[R] n ⊗ₜ[A] (1 ⊗ₜ[R] q) : A ⊗[R] N ⊗[A] (A ⊗[R] Q))

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
N : Type uN
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid N
inst_4 : Module R N
h :
  ∀ (x : A ⊗[A] (A ⊗[R] N)),
    Eq (α := A ⊗[R] N)
      (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) x :
        A ⊗[R] N)
      ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) x : A ⊗[R] N)
⊢ Eq (α := A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) (cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N)
    (TensorProduct.lid A (A ⊗[R] N) : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N)

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
N : Type uN
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid N
inst_4 : Module R N
⊢ Eq (α := A ⊗[R] N)
    (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) 0)
    ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) 0)

Tactic:
simp only [map_zero]

Premises used: map_zero
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
N : Type uN
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid N
inst_4 : Module R N
b : A
⊢ Eq (α := A ⊗[R] N)
    (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N)
        (b ⊗ₜ[A] 0) :
      A ⊗[R] N)
    ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) (b ⊗ₜ[A] 0) : A ⊗[R] N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
N : Type uN
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid N
inst_4 : Module R N
b a : A
m : N
⊢ Eq (α := A ⊗[R] N)
    (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N)
        (b ⊗ₜ[A] (a ⊗ₜ[R] m)) :
      A ⊗[R] N)
    ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) (b ⊗ₜ[A] (a ⊗ₜ[R] m)) : A ⊗[R] N)

Tactic:
simp only [cancelBaseChange_tmul, lid_tmul, smul_tmul', smul_eq_mul, mul_comm]

Premises used: TensorProduct.lid_tmul, TensorProduct.AlgebraTensorModule.cancelBaseChange_tmul, TensorProduct.smul_tmul', mul_comm, smul_eq_mul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
N : Type uN
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid N
inst_4 : Module R N
b : A
x y : A ⊗[R] N
hx :
  Eq (α := A ⊗[R] N)
    (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N)
        (b ⊗ₜ[A] x) :
      A ⊗[R] N)
    ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) (b ⊗ₜ[A] x) : A ⊗[R] N)
hy :
  Eq (α := A ⊗[R] N)
    (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N)
        (b ⊗ₜ[A] y) :
      A ⊗[R] N)
    ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) (b ⊗ₜ[A] y) : A ⊗[R] N)
⊢ Eq (α := A ⊗[R] N)
    (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N)
        (b ⊗ₜ[A] (x + y)) :
      A ⊗[R] N)
    ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) (b ⊗ₜ[A] (x + y)) : A ⊗[R] N)

Tactic:
simp only [tmul_add, map_add, lid_tmul, hx, hy]

Premises used: map_add, TensorProduct.lid_tmul, TensorProduct.tmul_add
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
N : Type uN
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid N
inst_4 : Module R N
b : A
y : A ⊗[R] N
h :
  Eq (α := A ⊗[R] N)
    (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N)
        (b ⊗ₜ[A] 0) :
      A ⊗[R] N)
    ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) (b ⊗ₜ[A] 0) : A ⊗[R] N)
h₁ :
  ∀ (a : A) (m : N),
    Eq (α := A ⊗[R] N)
      (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N)
          (b ⊗ₜ[A] (a ⊗ₜ[R] m)) :
        A ⊗[R] N)
      ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) (b ⊗ₜ[A] (a ⊗ₜ[R] m)) : A ⊗[R] N)
h₂ :
  ∀ (x y : A ⊗[R] N)
    (hx :
      Eq (α := A ⊗[R] N)
        (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N)
            (b ⊗ₜ[A] x) :
          A ⊗[R] N)
        ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) (b ⊗ₜ[A] x) : A ⊗[R] N))
    (hy :
      Eq (α := A ⊗[R] N)
        (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N)
            (b ⊗ₜ[A] y) :
          A ⊗[R] N)
        ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) (b ⊗ₜ[A] y) : A ⊗[R] N)),
    Eq (α := A ⊗[R] N)
      (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N)
          (b ⊗ₜ[A] (x + y)) :
        A ⊗[R] N)
      ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) (b ⊗ₜ[A] (x + y)) : A ⊗[R] N)
⊢ Eq (α := A ⊗[R] N)
    (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N)
        (b ⊗ₜ[A] y) :
      A ⊗[R] N)
    ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) (b ⊗ₜ[A] y) : A ⊗[R] N)

Tactic:
induction y using TensorProduct.induction_on with
    | zero => simp
    | tmul a m =>
      simp only [cancelBaseChange_tmul, lid_tmul, smul_tmul', smul_eq_mul, mul_comm]
    | add x y hx hy =>
      simp only [tmul_add, map_add, lid_tmul, hx, hy]

Premises used: map_add, TensorProduct.lid_tmul, TensorProduct.AlgebraTensorModule.cancelBaseChange_tmul, TensorProduct.smul_tmul', mul_comm, TensorProduct.tmul_add, TensorProduct.tmul, smul_eq_mul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
N : Type uN
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid N
inst_4 : Module R N
x y : A ⊗[A] (A ⊗[R] N)
hx :
  Eq (α := A ⊗[R] N)
    (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) x :
      A ⊗[R] N)
    ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) x : A ⊗[R] N)
hy :
  Eq (α := A ⊗[R] N)
    (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) y :
      A ⊗[R] N)
    ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) y : A ⊗[R] N)
⊢ Eq (α := A ⊗[R] N)
    (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) (x + y) :
      A ⊗[R] N)
    ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) (x + y) : A ⊗[R] N)

Tactic:
simp [hx, hy]
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
N : Type uN
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid N
inst_4 : Module R N
x : A ⊗[A] (A ⊗[R] N)
h :
  Eq (α := A ⊗[R] N)
    (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) 0)
    ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) 0)
h₁ :
  ∀ (b : A) (y : A ⊗[R] N),
    Eq (α := A ⊗[R] N)
      (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N)
          (b ⊗ₜ[A] y) :
        A ⊗[R] N)
      ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) (b ⊗ₜ[A] y) : A ⊗[R] N)
h₂ :
  ∀ (x y : A ⊗[A] (A ⊗[R] N))
    (hx :
      Eq (α := A ⊗[R] N)
        (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) x :
          A ⊗[R] N)
        ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) x : A ⊗[R] N))
    (hy :
      Eq (α := A ⊗[R] N)
        (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) y :
          A ⊗[R] N)
        ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) y : A ⊗[R] N)),
    Eq (α := A ⊗[R] N)
      (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) (x + y) :
        A ⊗[R] N)
      ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) (x + y) : A ⊗[R] N)
⊢ Eq (α := A ⊗[R] N)
    (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) x :
      A ⊗[R] N)
    ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) x : A ⊗[R] N)

Tactic:
induction x using TensorProduct.induction_on with
  | zero => simp only [map_zero]
  | tmul b y =>
    induction y using TensorProduct.induction_on with
    | zero => simp
    | tmul a m =>
      simp only [cancelBaseChange_tmul, lid_tmul, smul_tmul', smul_eq_mul, mul_comm]
    | add x y hx hy =>
      simp only [tmul_add, map_add, lid_tmul, hx, hy]
  | add x y hx hy => simp [hx, hy]

Premises used: map_zero, map_add, TensorProduct.lid_tmul, TensorProduct.AlgebraTensorModule.cancelBaseChange_tmul, TensorProduct.smul_tmul', mul_comm, TensorProduct.tmul_add, TensorProduct.tmul, smul_eq_mul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
M : Type uM
P : Type uP
Q : Type uQ
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
inst_7 : AddCommMonoid P
inst_8 : Module A P
inst_9 : AddCommMonoid Q
inst_10 : Module R Q
inst_11 : Module R P
inst_12 : IsScalarTower R A P
m : M
p : P
q : Q
⊢ Eq (α := P ⊗[A] (M ⊗[R] Q))
    (((leftComm R A M P Q : M ⊗[A] (P ⊗[R] Q) ≃ₗ[A] P ⊗[A] (M ⊗[R] Q)) : (a : M ⊗[A] (P ⊗[R] Q)) → P ⊗[A] (M ⊗[R] Q))
        (m ⊗ₜ[A] (p ⊗ₜ[R] q)) :
      P ⊗[A] (M ⊗[R] Q))
    (p ⊗ₜ[A] (m ⊗ₜ[R] q) : P ⊗[A] (M ⊗[R] Q))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
M : Type uM
P : Type uP
Q : Type uQ
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
inst_7 : AddCommMonoid P
inst_8 : Module A P
inst_9 : AddCommMonoid Q
inst_10 : Module R Q
inst_11 : Module R P
inst_12 : IsScalarTower R A P
m : M
p : P
q : Q
⊢ Eq (α := M ⊗[A] (P ⊗[R] Q))
    (((LinearEquiv.symm (leftComm R A M P Q) : P ⊗[A] (M ⊗[R] Q) ≃ₗ[A] M ⊗[A] (P ⊗[R] Q)) :
          (a : P ⊗[A] (M ⊗[R] Q)) → M ⊗[A] (P ⊗[R] Q))
        (p ⊗ₜ[A] (m ⊗ₜ[R] q)) :
      M ⊗[A] (P ⊗[R] Q))
    (m ⊗ₜ[A] (p ⊗ₜ[R] q) : M ⊗[A] (P ⊗[R] Q))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
M : Type uM
P : Type uP
Q : Type uQ
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R Q
inst_6 : Module R P
⊢ Eq (α := M ⊗[R] (P ⊗[R] Q) ≃ₗ[R] P ⊗[R] (M ⊗[R] Q)) (leftComm R R M P Q : M ⊗[R] (P ⊗[R] Q) ≃ₗ[R] P ⊗[R] (M ⊗[R] Q))
    (TensorProduct.leftComm R M P Q : M ⊗[R] (P ⊗[R] Q) ≃ₗ[R] P ⊗[R] (M ⊗[R] Q))

Tactic:
rfl

Premises used: LinearEquiv.symm, TensorProduct.AlgebraTensorModule.leftComm, addConGen, Quotient.liftOn', AddCon.liftOn, TensorProduct.leftComm, Quotient, LinearEquiv.toEquiv, TensorProduct, TensorProduct.tmul, AddCon.Quotient, LinearEquiv.trans, AddCon.toQuotient, FreeAddMonoid, rfl, TensorProduct.AlgebraTensorModule.lift
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
P' : Type uP'
Q' : Type uQ'
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : Module A M
inst_8 : Module B M
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
inst_12 : AddCommMonoid N
inst_13 : Module R N
inst_14 : AddCommMonoid P
inst_15 : Module A P
inst_16 : AddCommMonoid P'
inst_17 : Module A P'
inst_18 : AddCommMonoid Q
inst_19 : Module R Q
inst_20 : CommSemiring S
inst_21 : Module S M
inst_22 : Module S P
inst_23 : Algebra S B
inst_24 : IsScalarTower S B M
inst_25 : SMulCommClass R S M
inst_26 : SMulCommClass S R M
x : M
x_1 : Q
x_2 : P
⊢ Eq (α := M ⊗[R] Q ⊗[S] P)
    (((((((curry
                          (curry
                            ((lift
                                  (lift
                                    ((↑lflip :
                                          (Q →ₗ[R] P →ₗ[S] M ⊗[R] Q ⊗[S] P) →ₗ[B] P →ₗ[S] Q →ₗ[R] M ⊗[R] Q ⊗[S] P) ∘ₗ
                                        compr₂ (mk R B M Q) (mk S B (M ⊗[R] Q) P) :
                                      M →ₗ[B] P →ₗ[S] Q →ₗ[R] M ⊗[R] Q ⊗[S] P)) :
                                M ⊗[S] P ⊗[R] Q →ₗ[B] M ⊗[R] Q ⊗[S] P) ∘ₗ
                              (lift
                                  (lift
                                    ((↑lflip :
                                          (P →ₗ[S] Q →ₗ[R] M ⊗[S] P ⊗[R] Q) →ₗ[B] Q →ₗ[R] P →ₗ[S] M ⊗[S] P ⊗[R] Q) ∘ₗ
                                        compr₂ (mk S B M P) (mk R B (M ⊗[S] P) Q) :
                                      M →ₗ[B] Q →ₗ[R] P →ₗ[S] M ⊗[S] P ⊗[R] Q)) :
                                M ⊗[R] Q ⊗[S] P →ₗ[B] M ⊗[S] P ⊗[R] Q))) :
                        M →ₗ[B] Q →ₗ[R] P →ₗ[S] M ⊗[R] Q ⊗[S] P) :
                      (a : M) → Q →ₗ[R] P →ₗ[S] M ⊗[R] Q ⊗[S] P)
                    x :
                  Q →ₗ[R] P →ₗ[S] M ⊗[R] Q ⊗[S] P) :
                (a : Q) → P →ₗ[S] M ⊗[R] Q ⊗[S] P)
              x_1 :
            P →ₗ[S] M ⊗[R] Q ⊗[S] P) :
          (a : P) → M ⊗[R] Q ⊗[S] P)
        x_2 :
      M ⊗[R] Q ⊗[S] P)
    (((((((curry (curry LinearMap.id) : M →ₗ[B] Q →ₗ[R] P →ₗ[S] M ⊗[R] Q ⊗[S] P) :
                      (a : M) → Q →ₗ[R] P →ₗ[S] M ⊗[R] Q ⊗[S] P)
                    x :
                  Q →ₗ[R] P →ₗ[S] M ⊗[R] Q ⊗[S] P) :
                (a : Q) → P →ₗ[S] M ⊗[R] Q ⊗[S] P)
              x_1 :
            P →ₗ[S] M ⊗[R] Q ⊗[S] P) :
          (a : P) → M ⊗[R] Q ⊗[S] P)
        x_2 :
      M ⊗[R] Q ⊗[S] P)

Tactic:
simp