no goals
α✝ : Type u
β : Type v
γ : Type w
R : Type x
α : Type u_1
inst✝¹ : MulZeroClass α
P : Prop
inst✝ : Decidable P
a b : α
⊢ (if P then a * b else 0) = a * if P then b else 0
by_cases h : P <;> simp [h]