-- Mathlib/GroupTheory/Frattini.lean
theorem frattini_nilpotent [Finite G] : Group.IsNilpotent (frattini G)

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
⊢ Group.IsNilpotent ↥(frattini G)

Tactic:
have q := (isNilpotent_of_finite_tfae (G := frattini G)).out 0 3

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
q : Group.IsNilpotent ↥(frattini G) ↔ ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p ↥(frattini G)), (↑P).Normal
⊢ Group.IsNilpotent ↥(frattini G)

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
⊢ ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p ↥(frattini G)), (↑P).Normal

Tactic:
intro p p_prime P

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
p_prime : Fact (Nat.Prime p)
P : Sylow p ↥(frattini G)
⊢ (↑P).Normal

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
q : Group.IsNilpotent ↥(frattini G) ↔ ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p ↥(frattini G)), (↑P).Normal
⊢ ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p ↥(frattini G)), (↑P).Normal

Tactic:
clear q

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
⊢ ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p ↥(frattini G)), (↑P).Normal

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
p_prime : Fact (Nat.Prime p)
P : Sylow p ↥(frattini G)
⊢ (↑P).Normal

Tactic:
have frattini_argument := Sylow.normalizer_sup_eq_top P

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
p_prime : Fact (Nat.Prime p)
P : Sylow p ↥(frattini G)
frattini_argument : (map (frattini G).subtype ↑P).normalizer ⊔ frattini G = ⊤
⊢ (↑P).Normal

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
q : Group.IsNilpotent ↥(frattini G) ↔ ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p ↥(frattini G)), (↑P).Normal
⊢ Group.IsNilpotent ↥(frattini G)

Tactic:
rw [q]

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
q : Group.IsNilpotent ↥(frattini G) ↔ ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p ↥(frattini G)), (↑P).Normal
⊢ ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p ↥(frattini G)), (↑P).Normal

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
p_prime : Fact (Nat.Prime p)
P : Sylow p ↥(frattini G)
frattini_argument : (map (frattini G).subtype ↑P).normalizer ⊔ frattini G = ⊤
normalizer_P : (map (frattini G).subtype ↑P).normalizer = ⊤
P_normal_in_G : (map (frattini G).subtype ↑P).Normal
⊢ (↑P).Normal

Tactic:
exact P_normal_in_G.of_map_subtype

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
p_prime : Fact (Nat.Prime p)
P : Sylow p ↥(frattini G)
frattini_argument : (map (frattini G).subtype ↑P).normalizer ⊔ frattini G = ⊤
normalizer_P : (map (frattini G).subtype ↑P).normalizer = ⊤
⊢ (↑P).Normal

Tactic:
have P_normal_in_G : (map (frattini G).subtype P).Normal := normalizer_eq_top_iff.mp normalizer_P

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
p_prime : Fact (Nat.Prime p)
P : Sylow p ↥(frattini G)
frattini_argument : (map (frattini G).subtype ↑P).normalizer ⊔ frattini G = ⊤
normalizer_P : (map (frattini G).subtype ↑P).normalizer = ⊤
P_normal_in_G : (map (frattini G).subtype ↑P).Normal
⊢ (↑P).Normal

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
p_prime : Fact (Nat.Prime p)
P : Sylow p ↥(frattini G)
frattini_argument : (map (frattini G).subtype ↑P).normalizer ⊔ frattini G = ⊤
⊢ (↑P).Normal

Tactic:
have normalizer_P := frattini_nongenerating frattini_argument

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
p_prime : Fact (Nat.Prime p)
P : Sylow p ↥(frattini G)
frattini_argument : (map (frattini G).subtype ↑P).normalizer ⊔ frattini G = ⊤
normalizer_P : (map (frattini G).subtype ↑P).normalizer = ⊤
⊢ (↑P).Normal