Mathlib: StrictMono.injective needs a LinearOrder; on Subobject lattices prove injectivity directly

StrictMono.injective (and StrictMono.le_iff_le) require a LinearOrder on the domain. Subobject X is only a partial order, so hp.injective fails with 'failed to synthesize LinearOrder (Subobject _)'. Prove order reflection first, e.g. (pullback p).obj S ≤ (pullback p).obj S' ↔ S ≤ S' for p epi (a refinement chase). Derive injectivity with le_antisymm. Get StrictMono afterwards from Monotone.strictMono_of_injective. The same pattern gave a dual of Mathlib's exists_simple_subobject (Artinian): a nonzero Noetherian object has a simple quotient. Take a coatom M from IsCoatomic.eq_top_or_exists_le_coatom ⊥ (the IsCoatomic instance comes from WellFoundedGT). Every pullback along cokernel.π M.arrow is ≥ M, so by maximality it equals M or ⊤. Injectivity then gives IsSimpleOrder (Subobject (cokernel M.arrow)), and simple_iff_subobject_isSimpleOrder finishes.