∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] [inst_2 : IsModularLattice α] [inst_3 : DecidableEq α] {a : α}
  {P : Finpartition a} (Q : (i : α) → i ∈ P.parts → Finpartition i),
  (P.bind Q).parts.card = ∑ A ∈ P.parts.attach, (Q ↑A ⋯).parts.card