-- Mathlib/GroupTheory/Sylow.lean
theorem normal_of_all_max_subgroups_normal [Finite G]
    (hnc : ∀ H : Subgroup G, IsCoatom H → H.Normal) {p : ℕ} [Fact p.Prime] [Finite (Sylow p G)]
    (P : Sylow p G) : P.Normal :=
  normalizer_eq_top_iff.mp
    (by
      rcases eq_top_or_exists_le_coatom P.normalizer with (heq | ⟨K, hK, hNK⟩)
      · exact heq
      · haveI := hnc _ hK
        have hPK : P ≤ K := le_trans le_normalizer hNK
        refine (hK.1 ?_).elim
        rw [← sup_of_le_right hNK, P.normalizer_sup_eq_top' hPK])

Proof state:
case inr.intro.intro
G : Type u
inst✝³ : Group G
inst✝² : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
K : Subgroup G
hK : IsCoatom K
hNK : (↑P).normalizer ≤ K
this : K.Normal
hPK : ↑P ≤ K
⊢ K = ⊤

Tactic:
rw [← sup_of_le_right hNK, P.normalizer_sup_eq_top' hPK]

Result:
no goals

Proof state:
case inr.intro.intro
G : Type u
inst✝³ : Group G
inst✝² : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
K : Subgroup G
hK : IsCoatom K
hNK : (↑P).normalizer ≤ K
this : K.Normal
hPK : ↑P ≤ K
⊢ (↑P).normalizer = ⊤

Tactic:
refine (hK.1 ?_).elim

Result:
case inr.intro.intro
G : Type u
inst✝³ : Group G
inst✝² : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
K : Subgroup G
hK : IsCoatom K
hNK : (↑P).normalizer ≤ K
this : K.Normal
hPK : ↑P ≤ K
⊢ K = ⊤

Proof state:
case inr.intro.intro
G : Type u
inst✝³ : Group G
inst✝² : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
K : Subgroup G
hK : IsCoatom K
hNK : (↑P).normalizer ≤ K
this : K.Normal
⊢ (↑P).normalizer = ⊤

Tactic:
have hPK : P ≤ K := le_trans le_normalizer hNK

Result:
case inr.intro.intro
G : Type u
inst✝³ : Group G
inst✝² : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
K : Subgroup G
hK : IsCoatom K
hNK : (↑P).normalizer ≤ K
this : K.Normal
hPK : ↑P ≤ K
⊢ (↑P).normalizer = ⊤

Proof state:
case inl
G : Type u
inst✝³ : Group G
inst✝² : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
heq : (↑P).normalizer = ⊤
⊢ (↑P).normalizer = ⊤

Tactic:
exact heq

Result:
no goals

Proof state:
case inr.intro.intro
G : Type u
inst✝³ : Group G
inst✝² : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
K : Subgroup G
hK : IsCoatom K
hNK : (↑P).normalizer ≤ K
⊢ (↑P).normalizer = ⊤

Tactic:
haveI := hnc _ hK

Result:
case inr.intro.intro
G : Type u
inst✝³ : Group G
inst✝² : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
K : Subgroup G
hK : IsCoatom K
hNK : (↑P).normalizer ≤ K
this : K.Normal
⊢ (↑P).normalizer = ⊤

Proof state:
G : Type u
inst✝³ : Group G
inst✝² : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
⊢ (↑P).normalizer = ⊤

Tactic:
rcases eq_top_or_exists_le_coatom P.normalizer with (heq | ⟨K, hK, hNK⟩)

Result:
case inl
G : Type u
inst✝³ : Group G
inst✝² : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
heq : (↑P).normalizer = ⊤
⊢ (↑P).normalizer = ⊤

case inr.intro.intro
G : Type u
inst✝³ : Group G
inst✝² : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
K : Subgroup G
hK : IsCoatom K
hNK : (↑P).normalizer ≤ K
⊢ (↑P).normalizer = ⊤