∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {a b : α} (P P_1 : Finpartition a) (e_P : P = P_1)
  {parts parts_1 : Finset α} (e_parts : parts = parts_1) (subset : parts ⊆ P.parts) (sup_parts : parts.sup id = b),
  P.ofSubset subset sup_parts = P_1.ofSubset ⋯ ⋯