awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
R₂ : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring R₂
σ₁₂ : R →+* R₂
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
P₂ : Type u_17
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid P
inst_5 : AddCommMonoid Q
inst_6 : AddCommMonoid P₂
inst_7 : Module R M
inst_8 : Module R N
inst_9 : Module R₂ P₂
inst_10 : Module R P
inst_11 : Module R Q
g h : M ⊗[R] N ⊗[R] P ⊗[R] Q →ₛₗ[σ₁₂] P₂
H :
  ∀ (w : M) (x : N) (y : P) (z : Q),
    Eq.{u_17 + 1} (α := P₂) ((g : (a : M ⊗[R] N ⊗[R] P ⊗[R] Q) → P₂) (w ⊗ₜ[R] x ⊗ₜ[R] y ⊗ₜ[R] z) : P₂)
      ((h : (a : M ⊗[R] N ⊗[R] P ⊗[R] Q) → P₂) (w ⊗ₜ[R] x ⊗ₜ[R] y ⊗ₜ[R] z) : P₂)
w : M
x : N
y : P
z : Q
⊢ Eq.{u_17 + 1} (α := P₂)
    ((((((((LinearMap.compr₂ₛₗ (mk R M N)
                              (LinearMap.compr₂ₛₗ (mk R (M ⊗[R] N) P)
                                (LinearMap.compr₂ₛₗ (mk R (M ⊗[R] N ⊗[R] P) Q) g)) :
                            (a : M) → N →ₛₗ[σ₁₂] P →ₛₗ[σ₁₂] Q →ₛₗ[σ₁₂] P₂)
                          w :
                        N →ₛₗ[σ₁₂] P →ₛₗ[σ₁₂] Q →ₛₗ[σ₁₂] P₂) :
                      (a : N) → P →ₛₗ[σ₁₂] Q →ₛₗ[σ₁₂] P₂)
                    x :
                  P →ₛₗ[σ₁₂] Q →ₛₗ[σ₁₂] P₂) :
                (a : P) → Q →ₛₗ[σ₁₂] P₂)
              y :
            Q →ₛₗ[σ₁₂] P₂) :
          (a : Q) → P₂)
        z :
      P₂)
    ((((((((LinearMap.compr₂ₛₗ (mk R M N)
                              (LinearMap.compr₂ₛₗ (mk R (M ⊗[R] N) P)
                                (LinearMap.compr₂ₛₗ (mk R (M ⊗[R] N ⊗[R] P) Q) h)) :
                            (a : M) → N →ₛₗ[σ₁₂] P →ₛₗ[σ₁₂] Q →ₛₗ[σ₁₂] P₂)
                          w :
                        N →ₛₗ[σ₁₂] P →ₛₗ[σ₁₂] Q →ₛₗ[σ₁₂] P₂) :
                      (a : N) → P →ₛₗ[σ₁₂] Q →ₛₗ[σ₁₂] P₂)
                    x :
                  P →ₛₗ[σ₁₂] Q →ₛₗ[σ₁₂] P₂) :
                (a : P) → Q →ₛₗ[σ₁₂] P₂)
              y :
            Q →ₛₗ[σ₁₂] P₂) :
          (a : Q) → P₂)
        z :
      P₂)

Tactic:
H w x y z

Premises used: TensorProduct.tmul, AddCon.toQuotient
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
R₂ : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring R₂
σ₁₂ : R →+* R₂
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
P₂ : Type u_17
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid P
inst_5 : AddCommMonoid Q
inst_6 : AddCommMonoid P₂
inst_7 : Module R M
inst_8 : Module R N
inst_9 : Module R₂ P₂
inst_10 : Module R P
inst_11 : Module R Q
g h : M ⊗[R] N ⊗[R] P ⊗[R] Q →ₛₗ[σ₁₂] P₂
H :
  ∀ (w : M) (x : N) (y : P) (z : Q),
    Eq.{u_17 + 1} (α := P₂) ((g : (a : M ⊗[R] N ⊗[R] P ⊗[R] Q) → P₂) (w ⊗ₜ[R] x ⊗ₜ[R] y ⊗ₜ[R] z) : P₂)
      ((h : (a : M ⊗[R] N ⊗[R] P ⊗[R] Q) → P₂) (w ⊗ₜ[R] x ⊗ₜ[R] y ⊗ₜ[R] z) : P₂)
w : M
x : N
y : P
z : Q
⊢ Eq.{u_17 + 1} (α := P₂)
    ((((((((LinearMap.compr₂ₛₗ (mk R M N)
                              (LinearMap.compr₂ₛₗ (mk R (M ⊗[R] N) P)
                                (LinearMap.compr₂ₛₗ (mk R (M ⊗[R] N ⊗[R] P) Q) g)) :
                            (a : M) → N →ₛₗ[σ₁₂] P →ₛₗ[σ₁₂] Q →ₛₗ[σ₁₂] P₂)
                          w :
                        N →ₛₗ[σ₁₂] P →ₛₗ[σ₁₂] Q →ₛₗ[σ₁₂] P₂) :
                      (a : N) → P →ₛₗ[σ₁₂] Q →ₛₗ[σ₁₂] P₂)
                    x :
                  P →ₛₗ[σ₁₂] Q →ₛₗ[σ₁₂] P₂) :
                (a : P) → Q →ₛₗ[σ₁₂] P₂)
              y :
            Q →ₛₗ[σ₁₂] P₂) :
          (a : Q) → P₂)
        z :
      P₂)
    ((((((((LinearMap.compr₂ₛₗ (mk R M N)
                              (LinearMap.compr₂ₛₗ (mk R (M ⊗[R] N) P)
                                (LinearMap.compr₂ₛₗ (mk R (M ⊗[R] N ⊗[R] P) Q) h)) :
                            (a : M) → N →ₛₗ[σ₁₂] P →ₛₗ[σ₁₂] Q →ₛₗ[σ₁₂] P₂)
                          w :
                        N →ₛₗ[σ₁₂] P →ₛₗ[σ₁₂] Q →ₛₗ[σ₁₂] P₂) :
                      (a : N) → P →ₛₗ[σ₁₂] Q →ₛₗ[σ₁₂] P₂)
                    x :
                  P →ₛₗ[σ₁₂] Q →ₛₗ[σ₁₂] P₂) :
                (a : P) → Q →ₛₗ[σ₁₂] P₂)
              y :
            Q →ₛₗ[σ₁₂] P₂) :
          (a : Q) → P₂)
        z :
      P₂)

Tactic:
exact H w x y z
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
R₂ : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring R₂
σ₁₂ : R →+* R₂
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
P₂ : Type u_17
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid P
inst_5 : AddCommMonoid Q
inst_6 : AddCommMonoid P₂
inst_7 : Module R M
inst_8 : Module R N
inst_9 : Module R₂ P₂
inst_10 : Module R P
inst_11 : Module R Q
φ ψ : M ⊗[R] N ⊗[R] (P ⊗[R] Q) →ₛₗ[σ₁₂] P₂
H :
  ∀ (w : M) (x : N) (y : P) (z : Q),
    Eq.{u_17 + 1} (α := P₂) ((φ : (a : M ⊗[R] N ⊗[R] (P ⊗[R] Q)) → P₂) (w ⊗ₜ[R] x ⊗ₜ[R] (y ⊗ₜ[R] z)) : P₂)
      ((ψ : (a : M ⊗[R] N ⊗[R] (P ⊗[R] Q)) → P₂) (w ⊗ₜ[R] x ⊗ₜ[R] (y ⊗ₜ[R] z)) : P₂)
H₁ :
  ∀ (m : M) (n : N) (p : P) (q : Q),
    Eq.{u_17 + 1} (α := P₂)
      ((((LinearMap.compr₂ₛₗ (σ₃₄ := σ₁₂) (mk R P Q)
                    ((((LinearMap.compr₂ₛₗ (mk R M N) (LinearMap.compr₂ₛₗ (mk R (M ⊗[R] N) (P ⊗[R] Q)) φ) :
                              (a : M) → N →ₛₗ[σ₁₂] P ⊗[R] Q →ₛₗ[σ₁₂] P₂)
                            m :
                          N →ₛₗ[σ₁₂] P ⊗[R] Q →ₛₗ[σ₁₂] P₂) :
                        (a : N) → P ⊗[R] Q →ₛₗ[σ₁₂] P₂)
                      n) :
                  (a : P) → Q →ₛₗ[σ₁₂] P₂)
                p :
              Q →ₛₗ[σ₁₂] P₂) :
            (a : Q) → P₂)
          q :
        P₂)
      ((((LinearMap.compr₂ₛₗ (σ₃₄ := σ₁₂) (mk R P Q)
                    ((((LinearMap.compr₂ₛₗ (mk R M N) (LinearMap.compr₂ₛₗ (mk R (M ⊗[R] N) (P ⊗[R] Q)) ψ) :
                              (a : M) → N →ₛₗ[σ₁₂] P ⊗[R] Q →ₛₗ[σ₁₂] P₂)
                            m :
                          N →ₛₗ[σ₁₂] P ⊗[R] Q →ₛₗ[σ₁₂] P₂) :
                        (a : N) → P ⊗[R] Q →ₛₗ[σ₁₂] P₂)
                      n) :
                  (a : P) → Q →ₛₗ[σ₁₂] P₂)
                p :
              Q →ₛₗ[σ₁₂] P₂) :
            (a : Q) → P₂)
          q :
        P₂)
⊢ φ = ψ

Tactic:
ext m n p q
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
R₂ : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring R₂
σ₁₂ : R →+* R₂
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
P₂ : Type u_17
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid P
inst_5 : AddCommMonoid Q
inst_6 : AddCommMonoid P₂
inst_7 : Module R M
inst_8 : Module R N
inst_9 : Module R₂ P₂
inst_10 : Module R P
inst_11 : Module R Q
φ ψ : M ⊗[R] N ⊗[R] (P ⊗[R] Q) →ₛₗ[σ₁₂] P₂
H :
  ∀ (w : M) (x : N) (y : P) (z : Q),
    Eq.{u_17 + 1} (α := P₂) ((φ : (a : M ⊗[R] N ⊗[R] (P ⊗[R] Q)) → P₂) (w ⊗ₜ[R] x ⊗ₜ[R] (y ⊗ₜ[R] z)) : P₂)
      ((ψ : (a : M ⊗[R] N ⊗[R] (P ⊗[R] Q)) → P₂) (w ⊗ₜ[R] x ⊗ₜ[R] (y ⊗ₜ[R] z)) : P₂)
m : M
n : N
p : P
q : Q
⊢ Eq.{u_17 + 1} (α := P₂)
    ((((LinearMap.compr₂ₛₗ (σ₃₄ := σ₁₂) (mk R P Q)
                  ((((LinearMap.compr₂ₛₗ (mk R M N) (LinearMap.compr₂ₛₗ (mk R (M ⊗[R] N) (P ⊗[R] Q)) φ) :
                            (a : M) → N →ₛₗ[σ₁₂] P ⊗[R] Q →ₛₗ[σ₁₂] P₂)
                          m :
                        N →ₛₗ[σ₁₂] P ⊗[R] Q →ₛₗ[σ₁₂] P₂) :
                      (a : N) → P ⊗[R] Q →ₛₗ[σ₁₂] P₂)
                    n) :
                (a : P) → Q →ₛₗ[σ₁₂] P₂)
              p :
            Q →ₛₗ[σ₁₂] P₂) :
          (a : Q) → P₂)
        q :
      P₂)
    ((((LinearMap.compr₂ₛₗ (σ₃₄ := σ₁₂) (mk R P Q)
                  ((((LinearMap.compr₂ₛₗ (mk R M N) (LinearMap.compr₂ₛₗ (mk R (M ⊗[R] N) (P ⊗[R] Q)) ψ) :
                            (a : M) → N →ₛₗ[σ₁₂] P ⊗[R] Q →ₛₗ[σ₁₂] P₂)
                          m :
                        N →ₛₗ[σ₁₂] P ⊗[R] Q →ₛₗ[σ₁₂] P₂) :
                      (a : N) → P ⊗[R] Q →ₛₗ[σ₁₂] P₂)
                    n) :
                (a : P) → Q →ₛₗ[σ₁₂] P₂)
              p :
            Q →ₛₗ[σ₁₂] P₂) :
          (a : Q) → P₂)
        q :
      P₂)

Tactic:
H m n p q

Premises used: TensorProduct.tmul, AddCon.toQuotient
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
R₂ : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring R₂
σ₁₂ : R →+* R₂
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
P₂ : Type u_17
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid P
inst_5 : AddCommMonoid Q
inst_6 : AddCommMonoid P₂
inst_7 : Module R M
inst_8 : Module R N
inst_9 : Module R₂ P₂
inst_10 : Module R P
inst_11 : Module R Q
φ ψ : M ⊗[R] N ⊗[R] (P ⊗[R] Q) →ₛₗ[σ₁₂] P₂
H :
  ∀ (w : M) (x : N) (y : P) (z : Q),
    Eq.{u_17 + 1} (α := P₂) ((φ : (a : M ⊗[R] N ⊗[R] (P ⊗[R] Q)) → P₂) (w ⊗ₜ[R] x ⊗ₜ[R] (y ⊗ₜ[R] z)) : P₂)
      ((ψ : (a : M ⊗[R] N ⊗[R] (P ⊗[R] Q)) → P₂) (w ⊗ₜ[R] x ⊗ₜ[R] (y ⊗ₜ[R] z)) : P₂)
m : M
n : N
p : P
q : Q
⊢ Eq.{u_17 + 1} (α := P₂)
    ((((LinearMap.compr₂ₛₗ (σ₃₄ := σ₁₂) (mk R P Q)
                  ((((LinearMap.compr₂ₛₗ (mk R M N) (LinearMap.compr₂ₛₗ (mk R (M ⊗[R] N) (P ⊗[R] Q)) φ) :
                            (a : M) → N →ₛₗ[σ₁₂] P ⊗[R] Q →ₛₗ[σ₁₂] P₂)
                          m :
                        N →ₛₗ[σ₁₂] P ⊗[R] Q →ₛₗ[σ₁₂] P₂) :
                      (a : N) → P ⊗[R] Q →ₛₗ[σ₁₂] P₂)
                    n) :
                (a : P) → Q →ₛₗ[σ₁₂] P₂)
              p :
            Q →ₛₗ[σ₁₂] P₂) :
          (a : Q) → P₂)
        q :
      P₂)
    ((((LinearMap.compr₂ₛₗ (σ₃₄ := σ₁₂) (mk R P Q)
                  ((((LinearMap.compr₂ₛₗ (mk R M N) (LinearMap.compr₂ₛₗ (mk R (M ⊗[R] N) (P ⊗[R] Q)) ψ) :
                            (a : M) → N →ₛₗ[σ₁₂] P ⊗[R] Q →ₛₗ[σ₁₂] P₂)
                          m :
                        N →ₛₗ[σ₁₂] P ⊗[R] Q →ₛₗ[σ₁₂] P₂) :
                      (a : N) → P ⊗[R] Q →ₛₗ[σ₁₂] P₂)
                    n) :
                (a : P) → Q →ₛₗ[σ₁₂] P₂)
              p :
            Q →ₛₗ[σ₁₂] P₂) :
          (a : Q) → P₂)
        q :
      P₂)

Tactic:
exact H m n p q
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
R₂ : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring R₂
σ₁₂ : R →+* R₂
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
P₂ : Type u_17
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid P
inst_5 : AddCommMonoid Q
inst_6 : AddCommMonoid P₂
inst_7 : Module R M
inst_8 : Module R N
inst_9 : Module R₂ P₂
inst_10 : Module R P
inst_11 : Module R Q
φ ψ : M ⊗[R] (N ⊗[R] P) ⊗[R] Q →ₛₗ[σ₁₂] P₂
H :
  ∀ (w : M) (x : N) (y : P) (z : Q),
    Eq.{u_17 + 1} (α := P₂) ((φ : (a : M ⊗[R] (N ⊗[R] P) ⊗[R] Q) → P₂) (w ⊗ₜ[R] (x ⊗ₜ[R] y) ⊗ₜ[R] z) : P₂)
      ((ψ : (a : M ⊗[R] (N ⊗[R] P) ⊗[R] Q) → P₂) (w ⊗ₜ[R] (x ⊗ₜ[R] y) ⊗ₜ[R] z) : P₂)
H₁ :
  ∀ (m : M) (n : N) (p : P) (q : Q),
    Eq.{u_17 + 1} (α := P₂)
      ((((((LinearMap.compr₂ₛₗ (σ₃₄ := σ₁₂) (mk R N P)
                          ((LinearMap.compr₂ₛₗ (mk R M (N ⊗[R] P)) (LinearMap.compr₂ₛₗ (mk R (M ⊗[R] (N ⊗[R] P)) Q) φ) :
                              (a : M) → N ⊗[R] P →ₛₗ[σ₁₂] Q →ₛₗ[σ₁₂] P₂)
                            m) :
                        (a : N) → P →ₛₗ[σ₁₂] Q →ₛₗ[σ₁₂] P₂)
                      n :
                    P →ₛₗ[σ₁₂] Q →ₛₗ[σ₁₂] P₂) :
                  (a : P) → Q →ₛₗ[σ₁₂] P₂)
                p :
              Q →ₛₗ[σ₁₂] P₂) :
            (a : Q) → P₂)
          q :
        P₂)
      ((((((LinearMap.compr₂ₛₗ (σ₃₄ := σ₁₂) (mk R N P)
                          ((LinearMap.compr₂ₛₗ (mk R M (N ⊗[R] P)) (LinearMap.compr₂ₛₗ (mk R (M ⊗[R] (N ⊗[R] P)) Q) ψ) :
                              (a : M) → N ⊗[R] P →ₛₗ[σ₁₂] Q →ₛₗ[σ₁₂] P₂)
                            m) :
                        (a : N) → P →ₛₗ[σ₁₂] Q →ₛₗ[σ₁₂] P₂)
                      n :
                    P →ₛₗ[σ₁₂] Q →ₛₗ[σ₁₂] P₂) :
                  (a : P) → Q →ₛₗ[σ₁₂] P₂)
                p :
              Q →ₛₗ[σ₁₂] P₂) :
            (a : Q) → P₂)
          q :
        P₂)
⊢ φ = ψ

Tactic:
ext m n p q
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
R₂ : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring R₂
σ₁₂ : R →+* R₂
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
P₂ : Type u_17
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid P
inst_5 : AddCommMonoid Q
inst_6 : AddCommMonoid P₂
inst_7 : Module R M
inst_8 : Module R N
inst_9 : Module R₂ P₂
inst_10 : Module R P
inst_11 : Module R Q
φ ψ : M ⊗[R] (N ⊗[R] P) ⊗[R] Q →ₛₗ[σ₁₂] P₂
H :
  ∀ (w : M) (x : N) (y : P) (z : Q),
    Eq.{u_17 + 1} (α := P₂) ((φ : (a : M ⊗[R] (N ⊗[R] P) ⊗[R] Q) → P₂) (w ⊗ₜ[R] (x ⊗ₜ[R] y) ⊗ₜ[R] z) : P₂)
      ((ψ : (a : M ⊗[R] (N ⊗[R] P) ⊗[R] Q) → P₂) (w ⊗ₜ[R] (x ⊗ₜ[R] y) ⊗ₜ[R] z) : P₂)
m : M
n : N
p : P
q : Q
⊢ Eq.{u_17 + 1} (α := P₂)
    ((((((LinearMap.compr₂ₛₗ (σ₃₄ := σ₁₂) (mk R N P)
                        ((LinearMap.compr₂ₛₗ (mk R M (N ⊗[R] P)) (LinearMap.compr₂ₛₗ (mk R (M ⊗[R] (N ⊗[R] P)) Q) φ) :
                            (a : M) → N ⊗[R] P →ₛₗ[σ₁₂] Q →ₛₗ[σ₁₂] P₂)
                          m) :
                      (a : N) → P →ₛₗ[σ₁₂] Q →ₛₗ[σ₁₂] P₂)
                    n :
                  P →ₛₗ[σ₁₂] Q →ₛₗ[σ₁₂] P₂) :
                (a : P) → Q →ₛₗ[σ₁₂] P₂)
              p :
            Q →ₛₗ[σ₁₂] P₂) :
          (a : Q) → P₂)
        q :
      P₂)
    ((((((LinearMap.compr₂ₛₗ (σ₃₄ := σ₁₂) (mk R N P)
                        ((LinearMap.compr₂ₛₗ (mk R M (N ⊗[R] P)) (LinearMap.compr₂ₛₗ (mk R (M ⊗[R] (N ⊗[R] P)) Q) ψ) :
                            (a : M) → N ⊗[R] P →ₛₗ[σ₁₂] Q →ₛₗ[σ₁₂] P₂)
                          m) :
                      (a : N) → P →ₛₗ[σ₁₂] Q →ₛₗ[σ₁₂] P₂)
                    n :
                  P →ₛₗ[σ₁₂] Q →ₛₗ[σ₁₂] P₂) :
                (a : P) → Q →ₛₗ[σ₁₂] P₂)
              p :
            Q →ₛₗ[σ₁₂] P₂) :
          (a : Q) → P₂)
        q :
      P₂)

Tactic:
H m n p q

Premises used: TensorProduct.tmul, AddCon.toQuotient
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
R₂ : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring R₂
σ₁₂ : R →+* R₂
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
P₂ : Type u_17
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid P
inst_5 : AddCommMonoid Q
inst_6 : AddCommMonoid P₂
inst_7 : Module R M
inst_8 : Module R N
inst_9 : Module R₂ P₂
inst_10 : Module R P
inst_11 : Module R Q
φ ψ : M ⊗[R] (N ⊗[R] P) ⊗[R] Q →ₛₗ[σ₁₂] P₂
H :
  ∀ (w : M) (x : N) (y : P) (z : Q),
    Eq.{u_17 + 1} (α := P₂) ((φ : (a : M ⊗[R] (N ⊗[R] P) ⊗[R] Q) → P₂) (w ⊗ₜ[R] (x ⊗ₜ[R] y) ⊗ₜ[R] z) : P₂)
      ((ψ : (a : M ⊗[R] (N ⊗[R] P) ⊗[R] Q) → P₂) (w ⊗ₜ[R] (x ⊗ₜ[R] y) ⊗ₜ[R] z) : P₂)
m : M
n : N
p : P
q : Q
⊢ Eq.{u_17 + 1} (α := P₂)
    ((((((LinearMap.compr₂ₛₗ (σ₃₄ := σ₁₂) (mk R N P)
                        ((LinearMap.compr₂ₛₗ (mk R M (N ⊗[R] P)) (LinearMap.compr₂ₛₗ (mk R (M ⊗[R] (N ⊗[R] P)) Q) φ) :
                            (a : M) → N ⊗[R] P →ₛₗ[σ₁₂] Q →ₛₗ[σ₁₂] P₂)
                          m) :
                      (a : N) → P →ₛₗ[σ₁₂] Q →ₛₗ[σ₁₂] P₂)
                    n :
                  P →ₛₗ[σ₁₂] Q →ₛₗ[σ₁₂] P₂) :
                (a : P) → Q →ₛₗ[σ₁₂] P₂)
              p :
            Q →ₛₗ[σ₁₂] P₂) :
          (a : Q) → P₂)
        q :
      P₂)
    ((((((LinearMap.compr₂ₛₗ (σ₃₄ := σ₁₂) (mk R N P)
                        ((LinearMap.compr₂ₛₗ (mk R M (N ⊗[R] P)) (LinearMap.compr₂ₛₗ (mk R (M ⊗[R] (N ⊗[R] P)) Q) ψ) :
                            (a : M) → N ⊗[R] P →ₛₗ[σ₁₂] Q →ₛₗ[σ₁₂] P₂)
                          m) :
                      (a : N) → P →ₛₗ[σ₁₂] Q →ₛₗ[σ₁₂] P₂)
                    n :
                  P →ₛₗ[σ₁₂] Q →ₛₗ[σ₁₂] P₂) :
                (a : P) → Q →ₛₗ[σ₁₂] P₂)
              p :
            Q →ₛₗ[σ₁₂] P₂) :
          (a : Q) → P₂)
        q :
      P₂)

Tactic:
exact H m n p q
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
m : M
n : N
⊢ Eq (α := N ⊗[R] M) ((TensorProduct.comm R M N : (a : M ⊗[R] N) → N ⊗[R] M) (m ⊗ₜ[R] n) : N ⊗[R] M)
    (n ⊗ₜ[R] m : N ⊗[R] M)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
⊢ Eq (α := N ⊗[R] M ≃ₗ[R] M ⊗[R] N) (LinearEquiv.symm (TensorProduct.comm R M N)) (TensorProduct.comm R N M)

Tactic:
rfl

Premises used: LinearEquiv.symm, TensorProduct.comm, Quotient.liftOn', AddCon.liftOn, LinearEquiv.ofLinear, TensorProduct, TensorProduct.lift, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
m : M
n : N
⊢ Eq (α := M ⊗[R] N) ((LinearEquiv.symm (TensorProduct.comm R M N) : (a : N ⊗[R] M) → M ⊗[R] N) (n ⊗ₜ[R] m) : M ⊗[R] N)
    (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.Basic
Goal:
R : Type u_1
R₂ : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring R₂
σ₁₂ : R →+* R₂
M : Type u_7
N : Type u_8
P₂ : Type u_17
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid P₂
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R₂ P₂
f : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂
⊢ lift f ∘ₛₗ (↑(TensorProduct.comm R N M) : N ⊗[R] M →ₗ[R] M ⊗[R] N) = lift f.flip

Tactic:
ext rfl

Premises used: TensorProduct.ext, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
a :
  Eq (α := N ⊗[R] M →ₗ[R] N ⊗[R] M) (↑(TensorProduct.comm R N M ≪≫ₗ TensorProduct.comm R M N) : N ⊗[R] M →ₗ[R] N ⊗[R] M)
    (↑(LinearEquiv.refl R (N ⊗[R] M)) : N ⊗[R] M →ₗ[R] N ⊗[R] M)
⊢ Eq (α := N ⊗[R] M ≃ₗ[R] N ⊗[R] M) (TensorProduct.comm R N M ≪≫ₗ TensorProduct.comm R M N)
    (LinearEquiv.refl R (N ⊗[R] M))

Tactic:
apply LinearEquiv.toLinearMap_injective

Premises used: LinearEquiv.toLinearMap_injective
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
a :
  ∀ (x : N) (x_1 : M),
    Eq (α := N ⊗[R] M)
      ((((LinearMap.compr₂ₛₗ (mk R N M)
                    (↑(TensorProduct.comm R N M ≪≫ₗ TensorProduct.comm R M N) : N ⊗[R] M →ₗ[R] N ⊗[R] M) :
                  (a : N) → M →ₗ[R] N ⊗[R] M)
                x :
              M →ₗ[R] N ⊗[R] M) :
            (a : M) → N ⊗[R] M)
          x_1 :
        N ⊗[R] M)
      ((((LinearMap.compr₂ₛₗ (mk R N M) (↑(LinearEquiv.refl R (N ⊗[R] M)) : N ⊗[R] M →ₗ[R] N ⊗[R] M) :
                  (a : N) → M →ₗ[R] N ⊗[R] M)
                x :
              M →ₗ[R] N ⊗[R] M) :
            (a : M) → N ⊗[R] M)
          x_1 :
        N ⊗[R] M)
⊢ Eq (α := N ⊗[R] M →ₗ[R] N ⊗[R] M) (↑(TensorProduct.comm R N M ≪≫ₗ TensorProduct.comm R M N) : N ⊗[R] M →ₗ[R] N ⊗[R] M)
    (↑(LinearEquiv.refl R (N ⊗[R] M)) : N ⊗[R] M →ₗ[R] N ⊗[R] M)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x : N
x_1 : M
⊢ Eq (α := N ⊗[R] M)
    ((((LinearMap.compr₂ₛₗ (mk R N M)
                  (↑(TensorProduct.comm R N M ≪≫ₗ TensorProduct.comm R M N) : N ⊗[R] M →ₗ[R] N ⊗[R] M) :
                (a : N) → M →ₗ[R] N ⊗[R] M)
              x :
            M →ₗ[R] N ⊗[R] M) :
          (a : M) → N ⊗[R] M)
        x_1 :
      N ⊗[R] M)
    ((((LinearMap.compr₂ₛₗ (mk R N M) (↑(LinearEquiv.refl R (N ⊗[R] M)) : N ⊗[R] M →ₗ[R] N ⊗[R] M) :
                (a : N) → M →ₗ[R] N ⊗[R] M)
              x :
            M →ₗ[R] N ⊗[R] M) :
          (a : M) → N ⊗[R] M)
        x_1 :
      N ⊗[R] M)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
⊢ Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] N)
    ((↑(TensorProduct.comm R N M) : N ⊗[R] M →ₗ[R] M ⊗[R] N) ∘ₗ (↑(TensorProduct.comm R M N) : M ⊗[R] N →ₗ[R] N ⊗[R] M))
    LinearMap.id

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : P →ₗ[R] M ⊗[R] N
rw :
  ((↑(TensorProduct.comm R N M) : N ⊗[R] M →ₗ[R] M ⊗[R] N) ∘ₗ
        (↑(TensorProduct.comm R M N) : M ⊗[R] N →ₗ[R] N ⊗[R] M)) ∘ₗ
      f =
    f
rw₁ : LinearMap.id ∘ₗ f = f
rw₂ rw₃ : f = f
⊢ (↑(TensorProduct.comm R N M) : N ⊗[R] M →ₗ[R] M ⊗[R] N) ∘ₗ
      (↑(TensorProduct.comm R M N) : M ⊗[R] N →ₗ[R] N ⊗[R] M) ∘ₗ f =
    f

Tactic:
rw [← LinearMap.comp_assoc, comm_comp_comm, LinearMap.id_comp]

Premises used: LinearMap.comp_assoc, TensorProduct.comm_comp_comm, LinearMap.id_comp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x : N ⊗[R] M
⊢ (TensorProduct.comm R M N : (a : M ⊗[R] N) → N ⊗[R] M) ((TensorProduct.comm R N M : (a : N ⊗[R] M) → M ⊗[R] N) x) = x

Tactic:
congr($(comm_trans_comm _ _ _) x)

Premises used: congrArg, id, TensorProduct.comm_trans_comm, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : Monoid R'
inst_4 : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A_1 : Type u_6
M_1 : Type u_7
N_1 : Type u_8
P : Type u_9
Q : Type u_10
S_1 : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst_5 : AddCommMonoid M_1
inst_6 : AddCommMonoid N_1
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S_1
inst_10 : AddCommMonoid P'
inst_11 : AddCommMonoid Q'
inst_12 : AddCommMonoid M₂
inst_13 : AddCommMonoid N₂
inst_14 : AddCommMonoid P₂
inst_15 : AddCommMonoid Q₂
inst_16 : AddCommMonoid M₃
inst_17 : AddCommMonoid N₃
inst_18 : AddCommMonoid P₃
inst_19 : AddCommMonoid Q₃
inst_20 : DistribMulAction R' M_1
inst_21 : Module R'' M_1
inst_22 : Module R M_1
inst_23 : Module R N_1
inst_24 : Module R S_1
inst_25 : Module R P'
inst_26 : Module R Q'
inst_27 : Module R₂ M₂
inst_28 : Module R₂ N₂
inst_29 : Module R₂ P₂
inst_30 : Module R₂ Q₂
inst_31 : Module R₃ M₃
inst_32 : Module R₃ N₃
inst_33 : Module R₃ P₃
inst_34 : Module R₃ Q₃
inst_35 : Module R P
inst_36 : Module R Q
A : Type u_22
S : Type u_23
M : Type u_24
N : Type u_25
inst_37 : AddCommMonoid M
inst_38 : AddCommMonoid N
inst_39 : Module R M
inst_40 : Module R N
inst_41 : CommSemiring A
inst_42 : Module A M
inst_43 : Module A N
inst_44 : SMulCommClass R A M
inst_45 : CommSemiring S
inst_46 : Module S M
inst_47 : SMulCommClass R S M
inst_48 : SMulCommClass A S M
inst_49 : CompatibleSMul R A M N
x x_1 : M
⊢ ∀ (x_2 : N),
    Eq (α := M ⊗[R] N)
      ((let __spread.0 : N →ₗ[R] M ⊗[R] N := (mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) (x + x_1);
            { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ } :
            (a : N) → M ⊗[R] N)
          x_2 :
        M ⊗[R] N)
      ((HAdd.hAdd (α := N →ₗ[A] M ⊗[R] N)
              (let __spread.0 : N →ₗ[R] M ⊗[R] N := (mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) x;
              { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ : N →ₗ[A] M ⊗[R] N })
              (let __spread.0 : N →ₗ[R] M ⊗[R] N := (mk R M N : (a : M) → N →ₗ[R] M ⊗[R] N) x_1;
              { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ : N →ₗ[A] M ⊗[R] N }) :
            (a : N) → M ⊗[R] N)
          x_2 :
        M ⊗[R] N)

Tactic:
simp