no goals
α : Type ?u.1793
β : Type ?u.1796
G : Type ?u.1799
M : Type u
inst✝¹ : MulOneClass M
P : Prop
inst✝ : Decidable P
a b : M
⊢ (if P then a * b else 1) = (if P then a else 1) * if P then b else 1
by_cases h:P <;> simp [h]