awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
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 : SMul R' R
inst_36 : IsScalarTower R' R M
inst_37 : DistribMulAction R' N
inst_38 : IsScalarTower R' R N
r : R'
m : M
n : N
rw : Eq (α := M ⊗[R] N) ((HSMul.hSMul (β := R) r 1 • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (HSMul.hSMul (β := R) r 1 • n))
⊢ Eq (α := M ⊗[R] N) ((r • HSMul.hSMul.{u_1, u_7, u_7} (α := R) 1 m) ⊗ₜ[R] n)
    (m ⊗ₜ[R] (r • HSMul.hSMul.{u_1, u_8, u_8} (α := R) 1 n))

Tactic:
rw [← smul_assoc, ← smul_assoc]

Premises used: smul_assoc
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
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 : SMul R' R
inst_36 : IsScalarTower R' R M
inst_37 : DistribMulAction R' N
inst_38 : IsScalarTower R' R N
r : R'
m : M
n : N
⊢ Eq (α := M ⊗[R] N) ((HSMul.hSMul (β := R) r 1 • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (HSMul.hSMul (β := R) r 1 • n))

Tactic:
Quotient.sound' <| AddConGen.Rel.of _ _ <| Eqv.of_smul _ _ _

Premises used: Quotient.sound', TensorProduct.Eqv.of_smul, AddConGen.Rel.of, TensorProduct, TensorProduct.tmul, AddCon.Quotient, AddCon.toQuotient
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
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 : SMul R' R
inst_36 : IsScalarTower R' R M
inst_37 : DistribMulAction R' N
inst_38 : IsScalarTower R' R N
r : R'
m : M
n : N
⊢ Eq (α := M ⊗[R] N) ((HSMul.hSMul (β := R) r 1 • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (HSMul.hSMul (β := R) r 1 • n))

Tactic:
exact Quotient.sound' <| AddConGen.Rel.of _ _ <| Eqv.of_smul _ _ _

Premises used: Quotient.sound', TensorProduct.Eqv.of_smul, AddConGen.Rel.of
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
R' : Type u_4
inst : CommSemiring R
inst_1 : Monoid R'
M : Type u_7
N : Type u_8
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : DistribMulAction R' M
inst_5 : Module R M
inst_6 : Module R N
inst_7 : DistribMulAction R' N
inst_8 : CompatibleSMul R R' M N
r : R'
m : M
n : N
⊢ Eq (α := M ⊗[R] N) ((r • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (r • n))

Tactic:
CompatibleSMul.smul_tmul _ _ _

Premises used: TensorProduct.CompatibleSMul.smul_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
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
R' : Type u_22
inst_5 : SMul R' M
r : R'
m : M
n : N
⊢ Eq (α := M ⊗[R] N) ((aux r : (a : FreeAddMonoid (M × N)) → M ⊗[R] N) (FreeAddMonoid.of (m, n)) : M ⊗[R] N)
    ((r • m) ⊗ₜ[R] n : M ⊗[R] N)

Tactic:
rfl

Premises used: List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
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 : SMulCommClass R R' M
inst_36 : SMulCommClass R R'' M
r : R'
x y : FreeAddMonoid (M × N)
hxy : Eqv R M N x y
n : N
simp_rw :
  Eq (α := M ⊗[R] N) ((SMul.aux r : (a : FreeAddMonoid (M × N)) → M ⊗[R] N) (FreeAddMonoid.of (0, n)) : M ⊗[R] N)
    (0 : M ⊗[R] N)
simp_rw₁ : Eq (α := M ⊗[R] N) (HSMul.hSMul (β := M) r 0 ⊗ₜ[R] n) 0
simp_rw₂ : Eq (α := M ⊗[R] N) (0 ⊗ₜ[R] n) 0
⊢ Eq (α := M ⊗[R] N) ((SMul.aux r : (a : FreeAddMonoid (M × N)) → M ⊗[R] N) (FreeAddMonoid.of (0, n)) : M ⊗[R] N)
    ((SMul.aux r : (a : FreeAddMonoid (M × N)) → M ⊗[R] N) 0 : M ⊗[R] N)

Tactic:
simp_rw [map_zero, SMul.aux_of, smul_zero, zero_tmul]

Premises used: smul_zero, map_zero, TensorProduct.zero_tmul, TensorProduct.SMul.aux_of
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
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 : SMulCommClass R R' M
inst_36 : SMulCommClass R R'' M
r : R'
x y : FreeAddMonoid (M × N)
hxy : Eqv R M N x y
m : M
simp_rw :
  Eq (α := M ⊗[R] N) ((SMul.aux r : (a : FreeAddMonoid (M × N)) → M ⊗[R] N) (FreeAddMonoid.of (m, 0)) : M ⊗[R] N)
    (0 : M ⊗[R] N)
simp_rw₁ : Eq (α := M ⊗[R] N) ((r • m) ⊗ₜ[R] 0) 0
⊢ Eq (α := M ⊗[R] N) ((SMul.aux r : (a : FreeAddMonoid (M × N)) → M ⊗[R] N) (FreeAddMonoid.of (m, 0)) : M ⊗[R] N)
    ((SMul.aux r : (a : FreeAddMonoid (M × N)) → M ⊗[R] N) 0 : M ⊗[R] N)

Tactic:
simp_rw [map_zero, SMul.aux_of, tmul_zero]

Premises used: TensorProduct.tmul_zero, map_zero, TensorProduct.SMul.aux_of
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
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 : SMulCommClass R R' M
inst_36 : SMulCommClass R R'' M
r : R'
x y : FreeAddMonoid (M × N)
hxy : Eqv R M N x y
m₁ m₂ : M
n : N
simp_rw :
  HAdd.hAdd (α := M ⊗[R] N) (β := M ⊗[R] N)
      ((SMul.aux r : (a : FreeAddMonoid (M × N)) → M ⊗[R] N) (FreeAddMonoid.of (m₁, n)) : M ⊗[R] N)
      ((SMul.aux r : (a : FreeAddMonoid (M × N)) → M ⊗[R] N) (FreeAddMonoid.of (m₂, n)) : M ⊗[R] N) =
    (SMul.aux r : (a : FreeAddMonoid (M × N)) → M ⊗[R] N) (FreeAddMonoid.of (m₁ + m₂, n))
simp_rw₁ : HAdd.hAdd (α := M ⊗[R] N) ((r • m₁) ⊗ₜ[R] n) ((r • m₂) ⊗ₜ[R] n) = (r • (m₁ + m₂)) ⊗ₜ[R] n
simp_rw₂ : HAdd.hAdd (α := M ⊗[R] N) ((r • m₁) ⊗ₜ[R] n) ((r • m₂) ⊗ₜ[R] n) = (r • m₁ + r • m₂) ⊗ₜ[R] n
⊢ Eq (α := M ⊗[R] N)
    ((SMul.aux r : (a : FreeAddMonoid (M × N)) → M ⊗[R] N) (FreeAddMonoid.of (m₁, n) + FreeAddMonoid.of (m₂, n)) :
      M ⊗[R] N)
    ((SMul.aux r : (a : FreeAddMonoid (M × N)) → M ⊗[R] N) (FreeAddMonoid.of (m₁ + m₂, n)) : M ⊗[R] N)

Tactic:
simp_rw [map_add, SMul.aux_of, smul_add, add_tmul]

Premises used: map_add, TensorProduct.SMul.aux_of, TensorProduct.add_tmul, smul_add
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
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 : SMulCommClass R R' M
inst_36 : SMulCommClass R R'' M
r : R'
x y : FreeAddMonoid (M × N)
hxy : Eqv R M N x y
m : M
n₁ n₂ : N
simp_rw :
  HAdd.hAdd (α := M ⊗[R] N) (β := M ⊗[R] N)
      ((SMul.aux r : (a : FreeAddMonoid (M × N)) → M ⊗[R] N) (FreeAddMonoid.of (m, n₁)) : M ⊗[R] N)
      ((SMul.aux r : (a : FreeAddMonoid (M × N)) → M ⊗[R] N) (FreeAddMonoid.of (m, n₂)) : M ⊗[R] N) =
    (SMul.aux r : (a : FreeAddMonoid (M × N)) → M ⊗[R] N) (FreeAddMonoid.of (m, n₁ + n₂))
simp_rw₁ : HAdd.hAdd (α := M ⊗[R] N) ((r • m) ⊗ₜ[R] n₁) ((r • m) ⊗ₜ[R] n₂) = (r • m) ⊗ₜ[R] (n₁ + n₂)
⊢ Eq (α := M ⊗[R] N)
    ((SMul.aux r : (a : FreeAddMonoid (M × N)) → M ⊗[R] N) (FreeAddMonoid.of (m, n₁) + FreeAddMonoid.of (m, n₂)) :
      M ⊗[R] N)
    ((SMul.aux r : (a : FreeAddMonoid (M × N)) → M ⊗[R] N) (FreeAddMonoid.of (m, n₁ + n₂)) : M ⊗[R] N)

Tactic:
simp_rw [map_add, SMul.aux_of, tmul_add]

Premises used: map_add, TensorProduct.SMul.aux_of, TensorProduct.tmul_add
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
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 : SMulCommClass R R' M
inst_36 : SMulCommClass R R'' M
r : R'
x y : FreeAddMonoid (M × N)
hxy : Eqv R M N x y
s : R
m : M
n : N
rw :
  Eq (α := M ⊗[R] N) ((r • s • m) ⊗ₜ[R] n)
    ((SMul.aux r : (a : FreeAddMonoid (M × N)) → M ⊗[R] N) (FreeAddMonoid.of (m, s • n)))
rw₁ : Eq (α := M ⊗[R] N) ((r • s • m) ⊗ₜ[R] n) ((r • m) ⊗ₜ[R] (s • n))
rw₂ : Eq (α := M ⊗[R] N) ((s • r • m) ⊗ₜ[R] n) ((r • m) ⊗ₜ[R] (s • n))
rw₃ rw₄ : Eq (α := M ⊗[R] N) ((r • m) ⊗ₜ[R] (s • n)) ((r • m) ⊗ₜ[R] (s • n))
⊢ Eq (α := M ⊗[R] N) ((SMul.aux r : (a : FreeAddMonoid (M × N)) → M ⊗[R] N) (FreeAddMonoid.of (s • m, n)) : M ⊗[R] N)
    ((SMul.aux r : (a : FreeAddMonoid (M × N)) → M ⊗[R] N) (FreeAddMonoid.of (m, s • n)) : M ⊗[R] N)

Tactic:
rw [SMul.aux_of, SMul.aux_of, ← smul_comm, smul_tmul]

Premises used: TensorProduct.smul_tmul, TensorProduct.SMul.aux_of, SMulCommClass.smul_comm
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
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 : SMulCommClass R R' M
inst_36 : SMulCommClass R R'' M
r : R'
x_1 y_1 : FreeAddMonoid (M × N)
hxy : Eqv R M N x_1 y_1
x y : FreeAddMonoid (M × N)
simp_rw :
  HAdd.hAdd (α := M ⊗[R] N) (β := M ⊗[R] N) ((SMul.aux r : (a : FreeAddMonoid (M × N)) → M ⊗[R] N) x : M ⊗[R] N)
      ((SMul.aux r : (a : FreeAddMonoid (M × N)) → M ⊗[R] N) y : M ⊗[R] N) =
    HAdd.hAdd (α := M ⊗[R] N) (β := M ⊗[R] N) ((SMul.aux r : (a : FreeAddMonoid (M × N)) → M ⊗[R] N) y : M ⊗[R] N)
      ((SMul.aux r : (a : FreeAddMonoid (M × N)) → M ⊗[R] N) x : M ⊗[R] N)
⊢ Eq (α := M ⊗[R] N) ((SMul.aux r : (a : FreeAddMonoid (M × N)) → M ⊗[R] N) (x + y) : M ⊗[R] N)
    ((SMul.aux r : (a : FreeAddMonoid (M × N)) → M ⊗[R] N) (y + x) : M ⊗[R] N)

Tactic:
simp_rw [map_add, add_comm]

Premises used: map_add, add_comm
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
R' : Type u_4
inst : CommSemiring R
inst_1 : Monoid R'
M : Type u_7
N : Type u_8
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : DistribMulAction R' M
inst_5 : Module R M
inst_6 : Module R N
inst_7 : SMulCommClass R R' M
r : R'
⊢ HSMul.hSMul (β := M ⊗[R] N) r 0 = 0

Tactic:
map_zero _

Premises used: map_zero
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
R' : Type u_4
inst : CommSemiring R
inst_1 : Monoid R'
M : Type u_7
N : Type u_8
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : DistribMulAction R' M
inst_5 : Module R M
inst_6 : Module R N
inst_7 : SMulCommClass R R' M
r : R'
x y : M ⊗[R] N
⊢ r • (x + y) = r • x + r • y

Tactic:
map_add _ _ _

Premises used: map_add
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
R'' : Type u_5
inst : CommSemiring R
inst_1 : Semiring R''
M : Type u_7
N : Type u_8
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R'' M
inst_5 : Module R M
inst_6 : Module R N
inst_7 : SMulCommClass R R'' M
x : M ⊗[R] N
this : ∀ (r : R'') (m : M) (n : N), HSMul.hSMul (β := M ⊗[R] N) r (m ⊗ₜ[R] n) = (r • m) ⊗ₜ[R] n
rw rw₁ : Eq (α := M ⊗[R] N) 0 0
⊢ HSMul.hSMul (α := R'') (β := M ⊗[R] N) 0 0 = 0

Tactic:
rw [TensorProduct.smul_zero]

Premises used: TensorProduct.smul_zero
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
R'' : Type u_5
inst : CommSemiring R
inst_1 : Semiring R''
M : Type u_7
N : Type u_8
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R'' M
inst_5 : Module R M
inst_6 : Module R N
inst_7 : SMulCommClass R R'' M
x : M ⊗[R] N
this : ∀ (r : R'') (m : M) (n : N), HSMul.hSMul (β := M ⊗[R] N) r (m ⊗ₜ[R] n) = (r • m) ⊗ₜ[R] n
m : M
n : N
rw : Eq (α := M ⊗[R] N) (HSMul.hSMul.{u_5, u_7, u_7} (α := R'') 0 m ⊗ₜ[R] n) 0
rw₁ : Eq (α := M ⊗[R] N) (0 ⊗ₜ[R] n) 0
rw₂ rw₃ : Eq (α := M ⊗[R] N) 0 0
⊢ HSMul.hSMul (α := R'') (β := M ⊗[R] N) 0 (m ⊗ₜ[R] n) = 0

Tactic:
rw [this, zero_smul, zero_tmul]

Premises used: TensorProduct.zero_tmul, zero_smul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
R'' : Type u_5
inst : CommSemiring R
inst_1 : Semiring R''
M : Type u_7
N : Type u_8
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R'' M
inst_5 : Module R M
inst_6 : Module R N
inst_7 : SMulCommClass R R'' M
x_1 : M ⊗[R] N
this : ∀ (r : R'') (m : M) (n : N), HSMul.hSMul (β := M ⊗[R] N) r (m ⊗ₜ[R] n) = (r • m) ⊗ₜ[R] n
x y : M ⊗[R] N
ihx : HSMul.hSMul (α := R'') 0 x = 0
ihy : HSMul.hSMul (α := R'') 0 y = 0
rw : HSMul.hSMul (α := R'') 0 x + HSMul.hSMul (α := R'') 0 y = 0
rw₁ : 0 + HSMul.hSMul (α := R'') 0 y = 0
rw₂ : HAdd.hAdd (α := M ⊗[R] N) 0 0 = 0
rw₃ rw₄ : Eq (α := M ⊗[R] N) 0 0
⊢ HSMul.hSMul (α := R'') 0 (x + y) = 0

Tactic:
rw [TensorProduct.smul_add, ihx, ihy, add_zero]

Premises used: TensorProduct.smul_add, add_zero
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
R' : Type u_4
inst : CommSemiring R
inst_1 : Monoid R'
M : Type u_7
N : Type u_8
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : DistribMulAction R' M
inst_5 : Module R M
inst_6 : Module R N
inst_7 : SMulCommClass R R' M
x : M ⊗[R] N
this : ∀ (r : R') (m : M) (n : N), HSMul.hSMul (β := M ⊗[R] N) r (m ⊗ₜ[R] n) = (r • m) ⊗ₜ[R] n
rw rw₁ : Eq (α := M ⊗[R] N) 0 0
⊢ HSMul.hSMul (α := R') (β := M ⊗[R] N) 1 0 = 0

Tactic:
rw [TensorProduct.smul_zero]

Premises used: TensorProduct.smul_zero
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
R' : Type u_4
inst : CommSemiring R
inst_1 : Monoid R'
M : Type u_7
N : Type u_8
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : DistribMulAction R' M
inst_5 : Module R M
inst_6 : Module R N
inst_7 : SMulCommClass R R' M
x : M ⊗[R] N
this : ∀ (r : R') (m : M) (n : N), HSMul.hSMul (β := M ⊗[R] N) r (m ⊗ₜ[R] n) = (r • m) ⊗ₜ[R] n
m : M
n : N
rw : Eq (α := M ⊗[R] N) (HSMul.hSMul.{u_4, u_7, u_7} (α := R') 1 m ⊗ₜ[R] n) (m ⊗ₜ[R] n)
rw₁ rw₂ : Eq (α := M ⊗[R] N) (m ⊗ₜ[R] n) (m ⊗ₜ[R] n)
⊢ HSMul.hSMul (α := R') (β := M ⊗[R] N) 1 (m ⊗ₜ[R] n) = m ⊗ₜ[R] n

Tactic:
rw [this, one_smul]

Premises used: one_smul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
R' : Type u_4
inst : CommSemiring R
inst_1 : Monoid R'
M : Type u_7
N : Type u_8
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : DistribMulAction R' M
inst_5 : Module R M
inst_6 : Module R N
inst_7 : SMulCommClass R R' M
x_1 : M ⊗[R] N
this : ∀ (r : R') (m : M) (n : N), HSMul.hSMul (β := M ⊗[R] N) r (m ⊗ₜ[R] n) = (r • m) ⊗ₜ[R] n
x y : M ⊗[R] N
ihx : HSMul.hSMul (α := R') 1 x = x
ihy : HSMul.hSMul (α := R') 1 y = y
rw : HSMul.hSMul (α := R') 1 x + HSMul.hSMul (α := R') 1 y = x + y
rw₁ : x + HSMul.hSMul (α := R') 1 y = x + y
rw₂ rw₃ : x + y = x + y
⊢ HSMul.hSMul (α := R') 1 (x + y) = x + y

Tactic:
rw [TensorProduct.smul_add, ihx, ihy]

Premises used: TensorProduct.smul_add
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
R'' : Type u_5
inst : CommSemiring R
inst_1 : Semiring R''
M : Type u_7
N : Type u_8
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R'' M
inst_5 : Module R M
inst_6 : Module R N
inst_7 : SMulCommClass R R'' M
r s : R''
x : M ⊗[R] N
this : ∀ (r : R'') (m : M) (n : N), HSMul.hSMul (β := M ⊗[R] N) r (m ⊗ₜ[R] n) = (r • m) ⊗ₜ[R] n
m : M
n : N
simp_rw : ((r + s) • m) ⊗ₜ[R] n = HAdd.hAdd (α := M ⊗[R] N) ((r • m) ⊗ₜ[R] n) ((s • m) ⊗ₜ[R] n)
simp_rw₁ : (r • m + s • m) ⊗ₜ[R] n = HAdd.hAdd (α := M ⊗[R] N) ((r • m) ⊗ₜ[R] n) ((s • m) ⊗ₜ[R] n)
⊢ HSMul.hSMul (β := M ⊗[R] N) (r + s) (m ⊗ₜ[R] n) =
    HSMul.hSMul (β := M ⊗[R] N) r (m ⊗ₜ[R] n) + HSMul.hSMul (β := M ⊗[R] N) s (m ⊗ₜ[R] n)

Tactic:
simp_rw [this, add_smul, add_tmul]

Premises used: add_smul, TensorProduct.add_tmul