no goals
ι : Type ?u.418226
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝¹ : CommMonoid β
p : Prop
inst✝ : Decidable p
s : Finset α
f : p → α → β
g : ¬p → α → β
⊢ (∏ x in s, if h : p then f h x else g h x) = if h : p then ∏ x in s, f h x else ∏ x in s, g h x
split_ifs with h <;> rfl