case empty
ι : Type ?u.872555
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝² : CommMonoidWithZero β
inst✝¹ : Nontrivial β
inst✝ : NoZeroDivisors β
⊢ ∏ x in ∅, f x = 0 ↔ ∃ a, a ∈ ∅ ∧ f a = 0

case insert
ι : Type ?u.872555
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f g : α → β
inst✝² : CommMonoidWithZero β
inst✝¹ : Nontrivial β
inst✝ : NoZeroDivisors β
a : α
s : Finset α
ha : ¬a ∈ s
ih : ∏ x in s, f x = 0 ↔ ∃ a, a ∈ s ∧ f a = 0
⊢ ∏ x in insert a s, f x = 0 ↔ ∃ a_1, a_1 ∈ insert a s ∧ f a_1 = 0
ι : Type ?u.872555
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝² : CommMonoidWithZero β
inst✝¹ : Nontrivial β
inst✝ : NoZeroDivisors β
⊢ ∏ x in s, f x = 0 ↔ ∃ a, a ∈ s ∧ f a = 0
induction' s using Finset.induction_on with a s ha ih
no goals
case empty
ι : Type ?u.872555
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝² : CommMonoidWithZero β
inst✝¹ : Nontrivial β
inst✝ : NoZeroDivisors β
⊢ ∏ x in ∅, f x = 0 ↔ ∃ a, a ∈ ∅ ∧ f a = 0
exact ⟨Not.elim one_ne_zero, fun ⟨_, H, _⟩ => by simp at H⟩
no goals
ι : Type ?u.872555
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝² : CommMonoidWithZero β
inst✝¹ : Nontrivial β
inst✝ : NoZeroDivisors β
x✝ : ∃ a, a ∈ ∅ ∧ f a = 0
w✝ : α
H : w✝ ∈ ∅
right✝ : f w✝ = 0
⊢ ∏ x in ∅, f x = 0
simp at H
no goals
case insert
ι : Type ?u.872555
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f g : α → β
inst✝² : CommMonoidWithZero β
inst✝¹ : Nontrivial β
inst✝ : NoZeroDivisors β
a : α
s : Finset α
ha : ¬a ∈ s
ih : ∏ x in s, f x = 0 ↔ ∃ a, a ∈ s ∧ f a = 0
⊢ ∏ x in insert a s, f x = 0 ↔ ∃ a_1, a_1 ∈ insert a s ∧ f a_1 = 0
rw [prod_insert ha, mul_eq_zero, exists_mem_insert, ih, ← bex_def]