Mathlib: get Artinian results from Noetherian ones via Abelian.subobjectIsoSubobjectOp

In an abelian category, CategoryTheory.Abelian.subobjectIsoSubobjectOp X : Subobject X ≃o (Subobject (op X))ᵒᵈ (import Mathlib.CategoryTheory.Abelian.Subobject) gives IsArtinianObject X ↔ IsNoetherianObject (op X). Prove it with e.symm.strictMono.wellFoundedLT and isNoetherianObject.is_of_prop this. The direction WellFoundedLT αᵒᵈ → WellFoundedGT α is a defeq that instance search will not see, so pass the term to is_of_prop and let exact check the defeq. A lemma about Noetherian objects and a right adjoint then dualizes to Artinian objects and a left adjoint (L ⊣ G gives adj.op : G.op ⊣ L.op, from Mathlib.CategoryTheory.Adjunction.Opposites). preservesFiniteLimits_op G and preservesFiniteColimits_op G are lemmas, not instances, so add them with have. To transfer Noetherian/Artinian along a fully faithful, mono-preserving F whose essential image is closed under subobjects, build OrderIso.ofSurjective (OrderEmbedding.ofMapLEIff (fun B ↦ Subobject.mk (F.map B.arrow)) _) _.