p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type ?u.345348
inst✝³ : MulAction G α
inst✝² : Fintype α
inst✝¹ : Nontrivial G
inst✝ : Finite G
this : Nontrivial { x // x ∈ Subgroup.center G }
⊢ ⊥ < Subgroup.center G
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type ?u.345348
inst✝³ : MulAction G α
inst✝² : Fintype α
inst✝¹ : Nontrivial G
inst✝ : Finite G
⊢ ⊥ < Subgroup.center G
haveI := center_nontrivial hG
case intro
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type ?u.345348
inst✝³ : MulAction G α
inst✝² : Fintype α
inst✝¹ : Nontrivial G
inst✝ : Finite G
this : Nontrivial { x // x ∈ Subgroup.center G }
val✝ : Fintype G
⊢ ⊥ < Subgroup.center G
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type ?u.345348
inst✝³ : MulAction G α
inst✝² : Fintype α
inst✝¹ : Nontrivial G
inst✝ : Finite G
this : Nontrivial { x // x ∈ Subgroup.center G }
⊢ ⊥ < Subgroup.center G
cases nonempty_fintype G
no goals
case intro
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type ?u.345348
inst✝³ : MulAction G α
inst✝² : Fintype α
inst✝¹ : Nontrivial G
inst✝ : Finite G
this : Nontrivial { x // x ∈ Subgroup.center G }
val✝ : Fintype G
⊢ ⊥ < Subgroup.center G
classical exact
    bot_lt_iff_ne_bot.mpr ((Subgroup.center G).one_lt_card_iff_ne_bot.mp Fintype.one_lt_card)
no goals
case intro
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type ?u.345348
inst✝³ : MulAction G α
inst✝² : Fintype α
inst✝¹ : Nontrivial G
inst✝ : Finite G
this : Nontrivial { x // x ∈ Subgroup.center G }
val✝ : Fintype G
⊢ ⊥ < Subgroup.center G
exact
bot_lt_iff_ne_bot.mpr ((Subgroup.center G).one_lt_card_iff_ne_bot.mp Fintype.one_lt_card)