case a
ι : Type u_1
R : Type ?u.6059
M : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
f : Π₀ (x : ι), M
a✝ : ι
⊢ a✝ ∈ (toFinsupp f).support ↔ a✝ ∈ support f
ι : Type u_1
R : Type ?u.6059
M : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
f : Π₀ (x : ι), M
⊢ (toFinsupp f).support = support f
ext
no goals
case a
ι : Type u_1
R : Type ?u.6059
M : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
f : Π₀ (x : ι), M
a✝ : ι
⊢ a✝ ∈ (toFinsupp f).support ↔ a✝ ∈ support f
simp