Theorem: HFSet.mem_ofFinset_iff (Hfzfa.lean)

State before:
atoms : Type u_1
s : Finset (HFSet atoms)
x : HFSet atoms
⊢ x ∈ ofFinset s ↔ x ∈ s
Tactic:
simp [ofFinset]
State after:
no goals