Theorem: flatten_ofFinset (Examples.lean)

State before:
atoms : Type u_1
inst✝ : DecidableEq atoms
s : Finset (HFSet atoms)
⊢ flatten (ofFinset s) = Finset.biUnion s fun x => flatten x
Tactic:
rw [flatten, dif_neg] <;> simp [Finset.sup_eq_biUnion]
State after:
no goals