case tfae_1_to_2
G : Type u_1
hG : Group G
inst✝ : Fintype G
⊢ Group.IsNilpotent G → NormalizerCondition G

G : Type u_1
hG : Group G
inst✝ : Fintype G
tfae_1_to_2 : Group.IsNilpotent G → NormalizerCondition G
⊢ List.TFAE
    [Group.IsNilpotent G, NormalizerCondition G, ∀ (H : Subgroup G), IsCoatom H → Normal H,
      ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P,
      Nonempty (((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G)]
G : Type u_1
hG : Group G
inst✝ : Fintype G
⊢ List.TFAE
    [Group.IsNilpotent G, NormalizerCondition G, ∀ (H : Subgroup G), IsCoatom H → Normal H,
      ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P,
      Nonempty (((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G)]
tfae_have 1 → 2
case tfae_2_to_3
G : Type u_1
hG : Group G
inst✝ : Fintype G
tfae_1_to_2 : Group.IsNilpotent G → NormalizerCondition G
⊢ NormalizerCondition G → ∀ (H : Subgroup G), IsCoatom H → Normal H

G : Type u_1
hG : Group G
inst✝ : Fintype G
tfae_1_to_2 : Group.IsNilpotent G → NormalizerCondition G
tfae_2_to_3 : NormalizerCondition G → ∀ (H : Subgroup G), IsCoatom H → Normal H
⊢ List.TFAE
    [Group.IsNilpotent G, NormalizerCondition G, ∀ (H : Subgroup G), IsCoatom H → Normal H,
      ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P,
      Nonempty (((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G)]
G : Type u_1
hG : Group G
inst✝ : Fintype G
tfae_1_to_2 : Group.IsNilpotent G → NormalizerCondition G
⊢ List.TFAE
    [Group.IsNilpotent G, NormalizerCondition G, ∀ (H : Subgroup G), IsCoatom H → Normal H,
      ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P,
      Nonempty (((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G)]
tfae_have 2 → 3
case tfae_3_to_4
G : Type u_1
hG : Group G
inst✝ : Fintype G
tfae_1_to_2 : Group.IsNilpotent G → NormalizerCondition G
tfae_2_to_3 : NormalizerCondition G → ∀ (H : Subgroup G), IsCoatom H → Normal H
⊢ (∀ (H : Subgroup G), IsCoatom H → Normal H) → ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P

G : Type u_1
hG : Group G
inst✝ : Fintype G
tfae_1_to_2 : Group.IsNilpotent G → NormalizerCondition G
tfae_2_to_3 : NormalizerCondition G → ∀ (H : Subgroup G), IsCoatom H → Normal H
tfae_3_to_4 : (∀ (H : Subgroup G), IsCoatom H → Normal H) → ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P
⊢ List.TFAE
    [Group.IsNilpotent G, NormalizerCondition G, ∀ (H : Subgroup G), IsCoatom H → Normal H,
      ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P,
      Nonempty (((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G)]
G : Type u_1
hG : Group G
inst✝ : Fintype G
tfae_1_to_2 : Group.IsNilpotent G → NormalizerCondition G
tfae_2_to_3 : NormalizerCondition G → ∀ (H : Subgroup G), IsCoatom H → Normal H
⊢ List.TFAE
    [Group.IsNilpotent G, NormalizerCondition G, ∀ (H : Subgroup G), IsCoatom H → Normal H,
      ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P,
      Nonempty (((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G)]
tfae_have 3 → 4
case tfae_4_to_5
G : Type u_1
hG : Group G
inst✝ : Fintype G
tfae_1_to_2 : Group.IsNilpotent G → NormalizerCondition G
tfae_2_to_3 : NormalizerCondition G → ∀ (H : Subgroup G), IsCoatom H → Normal H
tfae_3_to_4 : (∀ (H : Subgroup G), IsCoatom H → Normal H) → ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P
⊢ (∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P) →
    Nonempty (((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G)

G : Type u_1
hG : Group G
inst✝ : Fintype G
tfae_1_to_2 : Group.IsNilpotent G → NormalizerCondition G
tfae_2_to_3 : NormalizerCondition G → ∀ (H : Subgroup G), IsCoatom H → Normal H
tfae_3_to_4 : (∀ (H : Subgroup G), IsCoatom H → Normal H) → ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P
tfae_4_to_5 :
  (∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P) →
    Nonempty (((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G)
⊢ List.TFAE
    [Group.IsNilpotent G, NormalizerCondition G, ∀ (H : Subgroup G), IsCoatom H → Normal H,
      ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P,
      Nonempty (((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G)]
G : Type u_1
hG : Group G
inst✝ : Fintype G
tfae_1_to_2 : Group.IsNilpotent G → NormalizerCondition G
tfae_2_to_3 : NormalizerCondition G → ∀ (H : Subgroup G), IsCoatom H → Normal H
tfae_3_to_4 : (∀ (H : Subgroup G), IsCoatom H → Normal H) → ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P
⊢ List.TFAE
    [Group.IsNilpotent G, NormalizerCondition G, ∀ (H : Subgroup G), IsCoatom H → Normal H,
      ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P,
      Nonempty (((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G)]
tfae_have 4 → 5
case tfae_5_to_1
G : Type u_1
hG : Group G
inst✝ : Fintype G
tfae_1_to_2 : Group.IsNilpotent G → NormalizerCondition G
tfae_2_to_3 : NormalizerCondition G → ∀ (H : Subgroup G), IsCoatom H → Normal H
tfae_3_to_4 : (∀ (H : Subgroup G), IsCoatom H → Normal H) → ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P
tfae_4_to_5 :
  (∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P) →
    Nonempty (((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G)
⊢ Nonempty (((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G) →
    Group.IsNilpotent G

G : Type u_1
hG : Group G
inst✝ : Fintype G
tfae_1_to_2 : Group.IsNilpotent G → NormalizerCondition G
tfae_2_to_3 : NormalizerCondition G → ∀ (H : Subgroup G), IsCoatom H → Normal H
tfae_3_to_4 : (∀ (H : Subgroup G), IsCoatom H → Normal H) → ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P
tfae_4_to_5 :
  (∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P) →
    Nonempty (((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G)
tfae_5_to_1 :
  Nonempty (((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G) →
    Group.IsNilpotent G
⊢ List.TFAE
    [Group.IsNilpotent G, NormalizerCondition G, ∀ (H : Subgroup G), IsCoatom H → Normal H,
      ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P,
      Nonempty (((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G)]
G : Type u_1
hG : Group G
inst✝ : Fintype G
tfae_1_to_2 : Group.IsNilpotent G → NormalizerCondition G
tfae_2_to_3 : NormalizerCondition G → ∀ (H : Subgroup G), IsCoatom H → Normal H
tfae_3_to_4 : (∀ (H : Subgroup G), IsCoatom H → Normal H) → ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P
tfae_4_to_5 :
  (∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P) →
    Nonempty (((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G)
⊢ List.TFAE
    [Group.IsNilpotent G, NormalizerCondition G, ∀ (H : Subgroup G), IsCoatom H → Normal H,
      ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P,
      Nonempty (((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G)]
tfae_have 5 → 1
no goals
G : Type u_1
hG : Group G
inst✝ : Fintype G
tfae_1_to_2 : Group.IsNilpotent G → NormalizerCondition G
tfae_2_to_3 : NormalizerCondition G → ∀ (H : Subgroup G), IsCoatom H → Normal H
tfae_3_to_4 : (∀ (H : Subgroup G), IsCoatom H → Normal H) → ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P
tfae_4_to_5 :
  (∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P) →
    Nonempty (((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G)
tfae_5_to_1 :
  Nonempty (((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G) →
    Group.IsNilpotent G
⊢ List.TFAE
    [Group.IsNilpotent G, NormalizerCondition G, ∀ (H : Subgroup G), IsCoatom H → Normal H,
      ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P,
      Nonempty (((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G)]
tfae_finish
no goals
case tfae_1_to_2
G : Type u_1
hG : Group G
inst✝ : Fintype G
⊢ Group.IsNilpotent G → NormalizerCondition G
exact @normalizerCondition_of_isNilpotent _ _
no goals
case tfae_2_to_3
G : Type u_1
hG : Group G
inst✝ : Fintype G
tfae_1_to_2 : Group.IsNilpotent G → NormalizerCondition G
⊢ NormalizerCondition G → ∀ (H : Subgroup G), IsCoatom H → Normal H
exact fun h H => NormalizerCondition.normal_of_coatom H h
case tfae_3_to_4
G : Type u_1
hG : Group G
inst✝ : Fintype G
tfae_1_to_2 : Group.IsNilpotent G → NormalizerCondition G
tfae_2_to_3 : NormalizerCondition G → ∀ (H : Subgroup G), IsCoatom H → Normal H
h : ∀ (H : Subgroup G), IsCoatom H → Normal H
p : ℕ
_hp✝ : Fact (Nat.Prime p)
P : Sylow p G
⊢ Normal ↑P
case tfae_3_to_4
G : Type u_1
hG : Group G
inst✝ : Fintype G
tfae_1_to_2 : Group.IsNilpotent G → NormalizerCondition G
tfae_2_to_3 : NormalizerCondition G → ∀ (H : Subgroup G), IsCoatom H → Normal H
⊢ (∀ (H : Subgroup G), IsCoatom H → Normal H) → ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P
intro h p _ P
no goals
case tfae_3_to_4
G : Type u_1
hG : Group G
inst✝ : Fintype G
tfae_1_to_2 : Group.IsNilpotent G → NormalizerCondition G
tfae_2_to_3 : NormalizerCondition G → ∀ (H : Subgroup G), IsCoatom H → Normal H
h : ∀ (H : Subgroup G), IsCoatom H → Normal H
p : ℕ
_hp✝ : Fact (Nat.Prime p)
P : Sylow p G
⊢ Normal ↑P
exact Sylow.normal_of_all_max_subgroups_normal h _
no goals
case tfae_4_to_5
G : Type u_1
hG : Group G
inst✝ : Fintype G
tfae_1_to_2 : Group.IsNilpotent G → NormalizerCondition G
tfae_2_to_3 : NormalizerCondition G → ∀ (H : Subgroup G), IsCoatom H → Normal H
tfae_3_to_4 : (∀ (H : Subgroup G), IsCoatom H → Normal H) → ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P
⊢ (∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P) →
    Nonempty (((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G)
exact fun h => Nonempty.intro (Sylow.directProductOfNormal fun {p hp hP} => h p hp hP)
case tfae_5_to_1.intro
G : Type u_1
hG : Group G
inst✝ : Fintype G
tfae_1_to_2 : Group.IsNilpotent G → NormalizerCondition G
tfae_2_to_3 : NormalizerCondition G → ∀ (H : Subgroup G), IsCoatom H → Normal H
tfae_3_to_4 : (∀ (H : Subgroup G), IsCoatom H → Normal H) → ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P
tfae_4_to_5 :
  (∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P) →
    Nonempty (((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G)
e : ((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G
⊢ Group.IsNilpotent G
case tfae_5_to_1
G : Type u_1
hG : Group G
inst✝ : Fintype G
tfae_1_to_2 : Group.IsNilpotent G → NormalizerCondition G
tfae_2_to_3 : NormalizerCondition G → ∀ (H : Subgroup G), IsCoatom H → Normal H
tfae_3_to_4 : (∀ (H : Subgroup G), IsCoatom H → Normal H) → ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P
tfae_4_to_5 :
  (∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P) →
    Nonempty (((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G)
⊢ Nonempty (((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G) →
    Group.IsNilpotent G
rintro ⟨e⟩
no goals
case tfae_5_to_1.intro
G : Type u_1
hG : Group G
inst✝ : Fintype G
tfae_1_to_2 : Group.IsNilpotent G → NormalizerCondition G
tfae_2_to_3 : NormalizerCondition G → ∀ (H : Subgroup G), IsCoatom H → Normal H
tfae_3_to_4 : (∀ (H : Subgroup G), IsCoatom H → Normal H) → ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P
tfae_4_to_5 :
  (∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P) →
    Nonempty (((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G)
e : ((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G
⊢ Group.IsNilpotent G
exact isNilpotent_of_product_of_sylow_group e