[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α✝ : Type u_5
β : Type u_6
inst✝⁶ : SMul M α✝
inst✝⁵ : SMul M β
inst✝⁴ : SMul N α✝
inst✝³ : SMul N β
a✝ : M
x : α✝ × β
α : Type u_7
inst✝² : Monoid M
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction M α
a : M
c : β
⊢ a • (0, c) = (0, a • c)
[PROOFSTEP]
rw [Prod.smul_mk, smul_zero]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β✝ : Type u_6
inst✝⁶ : SMul M α
inst✝⁵ : SMul M β✝
inst✝⁴ : SMul N α
inst✝³ : SMul N β✝
a✝ : M
x : α × β✝
β : Type u_7
inst✝² : Monoid M
inst✝¹ : AddMonoid β
inst✝ : DistribMulAction M β
a : M
b : α
⊢ a • (b, 0) = (a • b, 0)
[PROOFSTEP]
rw [Prod.smul_mk, smul_zero]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁷ : SMul M α
inst✝⁶ : SMul M β
inst✝⁵ : SMul N α
inst✝⁴ : SMul N β
a✝ : M
x : α × β
inst✝³ : Pow α E
inst✝² : Pow β E
inst✝¹ : FaithfulSMul M α
inst✝ : Nonempty β
m₁✝ m₂✝ : M
h : ∀ (a : α × β), m₁✝ • a = m₂✝ • a
b : β
a : α
⊢ m₁✝ • a = m₂✝ • a
[PROOFSTEP]
injection h (a, b)
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁷ : SMul M α
inst✝⁶ : SMul M β
inst✝⁵ : SMul N α
inst✝⁴ : SMul N β
a✝ : M
x : α × β
inst✝³ : Pow α E
inst✝² : Pow β E
inst✝¹ : Nonempty α
inst✝ : FaithfulSMul M β
m₁✝ m₂✝ : M
h : ∀ (a : α × β), m₁✝ • a = m₂✝ • a
a : α
b : β
⊢ m₁✝ • b = m₂✝ • b
[PROOFSTEP]
injection h (a, b)
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Mul N
inst✝⁴ : Mul P
inst✝³ : SMul M N
inst✝² : SMul M P
inst✝¹ : SMulCommClass M N N
inst✝ : SMulCommClass M P P
c : M
x y : N × P
⊢ c • x • y = x • c • y
[PROOFSTEP]
simp [smul_def, mul_def, mul_smul_comm]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Mul N
inst✝⁴ : Mul P
inst✝³ : SMul M N
inst✝² : SMul M P
inst✝¹ : IsScalarTower M N N
inst✝ : IsScalarTower M P P
c : M
x y : N × P
⊢ (c • x) • y = c • x • y
[PROOFSTEP]
simp [smul_def, mul_def, smul_mul_assoc]
