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