awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : Monoid R'
inst_4 : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S
inst_10 : AddCommMonoid P'
inst_11 : AddCommMonoid Q'
inst_12 : AddCommMonoid M₂
inst_13 : AddCommMonoid N₂
inst_14 : AddCommMonoid P₂
inst_15 : AddCommMonoid Q₂
inst_16 : AddCommMonoid M₃
inst_17 : AddCommMonoid N₃
inst_18 : AddCommMonoid P₃
inst_19 : AddCommMonoid Q₃
inst_20 : DistribMulAction R' M
inst_21 : Module R'' M
inst_22 : Module R M
inst_23 : Module R N
inst_24 : Module R S
inst_25 : Module R P'
inst_26 : Module R Q'
inst_27 : Module R₂ M₂
inst_28 : Module R₂ N₂
inst_29 : Module R₂ P₂
inst_30 : Module R₂ Q₂
inst_31 : Module R₃ M₃
inst_32 : Module R₃ N₃
inst_33 : Module R₃ P₃
inst_34 : Module R₃ Q₃
inst_35 : 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 : SMul R'₂ R'
inst_41 : IsScalarTower R'₂ R' M
s : R'₂
r : R'
x_1 x y : M ⊗[R] N
ihx : (s • r) • x = s • r • x
ihy : (s • r) • y = s • r • y
rw : (s • r) • x + (s • r) • y = s • r • (x + y)
rw₁ : (s • r) • x + (s • r) • y = s • (r • x + r • y)
rw₂ : (s • r) • x + (s • r) • y = s • r • x + s • r • y
rw₃ : s • r • x + (s • r) • y = s • r • x + s • r • y
⊢ (s • r) • (x + y) = s • r • (x + y)
have rw₄ : s • r • x + s • r • y = s • r • x + s • r • y
Tactic: rw [smul_add, smul_add, smul_add, ihx, ihy]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : Monoid R'
inst_4 : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S
inst_10 : AddCommMonoid P'
inst_11 : AddCommMonoid Q'
inst_12 : AddCommMonoid M₂
inst_13 : AddCommMonoid N₂
inst_14 : AddCommMonoid P₂
inst_15 : AddCommMonoid Q₂
inst_16 : AddCommMonoid M₃
inst_17 : AddCommMonoid N₃
inst_18 : AddCommMonoid P₃
inst_19 : AddCommMonoid Q₃
inst_20 : DistribMulAction R' M
inst_21 : Module R'' M
inst_22 : Module R M
inst_23 : Module R N
inst_24 : Module R S
inst_25 : Module R P'
inst_26 : Module R Q'
inst_27 : Module R₂ M₂
inst_28 : Module R₂ N₂
inst_29 : Module R₂ P₂
inst_30 : Module R₂ Q₂
inst_31 : Module R₃ M₃
inst_32 : Module R₃ N₃
inst_33 : Module R₃ P₃
inst_34 : Module R₃ Q₃
inst_35 : 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 : SMul R'₂ R'
inst_41 : DistribMulAction R'₂ N
inst_42 : DistribMulAction R' N
inst_43 : CompatibleSMul R R'₂ M N
inst_44 : CompatibleSMul R R' M N
inst_45 : IsScalarTower R'₂ R' N
s : R'₂
r : R'
x : M ⊗[R] N
m : M
n : N
⊢ HSMul.hSMul (β := M ⊗[R] N) (s • r) (m ⊗ₜ[R] n) = s • HSMul.hSMul (β := M ⊗[R] N) r (m ⊗ₜ[R] n)
have rw : m ⊗ₜ[R] ((s • r) • n) = s • HSMul.hSMul (β := M ⊗[R] N) r (m ⊗ₜ[R] n)
Tactic: rw [← tmul_smul, ← tmul_smul, ← tmul_smul, smul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : Monoid R'
inst_4 : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S
inst_10 : AddCommMonoid P'
inst_11 : AddCommMonoid Q'
inst_12 : AddCommMonoid M₂
inst_13 : AddCommMonoid N₂
inst_14 : AddCommMonoid P₂
inst_15 : AddCommMonoid Q₂
inst_16 : AddCommMonoid M₃
inst_17 : AddCommMonoid N₃
inst_18 : AddCommMonoid P₃
inst_19 : AddCommMonoid Q₃
inst_20 : DistribMulAction R' M
inst_21 : Module R'' M
inst_22 : Module R M
inst_23 : Module R N
inst_24 : Module R S
inst_25 : Module R P'
inst_26 : Module R Q'
inst_27 : Module R₂ M₂
inst_28 : Module R₂ N₂
inst_29 : Module R₂ P₂
inst_30 : Module R₂ Q₂
inst_31 : Module R₃ M₃
inst_32 : Module R₃ N₃
inst_33 : Module R₃ P₃
inst_34 : Module R₃ Q₃
inst_35 : 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 : SMul R'₂ R'
inst_41 : DistribMulAction R'₂ N
inst_42 : DistribMulAction R' N
inst_43 : CompatibleSMul R R'₂ M N
inst_44 : CompatibleSMul R R' M N
inst_45 : IsScalarTower R'₂ R' N
s : R'₂
r : R'
x : M ⊗[R] N
m : M
n : N
rw : m ⊗ₜ[R] ((s • r) • n) = s • HSMul.hSMul (β := M ⊗[R] N) r (m ⊗ₜ[R] n)
⊢ HSMul.hSMul (β := M ⊗[R] N) (s • r) (m ⊗ₜ[R] n) = s • HSMul.hSMul (β := M ⊗[R] N) r (m ⊗ₜ[R] n)
have rw₁ : m ⊗ₜ[R] ((s • r) • n) = HSMul.hSMul (β := M ⊗[R] N) s (m ⊗ₜ[R] (r • n))
Tactic: rw [← tmul_smul, ← tmul_smul, ← tmul_smul, smul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : Monoid R'
inst_4 : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S
inst_10 : AddCommMonoid P'
inst_11 : AddCommMonoid Q'
inst_12 : AddCommMonoid M₂
inst_13 : AddCommMonoid N₂
inst_14 : AddCommMonoid P₂
inst_15 : AddCommMonoid Q₂
inst_16 : AddCommMonoid M₃
inst_17 : AddCommMonoid N₃
inst_18 : AddCommMonoid P₃
inst_19 : AddCommMonoid Q₃
inst_20 : DistribMulAction R' M
inst_21 : Module R'' M
inst_22 : Module R M
inst_23 : Module R N
inst_24 : Module R S
inst_25 : Module R P'
inst_26 : Module R Q'
inst_27 : Module R₂ M₂
inst_28 : Module R₂ N₂
inst_29 : Module R₂ P₂
inst_30 : Module R₂ Q₂
inst_31 : Module R₃ M₃
inst_32 : Module R₃ N₃
inst_33 : Module R₃ P₃
inst_34 : Module R₃ Q₃
inst_35 : 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 : SMul R'₂ R'
inst_41 : DistribMulAction R'₂ N
inst_42 : DistribMulAction R' N
inst_43 : CompatibleSMul R R'₂ M N
inst_44 : CompatibleSMul R R' M N
inst_45 : IsScalarTower R'₂ R' N
s : R'₂
r : R'
x : M ⊗[R] N
m : M
n : N
rw : m ⊗ₜ[R] ((s • r) • n) = s • HSMul.hSMul (β := M ⊗[R] N) r (m ⊗ₜ[R] n)
rw₁ : m ⊗ₜ[R] ((s • r) • n) = HSMul.hSMul (β := M ⊗[R] N) s (m ⊗ₜ[R] (r • n))
⊢ HSMul.hSMul (β := M ⊗[R] N) (s • r) (m ⊗ₜ[R] n) = s • HSMul.hSMul (β := M ⊗[R] N) r (m ⊗ₜ[R] n)
have rw₂ : Eq (α := M ⊗[R] N) (m ⊗ₜ[R] ((s • r) • n)) (m ⊗ₜ[R] (s • r • n))
Tactic: rw [← tmul_smul, ← tmul_smul, ← tmul_smul, smul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : Monoid R'
inst_4 : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S
inst_10 : AddCommMonoid P'
inst_11 : AddCommMonoid Q'
inst_12 : AddCommMonoid M₂
inst_13 : AddCommMonoid N₂
inst_14 : AddCommMonoid P₂
inst_15 : AddCommMonoid Q₂
inst_16 : AddCommMonoid M₃
inst_17 : AddCommMonoid N₃
inst_18 : AddCommMonoid P₃
inst_19 : AddCommMonoid Q₃
inst_20 : DistribMulAction R' M
inst_21 : Module R'' M
inst_22 : Module R M
inst_23 : Module R N
inst_24 : Module R S
inst_25 : Module R P'
inst_26 : Module R Q'
inst_27 : Module R₂ M₂
inst_28 : Module R₂ N₂
inst_29 : Module R₂ P₂
inst_30 : Module R₂ Q₂
inst_31 : Module R₃ M₃
inst_32 : Module R₃ N₃
inst_33 : Module R₃ P₃
inst_34 : Module R₃ Q₃
inst_35 : 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 : SMul R'₂ R'
inst_41 : DistribMulAction R'₂ N
inst_42 : DistribMulAction R' N
inst_43 : CompatibleSMul R R'₂ M N
inst_44 : CompatibleSMul R R' M N
inst_45 : IsScalarTower R'₂ R' N
s : R'₂
r : R'
x : M ⊗[R] N
m : M
n : N
rw : m ⊗ₜ[R] ((s • r) • n) = s • HSMul.hSMul (β := M ⊗[R] N) r (m ⊗ₜ[R] n)
rw₁ : m ⊗ₜ[R] ((s • r) • n) = HSMul.hSMul (β := M ⊗[R] N) s (m ⊗ₜ[R] (r • n))
rw₂ : Eq (α := M ⊗[R] N) (m ⊗ₜ[R] ((s • r) • n)) (m ⊗ₜ[R] (s • r • n))
⊢ HSMul.hSMul (β := M ⊗[R] N) (s • r) (m ⊗ₜ[R] n) = s • HSMul.hSMul (β := M ⊗[R] N) r (m ⊗ₜ[R] n)
have rw₃ : Eq (α := M ⊗[R] N) (m ⊗ₜ[R] (s • r • n)) (m ⊗ₜ[R] (s • r • n))
Tactic: rw [← tmul_smul, ← tmul_smul, ← tmul_smul, smul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : Monoid R'
inst_4 : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S
inst_10 : AddCommMonoid P'
inst_11 : AddCommMonoid Q'
inst_12 : AddCommMonoid M₂
inst_13 : AddCommMonoid N₂
inst_14 : AddCommMonoid P₂
inst_15 : AddCommMonoid Q₂
inst_16 : AddCommMonoid M₃
inst_17 : AddCommMonoid N₃
inst_18 : AddCommMonoid P₃
inst_19 : AddCommMonoid Q₃
inst_20 : DistribMulAction R' M
inst_21 : Module R'' M
inst_22 : Module R M
inst_23 : Module R N
inst_24 : Module R S
inst_25 : Module R P'
inst_26 : Module R Q'
inst_27 : Module R₂ M₂
inst_28 : Module R₂ N₂
inst_29 : Module R₂ P₂
inst_30 : Module R₂ Q₂
inst_31 : Module R₃ M₃
inst_32 : Module R₃ N₃
inst_33 : Module R₃ P₃
inst_34 : Module R₃ Q₃
inst_35 : 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 : SMul R'₂ R'
inst_41 : DistribMulAction R'₂ N
inst_42 : DistribMulAction R' N
inst_43 : CompatibleSMul R R'₂ M N
inst_44 : CompatibleSMul R R' M N
inst_45 : IsScalarTower R'₂ R' N
s : R'₂
r : R'
x_1 x y : M ⊗[R] N
ihx : (s • r) • x = s • r • x
ihy : (s • r) • y = s • r • y
⊢ (s • r) • (x + y) = s • r • (x + y)
have rw : (s • r) • x + (s • r) • y = s • r • (x + y)
Tactic: rw [smul_add, smul_add, smul_add, ihx, ihy]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : Monoid R'
inst_4 : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S
inst_10 : AddCommMonoid P'
inst_11 : AddCommMonoid Q'
inst_12 : AddCommMonoid M₂
inst_13 : AddCommMonoid N₂
inst_14 : AddCommMonoid P₂
inst_15 : AddCommMonoid Q₂
inst_16 : AddCommMonoid M₃
inst_17 : AddCommMonoid N₃
inst_18 : AddCommMonoid P₃
inst_19 : AddCommMonoid Q₃
inst_20 : DistribMulAction R' M
inst_21 : Module R'' M
inst_22 : Module R M
inst_23 : Module R N
inst_24 : Module R S
inst_25 : Module R P'
inst_26 : Module R Q'
inst_27 : Module R₂ M₂
inst_28 : Module R₂ N₂
inst_29 : Module R₂ P₂
inst_30 : Module R₂ Q₂
inst_31 : Module R₃ M₃
inst_32 : Module R₃ N₃
inst_33 : Module R₃ P₃
inst_34 : Module R₃ Q₃
inst_35 : 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 : SMul R'₂ R'
inst_41 : DistribMulAction R'₂ N
inst_42 : DistribMulAction R' N
inst_43 : CompatibleSMul R R'₂ M N
inst_44 : CompatibleSMul R R' M N
inst_45 : IsScalarTower R'₂ R' N
s : R'₂
r : R'
x_1 x y : M ⊗[R] N
ihx : (s • r) • x = s • r • x
ihy : (s • r) • y = s • r • y
rw : (s • r) • x + (s • r) • y = s • r • (x + y)
⊢ (s • r) • (x + y) = s • r • (x + y)
have rw₁ : (s • r) • x + (s • r) • y = s • (r • x + r • y)
Tactic: rw [smul_add, smul_add, smul_add, ihx, ihy]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : Monoid R'
inst_4 : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S
inst_10 : AddCommMonoid P'
inst_11 : AddCommMonoid Q'
inst_12 : AddCommMonoid M₂
inst_13 : AddCommMonoid N₂
inst_14 : AddCommMonoid P₂
inst_15 : AddCommMonoid Q₂
inst_16 : AddCommMonoid M₃
inst_17 : AddCommMonoid N₃
inst_18 : AddCommMonoid P₃
inst_19 : AddCommMonoid Q₃
inst_20 : DistribMulAction R' M
inst_21 : Module R'' M
inst_22 : Module R M
inst_23 : Module R N
inst_24 : Module R S
inst_25 : Module R P'
inst_26 : Module R Q'
inst_27 : Module R₂ M₂
inst_28 : Module R₂ N₂
inst_29 : Module R₂ P₂
inst_30 : Module R₂ Q₂
inst_31 : Module R₃ M₃
inst_32 : Module R₃ N₃
inst_33 : Module R₃ P₃
inst_34 : Module R₃ Q₃
inst_35 : 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 : SMul R'₂ R'
inst_41 : DistribMulAction R'₂ N
inst_42 : DistribMulAction R' N
inst_43 : CompatibleSMul R R'₂ M N
inst_44 : CompatibleSMul R R' M N
inst_45 : IsScalarTower R'₂ R' N
s : R'₂
r : R'
x_1 x y : M ⊗[R] N
ihx : (s • r) • x = s • r • x
ihy : (s • r) • y = s • r • y
rw : (s • r) • x + (s • r) • y = s • r • (x + y)
rw₁ : (s • r) • x + (s • r) • y = s • (r • x + r • y)
⊢ (s • r) • (x + y) = s • r • (x + y)
have rw₂ : (s • r) • x + (s • r) • y = s • r • x + s • r • y
Tactic: rw [smul_add, smul_add, smul_add, ihx, ihy]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : Monoid R'
inst_4 : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S
inst_10 : AddCommMonoid P'
inst_11 : AddCommMonoid Q'
inst_12 : AddCommMonoid M₂
inst_13 : AddCommMonoid N₂
inst_14 : AddCommMonoid P₂
inst_15 : AddCommMonoid Q₂
inst_16 : AddCommMonoid M₃
inst_17 : AddCommMonoid N₃
inst_18 : AddCommMonoid P₃
inst_19 : AddCommMonoid Q₃
inst_20 : DistribMulAction R' M
inst_21 : Module R'' M
inst_22 : Module R M
inst_23 : Module R N
inst_24 : Module R S
inst_25 : Module R P'
inst_26 : Module R Q'
inst_27 : Module R₂ M₂
inst_28 : Module R₂ N₂
inst_29 : Module R₂ P₂
inst_30 : Module R₂ Q₂
inst_31 : Module R₃ M₃
inst_32 : Module R₃ N₃
inst_33 : Module R₃ P₃
inst_34 : Module R₃ Q₃
inst_35 : 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 : SMul R'₂ R'
inst_41 : DistribMulAction R'₂ N
inst_42 : DistribMulAction R' N
inst_43 : CompatibleSMul R R'₂ M N
inst_44 : CompatibleSMul R R' M N
inst_45 : IsScalarTower R'₂ R' N
s : R'₂
r : R'
x_1 x y : M ⊗[R] N
ihx : (s • r) • x = s • r • x
ihy : (s • r) • y = s • r • y
rw : (s • r) • x + (s • r) • y = s • r • (x + y)
rw₁ : (s • r) • x + (s • r) • y = s • (r • x + r • y)
rw₂ : (s • r) • x + (s • r) • y = s • r • x + s • r • y
⊢ (s • r) • (x + y) = s • r • (x + y)
have rw₃ : s • r • x + (s • r) • y = s • r • x + s • r • y
Tactic: rw [smul_add, smul_add, smul_add, ihx, ihy]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : Monoid R'
inst_4 : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S
inst_10 : AddCommMonoid P'
inst_11 : AddCommMonoid Q'
inst_12 : AddCommMonoid M₂
inst_13 : AddCommMonoid N₂
inst_14 : AddCommMonoid P₂
inst_15 : AddCommMonoid Q₂
inst_16 : AddCommMonoid M₃
inst_17 : AddCommMonoid N₃
inst_18 : AddCommMonoid P₃
inst_19 : AddCommMonoid Q₃
inst_20 : DistribMulAction R' M
inst_21 : Module R'' M
inst_22 : Module R M
inst_23 : Module R N
inst_24 : Module R S
inst_25 : Module R P'
inst_26 : Module R Q'
inst_27 : Module R₂ M₂
inst_28 : Module R₂ N₂
inst_29 : Module R₂ P₂
inst_30 : Module R₂ Q₂
inst_31 : Module R₃ M₃
inst_32 : Module R₃ N₃
inst_33 : Module R₃ P₃
inst_34 : Module R₃ Q₃
inst_35 : 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 : SMul R'₂ R'
inst_41 : DistribMulAction R'₂ N
inst_42 : DistribMulAction R' N
inst_43 : CompatibleSMul R R'₂ M N
inst_44 : CompatibleSMul R R' M N
inst_45 : IsScalarTower R'₂ R' N
s : R'₂
r : R'
x_1 x y : M ⊗[R] N
ihx : (s • r) • x = s • r • x
ihy : (s • r) • y = s • r • y
rw : (s • r) • x + (s • r) • y = s • r • (x + y)
rw₁ : (s • r) • x + (s • r) • y = s • (r • x + r • y)
rw₂ : (s • r) • x + (s • r) • y = s • r • x + s • r • y
rw₃ : s • r • x + (s • r) • y = s • r • x + s • r • y
⊢ (s • r) • (x + y) = s • r • (x + y)
have rw₄ : s • r • x + s • r • y = s • r • x + s • r • y
Tactic: rw [smul_add, smul_add, smul_add, ihx, ihy]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : Monoid R'
inst_4 : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S
inst_10 : AddCommMonoid P'
inst_11 : AddCommMonoid Q'
inst_12 : AddCommMonoid M₂
inst_13 : AddCommMonoid N₂
inst_14 : AddCommMonoid P₂
inst_15 : AddCommMonoid Q₂
inst_16 : AddCommMonoid M₃
inst_17 : AddCommMonoid N₃
inst_18 : AddCommMonoid P₃
inst_19 : AddCommMonoid Q₃
inst_20 : DistribMulAction R' M
inst_21 : Module R'' M
inst_22 : Module R M
inst_23 : Module R N
inst_24 : Module R S
inst_25 : Module R P'
inst_26 : Module R Q'
inst_27 : Module R₂ M₂
inst_28 : Module R₂ N₂
inst_29 : Module R₂ P₂
inst_30 : Module R₂ Q₂
inst_31 : Module R₃ M₃
inst_32 : Module R₃ N₃
inst_33 : Module R₃ P₃
inst_34 : Module R₃ Q₃
inst_35 : SMulCommClass R R' M
inst_36 : SMulCommClass R R'' M
c : R
m : M
n : N
simp_rw simp_rw₁ : (c • m) ⊗ₜ[R] n = HSMul.hSMul (β := M ⊗[R] N) c (m ⊗ₜ[R] n)
⊢ (fun (x1 : M) (x2 : N) ↦ (x1 ⊗ₜ[R] x2 : M ⊗[R] N)) (c • m) n =
    HSMul.hSMul (β := M ⊗[R] N) c ((fun (x1 : M) (x2 : N) ↦ (x1 ⊗ₜ[R] x2 : M ⊗[R] N)) m n)
have simp_rw₂ : m ⊗ₜ[R] (c • n) = HSMul.hSMul (β := M ⊗[R] N) c (m ⊗ₜ[R] n)
Tactic: simp_rw [smul_tmul, tmul_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x₁ : M
x₂ : N
P : Prop
inst_5 : Decidable P
⊢ Eq (α := M ⊗[R] N) ((if P then x₁ else 0) ⊗ₜ[R] x₂) (if P then x₁ ⊗ₜ[R] x₂ else 0)
have pos : P → Eq (α := M ⊗[R] N) (x₁ ⊗ₜ[R] x₂) (x₁ ⊗ₜ[R] x₂)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x₁ : M
x₂ : N
P : Prop
inst_5 : Decidable P
pos : P → Eq (α := M ⊗[R] N) (x₁ ⊗ₜ[R] x₂) (x₁ ⊗ₜ[R] x₂)
⊢ Eq (α := M ⊗[R] N) ((if P then x₁ else 0) ⊗ₜ[R] x₂) (if P then x₁ ⊗ₜ[R] x₂ else 0)
have neg : ¬P → Eq (α := M ⊗[R] N) (0 ⊗ₜ[R] x₂) 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x₁ : M
x₂ : N
P : Prop
inst_5 : Decidable P
⊢ Eq (α := M ⊗[R] N) (x₁ ⊗ₜ[R] if P then x₂ else 0) (if P then x₁ ⊗ₜ[R] x₂ else 0)
have pos : P → Eq (α := M ⊗[R] N) (x₁ ⊗ₜ[R] x₂) (x₁ ⊗ₜ[R] x₂)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x₁ : M
x₂ : N
P : Prop
inst_5 : Decidable P
pos : P → Eq (α := M ⊗[R] N) (x₁ ⊗ₜ[R] x₂) (x₁ ⊗ₜ[R] x₂)
⊢ Eq (α := M ⊗[R] N) (x₁ ⊗ₜ[R] if P then x₂ else 0) (if P then x₁ ⊗ₜ[R] x₂ else 0)
have neg : ¬P → Eq (α := M ⊗[R] N) (x₁ ⊗ₜ[R] 0) 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_8
inst_1 : AddCommMonoid N
inst_2 : Module R N
ι : Type u_22
inst_3 : DecidableEq ι
M : ι → Type u_23
inst_4 : (i : ι) → AddCommMonoid (M i)
inst_5 : (i : ι) → Module.{u_1, u_23} R (M i)
i : ι
x : N
m : M i
j : ι
⊢ Eq (α := TensorProduct.{u_1, u_8, u_23} R N (M j)) (x ⊗ₜ[R] Pi.single (M := M) i m j)
    (Pi.single (M := fun (i : ι) ↦ TensorProduct.{u_1, u_8, u_23} R N (M i)) i
      (x ⊗ₜ[R] m : TensorProduct.{u_1, u_8, u_23} R N (M i)) j)
have pos : ∀ (h : i = j),
  Eq (α := TensorProduct.{u_1, u_8, u_23} R N (M j)) (x ⊗ₜ[R] Pi.single (M := M) i m j)
    (Pi.single (M := fun (i : ι) ↦ TensorProduct.{u_1, u_8, u_23} R N (M i)) i
      (x ⊗ₜ[R] m : TensorProduct.{u_1, u_8, u_23} R N (M i)) j)
Tactic: by_cases h : i = j