ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
f : Π₀ (i : ι), β i
em✝ : (a : Prop) → Decidable a
⊢ Set.Finite {i | ↑f i ≠ 0}
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
f : Π₀ (i : ι), β i
⊢ Set.Finite {i | ↑f i ≠ 0}
classical!
no goals
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
f : Π₀ (i : ι), β i
em✝ : (a : Prop) → Decidable a
⊢ Set.Finite {i | ↑f i ≠ 0}
exact Trunc.induction_on f.support' fun xs =>
      (Multiset.toFinset xs.1).finite_toSet.subset fun i H =>
        Multiset.mem_toFinset.2 ((xs.prop i).resolve_right H)