-- Mathlib/GroupTheory/Nilpotent.lean
theorem IsPGroup.isNilpotent [Finite G] {p : ℕ} [hp : Fact (Nat.Prime p)] (h : IsPGroup p G) :
    IsNilpotent G

Proof state:
case intro.hstep
G✝ : Type u_1
inst✝² : Finite G✝
p : ℕ
hp : Fact (Nat.Prime p)
val✝ : Fintype G✝
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Nontrivial G
ih : ∀ (β : Type u_1) [inst : Fintype β], card β < card G → ∀ [hG : Group β], IsPGroup p β → IsNilpotent β
hG✝ : Group G
h : IsPGroup p G
hcq : card (G ⧸ center G) < card G
⊢ IsNilpotent G

Tactic:
have hnq : IsNilpotent (G ⧸ center G) := ih _ hcq (h.to_quotient (center G))

Result:
case intro.hstep
G✝ : Type u_1
inst✝² : Finite G✝
p : ℕ
hp : Fact (Nat.Prime p)
val✝ : Fintype G✝
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Nontrivial G
ih : ∀ (β : Type u_1) [inst : Fintype β], card β < card G → ∀ [hG : Group β], IsPGroup p β → IsNilpotent β
hG✝ : Group G
h : IsPGroup p G
hcq : card (G ⧸ center G) < card G
hnq : IsNilpotent (G ⧸ center G)
⊢ IsNilpotent G

Proof state:
G✝ : Type u_1
inst✝² : Finite G✝
p : ℕ
hp : Fact (Nat.Prime p)
val✝ : Fintype G✝
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Nontrivial G
ih : ∀ (β : Type u_1) [inst : Fintype β], card β < card G → ∀ [hG : Group β], IsPGroup p β → IsNilpotent β
hG✝ : Group G
h : IsPGroup p G
⊢ Nat.card (G ⧸ center G) < Nat.card (G ⧸ center G) * Nat.card ↥(center G)

Tactic:
simp only [Nat.card_eq_fintype_card]

Result:
G✝ : Type u_1
inst✝² : Finite G✝
p : ℕ
hp : Fact (Nat.Prime p)
val✝ : Fintype G✝
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Nontrivial G
ih : ∀ (β : Type u_1) [inst : Fintype β], card β < card G → ∀ [hG : Group β], IsPGroup p β → IsNilpotent β
hG✝ : Group G
h : IsPGroup p G
⊢ card (G ⧸ center G) < card (G ⧸ center G) * card ↥(center G)

Proof state:
G✝ : Type u_1
inst✝² : Finite G✝
p : ℕ
hp : Fact (Nat.Prime p)
val✝ : Fintype G✝
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Nontrivial G
ih : ∀ (β : Type u_1) [inst : Fintype β], card β < card G → ∀ [hG : Group β], IsPGroup p β → IsNilpotent β
hG✝ : Group G
h : IsPGroup p G
⊢ Nat.card (G ⧸ center G) < Nat.card G

Tactic:
rw [card_eq_card_quotient_mul_card_subgroup (center G)]

Result:
G✝ : Type u_1
inst✝² : Finite G✝
p : ℕ
hp : Fact (Nat.Prime p)
val✝ : Fintype G✝
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Nontrivial G
ih : ∀ (β : Type u_1) [inst : Fintype β], card β < card G → ∀ [hG : Group β], IsPGroup p β → IsNilpotent β
hG✝ : Group G
h : IsPGroup p G
⊢ Nat.card (G ⧸ center G) < Nat.card (G ⧸ center G) * Nat.card ↥(center G)

Proof state:
case intro
G : Type u_1
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
val✝ : Fintype G
⊢ ∀ [hG : Group G], IsPGroup p G → IsNilpotent G

Tactic:
apply @Fintype.induction_subsingleton_or_nontrivial _ G _

Result:
case intro.hbase
G : Type u_1
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
val✝ : Fintype G
⊢ ∀ (α : Type u_1) [inst : Fintype α] [inst : Subsingleton α] [hG : Group α], IsPGroup p α → IsNilpotent α

case intro.hstep
G : Type u_1
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
val✝ : Fintype G
⊢ ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : Nontrivial α],
    (∀ (β : Type u_1) [inst_2 : Fintype β], card β < card α → ∀ [hG : Group β], IsPGroup p β → IsNilpotent β) →
      ∀ [hG : Group α], IsPGroup p α → IsNilpotent α

Proof state:
case intro.hbase
G : Type u_1
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
val✝ : Fintype G
⊢ ∀ (α : Type u_1) [inst : Fintype α] [inst : Subsingleton α] [hG : Group α], IsPGroup p α → IsNilpotent α

Tactic:
intro _ _ _ _

Result:
case intro.hbase
G : Type u_1
inst✝² : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
val✝ : Fintype G
α✝ : Type u_1
inst✝¹ : Fintype α✝
inst✝ : Subsingleton α✝
hG✝ : Group α✝
⊢ IsPGroup p α✝ → IsNilpotent α✝

Proof state:
case intro
G : Type u_1
hG : Group G
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
h : IsPGroup p G
val✝ : Fintype G
⊢ IsNilpotent G

Tactic:
revert hG

Result:
case intro
G : Type u_1
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
val✝ : Fintype G
⊢ ∀ [hG : Group G], IsPGroup p G → IsNilpotent G

Proof state:
case intro.hbase
G : Type u_1
inst✝² : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
val✝ : Fintype G
α✝ : Type u_1
inst✝¹ : Fintype α✝
inst✝ : Subsingleton α✝
hG✝ : Group α✝
⊢ IsPGroup p α✝ → IsNilpotent α✝

Tactic:
infer_instance

Result:
no goals

Proof state:
case h
G✝ : Type u_1
inst✝² : Finite G✝
p : ℕ
hp : Fact (Nat.Prime p)
val✝ : Fintype G✝
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Nontrivial G
ih : ∀ (β : Type u_1) [inst : Fintype β], card β < card G → ∀ [hG : Group β], IsPGroup p β → IsNilpotent β
hG✝ : Group G
h : IsPGroup p G
⊢ 1 < card ↥(center G)

Tactic:
simp only [← Nat.card_eq_fintype_card]

Result:
case h
G✝ : Type u_1
inst✝² : Finite G✝
p : ℕ
hp : Fact (Nat.Prime p)
val✝ : Fintype G✝
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Nontrivial G
ih : ∀ (β : Type u_1) [inst : Fintype β], card β < card G → ∀ [hG : Group β], IsPGroup p β → IsNilpotent β
hG✝ : Group G
h : IsPGroup p G
⊢ 1 < Nat.card ↥(center G)

Proof state:
G✝ : Type u_1
inst✝² : Finite G✝
p : ℕ
hp : Fact (Nat.Prime p)
val✝ : Fintype G✝
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Nontrivial G
ih : ∀ (β : Type u_1) [inst : Fintype β], card β < card G → ∀ [hG : Group β], IsPGroup p β → IsNilpotent β
hG✝ : Group G
h : IsPGroup p G
⊢ card (G ⧸ center G) < card G

Tactic:
simp only [← Nat.card_eq_fintype_card]

Result:
G✝ : Type u_1
inst✝² : Finite G✝
p : ℕ
hp : Fact (Nat.Prime p)
val✝ : Fintype G✝
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Nontrivial G
ih : ∀ (β : Type u_1) [inst : Fintype β], card β < card G → ∀ [hG : Group β], IsPGroup p β → IsNilpotent β
hG✝ : Group G
h : IsPGroup p G
⊢ Nat.card (G ⧸ center G) < Nat.card G

Proof state:
case ha
G✝ : Type u_1
inst✝² : Finite G✝
p : ℕ
hp : Fact (Nat.Prime p)
val✝ : Fintype G✝
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Nontrivial G
ih : ∀ (β : Type u_1) [inst : Fintype β], card β < card G → ∀ [hG : Group β], IsPGroup p β → IsNilpotent β
hG✝ : Group G
h : IsPGroup p G
⊢ 0 < card (G ⧸ center G)

Tactic:
exact Fintype.card_pos_iff.mpr One.instNonempty

Result:
no goals

Proof state:
case intro.hstep
G✝ : Type u_1
inst✝² : Finite G✝
p : ℕ
hp : Fact (Nat.Prime p)
val✝ : Fintype G✝
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Nontrivial G
ih : ∀ (β : Type u_1) [inst : Fintype β], card β < card G → ∀ [hG : Group β], IsPGroup p β → IsNilpotent β
hG✝ : Group G
h : IsPGroup p G
hcq : card (G ⧸ center G) < card G
hnq : IsNilpotent (G ⧸ center G)
⊢ IsNilpotent G

Tactic:
exact of_quotient_center_nilpotent hnq

Result:
no goals

Proof state:
case h
G✝ : Type u_1
inst✝² : Finite G✝
p : ℕ
hp : Fact (Nat.Prime p)
val✝ : Fintype G✝
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Nontrivial G
ih : ∀ (β : Type u_1) [inst : Fintype β], card β < card G → ∀ [hG : Group β], IsPGroup p β → IsNilpotent β
hG✝ : Group G
h : IsPGroup p G
⊢ 1 < Nat.card ↥(center G)

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

Result:
no goals

Proof state:
case intro.hstep
G : Type u_1
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
val✝ : Fintype G
⊢ ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : Nontrivial α],
    (∀ (β : Type u_1) [inst_2 : Fintype β], card β < card α → ∀ [hG : Group β], IsPGroup p β → IsNilpotent β) →
      ∀ [hG : Group α], IsPGroup p α → IsNilpotent α

Tactic:
intro G _ _ ih _ h

Result:
case intro.hstep
G✝ : Type u_1
inst✝² : Finite G✝
p : ℕ
hp : Fact (Nat.Prime p)
val✝ : Fintype G✝
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Nontrivial G
ih : ∀ (β : Type u_1) [inst : Fintype β], card β < card G → ∀ [hG : Group β], IsPGroup p β → IsNilpotent β
hG✝ : Group G
h : IsPGroup p G
⊢ IsNilpotent G