∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : OrderBot α] [inst_2 : DecidableEq α] (parts : Finset α)
  (hdisjoint : (↑parts).PairwiseDisjoint id),
  Finpartition.ofPairwiseDisjoint parts hdisjoint =
    { parts := parts.erase ⊥, supIndep := ⋯, sup_parts := ⋯, bot_notMem := ⋯ }