Mathlib: Noetherian objects are a Serre class, via refinements, no modular lattice

In an abelian category, to show X₂ is Noetherian (or Artinian) for an exact X₁ →f X₂ →g X₃ with X₁ and X₃ Noetherian, prove that B ↦ ((Subobject.pullback f).obj B, (Subobject.exists g).obj B) is StrictMono into the product order. Then StrictMono.wellFoundedGT/LT together with the Prod.wellFoundedGT instance finishes. The key step is: B ≤ B' with equal pullback and equal image implies B = B'. Prove it as a chase with Abelian/Refinements.lean. Use surjective_up_to_refinements_of_epi on factorThruImageSubobject, then ShortComplex.Exact.exact_up_to_refinements, plus a helper: if S.Factors (π ≫ f) with π epi then S.Factors f (lift through Abelian.monoIsKernelOfCokernel). Gotchas: exists_eq_imageSubobject and Limits.pullback_factors_iff need import Mathlib.CategoryTheory.Subobject.Limits. Inside namespace CategoryTheory, Prod.fst is the functor, so write _root_.Prod.fst. IsNoetherianObject X is an abbrev for isNoetherianObject.Is X, so rw [is_iff] fails; use isNoetherianObject.is_of_prop / .prop_of_is instead.