In the proof of `wellFounded_lt_exact_sequence`, it is implicitly shown that `fun x : α ↦ (x ⊓ z, x ⊔ z)` is StrictMono in a modular lattice, with the lexicographic order on `α × α`. Here we show the stronger result with `α × α` equipped with the product order, and golf the proof.

If `G` is not an abelian group, then `α = Subgroup G` is not necessarily a modular lattice. However, if `z` is a normal subgroup, the result still holds true. We prove a closely related result `strictMono_comap_prod_map` which replaces `inf` with `comap` and `sup` with `map`, so it concerns a function to `Subgroup z × Subgroup (G ⧸ z)` instead. The same result for submodules immediately implies that Noetherian/Artinian are closed under extensions, which is proven in #17425 using `wellFounded_lt/gt_exact_sequence`.

If `z` is not even normal, the function to `Subgroup z × Set (G ⧸ z)` is still StrictMono.

…#17425)

+ Add `isNoetherian/Artinian_iff_submodule_quotient`.

+ Remove unnecessary assumptions from `isArtinian_of_range_eq_ker`, mimicking #12453.

+ Move up two instances `isArtinian_of_quotient_of_artinian` and `isNoetherian_of_finite`.

+ Golf `isNoetherian/Artinian_pi`.

…#17425)

+ Add `isNoetherian/Artinian_iff_submodule_quotient`.

+ Remove unnecessary assumptions from `isArtinian_of_range_eq_ker`, mimicking #12453.

+ Move up two instances `isArtinian_of_quotient_of_artinian` and `isNoetherian_of_finite`.

+ Golf `isNoetherian/Artinian_pi`.