no goals
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
F : Finset (Finset α)
⊢ t ∈ (atomise s F).parts ↔ Finset.Nonempty t ∧ ∃ Q x, filter (fun i => ∀ (u : Finset α), u ∈ F → (u ∈ Q ↔ i ∈ u)) s = t
simp only [atomise, ofErase, bot_eq_empty, mem_erase, mem_image, nonempty_iff_ne_empty,
  mem_singleton, and_comm, mem_powerset, exists_prop]