ι : Type ?u.869344
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoidWithZero β
ha : a ∈ s
h : f a = 0
this : DecidableEq α
⊢ ∏ x in s, f x = 0
ι : Type ?u.869344
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoidWithZero β
ha : a ∈ s
h : f a = 0
⊢ ∏ x in s, f x = 0
haveI := Classical.decEq α
no goals
ι : Type ?u.869344
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoidWithZero β
ha : a ∈ s
h : f a = 0
this : DecidableEq α
⊢ ∏ x in s, f x = 0
rw [← prod_erase_mul _ _ ha, h, mul_zero]