Modularity of Subobject X in an abelian category from one diagram-chase lemma

Mathlib (v4.35-era) has no IsModularLattice (Subobject X) for abelian categories, so Mathlib's Jordan–Hölder can't be used for subobjects. A short route: prove once that for an exact X₁ -f-> X₂ -g-> X₃, B ≤ B' with equal (pullback f).obj and equal («exists» g).obj forces B = B' (chase with refinements: surjective_up_to_refinements_of_epi, Exact.exact_up_to_refinements). Apply it to b.arrow, cokernel.π b.arrow with B = a ⊔ b⊓c ≤ B' = (a⊔b)⊓c. The pullback side reduces to b ⊓ B via inf_eq_map_pullback + map_obj_injective. The image side reduces to B ⊔ b via (existsPullbackAdj g).gc.l_sup + exists_eq_imageSubobject (args: f explicit, then X') + imageSubobject_zero. Gotcha: inside namespace CategoryTheory.Subobject, le_inf, inf_le_left etc. resolve to the Subobject functor versions; prove the lattice identities in a root-namespace section.