Theorem: HFSet.ofFinset_toFinset (Hfzfa.lean)

State before:
atoms : Type u_1
inst✝ : DecidableEq atoms
s : Finset (HFSet atoms)
⊢ toFinset (ofFinset s) = s
Tactic:
ext x
State after:
case a
atoms : Type u_1
inst✝ : DecidableEq atoms
s : Finset (HFSet atoms)
x : HFSet atoms
⊢ x ∈ toFinset (ofFinset s) ↔ x ∈ s

State before:
case a
atoms : Type u_1
inst✝ : DecidableEq atoms
s : Finset (HFSet atoms)
x : HFSet atoms
⊢ x ∈ toFinset (ofFinset s) ↔ x ∈ s
Tactic:
simp
State after:
no goals