no goals
α✝ : Type u
β : Type v
γ : Type w
R : Type x
α : Type u_1
inst✝² : MulZeroClass α
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b : α
⊢ (if P ∧ Q then a * b else 0) = (if P then a else 0) * if Q then b else 0
simp only [← ite_and, ite_mul, mul_ite, mul_zero, zero_mul, and_comm]