Theorem: Finsupp.ofSupportFinite_support (DividedPowers/PolynomialMap/Coeff.lean)

State before:
ι : Type u_1
α : Type u_2
inst✝ : Zero α
f : ι → α
hf : (Function.support f).Finite
⊢ (ofSupportFinite f hf).support = hf.toFinset
Tactic:
ext
State after:
case a
ι : Type u_1
α : Type u_2
inst✝ : Zero α
f : ι → α
hf : (Function.support f).Finite
a✝ : ι
⊢ a✝ ∈ (ofSupportFinite f hf).support ↔ a✝ ∈ hf.toFinset

State before:
case a
ι : Type u_1
α : Type u_2
inst✝ : Zero α
f : ι → α
hf : (Function.support f).Finite
a✝ : ι
⊢ a✝ ∈ (ofSupportFinite f hf).support ↔ a✝ ∈ hf.toFinset
Tactic:
simp only [Finsupp.ofSupportFinite_coe, Finsupp.mem_support_iff,
  Set.Finite.mem_toFinset, mem_support]
State after:
no goals