p : ℕ
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
inst✝¹ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
hn : 0 < n
inst✝ : Fintype { x // x ∈ center G }
hcG : IsPGroup p { x // x ∈ center G }
⊢ ∃ k, k > 0 ∧ card { x // x ∈ center G } = p ^ k
p : ℕ
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
inst✝¹ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
hn : 0 < n
inst✝ : Fintype { x // x ∈ center G }
⊢ ∃ k, k > 0 ∧ card { x // x ∈ center G } = p ^ k
have hcG := to_subgroup (of_card hGpn) (center G)
p : ℕ
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
inst✝¹ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
hn : 0 < n
inst✝ : Fintype { x // x ∈ center G }
hcG : IsPGroup p { x // x ∈ center G }
x✝ : ∃ n, card { x // x ∈ center G } = p ^ n
⊢ ∃ k, k > 0 ∧ card { x // x ∈ center G } = p ^ k
p : ℕ
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
inst✝¹ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
hn : 0 < n
inst✝ : Fintype { x // x ∈ center G }
hcG : IsPGroup p { x // x ∈ center G }
⊢ ∃ k, k > 0 ∧ card { x // x ∈ center G } = p ^ k
rcases iff_card.1 hcG with _
p : ℕ
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
inst✝¹ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
hn : 0 < n
inst✝ : Fintype { x // x ∈ center G }
hcG : IsPGroup p { x // x ∈ center G }
x✝ : ∃ n, card { x // x ∈ center G } = p ^ n
this : Nontrivial G
⊢ ∃ k, k > 0 ∧ card { x // x ∈ center G } = p ^ k
p : ℕ
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
inst✝¹ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
hn : 0 < n
inst✝ : Fintype { x // x ∈ center G }
hcG : IsPGroup p { x // x ∈ center G }
x✝ : ∃ n, card { x // x ∈ center G } = p ^ n
⊢ ∃ k, k > 0 ∧ card { x // x ∈ center G } = p ^ k
haveI : Nontrivial G := (nontrivial_iff_card <| of_card hGpn).2 ⟨n, hn, hGpn⟩
no goals
p : ℕ
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
inst✝¹ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
hn : 0 < n
inst✝ : Fintype { x // x ∈ center G }
hcG : IsPGroup p { x // x ∈ center G }
x✝ : ∃ n, card { x // x ∈ center G } = p ^ n
this : Nontrivial G
⊢ ∃ k, k > 0 ∧ card { x // x ∈ center G } = p ^ k
exact (nontrivial_iff_card hcG).mp (center_nontrivial (of_card hGpn))