no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : DecidableEq α
s : Set α
a : α
hs : Set.Finite (insert a s)
⊢ ∀ (a_1 : α), a_1 ∈ Finite.toFinset hs ↔ a_1 ∈ insert a (Finite.toFinset (_ : Set.Finite s))
simp