awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
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₂
g : M ⊗[R] N →ₛₗ[σ₁₂] P₂
H :
  ∀ (x : M) (y : N),
    Eq.{u_17 + 1} (α := P₂) ((g : (a : M ⊗[R] N) → P₂) (x ⊗ₜ[R] y) : P₂)
      ((((f' : (a : M) → N →ₛₗ[σ₁₂] P₂) x : N →ₛₗ[σ₁₂] P₂) : (a : N) → P₂) y : P₂)
m : M
n : N
⊢ Eq.{u_17 + 1} (α := P₂) ((g : (a : M ⊗[R] N) → P₂) (m ⊗ₜ[R] n) : P₂)
    ((lift f' : (a : M ⊗[R] N) → P₂) (m ⊗ₜ[R] n) : P₂)
have rw : Eq.{u_17 + 1} (α := P₂) ((((f' : (a : M) → N →ₛₗ[σ₁₂] P₂) m : N →ₛₗ[σ₁₂] P₂) : (a : N) → P₂) n : P₂)
  ((lift f' : (a : M ⊗[R] N) → P₂) (m ⊗ₜ[R] n) : P₂)
Tactic: rw [H, lift.tmul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
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₂
g : M ⊗[R] N →ₛₗ[σ₁₂] P₂
H :
  ∀ (x : M) (y : N),
    Eq.{u_17 + 1} (α := P₂) ((g : (a : M ⊗[R] N) → P₂) (x ⊗ₜ[R] y) : P₂)
      ((((f' : (a : M) → N →ₛₗ[σ₁₂] P₂) x : N →ₛₗ[σ₁₂] P₂) : (a : N) → P₂) y : P₂)
m : M
n : N
rw :
  Eq.{u_17 + 1} (α := P₂) ((((f' : (a : M) → N →ₛₗ[σ₁₂] P₂) m : N →ₛₗ[σ₁₂] P₂) : (a : N) → P₂) n : P₂)
    ((lift f' : (a : M ⊗[R] N) → P₂) (m ⊗ₜ[R] n) : P₂)
⊢ Eq.{u_17 + 1} (α := P₂) ((g : (a : M ⊗[R] N) → P₂) (m ⊗ₜ[R] n) : P₂)
    ((lift f' : (a : M ⊗[R] N) → P₂) (m ⊗ₜ[R] n) : P₂)
have rw₁ : Eq.{u_17 + 1} (α := P₂) ((((f' : (a : M) → N →ₛₗ[σ₁₂] P₂) m : N →ₛₗ[σ₁₂] P₂) : (a : N) → P₂) n : P₂)
  ((((f' : (a : M) → N →ₛₗ[σ₁₂] P₂) m : N →ₛₗ[σ₁₂] P₂) : (a : N) → P₂) n : P₂)
Tactic: rw [H, lift.tmul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
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₂
g : M ⊗[R] N →ₛₗ[σ₁₂] P₂
⊢ lift (LinearMap.compr₂ₛₗ (mk R M N) g) = g
have rw : g ∘ₛₗ lift (mk R M N) = g
Tactic: rw [lift_compr₂ₛₗ g, lift_mk, LinearMap.comp_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
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₂
g : M ⊗[R] N →ₛₗ[σ₁₂] P₂
rw : g ∘ₛₗ lift (mk R M N) = g
⊢ lift (LinearMap.compr₂ₛₗ (mk R M N) g) = g
have rw₁ : g ∘ₛₗ LinearMap.id = g
Tactic: rw [lift_compr₂ₛₗ g, lift_mk, LinearMap.comp_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
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₂
g : M ⊗[R] N →ₛₗ[σ₁₂] P₂
rw : g ∘ₛₗ lift (mk R M N) = g
rw₁ : g ∘ₛₗ LinearMap.id = g
⊢ lift (LinearMap.compr₂ₛₗ (mk R M N) g) = g
have rw₂ : g = g
Tactic: rw [lift_compr₂ₛₗ g, lift_mk, LinearMap.comp_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
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 : M ⊗[R] N →ₗ[R] P
⊢ lift (LinearMap.compr₂ (mk R M N) f) = f
have rw : f ∘ₗ lift (mk R M N) = f
Tactic: rw [lift_compr₂ f, lift_mk, LinearMap.comp_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
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 : M ⊗[R] N →ₗ[R] P
rw : f ∘ₗ lift (mk R M N) = f
⊢ lift (LinearMap.compr₂ (mk R M N) f) = f
have rw₁ : f ∘ₗ LinearMap.id = f
Tactic: rw [lift_compr₂ f, lift_mk, LinearMap.comp_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
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 : M ⊗[R] N →ₗ[R] P
rw : f ∘ₗ lift (mk R M N) = f
rw₁ : f ∘ₗ LinearMap.id = f
⊢ lift (LinearMap.compr₂ (mk R M N) f) = f
have rw₂ : f = f
Tactic: rw [lift_compr₂ f, lift_mk, LinearMap.comp_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
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₂
g h : M ⊗[R] N →ₛₗ[σ₁₂] P₂
H : LinearMap.compr₂ₛₗ (mk R M N) g = LinearMap.compr₂ₛₗ (mk R M N) h
⊢ g = h
have rw : lift (LinearMap.compr₂ₛₗ (mk R M N) g) = h
Tactic: rw [← lift_mk_compr₂ₛₗ g, H, lift_mk_compr₂ₛₗ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
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₂
g h : M ⊗[R] N →ₛₗ[σ₁₂] P₂
H : LinearMap.compr₂ₛₗ (mk R M N) g = LinearMap.compr₂ₛₗ (mk R M N) h
rw : lift (LinearMap.compr₂ₛₗ (mk R M N) g) = h
⊢ g = h
have rw₁ : lift (LinearMap.compr₂ₛₗ (mk R M N) h) = h
Tactic: rw [← lift_mk_compr₂ₛₗ g, H, lift_mk_compr₂ₛₗ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
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₂
g h : M ⊗[R] N →ₛₗ[σ₁₂] P₂
H : LinearMap.compr₂ₛₗ (mk R M N) g = LinearMap.compr₂ₛₗ (mk R M N) h
rw : lift (LinearMap.compr₂ₛₗ (mk R M N) g) = h
rw₁ : lift (LinearMap.compr₂ₛₗ (mk R M N) h) = h
⊢ g = h
have rw₂ : h = h
Tactic: rw [← lift_mk_compr₂ₛₗ g, H, lift_mk_compr₂ₛₗ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
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 : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : 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
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S
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
inst_21 : Module R'' M
inst_22 : Module R M
inst_23 : Module R N
inst_24 : Module R S
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
f_1 : M →ₗ[R] N →ₗ[R] P
f' f g : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂
⊢ lift (f + g) = lift f + lift g
have H : ∀ (x : M) (x_1 : N),
  Eq.{u_17 + 1} (α := P₂)
    ((((LinearMap.compr₂ₛₗ (mk R M N) (lift (f + g)) : (a : M) → N →ₛₗ[σ₁₂] P₂) x : N →ₛₗ[σ₁₂] P₂) : (a : N) → P₂) x_1 :
      P₂)
    ((((LinearMap.compr₂ₛₗ (mk R M N) (lift f + lift g) : (a : M) → N →ₛₗ[σ₁₂] P₂) x : N →ₛₗ[σ₁₂] P₂) : (a : N) → P₂)
        x_1 :
      P₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
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 : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : 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
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S
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
inst_21 : Module R'' M
inst_22 : Module R M
inst_23 : Module R N
inst_24 : Module R S
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
f : M →ₗ[R] N →ₗ[R] P
f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂
x : R₂
x_1 : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂
⊢ lift (x • x_1) = HSMul.hSMul (α := R₂) ((RingHom.id R₂ : (a : R₂) → R₂) x : R₂) (lift x_1)
have H : ∀ (x_2 : M) (x_3 : N),
  Eq.{u_17 + 1} (α := P₂)
    ((((LinearMap.compr₂ₛₗ (mk R M N) (lift (x • x_1)) : (a : M) → N →ₛₗ[σ₁₂] P₂) x_2 : N →ₛₗ[σ₁₂] P₂) : (a : N) → P₂)
        x_3 :
      P₂)
    ((((LinearMap.compr₂ₛₗ (mk R M N) (HSMul.hSMul (α := R₂) ((RingHom.id R₂ : (a : R₂) → R₂) x : R₂) (lift x_1)) :
                (a : M) → N →ₛₗ[σ₁₂] P₂)
              x_2 :
            N →ₛₗ[σ₁₂] P₂) :
          (a : N) → P₂)
        x_3 :
      P₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
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
P₂ : Type u_17
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid P
inst_5 : AddCommMonoid P₂
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R₂ P₂
inst_9 : Module R P
g h : M ⊗[R] N ⊗[R] P →ₛₗ[σ₁₂] P₂
H :
  ∀ (x : M) (y : N) (z : P),
    Eq.{u_17 + 1} (α := P₂) ((g : (a : M ⊗[R] N ⊗[R] P) → P₂) (x ⊗ₜ[R] y ⊗ₜ[R] z) : P₂)
      ((h : (a : M ⊗[R] N ⊗[R] P) → P₂) (x ⊗ₜ[R] y ⊗ₜ[R] z) : P₂)
⊢ g = h
have H₁ : ∀ (x : M) (y : N) (z : P),
  Eq.{u_17 + 1} (α := P₂)
    ((((((LinearMap.compr₂ₛₗ (mk R M N) (LinearMap.compr₂ₛₗ (mk R (M ⊗[R] N) P) g) : (a : M) → N →ₛₗ[σ₁₂] P →ₛₗ[σ₁₂] P₂)
                    x :
                  N →ₛₗ[σ₁₂] P →ₛₗ[σ₁₂] P₂) :
                (a : N) → P →ₛₗ[σ₁₂] P₂)
              y :
            P →ₛₗ[σ₁₂] P₂) :
          (a : P) → P₂)
        z :
      P₂)
    ((((((LinearMap.compr₂ₛₗ (mk R M N) (LinearMap.compr₂ₛₗ (mk R (M ⊗[R] N) P) h) : (a : M) → N →ₛₗ[σ₁₂] P →ₛₗ[σ₁₂] P₂)
                    x :
                  N →ₛₗ[σ₁₂] P →ₛₗ[σ₁₂] P₂) :
                (a : N) → P →ₛₗ[σ₁₂] P₂)
              y :
            P →ₛₗ[σ₁₂] P₂) :
          (a : P) → P₂)
        z :
      P₂)
Tactic: ext x y z
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
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
P₂ : Type u_17
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid P
inst_5 : AddCommMonoid P₂
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R₂ P₂
inst_9 : Module R P
g h : M ⊗[R] (N ⊗[R] P) →ₛₗ[σ₁₂] P₂
H :
  ∀ (x : M) (y : N) (z : P),
    Eq.{u_17 + 1} (α := P₂) ((g : (a : M ⊗[R] (N ⊗[R] P)) → P₂) (x ⊗ₜ[R] (y ⊗ₜ[R] z)) : P₂)
      ((h : (a : M ⊗[R] (N ⊗[R] P)) → P₂) (x ⊗ₜ[R] (y ⊗ₜ[R] z)) : P₂)
⊢ g = h
have H₁ : ∀ (x : M) (y : N) (z : P),
  Eq.{u_17 + 1} (α := P₂)
    ((((LinearMap.compr₂ₛₗ (σ₃₄ := σ₁₂) (mk R N P)
                  ((LinearMap.compr₂ₛₗ (mk R M (N ⊗[R] P)) g : (a : M) → N ⊗[R] P →ₛₗ[σ₁₂] P₂) x) :
                (a : N) → P →ₛₗ[σ₁₂] P₂)
              y :
            P →ₛₗ[σ₁₂] P₂) :
          (a : P) → P₂)
        z :
      P₂)
    ((((LinearMap.compr₂ₛₗ (σ₃₄ := σ₁₂) (mk R N P)
                  ((LinearMap.compr₂ₛₗ (mk R M (N ⊗[R] P)) h : (a : M) → N ⊗[R] P →ₛₗ[σ₁₂] P₂) x) :
                (a : N) → P →ₛₗ[σ₁₂] P₂)
              y :
            P →ₛₗ[σ₁₂] P₂) :
          (a : P) → P₂)
        z :
      P₂)
Tactic: ext x y z
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
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₂)
⊢ g = h
have H₁ : ∀ (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: ext w x y z
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
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₂)
⊢ φ = ψ
have 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
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₂)
⊢ φ = ψ
have 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
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] N ⊗[R] M) (TensorProduct.comm R N M ≪≫ₗ TensorProduct.comm R M N)
    (LinearEquiv.refl R (N ⊗[R] M))
have 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)
Tactic: apply LinearEquiv.toLinearMap_injective
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
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] 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
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
⊢ (↑(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
have 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
Tactic: rw [← LinearMap.comp_assoc, comm_comp_comm, LinearMap.id_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
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
⊢ (↑(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
have rw₁ : LinearMap.id ∘ₗ f = f
Tactic: rw [← LinearMap.comp_assoc, comm_comp_comm, LinearMap.id_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
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
⊢ (↑(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
have rw₂ : f = f
Tactic: rw [← LinearMap.comp_assoc, comm_comp_comm, LinearMap.id_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
inst_1 : AddCommGroup M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x_1 : M ⊗[R] N
x : M
y : N
⊢ HAdd.hAdd (α := M ⊗[R] N) (-x ⊗ₜ[R] y) (x ⊗ₜ[R] y) = 0
have h : Eq (α := M ⊗[R] N) 0 ((-x + x) ⊗ₜ[R] y)
Tactic: convert! (add_tmul (R := R) (-x) x y).symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
inst_1 : AddCommGroup M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x_1 : M ⊗[R] N
x : M
y : N
⊢ Eq (α := M ⊗[R] N) 0 ((-x + x) ⊗ₜ[R] y)
have h : Eq (α := M ⊗[R] N) 0 (0 ⊗ₜ[R] y)
Tactic: rw [neg_add_cancel, zero_tmul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
inst_1 : AddCommGroup M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x_1 : M ⊗[R] N
x : M
y : N
h : Eq (α := M ⊗[R] N) 0 (0 ⊗ₜ[R] y)
⊢ Eq (α := M ⊗[R] N) 0 ((-x + x) ⊗ₜ[R] y)
have h₁ : Eq (α := M ⊗[R] N) 0 0
Tactic: rw [neg_add_cancel, zero_tmul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
N : Type u_3
inst_1 : AddCommGroup M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x_1 x y : M ⊗[R] N
hx : -x + x = 0
hy : -y + y = 0
this : -x + x + (-y + y) = 0
⊢ -(x + y) + (x + y) = 0
have rw : -(x + y) + (x + y) = -x + x + (-y + y)
Tactic: rw [← this]