∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : OrderBot α] [inst_2 : DecidableEq α] {a b : α}
  (P : Finpartition a),
  ∀ x ∈ ↑((Finset.image (fun x => x ⊓ b) P.parts).erase ⊥),
    ∀ y ∈ ↑((Finset.image (fun x => x ⊓ b) P.parts).erase ⊥), x ≠ y → Function.onFun Disjoint id x y