Theorem: HFSet.ofFinset_insert (Hfzfa.lean)

State before:
atoms : Type u_1
inst✝ : DecidableEq atoms
x : HFSet atoms
s : Finset (HFSet atoms)
⊢ ofFinset (insert x s) = insert x (ofFinset s)
Tactic:
ext z <;> simp
State after:
no goals