-- Mathlib/GroupTheory/Nilpotent.lean
theorem isNilpotent_of_finite_tfae :
    List.TFAE
      [IsNilpotent G, NormalizerCondition G, ∀ H : Subgroup G, IsCoatom H → H.Normal,
        ∀ (p : ℕ) (_hp : Fact p.Prime) (P : Sylow p G), (↑P : Subgroup G).Normal,
        Nonempty
          ((∀ p : (Nat.card G).primeFactors, ∀ P : Sylow p G, (↑P : Subgroup G)) ≃* G)]

Proof state:
G : Type u_1
hG : Group G
inst✝ : Finite G
tfae_1_to_2 : IsNilpotent G → NormalizerCondition G
tfae_2_to_3 : NormalizerCondition G → ∀ (H : Subgroup G), IsCoatom H → H.Normal
⊢ [IsNilpotent G, NormalizerCondition G, ∀ (H : Subgroup G), IsCoatom H → H.Normal,
      ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), (↑P).Normal,
      Nonempty (((p : { x // x ∈ (Nat.card G).primeFactors }) → (P : Sylow (↑p) G) → ↥↑P) ≃* G)].TFAE

Tactic:
tfae_have 3 → 4
| h, p, _, P => Sylow.normal_of_all_max_subgroups_normal h _

Result:
G : Type u_1
hG : Group G
inst✝ : Finite G
tfae_1_to_2 : IsNilpotent G → NormalizerCondition G
tfae_2_to_3 : NormalizerCondition G → ∀ (H : Subgroup G), IsCoatom H → H.Normal
tfae_3_to_4 :
  (∀ (H : Subgroup G), IsCoatom H → H.Normal) → ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), (↑P).Normal
⊢ [IsNilpotent G, NormalizerCondition G, ∀ (H : Subgroup G), IsCoatom H → H.Normal,
      ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), (↑P).Normal,
      Nonempty (((p : { x // x ∈ (Nat.card G).primeFactors }) → (P : Sylow (↑p) G) → ↥↑P) ≃* G)].TFAE

Proof state:
G : Type u_1
hG : Group G
inst✝ : Finite G
⊢ [IsNilpotent G, NormalizerCondition G, ∀ (H : Subgroup G), IsCoatom H → H.Normal,
      ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), (↑P).Normal,
      Nonempty (((p : { x // x ∈ (Nat.card G).primeFactors }) → (P : Sylow (↑p) G) → ↥↑P) ≃* G)].TFAE

Tactic:
tfae_have 1 → 2 := @normalizerCondition_of_isNilpotent _ _

Result:
G : Type u_1
hG : Group G
inst✝ : Finite G
tfae_1_to_2 : IsNilpotent G → NormalizerCondition G
⊢ [IsNilpotent G, NormalizerCondition G, ∀ (H : Subgroup G), IsCoatom H → H.Normal,
      ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), (↑P).Normal,
      Nonempty (((p : { x // x ∈ (Nat.card G).primeFactors }) → (P : Sylow (↑p) G) → ↥↑P) ≃* G)].TFAE

Proof state:
G : Type u_1
hG : Group G
inst✝ : Finite G
tfae_1_to_2 : IsNilpotent G → NormalizerCondition G
tfae_2_to_3 : NormalizerCondition G → ∀ (H : Subgroup G), IsCoatom H → H.Normal
tfae_3_to_4 :
  (∀ (H : Subgroup G), IsCoatom H → H.Normal) → ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), (↑P).Normal
tfae_4_to_5 :
  (∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), (↑P).Normal) →
    Nonempty (((p : { x // x ∈ (Nat.card G).primeFactors }) → (P : Sylow (↑p) G) → ↥↑P) ≃* G)
⊢ [IsNilpotent G, NormalizerCondition G, ∀ (H : Subgroup G), IsCoatom H → H.Normal,
      ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), (↑P).Normal,
      Nonempty (((p : { x // x ∈ (Nat.card G).primeFactors }) → (P : Sylow (↑p) G) → ↥↑P) ≃* G)].TFAE

Tactic:
tfae_have 5 → 1
| ⟨e⟩ => isNilpotent_of_product_of_sylow_group e

Result:
G : Type u_1
hG : Group G
inst✝ : Finite G
tfae_1_to_2 : IsNilpotent G → NormalizerCondition G
tfae_2_to_3 : NormalizerCondition G → ∀ (H : Subgroup G), IsCoatom H → H.Normal
tfae_3_to_4 :
  (∀ (H : Subgroup G), IsCoatom H → H.Normal) → ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), (↑P).Normal
tfae_4_to_5 :
  (∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), (↑P).Normal) →
    Nonempty (((p : { x // x ∈ (Nat.card G).primeFactors }) → (P : Sylow (↑p) G) → ↥↑P) ≃* G)
tfae_5_to_1 : Nonempty (((p : { x // x ∈ (Nat.card G).primeFactors }) → (P : Sylow (↑p) G) → ↥↑P) ≃* G) → IsNilpotent G
⊢ [IsNilpotent G, NormalizerCondition G, ∀ (H : Subgroup G), IsCoatom H → H.Normal,
      ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), (↑P).Normal,
      Nonempty (((p : { x // x ∈ (Nat.card G).primeFactors }) → (P : Sylow (↑p) G) → ↥↑P) ≃* G)].TFAE

Proof state:
G : Type u_1
hG : Group G
inst✝ : Finite G
tfae_1_to_2 : IsNilpotent G → NormalizerCondition G
tfae_2_to_3 : NormalizerCondition G → ∀ (H : Subgroup G), IsCoatom H → H.Normal
tfae_3_to_4 :
  (∀ (H : Subgroup G), IsCoatom H → H.Normal) → ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), (↑P).Normal
⊢ [IsNilpotent G, NormalizerCondition G, ∀ (H : Subgroup G), IsCoatom H → H.Normal,
      ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), (↑P).Normal,
      Nonempty (((p : { x // x ∈ (Nat.card G).primeFactors }) → (P : Sylow (↑p) G) → ↥↑P) ≃* G)].TFAE

Tactic:
tfae_have 4 → 5
| h => Nonempty.intro (Sylow.directProductOfNormal fun {p hp hP} => h p hp hP)

Result:
G : Type u_1
hG : Group G
inst✝ : Finite G
tfae_1_to_2 : IsNilpotent G → NormalizerCondition G
tfae_2_to_3 : NormalizerCondition G → ∀ (H : Subgroup G), IsCoatom H → H.Normal
tfae_3_to_4 :
  (∀ (H : Subgroup G), IsCoatom H → H.Normal) → ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), (↑P).Normal
tfae_4_to_5 :
  (∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), (↑P).Normal) →
    Nonempty (((p : { x // x ∈ (Nat.card G).primeFactors }) → (P : Sylow (↑p) G) → ↥↑P) ≃* G)
⊢ [IsNilpotent G, NormalizerCondition G, ∀ (H : Subgroup G), IsCoatom H → H.Normal,
      ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), (↑P).Normal,
      Nonempty (((p : { x // x ∈ (Nat.card G).primeFactors }) → (P : Sylow (↑p) G) → ↥↑P) ≃* G)].TFAE

Proof state:
G : Type u_1
hG : Group G
inst✝ : Finite G
tfae_1_to_2 : IsNilpotent G → NormalizerCondition G
⊢ [IsNilpotent G, NormalizerCondition G, ∀ (H : Subgroup G), IsCoatom H → H.Normal,
      ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), (↑P).Normal,
      Nonempty (((p : { x // x ∈ (Nat.card G).primeFactors }) → (P : Sylow (↑p) G) → ↥↑P) ≃* G)].TFAE

Tactic:
tfae_have 2 → 3
| h, H => NormalizerCondition.normal_of_coatom H h

Result:
G : Type u_1
hG : Group G
inst✝ : Finite G
tfae_1_to_2 : IsNilpotent G → NormalizerCondition G
tfae_2_to_3 : NormalizerCondition G → ∀ (H : Subgroup G), IsCoatom H → H.Normal
⊢ [IsNilpotent G, NormalizerCondition G, ∀ (H : Subgroup G), IsCoatom H → H.Normal,
      ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), (↑P).Normal,
      Nonempty (((p : { x // x ∈ (Nat.card G).primeFactors }) → (P : Sylow (↑p) G) → ↥↑P) ≃* G)].TFAE

Proof state:
G : Type u_1
hG : Group G
inst✝ : Finite G
tfae_1_to_2 : IsNilpotent G → NormalizerCondition G
tfae_2_to_3 : NormalizerCondition G → ∀ (H : Subgroup G), IsCoatom H → H.Normal
tfae_3_to_4 :
  (∀ (H : Subgroup G), IsCoatom H → H.Normal) → ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), (↑P).Normal
tfae_4_to_5 :
  (∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), (↑P).Normal) →
    Nonempty (((p : { x // x ∈ (Nat.card G).primeFactors }) → (P : Sylow (↑p) G) → ↥↑P) ≃* G)
tfae_5_to_1 : Nonempty (((p : { x // x ∈ (Nat.card G).primeFactors }) → (P : Sylow (↑p) G) → ↥↑P) ≃* G) → IsNilpotent G
⊢ [IsNilpotent G, NormalizerCondition G, ∀ (H : Subgroup G), IsCoatom H → H.Normal,
      ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), (↑P).Normal,
      Nonempty (((p : { x // x ∈ (Nat.card G).primeFactors }) → (P : Sylow (↑p) G) → ↥↑P) ≃* G)].TFAE

Tactic:
tfae_finish

Result:
no goals