no goals
M : Type u_2
N : Type ?u.14217
G : Type ?u.14220
A : Type ?u.14223
B : Type ?u.14226
α : Type u_1
β : Type ?u.14232
γ : Type ?u.14235
δ : Type ?u.14238
inst✝¹ : SMul M α
p : Prop
inst✝ : Decidable p
a : M
b₁ b₂ : α
⊢ (a • if p then b₁ else b₂) = if p then a • b₁ else a • b₂
split_ifs <;> rfl