awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
M : Type uM
inst : CommSemiring R
inst_1 : Semiring 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
f₁ f₂ : M →ₗ[A] M
⊢ ((rTensor R M : (M →ₗ[A] M) →ₗ[R] M ⊗[R] M →ₗ[A] M ⊗[R] M) : (a : M →ₗ[A] M) → M ⊗[R] M →ₗ[A] M ⊗[R] M) (f₁ * f₂) =
    HMul.hMul (α := M ⊗[R] M →ₗ[A] M ⊗[R] M) (β := M ⊗[R] M →ₗ[A] M ⊗[R] M)
      (((rTensor R M : (M →ₗ[A] M) →ₗ[R] M ⊗[R] M →ₗ[A] M ⊗[R] M) : (a : M →ₗ[A] M) → M ⊗[R] M →ₗ[A] M ⊗[R] M) f₁ :
        M ⊗[R] M →ₗ[A] M ⊗[R] M)
      (((rTensor R M : (M →ₗ[A] M) →ₗ[R] M ⊗[R] M →ₗ[A] M ⊗[R] M) : (a : M →ₗ[A] M) → M ⊗[R] M →ₗ[A] M ⊗[R] M) f₂ :
        M ⊗[R] M →ₗ[A] M ⊗[R] M)

Tactic:
rTensor_comp _ _

Premises used: TensorProduct.AlgebraTensorModule.rTensor_comp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst : CommSemiring R
inst_1 : Semiring 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 : IsScalarTower R A M
inst_9 : AddCommMonoid N
inst_10 : Module R N
inst_11 : AddCommMonoid P
inst_12 : Module R P
inst_13 : Module A P
inst_14 : IsScalarTower R A P
inst_15 : AddCommMonoid Q
inst_16 : Module R Q
inst_17 : Module B P
inst_18 : IsScalarTower R B P
inst_19 : SMulCommClass A B P
f : M →ₗ[A] P
g : N →ₗ[R] Q
⊢ Eq (α := M ⊗[R] N →ₗ[A] P ⊗[R] Q)
    (((((mapBilinear R A B M N P Q : (M →ₗ[A] P) →ₗ[B] (N →ₗ[R] Q) →ₗ[R] M ⊗[R] N →ₗ[A] P ⊗[R] Q) :
                (a : M →ₗ[A] P) → (N →ₗ[R] Q) →ₗ[R] M ⊗[R] N →ₗ[A] P ⊗[R] Q)
              f :
            (N →ₗ[R] Q) →ₗ[R] M ⊗[R] N →ₗ[A] P ⊗[R] Q) :
          (a : N →ₗ[R] Q) → M ⊗[R] N →ₗ[A] P ⊗[R] Q)
        g :
      M ⊗[R] N →ₗ[A] P ⊗[R] Q)
    (map f g : M ⊗[R] N →ₗ[A] P ⊗[R] Q)

Tactic:
rfl

Premises used: TensorProduct.AlgebraTensorModule.map, rfl, TensorProduct.AlgebraTensorModule.lift
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst : CommSemiring R
inst_1 : Semiring 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 : IsScalarTower R A M
inst_9 : AddCommMonoid N
inst_10 : Module R N
inst_11 : AddCommMonoid P
inst_12 : Module R P
inst_13 : Module A P
inst_14 : IsScalarTower R A P
inst_15 : AddCommMonoid Q
inst_16 : Module R Q
inst_17 : Module B P
inst_18 : IsScalarTower R B P
inst_19 : SMulCommClass A B P
f : M →ₗ[A] P
g : N →ₗ[R] Q
⊢ Eq (α := M ⊗[R] N →ₗ[A] P ⊗[R] Q)
    (((homTensorHomMap R A B M N P Q : (M →ₗ[A] P) ⊗[R] (N →ₗ[R] Q) →ₗ[B] M ⊗[R] N →ₗ[A] P ⊗[R] Q) :
          (a : (M →ₗ[A] P) ⊗[R] (N →ₗ[R] Q)) → M ⊗[R] N →ₗ[A] P ⊗[R] Q)
        (f ⊗ₜ[R] g) :
      M ⊗[R] N →ₗ[A] P ⊗[R] Q)
    (map f g : M ⊗[R] N →ₗ[A] P ⊗[R] Q)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, TensorProduct.AlgebraTensorModule.map, rfl, TensorProduct.AlgebraTensorModule.lift
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
inst : CommSemiring R
inst_1 : Semiring 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 N
inst_8 : Module R N
⊢ Eq (α := M ⊗[R] N ≃ₗ[A] M ⊗[R] N) (congr (LinearEquiv.refl A M) (LinearEquiv.refl R N) : M ⊗[R] N ≃ₗ[A] M ⊗[R] N)
    (LinearEquiv.refl A (M ⊗[R] N) : M ⊗[R] N ≃ₗ[A] M ⊗[R] N)

Tactic:
LinearEquiv.toLinearMap_injective <| map_id

Premises used: TensorProduct.AlgebraTensorModule.map_id, LinearEquiv.toLinearMap_injective
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
P' : Type uP'
Q' : Type uQ'
inst : CommSemiring R
inst_1 : Semiring 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 N
inst_8 : Module R N
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : Module A P
inst_12 : IsScalarTower R A P
inst_13 : AddCommMonoid Q
inst_14 : Module R Q
inst_15 : AddCommMonoid P'
inst_16 : Module R P'
inst_17 : Module A P'
inst_18 : IsScalarTower R A P'
inst_19 : AddCommMonoid Q'
inst_20 : Module R Q'
f₁ : M ≃ₗ[A] P
f₂ : P ≃ₗ[A] P'
g₁ : N ≃ₗ[R] Q
g₂ : Q ≃ₗ[R] Q'
⊢ Eq (α := M ⊗[R] N ≃ₗ[A] P' ⊗[R] Q') (congr (f₁ ≪≫ₗ f₂) (g₁ ≪≫ₗ g₂) : M ⊗[R] N ≃ₗ[A] P' ⊗[R] Q')
    ((congr f₁ g₁ : M ⊗[R] N ≃ₗ[A] P ⊗[R] Q) ≪≫ₗ (congr f₂ g₂ : P ⊗[R] Q ≃ₗ[A] P' ⊗[R] Q') : M ⊗[R] N ≃ₗ[A] P' ⊗[R] Q')

Tactic:
LinearEquiv.toLinearMap_injective <| map_comp _ _ _ _

Premises used: LinearEquiv.toLinearMap_injective, TensorProduct.AlgebraTensorModule.map_comp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst : CommSemiring R
inst_1 : Semiring 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 N
inst_8 : Module R N
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : Module A P
inst_12 : IsScalarTower R A P
inst_13 : AddCommMonoid Q
inst_14 : Module R Q
f : M ≃ₗ[A] P
g : N ≃ₗ[R] Q
⊢ Eq (α := P ⊗[R] Q ≃ₗ[A] M ⊗[R] N) (congr f.symm g.symm : P ⊗[R] Q ≃ₗ[A] M ⊗[R] N)
    (LinearEquiv.symm (congr f g) : P ⊗[R] Q ≃ₗ[A] M ⊗[R] N)

Tactic:
rfl

Premises used: LinearEquiv.symm, Quotient.liftOn', AddCon.liftOn, LinearEquiv.ofLinear, TensorProduct.AlgebraTensorModule.congr, TensorProduct, TensorProduct.AlgebraTensorModule.map, rfl, TensorProduct.AlgebraTensorModule.lift
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
inst : CommSemiring R
inst_1 : Semiring 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 N
inst_8 : Module R N
⊢ Eq (α := M ⊗[R] N ≃ₗ[A] M ⊗[R] N) (congr 1 1 : M ⊗[R] N ≃ₗ[A] M ⊗[R] N) (1 : M ⊗[R] N ≃ₗ[A] M ⊗[R] N)

Tactic:
congr_refl

Premises used: TensorProduct.AlgebraTensorModule.congr_refl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
inst : CommSemiring R
inst_1 : Semiring 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 N
inst_8 : Module R N
f₁ f₂ : M ≃ₗ[A] M
g₁ g₂ : N ≃ₗ[R] N
⊢ congr (f₁ * f₂) (g₁ * g₂) =
    HMul.hMul (α := M ⊗[R] N ≃ₗ[A] M ⊗[R] N) (β := M ⊗[R] N ≃ₗ[A] M ⊗[R] N) (congr f₁ g₁ : M ⊗[R] N ≃ₗ[A] M ⊗[R] N)
      (congr f₂ g₂ : M ⊗[R] N ≃ₗ[A] M ⊗[R] N)

Tactic:
congr_trans _ _ _ _

Premises used: TensorProduct.AlgebraTensorModule.congr_trans
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst : CommSemiring R
inst_1 : Semiring 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 N
inst_8 : Module R N
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : Module A P
inst_12 : IsScalarTower R A P
inst_13 : AddCommMonoid Q
inst_14 : Module R Q
f : M ≃ₗ[A] P
g : N ≃ₗ[R] Q
m : M
n : N
⊢ Eq (α := P ⊗[R] Q) (((congr f g : M ⊗[R] N ≃ₗ[A] P ⊗[R] Q) : (a : M ⊗[R] N) → P ⊗[R] Q) (m ⊗ₜ[R] n) : P ⊗[R] Q)
    ((f : (a : M) → P) m ⊗ₜ[R] (g : (a : N) → Q) n : 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
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst : CommSemiring R
inst_1 : Semiring 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 N
inst_8 : Module R N
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : Module A P
inst_12 : IsScalarTower R A P
inst_13 : AddCommMonoid Q
inst_14 : Module R Q
f : M ≃ₗ[A] P
g : N ≃ₗ[R] Q
p : P
q : Q
⊢ Eq (α := M ⊗[R] N)
    (((LinearEquiv.symm (congr f g) : P ⊗[R] Q ≃ₗ[A] M ⊗[R] N) : (a : P ⊗[R] Q) → M ⊗[R] N) (p ⊗ₜ[R] q) : M ⊗[R] N)
    ((f.symm : (a : P) → M) p ⊗ₜ[R] (g.symm : (a : Q) → N) q : M ⊗[R] N)

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
N : Type uN
P : Type uP
Q : Type uQ
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid P
inst_6 : Module R P
inst_7 : AddCommMonoid Q
inst_8 : Module R Q
f : M ≃ₗ[R] P
g : N ≃ₗ[R] Q
⊢ congr f g = TensorProduct.congr f g

Tactic:
rfl

Premises used: TensorProduct.congr, TensorProduct.map, TensorProduct.AlgebraTensorModule.congr, TensorProduct.tmul, TensorProduct.lift, AddCon.toQuotient, TensorProduct.AlgebraTensorModule.map, rfl, TensorProduct.AlgebraTensorModule.lift
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
M : Type uM
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := M ⊗[R] R ≃ₗ[R] M) (AlgebraTensorModule.rid R R M : M ⊗[R] R ≃ₗ[R] M)
    (TensorProduct.rid R M : M ⊗[R] R ≃ₗ[R] M)

Tactic:
rfl

Premises used: TensorProduct.rid, TensorProduct.AlgebraTensorModule.rid, TensorProduct.lift, rfl, TensorProduct.AlgebraTensorModule.lift
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
M : Type uM
inst : CommSemiring R
inst_1 : Semiring 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
r : R
m : M
⊢ ((AlgebraTensorModule.rid R A M : M ⊗[R] R ≃ₗ[A] M) : (a : M ⊗[R] R) → M) (m ⊗ₜ[R] r) = r • m

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
M : Type uM
inst : CommSemiring R
inst_1 : Semiring 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
m : M
⊢ Eq (α := M ⊗[R] R)
    (((LinearEquiv.symm (AlgebraTensorModule.rid R A M) : M ≃ₗ[A] M ⊗[R] R) : (a : M) → M ⊗[R] R) m : M ⊗[R] R)
    (m ⊗ₜ[R] 1 : M ⊗[R] R)

Tactic:
rfl

Premises used: TensorProduct.tmul, AddCon.toQuotient, rfl
-- 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 : Module R P
inst_21 : IsScalarTower R A P
inst_22 : Algebra A B
inst_23 : IsScalarTower A B M
x : M
x_1 : P
x_2 : Q
⊢ Eq (α := M ⊗[A] (P ⊗[R] Q))
    (((((curry
                    (((curry
                            ((lift
                                  (lift
                                    ((lcurry R A B P Q (M ⊗[A] (P ⊗[R] Q)) :
                                          (P ⊗[R] Q →ₗ[A] M ⊗[A] (P ⊗[R] Q)) →ₗ[B] P →ₗ[A] Q →ₗ[R] M ⊗[A] (P ⊗[R] Q)) ∘ₗ
                                        (mk A B M (P ⊗[R] Q) : M →ₗ[B] P ⊗[R] Q →ₗ[A] M ⊗[A] (P ⊗[R] Q)) :
                                      M →ₗ[B] P →ₗ[A] Q →ₗ[R] M ⊗[A] (P ⊗[R] Q))) :
                                M ⊗[A] P ⊗[R] Q →ₗ[B] M ⊗[A] (P ⊗[R] Q)) ∘ₗ
                              (lift
                                  ((uncurry R A B P Q (M ⊗[A] P ⊗[R] Q) :
                                      (P →ₗ[A] Q →ₗ[R] M ⊗[A] P ⊗[R] Q) →ₗ[B] P ⊗[R] Q →ₗ[A] M ⊗[A] P ⊗[R] Q) ∘ₗ
                                    (curry (mk R B (M ⊗[A] P) Q) : M →ₗ[B] P →ₗ[A] Q →ₗ[R] M ⊗[A] P ⊗[R] Q)) :
                                M ⊗[A] (P ⊗[R] Q) →ₗ[B] M ⊗[A] P ⊗[R] Q)) :
                          M →ₗ[B] P ⊗[R] Q →ₗ[A] M ⊗[A] (P ⊗[R] Q)) :
                        (a : M) → P ⊗[R] Q →ₗ[A] M ⊗[A] (P ⊗[R] Q))
                      x) :
                  P →ₗ[A] Q →ₗ[R] M ⊗[A] (P ⊗[R] Q)) :
                (a : P) → Q →ₗ[R] M ⊗[A] (P ⊗[R] Q))
              x_1 :
            Q →ₗ[R] M ⊗[A] (P ⊗[R] Q)) :
          (a : Q) → M ⊗[A] (P ⊗[R] Q))
        x_2 :
      M ⊗[A] (P ⊗[R] Q))
    (((((curry
                    (((curry LinearMap.id : M →ₗ[B] P ⊗[R] Q →ₗ[A] M ⊗[A] (P ⊗[R] Q)) :
                        (a : M) → P ⊗[R] Q →ₗ[A] M ⊗[A] (P ⊗[R] Q))
                      x) :
                  P →ₗ[A] Q →ₗ[R] M ⊗[A] (P ⊗[R] Q)) :
                (a : P) → Q →ₗ[R] M ⊗[A] (P ⊗[R] Q))
              x_1 :
            Q →ₗ[R] M ⊗[A] (P ⊗[R] Q)) :
          (a : Q) → M ⊗[A] (P ⊗[R] Q))
        x_2 :
      M ⊗[A] (P ⊗[R] Q))

Tactic:
rfl
-- 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 : Module R P
inst_21 : IsScalarTower R A P
inst_22 : Algebra A B
inst_23 : IsScalarTower A B M
x : M
x_1 : P
x_2 : Q
⊢ Eq (α := M ⊗[A] P ⊗[R] Q)
    (((((((curry
                          (curry
                            ((lift
                                  ((uncurry R A B P Q (M ⊗[A] P ⊗[R] Q) :
                                      (P →ₗ[A] Q →ₗ[R] M ⊗[A] P ⊗[R] Q) →ₗ[B] P ⊗[R] Q →ₗ[A] M ⊗[A] P ⊗[R] Q) ∘ₗ
                                    (curry (mk R B (M ⊗[A] P) Q) : M →ₗ[B] P →ₗ[A] Q →ₗ[R] M ⊗[A] P ⊗[R] Q)) :
                                M ⊗[A] (P ⊗[R] Q) →ₗ[B] M ⊗[A] P ⊗[R] Q) ∘ₗ
                              (lift
                                  (lift
                                    ((lcurry R A B P Q (M ⊗[A] (P ⊗[R] Q)) :
                                          (P ⊗[R] Q →ₗ[A] M ⊗[A] (P ⊗[R] Q)) →ₗ[B] P →ₗ[A] Q →ₗ[R] M ⊗[A] (P ⊗[R] Q)) ∘ₗ
                                        (mk A B M (P ⊗[R] Q) : M →ₗ[B] P ⊗[R] Q →ₗ[A] M ⊗[A] (P ⊗[R] Q)) :
                                      M →ₗ[B] P →ₗ[A] Q →ₗ[R] M ⊗[A] (P ⊗[R] Q))) :
                                M ⊗[A] P ⊗[R] Q →ₗ[B] M ⊗[A] (P ⊗[R] Q)))) :
                        M →ₗ[B] P →ₗ[A] Q →ₗ[R] M ⊗[A] P ⊗[R] Q) :
                      (a : M) → P →ₗ[A] Q →ₗ[R] M ⊗[A] P ⊗[R] Q)
                    x :
                  P →ₗ[A] Q →ₗ[R] M ⊗[A] P ⊗[R] Q) :
                (a : P) → Q →ₗ[R] M ⊗[A] P ⊗[R] Q)
              x_1 :
            Q →ₗ[R] M ⊗[A] P ⊗[R] Q) :
          (a : Q) → M ⊗[A] P ⊗[R] Q)
        x_2 :
      M ⊗[A] P ⊗[R] Q)
    (((((((curry (curry LinearMap.id) : M →ₗ[B] P →ₗ[A] Q →ₗ[R] M ⊗[A] P ⊗[R] Q) :
                      (a : M) → P →ₗ[A] Q →ₗ[R] M ⊗[A] P ⊗[R] Q)
                    x :
                  P →ₗ[A] Q →ₗ[R] M ⊗[A] P ⊗[R] Q) :
                (a : P) → Q →ₗ[R] M ⊗[A] P ⊗[R] Q)
              x_1 :
            Q →ₗ[R] M ⊗[A] P ⊗[R] Q) :
          (a : Q) → M ⊗[A] P ⊗[R] Q)
        x_2 :
      M ⊗[A] P ⊗[R] Q)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
B : Type uB
M : Type uM
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 P
inst_13 : Module A P
inst_14 : AddCommMonoid Q
inst_15 : Module R Q
inst_16 : Module R P
inst_17 : IsScalarTower R A P
inst_18 : Algebra A B
inst_19 : IsScalarTower A B M
m : M
p : P
q : Q
⊢ Eq (α := M ⊗[A] (P ⊗[R] Q))
    (((assoc R A B M P Q : M ⊗[A] P ⊗[R] Q ≃ₗ[B] M ⊗[A] (P ⊗[R] Q)) : (a : M ⊗[A] P ⊗[R] Q) → M ⊗[A] (P ⊗[R] Q))
        (m ⊗ₜ[A] p ⊗ₜ[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
A : Type uA
B : Type uB
M : Type uM
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 P
inst_13 : Module A P
inst_14 : AddCommMonoid Q
inst_15 : Module R Q
inst_16 : Module R P
inst_17 : IsScalarTower R A P
inst_18 : Algebra A B
inst_19 : IsScalarTower A B M
m : M
p : P
q : Q
⊢ Eq (α := M ⊗[A] P ⊗[R] Q)
    (((LinearEquiv.symm (assoc R A B M P Q) : M ⊗[A] (P ⊗[R] Q) ≃ₗ[B] M ⊗[A] P ⊗[R] Q) :
          (a : M ⊗[A] (P ⊗[R] Q)) → M ⊗[A] P ⊗[R] Q)
        (m ⊗ₜ[A] (p ⊗ₜ[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] M ⊗[R] (P ⊗[R] Q)) (assoc R R R M P Q : M ⊗[R] P ⊗[R] Q ≃ₗ[R] M ⊗[R] (P ⊗[R] Q))
    (TensorProduct.assoc R M P Q : M ⊗[R] P ⊗[R] Q ≃ₗ[R] M ⊗[R] (P ⊗[R] Q))

Tactic:
rfl

Premises used: TensorProduct.assoc, TensorProduct.tmul, TensorProduct.lift, AddCon.toQuotient, rfl, TensorProduct.AlgebraTensorModule.assoc, TensorProduct.AlgebraTensorModule.lift
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
P' : Type uP'
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 N
inst_8 : Module R N
inst_9 : AddCommMonoid P
inst_10 : Module A P
inst_11 : AddCommMonoid P'
inst_12 : Module A P'
inst_13 : Module R P
inst_14 : IsScalarTower R A P
inst_15 : Module R P'
inst_16 : IsScalarTower R A P'
g : P →ₗ[A] P'
⊢ Eq (α := P ⊗[A] (M ⊗[R] N) →ₗ[A] P' ⊗[A] (M ⊗[R] N))
    (LinearMap.rTensor (M ⊗[R] N) g : P ⊗[A] (M ⊗[R] N) →ₗ[A] P' ⊗[A] (M ⊗[R] N))
    (((↑(assoc R A A P' M N) : P' ⊗[A] M ⊗[R] N →ₗ[A] P' ⊗[A] (M ⊗[R] N)) :
          P' ⊗[A] M ⊗[R] N →ₗ[A] P' ⊗[A] (M ⊗[R] N)) ∘ₗ
        ((map (LinearMap.rTensor M g) LinearMap.id : P ⊗[A] M ⊗[R] N →ₗ[A] P' ⊗[A] M ⊗[R] N) ∘ₗ
            ((↑(LinearEquiv.symm (assoc R A A P M N)) : P ⊗[A] (M ⊗[R] N) →ₗ[A] P ⊗[A] M ⊗[R] N) :
              P ⊗[A] (M ⊗[R] N) →ₗ[A] P ⊗[A] M ⊗[R] N) :
          P ⊗[A] (M ⊗[R] N) →ₗ[A] P' ⊗[A] M ⊗[R] N) :
      P ⊗[A] (M ⊗[R] N) →ₗ[A] P' ⊗[A] (M ⊗[R] N))

Tactic:
TensorProduct.ext <| LinearMap.ext fun _ ↦ ext fun _ _ ↦ rfl

Premises used: TensorProduct.AlgebraTensorModule.ext, LinearMap.ext, TensorProduct.ext, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
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 : Algebra A B
inst_15 : IsScalarTower A B M
m : M
n : N
a : A
⊢ Eq (α := M ⊗[R] N)
    (((cancelBaseChange R A B M N : M ⊗[A] (A ⊗[R] N) ≃ₗ[B] M ⊗[R] N) : (a : M ⊗[A] (A ⊗[R] N)) → M ⊗[R] N)
        (m ⊗ₜ[A] (a ⊗ₜ[R] n)) :
      M ⊗[R] N)
    ((a • m) ⊗ₜ[R] n : M ⊗[R] N)

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
B : Type uB
M : Type uM
N : Type uN
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 : Algebra A B
inst_15 : IsScalarTower A B M
m : M
n : N
⊢ Eq (α := M ⊗[A] (A ⊗[R] N))
    (((LinearEquiv.symm (cancelBaseChange R A B M N) : M ⊗[R] N ≃ₗ[B] M ⊗[A] (A ⊗[R] N)) :
          (a : M ⊗[R] N) → M ⊗[A] (A ⊗[R] N))
        (m ⊗ₜ[R] n) :
      M ⊗[A] (A ⊗[R] N))
    (m ⊗ₜ[A] (1 ⊗ₜ[R] n) : M ⊗[A] (A ⊗[R] N))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl