α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
F : Finset (Finset α)
hs : Finset.Nonempty s
⊢ (ofErase {s} (_ : SupIndep {s} id) (_ : sup {s} id = s)).parts = {s}
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
F : Finset (Finset α)
hs : Finset.Nonempty s
⊢ (atomise s ∅).parts = {s}
simp only [atomise, powerset_empty, image_singleton, not_mem_empty, IsEmpty.forall_iff,
  imp_true_iff, filter_True]
no goals
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
F : Finset (Finset α)
hs : Finset.Nonempty s
⊢ (ofErase {s} (_ : SupIndep {s} id) (_ : sup {s} id = s)).parts = {s}
exact erase_eq_of_not_mem (not_mem_singleton.2 hs.ne_empty.symm)