no goals
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : (i : ι) → β i
s : Multiset ι
h : ∀ (i : ι), i ∈ s ∨ f i = 0
i : ι
H : i ∈ support { toFun := f, support' := Trunc.mk { val := s, property := h } }
⊢ i ∈ Multiset.toFinset (Multiset.toFinset s).val
simpa using (Finset.mem_filter.1 H).1