awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
inst_1 : IsNilpotent G
ih :
  ∀ (H : Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G))),
    normalizer (↑H : Set (G ⧸ center G)) = H → H = ⊤
H : Subgroup G
hH : normalizer (↑H : Set G) = H
hch : center G ≤ H
hkh : MonoidHom.ker (M := HasQuotient.Quotient G (B := Subgroup G) (center G)) (mk' (center G)) ≤ H
hsur :
  Function.Surjective (α := G) (β := HasQuotient.Quotient G (B := Subgroup G) (center G))
    (⇑(mk' (center G)) : (a : G) → G ⧸ center G)
H' : Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G)) := Subgroup.map (mk' (center G)) H
hH' : normalizer (↑H' : Set (G ⧸ center G)) = H'
⊢ Eq (α := Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G))) (Subgroup.map (mk' (center G)) H)
    (Subgroup.map (mk' (center G)) ⊤)

Tactic:
(ih H' hH').trans (symm (map_top_of_surjective _ hsur))

Premises used: Subgroup.map_top_of_surjective, symm, Eq.trans
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
inst_1 : IsNilpotent G
ih :
  ∀ (H : Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G))),
    normalizer (↑H : Set (G ⧸ center G)) = H → H = ⊤
H : Subgroup G
hH : normalizer (↑H : Set G) = H
hch : center G ≤ H
hkh : MonoidHom.ker (M := HasQuotient.Quotient G (B := Subgroup G) (center G)) (mk' (center G)) ≤ H
hsur :
  Function.Surjective (α := G) (β := HasQuotient.Quotient G (B := Subgroup G) (center G))
    (⇑(mk' (center G)) : (a : G) → G ⧸ center G)
H' : Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G)) := Subgroup.map (mk' (center G)) H
hH' : normalizer (↑H' : Set (G ⧸ center G)) = H'
⊢ Eq (α := Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G))) (Subgroup.map (mk' (center G)) H)
    (Subgroup.map (mk' (center G)) ⊤)

Tactic:
exact (ih H' hH').trans (symm (map_top_of_surjective _ hsur))

Premises used: Subgroup.map_top_of_surjective, symm, Eq.trans
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
hG : Group G
inst : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
h : IsPGroup p G
intro : ∀ (val : Fintype G), Group.IsNilpotent G
⊢ Group.IsNilpotent G

Tactic:
cases nonempty_fintype G

Premises used: nonempty_fintype
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
hG : Group G
inst : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
h : IsPGroup p G
val : Fintype G
intro : ∀ [hG : Group G] (h : IsPGroup p G), Group.IsNilpotent G
⊢ Group.IsNilpotent G

Tactic:
revert hG
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
val : Fintype G
intro : ∀ (α : Type u_1) [Fintype α] [Subsingleton α] [hG : Group α] (h : IsPGroup p α), Group.IsNilpotent α
intro₁ :
  ∀ (α : Type u_1) [inst : Fintype α] [Nontrivial α],
    (∀ (β : Type u_1) [inst_2 : Fintype β],
        card β < card α → ∀ [hG : Group β] (h : IsPGroup p β), Group.IsNilpotent β) →
      ∀ [hG : Group α] (h : IsPGroup p α), Group.IsNilpotent α
⊢ ∀ [hG : Group G] (h : IsPGroup p G), Group.IsNilpotent G

Tactic:
apply @Fintype.induction_subsingleton_or_nontrivial _ G _

Premises used: Fintype.induction_subsingleton_or_nontrivial
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
val : Fintype G
α : Type u_1
intro : ∀ [Fintype α] [Subsingleton α] [hG : Group α] (h : IsPGroup p α), Group.IsNilpotent α
⊢ ∀ [Fintype α] [Subsingleton α] [hG : Group α] (h : IsPGroup p α), Group.IsNilpotent α

Tactic:
_
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
val : Fintype G
α : Type u_1
inst_1 : Fintype α
intro : ∀ [Subsingleton α] [hG : Group α] (h : IsPGroup p α), Group.IsNilpotent α
⊢ ∀ [Subsingleton α] [hG : Group α] (h : IsPGroup p α), Group.IsNilpotent α

Tactic:
_
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
val : Fintype G
α : Type u_1
inst_1 : Fintype α
inst_2 : Subsingleton α
intro : ∀ [hG : Group α] (h : IsPGroup p α), Group.IsNilpotent α
⊢ ∀ [hG : Group α] (h : IsPGroup p α), Group.IsNilpotent α

Tactic:
_
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
val : Fintype G
α : Type u_1
inst_1 : Fintype α
inst_2 : Subsingleton α
hG : Group α
⊢ ∀ (h : IsPGroup p α), Group.IsNilpotent α

Tactic:
infer_instance
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G_1 : Type u_1
inst : Finite G_1
p : ℕ
hp : Fact (Nat.Prime p)
val : Fintype G_1
G : Type u_1
intro :
  ∀ [inst : Fintype G] [Nontrivial G],
    (∀ (β : Type u_1) [inst_2 : Fintype β],
        card β < card G → ∀ [hG : Group β] (h : IsPGroup p β), Group.IsNilpotent β) →
      ∀ [hG : Group G] (h : IsPGroup p G), Group.IsNilpotent G
⊢ ∀ [inst : Fintype G] [Nontrivial G],
    (∀ (β : Type u_1) [inst_2 : Fintype β],
        card β < card G → ∀ [hG : Group β] (h : IsPGroup p β), Group.IsNilpotent β) →
      ∀ [hG : Group G] (h : IsPGroup p G), Group.IsNilpotent G

Tactic:
_
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G_1 : Type u_1
inst : Finite G_1
p : ℕ
hp : Fact (Nat.Prime p)
val : Fintype G_1
G : Type u_1
inst_1 : Fintype G
intro :
  ∀ [Nontrivial G],
    (∀ (β : Type u_1) [inst : Fintype β], card β < card G → ∀ [hG : Group β] (h : IsPGroup p β), Group.IsNilpotent β) →
      ∀ [hG : Group G] (h : IsPGroup p G), Group.IsNilpotent G
⊢ ∀ [Nontrivial G],
    (∀ (β : Type u_1) [inst : Fintype β], card β < card G → ∀ [hG : Group β] (h : IsPGroup p β), Group.IsNilpotent β) →
      ∀ [hG : Group G] (h : IsPGroup p G), Group.IsNilpotent G

Tactic:
_
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G_1 : Type u_1
inst : Finite G_1
p : ℕ
hp : Fact (Nat.Prime p)
val : Fintype G_1
G : Type u_1
inst_1 : Fintype G
inst_2 : Nontrivial G
ih : ∀ (β : Type u_1) [inst : Fintype β], card β < card G → ∀ [hG : Group β] (h : IsPGroup p β), Group.IsNilpotent β
intro : ∀ [hG : Group G] (h : IsPGroup p G), Group.IsNilpotent G
⊢ ∀ [hG : Group G] (h : IsPGroup p G), Group.IsNilpotent G

Tactic:
_
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G_1 : Type u_1
inst : Finite G_1
p : ℕ
hp : Fact (Nat.Prime p)
val : Fintype G_1
G : Type u_1
inst_1 : Fintype G
inst_2 : Nontrivial G
ih : ∀ (β : Type u_1) [inst : Fintype β], card β < card G → ∀ [hG : Group β] (h : IsPGroup p β), Group.IsNilpotent β
hG : Group G
h : IsPGroup p G
simp : Nat.card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) < Nat.card G
⊢ card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) < card G

Tactic:
simp only [← Nat.card_eq_fintype_card]

Premises used: Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G_1 : Type u_1
inst : Finite G_1
p : ℕ
hp : Fact (Nat.Prime p)
val : Fintype G_1
G : Type u_1
inst_1 : Fintype G
inst_2 : Nontrivial G
ih : ∀ (β : Type u_1) [inst : Fintype β], card β < card G → ∀ [hG : Group β] (h : IsPGroup p β), Group.IsNilpotent β
hG : Group G
h : IsPGroup p G
rw :
  Nat.card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) <
    Nat.card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) * Nat.card.{u_1} ↥(center G)
⊢ Nat.card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) < Nat.card G

Tactic:
rw [card_eq_card_quotient_mul_card_subgroup (center G)]

Premises used: Subgroup.card_eq_card_quotient_mul_card_subgroup, Subgroup.center
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G_1 : Type u_1
inst : Finite G_1
p : ℕ
hp : Fact (Nat.Prime p)
val : Fintype G_1
G : Type u_1
inst_1 : Fintype G
inst_2 : Nontrivial G
ih : ∀ (β : Type u_1) [inst : Fintype β], card β < card G → ∀ [hG : Group β] (h : IsPGroup p β), Group.IsNilpotent β
hG : Group G
h : IsPGroup p G
simp :
  card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) <
    card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) * card.{u_1} ↥(center G)
⊢ Nat.card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) <
    Nat.card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) * Nat.card.{u_1} ↥(center G)

Tactic:
simp only [Nat.card_eq_fintype_card]

Premises used: Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G_1 : Type u_1
inst : Finite G_1
p : ℕ
hp : Fact (Nat.Prime p)
val : Fintype G_1
G : Type u_1
inst_1 : Fintype G
inst_2 : Nontrivial G
ih : ∀ (β : Type u_1) [inst : Fintype β], card β < card G → ∀ [hG : Group β] (h : IsPGroup p β), Group.IsNilpotent β
hG : Group G
h : IsPGroup p G
ha : 0 < card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G))
h₁ : 1 < card.{u_1} ↥(center G)
⊢ card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) <
    card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) * card.{u_1} ↥(center G)

Tactic:
apply lt_mul_of_one_lt_right

Premises used: lt_mul_of_one_lt_right
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G_1 : Type u_1
inst : Finite G_1
p : ℕ
hp : Fact (Nat.Prime p)
val : Fintype G_1
G : Type u_1
inst_1 : Fintype G
inst_2 : Nontrivial G
ih : ∀ (β : Type u_1) [inst : Fintype β], card β < card G → ∀ [hG : Group β] (h : IsPGroup p β), Group.IsNilpotent β
hG : Group G
h : IsPGroup p G
⊢ 0 < card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G))

Tactic:
Fintype.card_pos_iff.mpr One.instNonempty

Premises used: Iff.mpr, One.instNonempty, Fintype.card_pos_iff
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G_1 : Type u_1
inst : Finite G_1
p : ℕ
hp : Fact (Nat.Prime p)
val : Fintype G_1
G : Type u_1
inst_1 : Fintype G
inst_2 : Nontrivial G
ih : ∀ (β : Type u_1) [inst : Fintype β], card β < card G → ∀ [hG : Group β] (h : IsPGroup p β), Group.IsNilpotent β
hG : Group G
h : IsPGroup p G
⊢ 0 < card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G))

Tactic:
exact Fintype.card_pos_iff.mpr One.instNonempty

Premises used: Iff.mpr, One.instNonempty, Fintype.card_pos_iff
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G_1 : Type u_1
inst : Finite G_1
p : ℕ
hp : Fact (Nat.Prime p)
val : Fintype G_1
G : Type u_1
inst_1 : Fintype G
inst_2 : Nontrivial G
ih : ∀ (β : Type u_1) [inst : Fintype β], card β < card G → ∀ [hG : Group β] (h : IsPGroup p β), Group.IsNilpotent β
hG : Group G
h : IsPGroup p G
h₁ : 1 < Nat.card.{u_1} ↥(center G)
⊢ 1 < card.{u_1} ↥(center G)

Tactic:
simp only [← Nat.card_eq_fintype_card]

Premises used: Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G_1 : Type u_1
inst : Finite G_1
p : ℕ
hp : Fact (Nat.Prime p)
val : Fintype G_1
G : Type u_1
inst_1 : Fintype G
inst_2 : Nontrivial G
ih : ∀ (β : Type u_1) [inst : Fintype β], card β < card G → ∀ [hG : Group β] (h : IsPGroup p β), Group.IsNilpotent β
hG : Group G
h : IsPGroup p G
⊢ 1 < Nat.card.{u_1} ↥(center G)

Tactic:
(Subgroup.one_lt_card_iff_ne_bot _).mpr (ne_of_gt h.bot_lt_center)

Premises used: Iff.mpr, Subgroup.one_lt_card_iff_ne_bot, ne_of_gt, IsPGroup.bot_lt_center
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G_1 : Type u_1
inst : Finite G_1
p : ℕ
hp : Fact (Nat.Prime p)
val : Fintype G_1
G : Type u_1
inst_1 : Fintype G
inst_2 : Nontrivial G
ih : ∀ (β : Type u_1) [inst : Fintype β], card β < card G → ∀ [hG : Group β] (h : IsPGroup p β), Group.IsNilpotent β
hG : Group G
h : IsPGroup p G
⊢ 1 < Nat.card.{u_1} ↥(center G)

Tactic:
exact (Subgroup.one_lt_card_iff_ne_bot _).mpr (ne_of_gt h.bot_lt_center)

Premises used: Iff.mpr, Subgroup.one_lt_card_iff_ne_bot, ne_of_gt, IsPGroup.bot_lt_center
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G_1 : Type u_1
inst : Finite G_1
p : ℕ
hp : Fact (Nat.Prime p)
val : Fintype G_1
G : Type u_1
inst_1 : Fintype G
inst_2 : Nontrivial G
ih : ∀ (β : Type u_1) [inst : Fintype β], card β < card G → ∀ [hG : Group β] (h : IsPGroup p β), Group.IsNilpotent β
hG : Group G
h : IsPGroup p G
⊢ card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) < card G

Tactic:
have hcq : Fintype.card (G ⧸ center G) < Fintype.card G := by
        simp only [← Nat.card_eq_fintype_card]
        rw [card_eq_card_quotient_mul_card_subgroup (center G)]
        simp only [Nat.card_eq_fintype_card]
        apply lt_mul_of_one_lt_right
        · exact Fintype.card_pos_iff.mpr One.instNonempty
        · simp only [← Nat.card_eq_fintype_card]
          exact (Subgroup.one_lt_card_iff_ne_bot _).mpr (ne_of_gt h.bot_lt_center)
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G_1 : Type u_1
inst : Finite G_1
p : ℕ
hp : Fact (Nat.Prime p)
val : Fintype G_1
G : Type u_1
inst_1 : Fintype G
inst_2 : Nontrivial G
ih : ∀ (β : Type u_1) [inst : Fintype β], card β < card G → ∀ [hG : Group β] (h : IsPGroup p β), Group.IsNilpotent β
hG : Group G
h : IsPGroup p G
hcq : card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) < card G
⊢ Group.IsNilpotent.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G))

Tactic:
have hnq : IsNilpotent (G ⧸ center G) := ih _ hcq (h.to_quotient (center G))
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G_1 : Type u_1
inst : Finite G_1
p : ℕ
hp : Fact (Nat.Prime p)
val : Fintype G_1
G : Type u_1
inst_1 : Fintype G
inst_2 : Nontrivial G
ih : ∀ (β : Type u_1) [inst : Fintype β], card β < card G → ∀ [hG : Group β] (h : IsPGroup p β), Group.IsNilpotent β
hG : Group G
h : IsPGroup p G
hcq : card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) < card G
hnq : Group.IsNilpotent.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G))
⊢ Group.IsNilpotent G

Tactic:
of_quotient_center_nilpotent hnq

Premises used: Group.of_quotient_center_nilpotent
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G_1 : Type u_1
inst : Finite G_1
p : ℕ
hp : Fact (Nat.Prime p)
val : Fintype G_1
G : Type u_1
inst_1 : Fintype G
inst_2 : Nontrivial G
ih : ∀ (β : Type u_1) [inst : Fintype β], card β < card G → ∀ [hG : Group β] (h : IsPGroup p β), Group.IsNilpotent β
hG : Group G
h : IsPGroup p G
hcq : card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) < card G
hnq : Group.IsNilpotent.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G))
⊢ Group.IsNilpotent G

Tactic:
exact of_quotient_center_nilpotent hnq

Premises used: Group.of_quotient_center_nilpotent
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
hG : Group G
inst : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
h : IsPGroup p G
val : Fintype G
intro : ∀ [hG : Group G] (h : IsPGroup p G), Group.IsNilpotent G
intro₁ : ∀ (α : Type u_1) [Fintype α] [Subsingleton α] [hG : Group α] (h : IsPGroup p α), Group.IsNilpotent α
intro₂ intro₃ :
  ∀ (α : Type u_1) [inst : Fintype α] [Nontrivial α],
    (∀ (β : Type u_1) [inst_2 : Fintype β],
        card β < card α → ∀ [hG : Group β] (h : IsPGroup p β), Group.IsNilpotent β) →
      ∀ [hG : Group α] (h : IsPGroup p α), Group.IsNilpotent α
⊢ Group.IsNilpotent G

Tactic:
classical
    revert hG
    apply @Fintype.induction_subsingleton_or_nontrivial _ G _
    · intro _ _ _ _
      infer_instance
    · intro G _ _ ih _ h
      have hcq : Fintype.card (G ⧸ center G) < Fintype.card G := by
        simp only [← Nat.card_eq_fintype_card]
        rw [card_eq_card_quotient_mul_card_subgroup (center G)]
        simp only [Nat.card_eq_fintype_card]
        apply lt_mul_of_one_lt_right
        · exact Fintype.card_pos_iff.mpr One.instNonempty
        · simp only [← Nat.card_eq_fintype_card]
          exact (Subgroup.one_lt_card_iff_ne_bot _).mpr (ne_of_gt h.bot_lt_center)
      have hnq : IsNilpotent (G ⧸ center G) := ih _ hcq (h.to_quotient (center G))
      exact of_quotient_center_nilpotent hnq

Premises used: Fintype.induction_subsingleton_or_nontrivial
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
hG : Group G
inst : Finite G
e : ((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) ≃* G
ps : Finset ℕ := (Nat.card G).primeFactors
p : ↥ps
P : Sylow (↑p : ℕ) G
⊢ Fact (Nat.Prime (↑p : ℕ))

Tactic:
haveI : Fact (Nat.Prime ↑p) := Fact.mk <| Nat.prime_of_mem_primeFactors p.2
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
hG : Group G
inst : Finite G
e : ((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) ≃* G
ps : Finset ℕ := (Nat.card G).primeFactors
p : ↥ps
P : Sylow (↑p : ℕ) G
this : Fact (Nat.Prime (↑p : ℕ))
⊢ IsNilpotent.{u_1} ↥(↑P : Subgroup G)

Tactic:
P.isPGroup'.isNilpotent

Premises used: Sylow.isPGroup', IsPGroup.isNilpotent
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
hG : Group G
inst : Finite G
e : ((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) ≃* G
ps : Finset ℕ := (Nat.card G).primeFactors
p : ↥ps
P : Sylow (↑p : ℕ) G
this : Fact (Nat.Prime (↑p : ℕ))
⊢ IsNilpotent.{u_1} ↥(↑P : Subgroup G)

Tactic:
exact P.isPGroup'.isNilpotent

Premises used: Sylow.isPGroup', IsPGroup.isNilpotent
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
hG : Group G
inst : Finite G
e : ((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) ≃* G
ps : Finset ℕ := (Nat.card G).primeFactors
⊢ ∀ (p : ↥ps) (P : Sylow (↑p : ℕ) G), IsNilpotent.{u_1} ↥(↑P : Subgroup G)

Tactic:
have : ∀ (p : ps) (P : Sylow p G), IsNilpotent (↑P : Subgroup G) := by
      intro p P
      haveI : Fact (Nat.Prime ↑p) := Fact.mk <| Nat.prime_of_mem_primeFactors p.2
      exact P.isPGroup'.isNilpotent
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
hG : Group G
inst : Finite G
e : ((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) ≃* G
ps : Finset ℕ := (Nat.card G).primeFactors
this : ∀ (p : ↥ps) (P : Sylow (↑p : ℕ) G), IsNilpotent.{u_1} ↥(↑P : Subgroup G)
⊢ IsNilpotent G

Tactic:
nilpotent_of_mulEquiv e

Premises used: Group.nilpotent_of_mulEquiv
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
hG : Group G
inst : Finite G
e : ((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) ≃* G
ps : Finset ℕ := (Nat.card G).primeFactors
this : ∀ (p : ↥ps) (P : Sylow (↑p : ℕ) G), IsNilpotent.{u_1} ↥(↑P : Subgroup G)
⊢ IsNilpotent G

Tactic:
exact nilpotent_of_mulEquiv e

Premises used: Group.nilpotent_of_mulEquiv
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
hG : Group G
inst : Finite G
e : ((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) ≃* G
let let₁ let₂ : IsNilpotent G
let₃ :
  let ps := (Nat.card G).primeFactors;
  ∀ (this : ∀ (p : ↥ps) (P : Sylow (↑p : ℕ) G), IsNilpotent.{u_1} ↥(↑P : Subgroup G)), IsNilpotent G
⊢ IsNilpotent G

Tactic:
classical
    let ps := (Nat.card G).primeFactors
    have : ∀ (p : ps) (P : Sylow p G), IsNilpotent (↑P : Subgroup G) := by
      intro p P
      haveI : Fact (Nat.Prime ↑p) := Fact.mk <| Nat.prime_of_mem_primeFactors p.2
      exact P.isPGroup'.isNilpotent
    exact nilpotent_of_mulEquiv e
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
hG : Group G
inst : Finite G
⊢ IsNilpotent G

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
hG : Group G
inst : Finite G
⊢ NormalizerCondition G

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
hG : Group G
inst : Finite G
⊢ ∀ (a : IsNilpotent G), NormalizerCondition G

Tactic:
1 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
hG : Group G
inst : Finite G
⊢ ∀ (a : IsNilpotent G), NormalizerCondition G

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

Premises used: Group.normalizerCondition_of_isNilpotent
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
hG : Group G
inst : Finite G
tfae_1_to_2 : ∀ (a : IsNilpotent G), NormalizerCondition G
⊢ NormalizerCondition G

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
hG : Group G
inst : Finite G
tfae_1_to_2 : ∀ (a : IsNilpotent G), NormalizerCondition G
⊢ ∀ (H : Subgroup G), IsCoatom H → H.Normal

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
hG : Group G
inst : Finite G
tfae_1_to_2 : ∀ (a : IsNilpotent G), NormalizerCondition G
⊢ ∀ (a : NormalizerCondition G) (H : Subgroup G), IsCoatom H → H.Normal

Tactic:
2 → 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
hG : Group G
inst : Finite G
tfae_1_to_2 : ∀ (a : IsNilpotent G), NormalizerCondition G
⊢ ∀ (a : NormalizerCondition G) (H : Subgroup G), IsCoatom H → H.Normal

Tactic:
tfae_have 2 → 3
  | h, H => NormalizerCondition.normal_of_coatom H h
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
hG : Group G
inst : Finite G
tfae_1_to_2 : ∀ (a : IsNilpotent G), NormalizerCondition G
tfae_2_to_3 : ∀ (a : NormalizerCondition G) (H : Subgroup G), IsCoatom H → H.Normal
⊢ ∀ (H : Subgroup G), IsCoatom H → H.Normal

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
hG : Group G
inst : Finite G
tfae_1_to_2 : ∀ (a : IsNilpotent G), NormalizerCondition G
tfae_2_to_3 : ∀ (a : NormalizerCondition G) (H : Subgroup G), IsCoatom H → H.Normal
⊢ ∀ (p : ℕ) (_hp : Fact (Nat.Prime p)) (P : Sylow p G), (↑P : Subgroup G).Normal

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
hG : Group G
inst : Finite G
tfae_1_to_2 : ∀ (a : IsNilpotent G), NormalizerCondition G
tfae_2_to_3 : ∀ (a : NormalizerCondition G) (H : Subgroup G), IsCoatom H → H.Normal
⊢ ∀ (a : ∀ (H : Subgroup G), IsCoatom H → H.Normal) (p : ℕ) (_hp : Fact (Nat.Prime p)) (P : Sylow p G),
    (↑P : Subgroup G).Normal

Tactic:
3 → 4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
hG : Group G
inst : Finite G
tfae_1_to_2 : ∀ (a : IsNilpotent G), NormalizerCondition G
tfae_2_to_3 : ∀ (a : NormalizerCondition G) (H : Subgroup G), IsCoatom H → H.Normal
⊢ ∀ (a : ∀ (H : Subgroup G), IsCoatom H → H.Normal) (p : ℕ) (_hp : Fact (Nat.Prime p)) (P : Sylow p G),
    (↑P : Subgroup G).Normal

Tactic:
tfae_have 3 → 4
  | h, p, _, P => Sylow.normal_of_all_max_subgroups_normal h _
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
hG : Group G
inst : Finite G
tfae_1_to_2 : ∀ (a : IsNilpotent G), NormalizerCondition G
tfae_2_to_3 : ∀ (a : NormalizerCondition G) (H : Subgroup G), IsCoatom H → H.Normal
tfae_3_to_4 :
  ∀ (a : ∀ (H : Subgroup G), IsCoatom H → H.Normal) (p : ℕ) (_hp : Fact (Nat.Prime p)) (P : Sylow p G),
    (↑P : Subgroup G).Normal
⊢ ∀ (p : ℕ) (_hp : Fact (Nat.Prime p)) (P : Sylow p G), (↑P : Subgroup G).Normal

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
hG : Group G
inst : Finite G
tfae_1_to_2 : ∀ (a : IsNilpotent G), NormalizerCondition G
tfae_2_to_3 : ∀ (a : NormalizerCondition G) (H : Subgroup G), IsCoatom H → H.Normal
tfae_3_to_4 :
  ∀ (a : ∀ (H : Subgroup G), IsCoatom H → H.Normal) (p : ℕ) (_hp : Fact (Nat.Prime p)) (P : Sylow p G),
    (↑P : Subgroup G).Normal
⊢ Nonempty.{u_1 + 1} (((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) ≃* G)

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
hG : Group G
inst : Finite G
tfae_1_to_2 : ∀ (a : IsNilpotent G), NormalizerCondition G
tfae_2_to_3 : ∀ (a : NormalizerCondition G) (H : Subgroup G), IsCoatom H → H.Normal
tfae_3_to_4 :
  ∀ (a : ∀ (H : Subgroup G), IsCoatom H → H.Normal) (p : ℕ) (_hp : Fact (Nat.Prime p)) (P : Sylow p G),
    (↑P : Subgroup G).Normal
⊢ ∀ (a : ∀ (p : ℕ) (_hp : Fact (Nat.Prime p)) (P : Sylow p G), (↑P : Subgroup G).Normal),
    Nonempty.{u_1 + 1} (((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) ≃* G)

Tactic:
4 → 5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false