awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
g : P →ₗ[R] Q
f_1 : N →ₗ[R] P
r : R
f : N →ₗ[R] P
H :
  ∀ (x : M) (y : N),
    Eq (α := M ⊗[R] P)
      ((((compr₂ₛₗ (TensorProduct.mk R M N) (lTensor M (r • f)) : (a : M) → N →ₗ[R] M ⊗[R] P) x : N →ₗ[R] M ⊗[R] P) :
            (a : N) → M ⊗[R] P)
          y :
        M ⊗[R] P)
      ((((compr₂ₛₗ (TensorProduct.mk R M N) (HSMul.hSMul (β := M ⊗[R] N →ₗ[R] M ⊗[R] P) r (lTensor M f)) :
                  (a : M) → N →ₗ[R] M ⊗[R] P)
                x :
              N →ₗ[R] M ⊗[R] P) :
            (a : N) → M ⊗[R] P)
          y :
        M ⊗[R] P)
⊢ lTensor M (r • f) = HSMul.hSMul (β := M ⊗[R] N →ₗ[R] M ⊗[R] P) r (lTensor M f)

Tactic:
ext x y
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
g : P →ₗ[R] Q
f_1 : N →ₗ[R] P
r : R
f : N →ₗ[R] P
x : M
y : N
⊢ Eq (α := M ⊗[R] P)
    ((((compr₂ₛₗ (TensorProduct.mk R M N) (lTensor M (r • f)) : (a : M) → N →ₗ[R] M ⊗[R] P) x : N →ₗ[R] M ⊗[R] P) :
          (a : N) → M ⊗[R] P)
        y :
      M ⊗[R] P)
    ((((compr₂ₛₗ (TensorProduct.mk R M N) (HSMul.hSMul (β := M ⊗[R] N →ₗ[R] M ⊗[R] P) r (lTensor M f)) :
                (a : M) → N →ₗ[R] M ⊗[R] P)
              x :
            N →ₗ[R] M ⊗[R] P) :
          (a : N) → M ⊗[R] P)
        y :
      M ⊗[R] P)

Tactic:
simp only [compr₂ₛₗ_apply, mk_apply, tmul_smul, smul_apply, lTensor_tmul]

Premises used: LinearMap.smul_apply, TensorProduct.mk_apply, TensorProduct.tmul_smul, LinearMap.compr₂ₛₗ_apply, LinearMap.lTensor_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
g_1 : P →ₗ[R] Q
f_1 f g : N →ₗ[R] P
H :
  ∀ (x : N) (y : M),
    Eq (α := P ⊗[R] M)
      ((((compr₂ₛₗ (TensorProduct.mk R N M) (rTensor M (f + g)) : (a : N) → M →ₗ[R] P ⊗[R] M) x : M →ₗ[R] P ⊗[R] M) :
            (a : M) → P ⊗[R] M)
          y :
        P ⊗[R] M)
      ((((compr₂ₛₗ (TensorProduct.mk R N M) (HAdd.hAdd (α := N ⊗[R] M →ₗ[R] P ⊗[R] M) (rTensor M f) (rTensor M g)) :
                  (a : N) → M →ₗ[R] P ⊗[R] M)
                x :
              M →ₗ[R] P ⊗[R] M) :
            (a : M) → P ⊗[R] M)
          y :
        P ⊗[R] M)
⊢ rTensor M (f + g) = HAdd.hAdd (α := N ⊗[R] M →ₗ[R] P ⊗[R] M) (rTensor M f) (rTensor M g)

Tactic:
ext x y
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
g_1 : P →ₗ[R] Q
f_1 f g : N →ₗ[R] P
x : N
y : M
⊢ Eq (α := P ⊗[R] M)
    ((((compr₂ₛₗ (TensorProduct.mk R N M) (rTensor M (f + g)) : (a : N) → M →ₗ[R] P ⊗[R] M) x : M →ₗ[R] P ⊗[R] M) :
          (a : M) → P ⊗[R] M)
        y :
      P ⊗[R] M)
    ((((compr₂ₛₗ (TensorProduct.mk R N M) (HAdd.hAdd (α := N ⊗[R] M →ₗ[R] P ⊗[R] M) (rTensor M f) (rTensor M g)) :
                (a : N) → M →ₗ[R] P ⊗[R] M)
              x :
            M →ₗ[R] P ⊗[R] M) :
          (a : M) → P ⊗[R] M)
        y :
      P ⊗[R] M)

Tactic:
simp only [compr₂ₛₗ_apply, mk_apply, add_apply, rTensor_tmul, add_tmul]

Premises used: LinearMap.rTensor_tmul, LinearMap.add_apply, TensorProduct.mk_apply, TensorProduct.add_tmul, LinearMap.compr₂ₛₗ_apply
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
g : P →ₗ[R] Q
f_1 : N →ₗ[R] P
r : R
f : N →ₗ[R] P
dsimp : rTensor M (r • f) = HSMul.hSMul (β := N ⊗[R] M →ₗ[R] P ⊗[R] M) r (rTensor M f)
⊢ rTensor M (r • f) =
    HSMul.hSMul (α := R) (β := N ⊗[R] M →ₗ[R] P ⊗[R] M) ((RingHom.id R : (a : R) → R) r : R) (rTensor M f)

Tactic:
dsimp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
g : P →ₗ[R] Q
f_1 : N →ₗ[R] P
r : R
f : N →ₗ[R] P
H :
  ∀ (x : N) (y : M),
    Eq (α := P ⊗[R] M)
      ((((compr₂ₛₗ (TensorProduct.mk R N M) (rTensor M (r • f)) : (a : N) → M →ₗ[R] P ⊗[R] M) x : M →ₗ[R] P ⊗[R] M) :
            (a : M) → P ⊗[R] M)
          y :
        P ⊗[R] M)
      ((((compr₂ₛₗ (TensorProduct.mk R N M) (HSMul.hSMul (β := N ⊗[R] M →ₗ[R] P ⊗[R] M) r (rTensor M f)) :
                  (a : N) → M →ₗ[R] P ⊗[R] M)
                x :
              M →ₗ[R] P ⊗[R] M) :
            (a : M) → P ⊗[R] M)
          y :
        P ⊗[R] M)
⊢ rTensor M (r • f) = HSMul.hSMul (β := N ⊗[R] M →ₗ[R] P ⊗[R] M) r (rTensor M f)

Tactic:
ext x y
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
g : P →ₗ[R] Q
f_1 : N →ₗ[R] P
r : R
f : N →ₗ[R] P
x : N
y : M
⊢ Eq (α := P ⊗[R] M)
    ((((compr₂ₛₗ (TensorProduct.mk R N M) (rTensor M (r • f)) : (a : N) → M →ₗ[R] P ⊗[R] M) x : M →ₗ[R] P ⊗[R] M) :
          (a : M) → P ⊗[R] M)
        y :
      P ⊗[R] M)
    ((((compr₂ₛₗ (TensorProduct.mk R N M) (HSMul.hSMul (β := N ⊗[R] M →ₗ[R] P ⊗[R] M) r (rTensor M f)) :
                (a : N) → M →ₗ[R] P ⊗[R] M)
              x :
            M →ₗ[R] P ⊗[R] M) :
          (a : M) → P ⊗[R] M)
        y :
      P ⊗[R] M)

Tactic:
simp only [compr₂ₛₗ_apply, mk_apply, smul_tmul, tmul_smul, smul_apply, rTensor_tmul]

Premises used: TensorProduct.smul_tmul, LinearMap.smul_apply, LinearMap.rTensor_tmul, TensorProduct.mk_apply, TensorProduct.tmul_smul, LinearMap.compr₂ₛₗ_apply
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
⊢ Eq (α := (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[R] M ⊗[R] P) (⇑(lTensorHom M) : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[R] M ⊗[R] P)
    (lTensor M)

Tactic:
rfl

Premises used: LinearMap.lTensor, TensorProduct.map, TensorProduct.lift, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
⊢ Eq (α := (a : N →ₗ[R] P) → N ⊗[R] M →ₗ[R] P ⊗[R] M) (⇑(rTensorHom M) : (a : N →ₗ[R] P) → N ⊗[R] M →ₗ[R] P ⊗[R] M)
    (rTensor M)

Tactic:
rfl

Premises used: TensorProduct.map, TensorProduct.lift, rfl, LinearMap.rTensor
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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 g : N →ₗ[R] P
⊢ lTensor M (f + g) = HAdd.hAdd (α := M ⊗[R] N →ₗ[R] M ⊗[R] P) (lTensor M f) (lTensor M g)

Tactic:
(lTensorHom M).map_add f g

Premises used: LinearMap.map_add, LinearMap.lTensor, TensorProduct.map, LinearMap.lTensorHom, TensorProduct.lift
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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 g : N →ₗ[R] P
⊢ rTensor M (f + g) = HAdd.hAdd (α := N ⊗[R] M →ₗ[R] P ⊗[R] M) (rTensor M f) (rTensor M g)

Tactic:
(rTensorHom M).map_add f g

Premises used: LinearMap.map_add, LinearMap.rTensorHom, TensorProduct.map, TensorProduct.lift, LinearMap.rTensor
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
⊢ Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] P) (lTensor M 0) 0

Tactic:
(lTensorHom M).map_zero

Premises used: LinearMap.lTensor, LinearMap.map_zero, TensorProduct.map, LinearMap.lTensorHom, TensorProduct.lift
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
⊢ Eq (α := N ⊗[R] M →ₗ[R] P ⊗[R] M) (rTensor M 0) 0

Tactic:
(rTensorHom M).map_zero

Premises used: LinearMap.rTensorHom, LinearMap.map_zero, TensorProduct.map, TensorProduct.lift, LinearMap.rTensor
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
r : R
f : N →ₗ[R] P
⊢ lTensor M (r • f) = HSMul.hSMul (β := M ⊗[R] N →ₗ[R] M ⊗[R] P) r (lTensor M f)

Tactic:
(lTensorHom M).map_smul r f

Premises used: LinearMap.lTensor, TensorProduct.map, LinearMap.lTensorHom, LinearMap.map_smul, TensorProduct.lift
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
r : R
f : N →ₗ[R] P
⊢ rTensor M (r • f) = HSMul.hSMul (β := N ⊗[R] M →ₗ[R] P ⊗[R] M) r (rTensor M f)

Tactic:
(rTensorHom M).map_smul r f

Premises used: LinearMap.rTensorHom, TensorProduct.map, LinearMap.map_smul, TensorProduct.lift, LinearMap.rTensor
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
g : P →ₗ[R] Q
f : N →ₗ[R] P
H :
  ∀ (m : M) (n : N),
    Eq (α := M ⊗[R] Q)
      ((((compr₂ₛₗ (TensorProduct.mk R M N) (lTensor M (g ∘ₗ f)) : (a : M) → N →ₗ[R] M ⊗[R] Q) m : N →ₗ[R] M ⊗[R] Q) :
            (a : N) → M ⊗[R] Q)
          n :
        M ⊗[R] Q)
      ((((compr₂ₛₗ (TensorProduct.mk R M N) (lTensor M g ∘ₗ lTensor M f) : (a : M) → N →ₗ[R] M ⊗[R] Q) m :
              N →ₗ[R] M ⊗[R] Q) :
            (a : N) → M ⊗[R] Q)
          n :
        M ⊗[R] Q)
⊢ Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] Q) (lTensor M (g ∘ₗ f)) (lTensor M g ∘ₗ lTensor M f)

Tactic:
ext m n
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
g : P →ₗ[R] Q
f : N →ₗ[R] P
m : M
n : N
⊢ Eq (α := M ⊗[R] Q)
    ((((compr₂ₛₗ (TensorProduct.mk R M N) (lTensor M (g ∘ₗ f)) : (a : M) → N →ₗ[R] M ⊗[R] Q) m : N →ₗ[R] M ⊗[R] Q) :
          (a : N) → M ⊗[R] Q)
        n :
      M ⊗[R] Q)
    ((((compr₂ₛₗ (TensorProduct.mk R M N) (lTensor M g ∘ₗ lTensor M f) : (a : M) → N →ₗ[R] M ⊗[R] Q) m :
            N →ₗ[R] M ⊗[R] Q) :
          (a : N) → M ⊗[R] Q)
        n :
      M ⊗[R] Q)

Tactic:
simp only [compr₂ₛₗ_apply, mk_apply, comp_apply, lTensor_tmul]

Premises used: TensorProduct.mk_apply, LinearMap.comp_apply, LinearMap.compr₂ₛₗ_apply, LinearMap.lTensor_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
g : P →ₗ[R] Q
f : N →ₗ[R] P
x : M ⊗[R] N
rw :
  Eq (α := M ⊗[R] Q)
    (Function.comp (β := M ⊗[R] P) (⇑(lTensor M g) : (a : M ⊗[R] P) → M ⊗[R] Q)
        (⇑(lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] P) x :
      M ⊗[R] Q)
    ((lTensor M g : (a : M ⊗[R] P) → M ⊗[R] Q) ((lTensor M f : (a : M ⊗[R] N) → M ⊗[R] P) x) : M ⊗[R] Q)
⊢ Eq (α := M ⊗[R] Q) ((lTensor M (g ∘ₗ f) : (a : M ⊗[R] N) → M ⊗[R] Q) x : M ⊗[R] Q)
    ((lTensor M g : (a : M ⊗[R] P) → M ⊗[R] Q) ((lTensor M f : (a : M ⊗[R] N) → M ⊗[R] P) x) : M ⊗[R] Q)

Tactic:
rw [lTensor_comp, coe_comp]

Premises used: LinearMap.coe_comp, LinearMap.lTensor_comp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
g : P →ₗ[R] Q
f : N →ₗ[R] P
x : M ⊗[R] N
⊢ Eq (α := M ⊗[R] Q)
    (Function.comp (β := M ⊗[R] P) (⇑(lTensor M g) : (a : M ⊗[R] P) → M ⊗[R] Q)
        (⇑(lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] P) x :
      M ⊗[R] Q)
    ((lTensor M g : (a : M ⊗[R] P) → M ⊗[R] Q) ((lTensor M f : (a : M ⊗[R] N) → M ⊗[R] P) x) : M ⊗[R] Q)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
g : P →ₗ[R] Q
f : N →ₗ[R] P
H :
  ∀ (m : N) (n : M),
    Eq (α := Q ⊗[R] M)
      ((((compr₂ₛₗ (TensorProduct.mk R N M) (rTensor M (g ∘ₗ f)) : (a : N) → M →ₗ[R] Q ⊗[R] M) m : M →ₗ[R] Q ⊗[R] M) :
            (a : M) → Q ⊗[R] M)
          n :
        Q ⊗[R] M)
      ((((compr₂ₛₗ (TensorProduct.mk R N M) (rTensor M g ∘ₗ rTensor M f) : (a : N) → M →ₗ[R] Q ⊗[R] M) m :
              M →ₗ[R] Q ⊗[R] M) :
            (a : M) → Q ⊗[R] M)
          n :
        Q ⊗[R] M)
⊢ Eq (α := N ⊗[R] M →ₗ[R] Q ⊗[R] M) (rTensor M (g ∘ₗ f)) (rTensor M g ∘ₗ rTensor M f)

Tactic:
ext m n
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
g : P →ₗ[R] Q
f : N →ₗ[R] P
m : N
n : M
⊢ Eq (α := Q ⊗[R] M)
    ((((compr₂ₛₗ (TensorProduct.mk R N M) (rTensor M (g ∘ₗ f)) : (a : N) → M →ₗ[R] Q ⊗[R] M) m : M →ₗ[R] Q ⊗[R] M) :
          (a : M) → Q ⊗[R] M)
        n :
      Q ⊗[R] M)
    ((((compr₂ₛₗ (TensorProduct.mk R N M) (rTensor M g ∘ₗ rTensor M f) : (a : N) → M →ₗ[R] Q ⊗[R] M) m :
            M →ₗ[R] Q ⊗[R] M) :
          (a : M) → Q ⊗[R] M)
        n :
      Q ⊗[R] M)

Tactic:
simp only [compr₂ₛₗ_apply, mk_apply, comp_apply, rTensor_tmul]

Premises used: LinearMap.rTensor_tmul, TensorProduct.mk_apply, LinearMap.comp_apply, LinearMap.compr₂ₛₗ_apply
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
g : P →ₗ[R] Q
f : N →ₗ[R] P
x : N ⊗[R] M
rw :
  Eq (α := Q ⊗[R] M)
    (Function.comp (β := P ⊗[R] M) (⇑(rTensor M g) : (a : P ⊗[R] M) → Q ⊗[R] M)
        (⇑(rTensor M f) : (a : N ⊗[R] M) → P ⊗[R] M) x :
      Q ⊗[R] M)
    ((rTensor M g : (a : P ⊗[R] M) → Q ⊗[R] M) ((rTensor M f : (a : N ⊗[R] M) → P ⊗[R] M) x) : Q ⊗[R] M)
⊢ Eq (α := Q ⊗[R] M) ((rTensor M (g ∘ₗ f) : (a : N ⊗[R] M) → Q ⊗[R] M) x : Q ⊗[R] M)
    ((rTensor M g : (a : P ⊗[R] M) → Q ⊗[R] M) ((rTensor M f : (a : N ⊗[R] M) → P ⊗[R] M) x) : Q ⊗[R] M)

Tactic:
rw [rTensor_comp, coe_comp]

Premises used: LinearMap.coe_comp, LinearMap.rTensor_comp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
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
g : P →ₗ[R] Q
f : N →ₗ[R] P
x : N ⊗[R] M
⊢ Eq (α := Q ⊗[R] M)
    (Function.comp (β := P ⊗[R] M) (⇑(rTensor M g) : (a : P ⊗[R] M) → Q ⊗[R] M)
        (⇑(rTensor M f) : (a : N ⊗[R] M) → P ⊗[R] M) x :
      Q ⊗[R] M)
    ((rTensor M g : (a : P ⊗[R] M) → Q ⊗[R] M) ((rTensor M f : (a : N ⊗[R] M) → P ⊗[R] M) x) : Q ⊗[R] M)

Tactic:
rfl