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
⊢ Group.IsNilpotent G
G : Type u_1
hG : Group G
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
h : IsPGroup p G
⊢ Group.IsNilpotent G
cases' nonempty_fintype G
case intro
G : Type u_1
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
val✝ : Fintype G
⊢ ∀ [hG : Group G], IsPGroup p G → Group.IsNilpotent G
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
⊢ Group.IsNilpotent G
revert hG
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 α → Group.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 β → Group.IsNilpotent β) →
      ∀ [hG : Group α], IsPGroup p α → Group.IsNilpotent α
case intro
G : Type u_1
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
val✝ : Fintype G
⊢ ∀ [hG : Group G], IsPGroup p G → Group.IsNilpotent G
apply @Fintype.induction_subsingleton_or_nontrivial _ G _
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 α✝ → Group.IsNilpotent α✝
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 α → Group.IsNilpotent α
intro _ _ _ _
no goals
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 α✝ → Group.IsNilpotent α✝
infer_instance
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 β → Group.IsNilpotent β
hG✝ : Group G
h : IsPGroup p G
⊢ Group.IsNilpotent G
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 β → Group.IsNilpotent β) →
      ∀ [hG : Group α], IsPGroup p α → Group.IsNilpotent α
intro G _ _ ih _ h
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 β → Group.IsNilpotent β
hG✝ : Group G
h : IsPGroup p G
hcq : card (G ⧸ center G) < card G
⊢ Group.IsNilpotent G
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 β → Group.IsNilpotent β
hG✝ : Group G
h : IsPGroup p G
⊢ Group.IsNilpotent G
have hcq : Fintype.card (G ⧸ center G) < Fintype.card G := by
  rw [card_eq_card_quotient_mul_card_subgroup (center G)]
  apply lt_mul_of_one_lt_right
  exact Fintype.card_pos_iff.mpr One.nonempty
  exact (Subgroup.one_lt_card_iff_ne_bot _).mpr (ne_of_gt h.bot_lt_center)
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 β → Group.IsNilpotent β
hG✝ : Group G
h : IsPGroup p G
hcq : card (G ⧸ center G) < card G
hnq : Group.IsNilpotent (G ⧸ center G)
⊢ Group.IsNilpotent G
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 β → Group.IsNilpotent β
hG✝ : Group G
h : IsPGroup p G
hcq : card (G ⧸ center G) < card G
⊢ Group.IsNilpotent G
have hnq : IsNilpotent (G ⧸ center G) := ih _ hcq (h.to_quotient (center G))
no goals
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 β → Group.IsNilpotent β
hG✝ : Group G
h : IsPGroup p G
hcq : card (G ⧸ center G) < card G
hnq : Group.IsNilpotent (G ⧸ center G)
⊢ Group.IsNilpotent G
exact of_quotient_center_nilpotent hnq
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 β → Group.IsNilpotent β
hG✝ : Group G
h : IsPGroup p G
⊢ card (G ⧸ center G) < card (G ⧸ center G) * card { x // x ∈ center G }
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 β → Group.IsNilpotent β
hG✝ : Group G
h : IsPGroup p G
⊢ card (G ⧸ center G) < card G
rw [card_eq_card_quotient_mul_card_subgroup (center G)]
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 β → Group.IsNilpotent β
hG✝ : Group G
h : IsPGroup p G
⊢ 0 < card (G ⧸ center G)

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 β → Group.IsNilpotent β
hG✝ : Group G
h : IsPGroup p G
⊢ 1 < card { x // x ∈ center G }
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 β → Group.IsNilpotent β
hG✝ : Group G
h : IsPGroup p G
⊢ card (G ⧸ center G) < card (G ⧸ center G) * card { x // x ∈ center G }
apply lt_mul_of_one_lt_right
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 β → Group.IsNilpotent β
hG✝ : Group G
h : IsPGroup p G
⊢ 1 < card { x // x ∈ center G }
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 β → Group.IsNilpotent β
hG✝ : Group G
h : IsPGroup p G
⊢ 0 < card (G ⧸ center G)

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 β → Group.IsNilpotent β
hG✝ : Group G
h : IsPGroup p G
⊢ 1 < card { x // x ∈ center G }
exact Fintype.card_pos_iff.mpr One.nonempty
no goals
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 β → Group.IsNilpotent β
hG✝ : Group G
h : IsPGroup p G
⊢ 1 < card { x // x ∈ center G }
exact (Subgroup.one_lt_card_iff_ne_bot _).mpr (ne_of_gt h.bot_lt_center)