no goals
M : Type u_2
N : Type ?u.13476
G : Type ?u.13479
A : Type ?u.13482
B : Type ?u.13485
α : Type u_1
β : Type ?u.13491
γ : Type ?u.13494
δ : Type ?u.13497
inst✝¹ : SMul M α
p : Prop
inst✝ : Decidable p
a₁ a₂ : M
b : α
⊢ (if p then a₁ else a₂) • b = if p then a₁ • b else a₂ • b
split_ifs <;> rfl