awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
Q : Type u_10
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
f : M →ₗ[R] N →ₗ[R] P
g : P →ₗ[R] Q
x : M
x_1 : N
⊢ Eq.{u_10 + 1} (α := Q) ((g ∘ₗ lift f : (a : M ⊗[R] N) → Q) (x ⊗ₜ[R] x_1) : Q)
    ((((f.compr₂ g : (a : M) → N →ₗ[R] Q) x : N →ₗ[R] Q) : (a : N) → Q) x_1 : Q)

Tactic:
simp
-- 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₂
g : M ⊗[R] N →ₛₗ[σ₁₂] P₂
rw : g ∘ₛₗ lift (mk R M N) = g
rw₁ : g ∘ₛₗ LinearMap.id = g
rw₂ rw₃ : g = g
⊢ lift (LinearMap.compr₂ₛₗ (mk R M N) g) = g

Tactic:
rw [lift_compr₂ₛₗ g, lift_mk, LinearMap.comp_id]

Premises used: TensorProduct.lift_compr₂ₛₗ, TensorProduct.lift_mk, LinearMap.comp_id
-- 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 : M ⊗[R] N →ₗ[R] P
rw : f ∘ₗ lift (mk R M N) = f
rw₁ : f ∘ₗ LinearMap.id = f
rw₂ rw₃ : f = f
⊢ lift (LinearMap.compr₂ (mk R M N) f) = f

Tactic:
rw [lift_compr₂ f, lift_mk, LinearMap.comp_id]

Premises used: TensorProduct.lift_mk, LinearMap.comp_id, TensorProduct.lift_compr₂
-- 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₂
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
rw₂ rw₃ : h = h
⊢ g = h

Tactic:
rw [← lift_mk_compr₂ₛₗ g, H, lift_mk_compr₂ₛₗ]

Premises used: TensorProduct.lift_mk_compr₂ₛₗ
-- 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 : 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₂
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₂)
⊢ lift (f + g) = lift f + lift g

Tactic:
ext
-- 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 : 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₂
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:
rfl
-- 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 : 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₂
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₂)
⊢ lift (x • x_1) = HSMul.hSMul (α := R₂) ((RingHom.id R₂ : (a : R₂) → R₂) x : R₂) (lift x_1)

Tactic:
ext
-- 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 : 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₂
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:
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₂
m : M
n : N
⊢ Eq.{u_17 + 1} (α := P₂)
    ((((uncurry σ₁₂ M N P₂ : (a : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂) → M ⊗[R] N →ₛₗ[σ₁₂] P₂) f : M ⊗[R] N →ₛₗ[σ₁₂] P₂) :
          (a : M ⊗[R] N) → P₂)
        (m ⊗ₜ[R] n) :
      P₂)
    ((((f : (a : M) → N →ₛₗ[σ₁₂] P₂) m : N →ₛₗ[σ₁₂] P₂) : (a : N) → P₂) n : P₂)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, 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₂
m : M
n : N
⊢ Eq.{u_17 + 1} (α := P₂)
    ((((equiv σ₁₂ M N P₂ : (a : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂) → M ⊗[R] N →ₛₗ[σ₁₂] P₂) f : M ⊗[R] N →ₛₗ[σ₁₂] P₂) :
          (a : M ⊗[R] N) → P₂)
        (m ⊗ₜ[R] n) :
      P₂)
    ((((f : (a : M) → N →ₛₗ[σ₁₂] P₂) m : N →ₛₗ[σ₁₂] P₂) : (a : N) → P₂) n : P₂)

Tactic:
uncurry_apply f m n

Premises used: TensorProduct.uncurry_apply
-- 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 ⊗[R] N →ₛₗ[σ₁₂] P₂
m : M
n : N
⊢ Eq.{u_17 + 1} (α := P₂)
    ((((((LinearEquiv.symm (equiv σ₁₂ M N P₂) : (a : M ⊗[R] N →ₛₗ[σ₁₂] P₂) → M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂) f :
                  M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂) :
                (a : M) → N →ₛₗ[σ₁₂] P₂)
              m :
            N →ₛₗ[σ₁₂] P₂) :
          (a : N) → P₂)
        n :
      P₂)
    ((f : (a : M ⊗[R] N) → P₂) (m ⊗ₜ[R] n) : P₂)

Tactic:
rfl

Premises used: TensorProduct.tmul, AddCon.toQuotient, 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 ⊗[R] N →ₛₗ[σ₁₂] P₂
m : M
n : N
⊢ Eq.{u_17 + 1} (α := P₂)
    ((((((lcurry σ₁₂ M N P₂ : (a : M ⊗[R] N →ₛₗ[σ₁₂] P₂) → M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂) f : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂) :
                (a : M) → N →ₛₗ[σ₁₂] P₂)
              m :
            N →ₛₗ[σ₁₂] P₂) :
          (a : N) → P₂)
        n :
      P₂)
    ((f : (a : M ⊗[R] N) → P₂) (m ⊗ₜ[R] n) : P₂)

Tactic:
rfl

Premises used: TensorProduct.tmul, AddCon.toQuotient, 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 ⊗[R] N →ₛₗ[σ₁₂] P₂
m : M
n : N
⊢ Eq.{u_17 + 1} (α := P₂) ((((curry f : (a : M) → N →ₛₗ[σ₁₂] P₂) m : N →ₛₗ[σ₁₂] P₂) : (a : N) → P₂) n : P₂)
    ((f : (a : M ⊗[R] N) → P₂) (m ⊗ₜ[R] n) : P₂)

Tactic:
rfl

Premises used: TensorProduct.tmul, AddCon.toQuotient, 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₂
⊢ Function.Injective (α := M ⊗[R] N →ₛₗ[σ₁₂] P₂) curry

Tactic:
fun _ _ H => ext H

Premises used: Function.Injective, TensorProduct.ext
-- 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
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₂)
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₂)
⊢ g = h

Tactic:
ext 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
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₂)
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:
H 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
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₂)
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:
exact H 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
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₂)
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₂)
⊢ g = h

Tactic:
ext 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
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₂)
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:
H 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
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₂)
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:
exact H 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
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₂)
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₂)
⊢ g = h

Tactic:
ext w x y z