diff --git a/Mathlib/GroupTheory/PGroup.lean b/Mathlib/GroupTheory/PGroup.lean
index dc5803d822673a..81fa520442bac8 100644
--- a/Mathlib/GroupTheory/PGroup.lean
+++ b/Mathlib/GroupTheory/PGroup.lean
@@ -5,6 +5,7 @@ Authors: Chris Hughes, Thomas Browning
 -/
 module
 
+public import Mathlib.Data.SetLike.Fintype
 public import Mathlib.GroupTheory.Perm.Cycle.Type
 public import Mathlib.GroupTheory.SpecificGroups.Cyclic
 
@@ -392,6 +393,39 @@ end P2comm
 
 end IsPGroup
 
+open Subgroup in
+/-- In an abelian `p`-group (finite or infinite), the maximal subgroups are exactly the subgroups
+of index `p`. Finiteness is unnecessary: for a maximal `M`, the quotient `G ⧸ M` is simple *and
+abelian*, hence `≅ ℤ/q` for a prime `q` (a simple abelian group is automatically finite), and being
+a quotient of a `p`-group forces `q = p`; thus `[G : M] = p`. (This fails for non-abelian infinite
+`p`-groups, e.g. Tarski monsters, whose maximal subgroups have order `p` and infinite index.)
+
+The proof goes `IsCoatom M ↔ IsSimpleGroup (G ⧸ M)` (`CommGroup.isSimpleGroup_iff_isCoatom`), then
+`CommGroup.is_simple_iff_prime_card` turns that into `(Nat.card (G ⧸ M)).Prime`, and
+`IsPGroup.card_eq_or_dvd` (for the `p`-group quotient) forces that prime to be `p`;
+`Subgroup.index_eq_card` converts card to index. -/
+theorem CommGroup.isCoatom_iff_index_eq_prime {G : Type*} [CommGroup G] {p : ℕ} [hp : Fact p.Prime]
+    (hG : IsPGroup p G) (M : Subgroup G) : IsCoatom M ↔ M.index = p := by
+  rw [← CommGroup.isSimpleGroup_iff_isCoatom, CommGroup.is_simple_iff_prime_card,
+    Subgroup.index_eq_card]
+  refine ⟨fun h ↦ ?_, fun h ↦ h ▸ hp.out⟩
+  have h_dvd := (IsPGroup.card_eq_or_dvd (hG.to_quotient M)).resolve_left h.ne_one
+  exact ((Nat.prime_dvd_prime_iff_eq hp.out h).mp h_dvd).symm
+
+open Subgroup in
+/-- A finite non-cyclic abelian `p`-group has two distinct subgroups of index `p`. Contrapositive
+route: if there is at most one index-`p` subgroup then, since maximal subgroups are exactly the
+index-`p` subgroups (`CommGroup.isCoatom_iff_index_eq_prime`), there is at most one maximal
+subgroup, so `G` is cyclic (`isCyclic_of_isCoatom_subsingleton`), contradicting `hnc`. -/
+theorem IsPGroup.exists_index_eq_prime_ne_of_not_isCyclic {G : Type*} [CommGroup G] [Finite G]
+    {p : ℕ} [Fact p.Prime] (hG : IsPGroup p G) (hnc : ¬ IsCyclic G) :
+    ∃ H₁ H₂ : Subgroup G, H₁.index = p ∧ H₂.index = p ∧ H₁ ≠ H₂ := by
+  by_contra hcon
+  push Not at hcon
+  refine hnc (isCyclic_of_isCoatom_subsingleton fun M₁ M₂ hM₁ hM₂ => ?_)
+  exact hcon M₁ M₂ ((CommGroup.isCoatom_iff_index_eq_prime hG M₁).mp hM₁)
+    ((CommGroup.isCoatom_iff_index_eq_prime hG M₂).mp hM₂)
+
 namespace ZModModule
 variable {n : ℕ} {G : Type*} [AddCommGroup G] [Module (ZMod n) G]
 
diff --git a/Mathlib/GroupTheory/QuotientGroup/Basic.lean b/Mathlib/GroupTheory/QuotientGroup/Basic.lean
index 43921ef5032ee4..67d7b833df7b9c 100644
--- a/Mathlib/GroupTheory/QuotientGroup/Basic.lean
+++ b/Mathlib/GroupTheory/QuotientGroup/Basic.lean
@@ -377,6 +377,24 @@ def comapMk'OrderIso (N : Subgroup G) [hn : N.Normal] :
   right_inv := fun ⟨H, hH⟩ => Subtype.ext <| by simpa
   map_rel_iff' := Subgroup.comap_le_comap_of_surjective <| mk'_surjective _
 
+/-- The **correspondence theorem** as an order isomorphism onto the interval `Set.Ici N`.
+
+Compared to `comapMk'OrderIso`, whose codomain is the bare subtype `{H : Subgroup G // N ≤ H}`,
+landing in `Set.Ici N` makes the interval order API available (e.g.
+`Set.isSimpleOrder_Ici_iff_isCoatom`), mirroring the submodule side `Submodule.comapMkQRelIso`. -/
+@[to_additive (attr := simps apply_coe) /-- The **correspondence theorem** as an order isomorphism
+onto the interval `Set.Ici N`.
+
+Compared to `comapMk'AddOrderIso`, whose codomain is the bare subtype
+`{H : AddSubgroup G // N ≤ H}`, landing in `Set.Ici N` makes the interval order API available. -/]
+def comapMk'OrderIso' (N : Subgroup G) [hn : N.Normal] :
+    Subgroup (G ⧸ N) ≃o Set.Ici N where
+  toFun H' := ⟨Subgroup.comap (mk' N) H', le_comap_mk' N _⟩
+  invFun H := Subgroup.map (mk' N) H
+  left_inv H' := Subgroup.map_comap_eq_self <| by simp
+  right_inv := fun ⟨H, hH⟩ => Subtype.ext <| by simpa
+  map_rel_iff' := Subgroup.comap_le_comap_of_surjective <| mk'_surjective _
+
 end CorrespTheorem
 
 section trivial
diff --git a/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean b/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
index a5247cb57e02cb..f6c5608d4a0c64 100644
--- a/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
+++ b/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
@@ -275,6 +275,39 @@ theorem CommGroup.is_simple_iff_prime_card [CommGroup α] : IsSimpleGroup α ↔
 @[deprecated (since := "2025-11-19")]
 alias CommGroup.is_simple_iff_isCyclic_and_prime_card := CommGroup.is_simple_iff_prime_card
 
+open Subgroup in
+/-- A group with at most one maximal subgroup is cyclic. Maximal subgroups are the coatoms
+`IsCoatom (· : Subgroup G)` of the subgroup lattice; only `IsCoatomic (Subgroup G)` is required
+(automatic for finite `G`), with no finiteness, commutativity, or `p`-group hypothesis. -/
+@[to_additive /-- An additive group with at most one maximal subgroup is cyclic. Maximal subgroups
+are the coatoms `IsCoatom (· : AddSubgroup G)` of the subgroup lattice; only
+`IsCoatomic (AddSubgroup G)` is required (automatic for finite `G`), with no finiteness,
+commutativity, or `p`-group hypothesis. -/]
+theorem isCyclic_of_isCoatom_subsingleton {G : Type*} [Group G] [IsCoatomic (Subgroup G)]
+    (h : ∀ M₁ M₂ : Subgroup G, IsCoatom M₁ → IsCoatom M₂ → M₁ = M₂) :
+    IsCyclic G := by
+  rw [isCyclic_iff_exists_zpowers_eq_top]
+  obtain hbot | ⟨M, hM, -⟩ := eq_top_or_exists_le_coatom (⊥ : Subgroup G)
+  · exact ⟨1, eq_top_of_bot_eq_top hbot _⟩
+  · obtain ⟨g, -, hg⟩ := SetLike.exists_of_lt hM.lt_top
+    refine ⟨g, ?_⟩
+    by_contra hne
+    obtain ⟨M', hM', hle⟩ := (eq_top_or_exists_le_coatom (zpowers g)).resolve_left hne
+    exact hg (h M' M hM' hM ▸ hle (mem_zpowers g))
+
+/-- A subgroup of a commutative group is maximal (a coatom in the subgroup lattice) iff the quotient
+by it is simple. Group analogue of `isSimpleModule_iff_isCoatom`. -/
+@[to_additive /-- A subgroup of an additive commutative group is maximal (a coatom in the subgroup
+lattice) iff the quotient by it is simple. Additive group analogue of
+`isSimpleModule_iff_isCoatom`. -/]
+theorem CommGroup.isSimpleGroup_iff_isCoatom {G : Type*} [CommGroup G] {M : Subgroup G} :
+    IsSimpleGroup (G ⧸ M) ↔ IsCoatom M := by
+  rw [← Set.isSimpleOrder_Ici_iff_isCoatom,
+    ← (QuotientGroup.comapMk'OrderIso' M).isSimpleOrder_iff, isSimpleGroup_iff, isSimpleOrder_iff]
+  by_cases hG : Nontrivial (G ⧸ M)
+  · simp [hG, Subgroup.normal_of_isMulCommutative]
+  · simp [hG]
+
 section SpecificInstances
 
 instance : IsAddCyclic ℤ := ⟨1, fun n ↦ ⟨n, by simp only [smul_eq_mul, mul_one]⟩⟩