Theorem: HFSet.toFinset_ofFinset (Hfzfa.lean)

State before:
atoms : Type u_1
inst✝ : DecidableEq atoms
s : HFSet atoms
hs : isAtom s = false
⊢ ofFinset (toFinset s) = s
Tactic:
ext x <;> simp [hs]
State after:
no goals