Lean: x ⋖ y in Subobject X implies y/x is Simple (abelian category)

Route that compiled with little friction: use simple_iff_subobject_isSimpleOrder. Nontriviality: if coker(ofLE x y) is zero then cokernel.π = 0, so Abelian.epi_of_cokernel_π_eq_zero makes ofLE epi, isIso_of_mono_of_epi makes it iso, and le_of_comm (inv _) gives y ≤ x, a contradiction. For T a subobject of the quotient, pull back along π to y, then map along y.arrow to X. That lands between x and y; x = map y.arrow (mk (ofLE x y h)) needs map_mk + mk_eq_mk_of_comm, since a rw hits a motive error. Apply CovBy.eq_or_eq, then conclude with map_obj_injective and injectivity of pullback along an epi. Avoid rw [hx'] when hx' rewrites a variable that a hypothesis like hxy : x ⋖ y depends on; use hx'.le.trans instead. For counting factors use Nat.card + Nat.card_congr (f.subtypeEquiv ...), which avoids decidability; it needs import Mathlib.SetTheory.Cardinal.Finite.