[GOAL]
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
inst✝³ : (i : ι) → SMul M (α i)
inst✝² : (i : ι) → SMul N (α i)
a✝ : M
i : ι
b✝ : α i
x✝ : (i : ι) × α i
inst✝¹ : SMul M N
inst✝ : ∀ (i : ι), IsScalarTower M N (α i)
a : M
b : N
x : (i : ι) × α i
⊢ (a • b) • x = a • b • x
[PROOFSTEP]
cases x
[GOAL]
case mk
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
inst✝³ : (i : ι) → SMul M (α i)
inst✝² : (i : ι) → SMul N (α i)
a✝ : M
i : ι
b✝ : α i
x : (i : ι) × α i
inst✝¹ : SMul M N
inst✝ : ∀ (i : ι), IsScalarTower M N (α i)
a : M
b : N
fst✝ : ι
snd✝ : α fst✝
⊢ (a • b) • { fst := fst✝, snd := snd✝ } = a • b • { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
rw [smul_mk, smul_mk, smul_mk, smul_assoc]
[GOAL]
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → SMul M (α i)
inst✝¹ : (i : ι) → SMul N (α i)
a✝ : M
i : ι
b✝ : α i
x✝ : (i : ι) × α i
inst✝ : ∀ (i : ι), SMulCommClass M N (α i)
a : M
b : N
x : (i : ι) × α i
⊢ a • b • x = b • a • x
[PROOFSTEP]
cases x
[GOAL]
case mk
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → SMul M (α i)
inst✝¹ : (i : ι) → SMul N (α i)
a✝ : M
i : ι
b✝ : α i
x : (i : ι) × α i
inst✝ : ∀ (i : ι), SMulCommClass M N (α i)
a : M
b : N
fst✝ : ι
snd✝ : α fst✝
⊢ a • b • { fst := fst✝, snd := snd✝ } = b • a • { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
rw [smul_mk, smul_mk, smul_mk, smul_mk, smul_comm]
[GOAL]
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
inst✝³ : (i : ι) → SMul M (α i)
inst✝² : (i : ι) → SMul N (α i)
a✝ : M
i : ι
b : α i
x✝ : (i : ι) × α i
inst✝¹ : (i : ι) → SMul Mᵐᵒᵖ (α i)
inst✝ : ∀ (i : ι), IsCentralScalar M (α i)
a : M
x : (i : ι) × α i
⊢ MulOpposite.op a • x = a • x
[PROOFSTEP]
cases x
[GOAL]
case mk
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
inst✝³ : (i : ι) → SMul M (α i)
inst✝² : (i : ι) → SMul N (α i)
a✝ : M
i : ι
b : α i
x : (i : ι) × α i
inst✝¹ : (i : ι) → SMul Mᵐᵒᵖ (α i)
inst✝ : ∀ (i : ι), IsCentralScalar M (α i)
a : M
fst✝ : ι
snd✝ : α fst✝
⊢ MulOpposite.op a • { fst := fst✝, snd := snd✝ } = a • { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
rw [smul_mk, smul_mk, op_smul_eq_smul]
[GOAL]
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
m : Monoid M
inst✝ : (i : ι) → MulAction M (α i)
x : (i : ι) × α i
⊢ 1 • x = x
[PROOFSTEP]
cases x
[GOAL]
case mk
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
m : Monoid M
inst✝ : (i : ι) → MulAction M (α i)
fst✝ : ι
snd✝ : α fst✝
⊢ 1 • { fst := fst✝, snd := snd✝ } = { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
rw [smul_mk, one_smul]
[GOAL]
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
m : Monoid M
inst✝ : (i : ι) → MulAction M (α i)
a b : M
x : (i : ι) × α i
⊢ (a * b) • x = a • b • x
[PROOFSTEP]
cases x
[GOAL]
case mk
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
m : Monoid M
inst✝ : (i : ι) → MulAction M (α i)
a b : M
fst✝ : ι
snd✝ : α fst✝
⊢ (a * b) • { fst := fst✝, snd := snd✝ } = a • b • { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
rw [smul_mk, smul_mk, smul_mk, mul_smul]
