awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_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 : (r + s) • x = r • x + s • x
ihy : (r + s) • y = r • y + s • y
simp_rw : (r + s) • x + (r + s) • y = r • x + r • y + (s • x + s • y)
⊢ (r + s) • (x + y) = r • (x + y) + s • (x + y)

Tactic:
simp_rw [TensorProduct.smul_add]

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_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 : (r + s) • x = r • x + s • x
ihy : (r + s) • y = r • y + s • y
rw : r • x + s • x + (r + s) • y = r • x + r • y + (s • x + s • y)
rw₁ : r • x + s • x + (r • y + s • y) = r • x + r • y + (s • x + s • y)
rw₂ rw₃ : r • x + r • y + (s • x + s • y) = r • x + r • y + (s • x + s • y)
⊢ (r + s) • x + (r + s) • y = r • x + r • y + (s • x + s • y)

Tactic:
rw [ihx, ihy, add_add_add_comm]

Premises used: add_add_add_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
⊢ ∀ (x : M ⊗[R] N), HSMul.hSMul (α := ℕ) 0 x = 0

Tactic:
simp [TensorProduct.zero_smul]

Premises used: TensorProduct.zero_smul
-- 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
⊢ ∀ (n : ℕ) (x : M ⊗[R] N), (n + 1) • x = n • x + x

Tactic:
simp only [TensorProduct.one_smul, TensorProduct.add_smul, add_comm,
    forall_const]

Premises used: add_comm, TensorProduct.add_smul, forall_const, TensorProduct.one_smul
-- 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
n : N
hn : IsAddUnit n
m : M
rw : ∀ (hn : ∃ (b : N), n + b = 0) (m : M), ∃ (b : M ⊗[R] N), m ⊗ₜ[R] n + b = 0
⊢ IsAddUnit (M := M ⊗[R] N) (m ⊗ₜ[R] n)

Tactic:
rw [isAddUnit_iff_exists_neg] at hn ⊢

Premises used: isAddUnit_iff_exists_neg
-- 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
n : N
hn : ∃ (b : N), n + b = 0
m : M
have : ∀ (b : N) (eq : n + b = 0), ∃ (b : M ⊗[R] N), m ⊗ₜ[R] n + b = 0
⊢ ∃ (b : M ⊗[R] N), m ⊗ₜ[R] n + b = 0

Tactic:
have ⟨b, eq⟩ := hn
-- 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
n : N
hn : ∃ (b : N), n + b = 0
m : M
b : N
eq : n + b = 0
rw : Eq (α := M ⊗[R] N) (m ⊗ₜ[R] (n + b)) 0
rw₁ : Eq (α := M ⊗[R] N) (m ⊗ₜ[R] 0) 0
rw₂ rw₃ : Eq (α := M ⊗[R] N) 0 0
⊢ HAdd.hAdd (α := M ⊗[R] N) (m ⊗ₜ[R] n) (m ⊗ₜ[R] b) = 0

Tactic:
rw [← tmul_add, eq, tmul_zero]

Premises used: TensorProduct.tmul_zero, TensorProduct.tmul_add
-- 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
n : N
hn : ∃ (b : N), n + b = 0
m : M
b : N
eq : n + b = 0
⊢ ∃ (b : M ⊗[R] N), m ⊗ₜ[R] n + b = 0

Tactic:
exact ⟨m ⊗ₜ[R] b, by rw [← tmul_add, eq, tmul_zero]⟩
-- 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
m : M
hm : IsAddUnit m
n : N
rw : ∀ (hm : ∃ (b : M), m + b = 0) (n : N), ∃ (b : M ⊗[R] N), m ⊗ₜ[R] n + b = 0
⊢ IsAddUnit (M := M ⊗[R] N) (m ⊗ₜ[R] n)

Tactic:
rw [isAddUnit_iff_exists_neg] at hm ⊢

Premises used: isAddUnit_iff_exists_neg
-- 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
m : M
hm : ∃ (b : M), m + b = 0
n : N
have : ∀ (b : M) (eq : m + b = 0), ∃ (b : M ⊗[R] N), m ⊗ₜ[R] n + b = 0
⊢ ∃ (b : M ⊗[R] N), m ⊗ₜ[R] n + b = 0

Tactic:
have ⟨b, eq⟩ := hm
-- 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
m : M
hm : ∃ (b : M), m + b = 0
n : N
b : M
eq : m + b = 0
rw : Eq (α := M ⊗[R] N) ((m + b) ⊗ₜ[R] n) 0
rw₁ : Eq (α := M ⊗[R] N) (0 ⊗ₜ[R] n) 0
rw₂ rw₃ : Eq (α := M ⊗[R] N) 0 0
⊢ HAdd.hAdd (α := M ⊗[R] N) (m ⊗ₜ[R] n) (b ⊗ₜ[R] n) = 0

Tactic:
rw [← add_tmul, eq, zero_tmul]

Premises used: TensorProduct.zero_tmul, TensorProduct.add_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
m : M
hm : ∃ (b : M), m + b = 0
n : N
b : M
eq : m + b = 0
⊢ ∃ (b : M ⊗[R] N), m ⊗ₜ[R] n + b = 0

Tactic:
exact ⟨b ⊗ₜ[R] n, by rw [← add_tmul, eq, zero_tmul]⟩
-- 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
this : ∀ (r : R') (m : M) (n : N), HSMul.hSMul (β := M ⊗[R] N) r (m ⊗ₜ[R] n) = (r • m) ⊗ₜ[R] n
r s : R'
x : M ⊗[R] N
⊢ HSMul.hSMul (β := M ⊗[R] N) (r * s) 0 = r • HSMul.hSMul (β := M ⊗[R] N) s 0

Tactic:
simp_rw [TensorProduct.smul_zero]

Premises used: TensorProduct.smul_zero
-- 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
this : ∀ (r : R') (m : M) (n : N), HSMul.hSMul (β := M ⊗[R] N) r (m ⊗ₜ[R] n) = (r • m) ⊗ₜ[R] n
r s : R'
x : M ⊗[R] N
m : M
n : N
simp_rw : Eq (α := M ⊗[R] N) (((r * s) • m) ⊗ₜ[R] n) ((r • s • m) ⊗ₜ[R] n)
⊢ HSMul.hSMul (β := M ⊗[R] N) (r * s) (m ⊗ₜ[R] n) = r • HSMul.hSMul (β := M ⊗[R] N) s (m ⊗ₜ[R] n)

Tactic:
simp_rw [this, mul_smul]

Premises used: SemigroupAction.mul_smul
-- 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
this : ∀ (r : R') (m : M) (n : N), HSMul.hSMul (β := M ⊗[R] N) r (m ⊗ₜ[R] n) = (r • m) ⊗ₜ[R] n
r s : R'
x_1 x y : M ⊗[R] N
ihx : (r * s) • x = r • s • x
ihy : (r * s) • y = r • s • y
simp_rw : (r * s) • x + (r * s) • y = r • s • x + r • s • y
⊢ (r * s) • (x + y) = r • s • (x + y)

Tactic:
simp_rw [TensorProduct.smul_add]

Premises used: TensorProduct.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
this : ∀ (r : R') (m : M) (n : N), HSMul.hSMul (β := M ⊗[R] N) r (m ⊗ₜ[R] n) = (r • m) ⊗ₜ[R] n
r s : R'
x_1 x y : M ⊗[R] N
ihx : (r * s) • x = r • s • x
ihy : (r * s) • y = r • s • y
rw : r • s • x + (r * s) • y = r • s • x + r • s • y
rw₁ rw₂ : r • s • x + r • s • y = r • s • x + r • s • y
⊢ (r * s) • x + (r * s) • y = r • s • x + r • s • y

Tactic:
rw [ihx, ihy]
-- 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'
m : M
n : N
⊢ HSMul.hSMul (β := M ⊗[R] N) r (m ⊗ₜ[R] n) = (r • m) ⊗ₜ[R] n

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- 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
inst_8 : DistribMulAction R' N
inst_9 : CompatibleSMul R R' M N
r : R'
x : M
y : N
⊢ x ⊗ₜ[R] (r • y) = HSMul.hSMul (β := M ⊗[R] N) r (x ⊗ₜ[R] y)

Tactic:
(smul_tmul _ _ _).symm

Premises used: TensorProduct.smul_tmul, Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, Eq.symm, AddCon.toQuotient, FreeAddMonoid.sumAux
-- 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 s : R
m : M
n : N
simp_rw : m ⊗ₜ[R] (r • s • n) = HSMul.hSMul (β := M ⊗[R] N) (r * s) (m ⊗ₜ[R] n)
simp_rw₁ : r • HSMul.hSMul (β := M ⊗[R] N) s (m ⊗ₜ[R] n) = HSMul.hSMul (β := M ⊗[R] N) (r * s) (m ⊗ₜ[R] n)
⊢ (r • m) ⊗ₜ[R] (s • n) = HSMul.hSMul (β := M ⊗[R] N) (r * s) (m ⊗ₜ[R] n)

Tactic:
simp_rw [smul_tmul, tmul_smul, mul_smul]

Premises used: TensorProduct.smul_tmul, TensorProduct.tmul_smul, SemigroupAction.mul_smul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_22
inst_3 : Semiring S
inst_4 : Module R S
inst_5 : SMulCommClass R S S
s : S
m : M
nth_rw : (s * 1) ⊗ₜ[R] m = HSMul.hSMul (β := S ⊗[R] M) s (1 ⊗ₜ[R] m)
nth_rw₁ : HSMul.hSMul (β := S) s 1 ⊗ₜ[R] m = HSMul.hSMul (β := S ⊗[R] M) s (1 ⊗ₜ[R] m)
nth_rw₂ nth_rw₃ : Eq (α := S ⊗[R] M) (HSMul.hSMul (β := S) s 1 ⊗ₜ[R] m) (HSMul.hSMul (β := S) s 1 ⊗ₜ[R] m)
⊢ s ⊗ₜ[R] m = HSMul.hSMul (β := S ⊗[R] M) s (1 ⊗ₜ[R] m)

Tactic:
nth_rw 1 [← mul_one s, ← smul_eq_mul, smul_tmul']

Premises used: TensorProduct.smul_tmul', smul_eq_mul, mul_one
-- 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
inst_37 : Module.{u_5, u_7} R''ᵐᵒᵖ M
inst_38 : IsCentralScalar R'' M
r : R''
x : M ⊗[R] N
rw : 0 = HSMul.hSMul (β := M ⊗[R] N) r 0
rw₁ rw₂ : Eq (α := M ⊗[R] N) 0 0
⊢ HSMul.hSMul (β := M ⊗[R] N) (MulOpposite.op r) 0 = HSMul.hSMul (β := M ⊗[R] N) r 0

Tactic:
rw [smul_zero, smul_zero]

Premises used: smul_zero
-- 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
inst_37 : Module.{u_5, u_7} R''ᵐᵒᵖ M
inst_38 : IsCentralScalar R'' M
r : R''
x_1 : M ⊗[R] N
x : M
y : N
rw : (MulOpposite.op r • x) ⊗ₜ[R] y = HSMul.hSMul (β := M ⊗[R] N) r (x ⊗ₜ[R] y)
rw₁ : Eq (α := M ⊗[R] N) ((MulOpposite.op r • x) ⊗ₜ[R] y) ((r • x) ⊗ₜ[R] y)
rw₂ rw₃ : Eq (α := M ⊗[R] N) ((r • x) ⊗ₜ[R] y) ((r • x) ⊗ₜ[R] y)
⊢ HSMul.hSMul (β := M ⊗[R] N) (MulOpposite.op r) (x ⊗ₜ[R] y) = HSMul.hSMul (β := M ⊗[R] N) r (x ⊗ₜ[R] y)

Tactic:
rw [smul_tmul', smul_tmul', op_smul_eq_smul]

Premises used: TensorProduct.smul_tmul', IsCentralScalar.op_smul_eq_smul
-- 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
inst_37 : Module.{u_5, u_7} R''ᵐᵒᵖ M
inst_38 : IsCentralScalar R'' M
r : R''
x_1 x y : M ⊗[R] N
hx : MulOpposite.op r • x = r • x
hy : MulOpposite.op r • y = r • y
rw : MulOpposite.op r • x + MulOpposite.op r • y = r • (x + y)
rw₁ : MulOpposite.op r • x + MulOpposite.op r • y = r • x + r • y
rw₂ : r • x + MulOpposite.op r • y = r • x + r • y
rw₃ rw₄ : r • x + r • y = r • x + r • y
⊢ MulOpposite.op r • (x + y) = r • (x + y)

Tactic:
rw [smul_add, smul_add, hx, hy]

Premises used: 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'₂ : Type u_22
inst_37 : Monoid R'₂
inst_38 : DistribMulAction R'₂ M
inst_39 : SMulCommClass R R'₂ M
inst_40 : SMulCommClass R' R'₂ M
r' : R'
r'₂ : R'₂
x : M ⊗[R] N
⊢ r' • HSMul.hSMul (β := M ⊗[R] N) r'₂ 0 = r'₂ • HSMul.hSMul (β := M ⊗[R] N) r' 0

Tactic:
simp_rw [TensorProduct.smul_zero]

Premises used: TensorProduct.smul_zero