awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
h : Group.IsNilpotent G
n : ℕ
hn : Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
⊢ IsSolvable G
have h₁ : Eq (α := Subgroup G) (derivedSeries G n) ⊥
Tactic: use n
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
h : Group.IsNilpotent G
n : ℕ
hn : Eq (α := Subgroup G) (lowerCentralSeries G n) ⊥
⊢ Eq (α := Subgroup G) (derivedSeries G n) ⊥
have h₁ : LE.le (α := Subgroup G) (derivedSeries G n) (lowerCentralSeries G n)
Tactic: rw [eq_bot_iff, ← hn]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
h : IsNilpotent G
⊢ NormalizerCondition G
have rw : ∀ (H : Subgroup G), normalizer (↑H : Set G) = H → H = ⊤
Tactic: rw [normalizerCondition_iff_only_full_group_self_normalizing]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
h : IsNilpotent G
⊢ ∀ (H : Subgroup G), normalizer (↑H : Set G) = H → H = ⊤
have hbase : ∀ (G : Type u_1) [inst : Group G] [Subsingleton G] (H : Subgroup G), normalizer (↑H : Set G) = H → H = ⊤
Tactic: apply @nilpotent_center_quotient_ind _ G _ _
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
h : IsNilpotent G
hbase : ∀ (G : Type u_1) [inst : Group G] [Subsingleton G] (H : Subgroup G), normalizer (↑H : Set G) = H → H = ⊤
⊢ ∀ (H : Subgroup G), normalizer (↑H : Set G) = H → H = ⊤
have hstep : ∀ (G : Type u_1) [inst : Group G] [IsNilpotent G],
  (∀ (H : Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G))),
      normalizer (↑H : Set (G ⧸ center G)) = H → H = ⊤) →
    ∀ (H : Subgroup G), normalizer (↑H : Set G) = H → H = ⊤
Tactic: apply @nilpotent_center_quotient_ind _ G _ _
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (hypothesis)
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
⊢ H = ⊤
have hch : center G ≤ H
Tactic: have hch : center G ≤ H := Subgroup.center_le_normalizer H |>.trans (le_of_eq hH)
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (hypothesis)
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
⊢ H = ⊤
have hkh : MonoidHom.ker (M := HasQuotient.Quotient G (B := Subgroup G) (center G)) (mk' (center G)) ≤ H
Tactic: have hkh : (mk' (center G)).ker ≤ H := by simpa using hch
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (hypothesis)
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
⊢ H = ⊤
have hsur : Function.Surjective (α := G) (β := HasQuotient.Quotient G (B := Subgroup G) (center G))
  (⇑(mk' (center G)) : (a : G) → G ⧸ center G)
Tactic: have hsur : Function.Surjective (mk' (center G)) := Quot.mk_surjective
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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
⊢ normalizer (↑H' : Set (G ⧸ center G)) = H'
have a : comap (mk' (center G)) (normalizer (↑H' : Set (G ⧸ center G))) = comap (mk' (center G)) H'
Tactic: apply comap_injective hsur
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (hypothesis)
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
⊢ H = ⊤
have hH' : normalizer (↑H' : Set (G ⧸ center G)) = H'
Tactic: have hH' : normalizer H' = H' := by
      apply comap_injective hsur
      rw [comap_normalizer_eq_of_surjective _ hsur, comap_map_eq_self hkh]
      exact hH
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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'
⊢ H = ⊤
have hstep : Eq (α := Subgroup (HasQuotient.Quotient G (B := Subgroup G) (center G))) (Subgroup.map (mk' (center G)) H)
  (Subgroup.map (mk' (center G)) ⊤)
Tactic: apply map_injective_of_ker_le (mk' (center G)) hkh le_top
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
hG : Group G
inst : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
h : IsPGroup p G
⊢ Group.IsNilpotent G
have intro : ∀ (val : Fintype G), Group.IsNilpotent G
Tactic: cases nonempty_fintype G
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
hG : Group G
inst : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
h : IsPGroup p G
val : Fintype G
⊢ Group.IsNilpotent G
have intro : ∀ [hG : Group G] (h : IsPGroup p G), Group.IsNilpotent G
Tactic: revert hG
Cleared hypotheses: hG, h
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
val : Fintype G
⊢ ∀ [hG : Group G] (h : IsPGroup p G), Group.IsNilpotent G
have intro : ∀ (α : Type u_1) [Fintype α] [Subsingleton α] [hG : Group α] (h : IsPGroup p α), Group.IsNilpotent α
Tactic: apply @Fintype.induction_subsingleton_or_nontrivial _ G _
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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 α
⊢ ∀ [hG : Group G] (h : IsPGroup p G), Group.IsNilpotent G
have 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 α
Tactic: apply @Fintype.induction_subsingleton_or_nontrivial _ G _
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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
have simp : Nat.card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) < Nat.card G
Tactic: simp only [← Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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
⊢ Nat.card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) < Nat.card G
have 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)
Tactic: rw [card_eq_card_quotient_mul_card_subgroup (center G)]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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
⊢ 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)
have 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)
Tactic: simp only [Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) * card.{u_1} ↥(center G)
have ha : 0 < card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G))
Tactic: apply lt_mul_of_one_lt_right
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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))
⊢ 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)
have h₁ : 1 < card.{u_1} ↥(center G)
Tactic: apply lt_mul_of_one_lt_right
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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 < card.{u_1} ↥(center G)
have h₁ : 1 < Nat.card.{u_1} ↥(center G)
Tactic: simp only [← Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (hypothesis)
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
⊢ Group.IsNilpotent G
have hcq : 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)
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (hypothesis)
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 G
have hnq : 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))
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
hG : Group G
inst : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
h : IsPGroup p G
val : Fintype G
⊢ Group.IsNilpotent G
have intro : ∀ [hG : Group G] (h : IsPGroup p G), 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
Cleared hypotheses: hG, h
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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
have intro₁ : ∀ (α : Type u_1) [Fintype α] [Subsingleton α] [hG : Group α] (h : IsPGroup p α), Group.IsNilpotent α
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
Cleared hypotheses: hG, h
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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 α
⊢ Group.IsNilpotent G
have 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 α
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
Cleared hypotheses: hG, h
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (hypothesis)
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)
have this : Fact (Nat.Prime (↑p : ℕ))
Tactic: haveI : Fact (Nat.Prime ↑p) := Fact.mk <| Nat.prime_of_mem_primeFactors p.2
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (hypothesis)
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
⊢ IsNilpotent G
have this : ∀ (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
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
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
⊢ IsNilpotent G
have let₃ : let ps := (Nat.card G).primeFactors;
∀ (this : ∀ (p : ↥ps) (P : Sylow (↑p : ℕ) G), IsNilpotent.{u_1} ↥(↑P : Subgroup 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
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (hypothesis)
Goal:
G : Type u_1
hG : Group G
inst : Finite G
⊢ [IsNilpotent G, NormalizerCondition G, ∀ (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)].TFAE
have tfae_1_to_2 : ∀ (a : IsNilpotent G), NormalizerCondition G
Tactic: tfae_have 1 → 2 := @normalizerCondition_of_isNilpotent _ _
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (hypothesis)
Goal:
G : Type u_1
hG : Group G
inst : Finite G
tfae_1_to_2 : ∀ (a : IsNilpotent G), NormalizerCondition G
⊢ [IsNilpotent G, NormalizerCondition G, ∀ (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)].TFAE
have tfae_2_to_3 : ∀ (a : NormalizerCondition G) (H : Subgroup G), IsCoatom H → H.Normal
Tactic: tfae_have 2 → 3
  | h, H => NormalizerCondition.normal_of_coatom H h
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (hypothesis)
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
⊢ [IsNilpotent G, NormalizerCondition G, ∀ (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)].TFAE
have 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
Tactic: tfae_have 3 → 4
  | h, p, _, P => Sylow.normal_of_all_max_subgroups_normal h _
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (hypothesis)
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
⊢ [IsNilpotent G, NormalizerCondition G, ∀ (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)].TFAE
have tfae_4_to_5 : ∀ (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: tfae_have 4 → 5
  | h => Nonempty.intro (Sylow.directProductOfNormal fun {p hp hP} => h p hp hP)
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (hypothesis)
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
tfae_4_to_5 :
  ∀ (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)
⊢ [IsNilpotent G, NormalizerCondition G, ∀ (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)].TFAE
have tfae_5_to_1 : ∀ (a : Nonempty.{u_1 + 1} (((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) ≃* G)),
  IsNilpotent G
Tactic: tfae_have 5 → 1
  | ⟨e⟩ => isNilpotent_of_product_of_sylow_group e
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommCoprod (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Mul M
inst_1 : Mul N
inst_2 : Semigroup P
f : M →ₙ* P
g : N →ₙ* P
comm : ∀ (m : M) (n : N), Commute.{u_3} (S := P) ((f : (a : M) → P) m : P) ((g : (a : N) → P) n : P)
mn : M × N
⊢ (f.noncommCoprod g comm : (a : M × N) → P) mn =
    HMul.hMul (α := P) (β := P) ((g : (a : N) → P) mn.2 : P) ((f : (a : M) → P) mn.1 : P)
have rw : (f.noncommCoprod g comm : (a : M × N) → P) mn =
  HMul.hMul (α := P) (β := P) ((f : (a : M) → P) mn.1 : P) ((g : (a : N) → P) mn.2 : P)
Tactic: rw [← comm, noncommCoprod_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommCoprod (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Mul M
inst_1 : Mul N
inst_2 : Semigroup P
f : M →ₙ* P
g : N →ₙ* P
comm : ∀ (m : M) (n : N), Commute.{u_3} (S := P) ((f : (a : M) → P) m : P) ((g : (a : N) → P) n : P)
mn : M × N
rw :
  (f.noncommCoprod g comm : (a : M × N) → P) mn =
    HMul.hMul (α := P) (β := P) ((f : (a : M) → P) mn.1 : P) ((g : (a : N) → P) mn.2 : P)
⊢ (f.noncommCoprod g comm : (a : M × N) → P) mn =
    HMul.hMul (α := P) (β := P) ((g : (a : N) → P) mn.2 : P) ((f : (a : M) → P) mn.1 : P)
have rw₁ : HMul.hMul (α := P) (β := P) ((f : (a : M) → P) mn.1 : P) ((g : (a : N) → P) mn.2 : P) =
  HMul.hMul (α := P) (β := P) ((f : (a : M) → P) mn.1 : P) ((g : (a : N) → P) mn.2 : P)
Tactic: rw [← comm, noncommCoprod_apply]