p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst✝ : Fintype G
hGnt : Nontrivial G
k : ℕ
hk : card G = 1
hk0 : k = 0
⊢ False
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst✝ : Fintype G
hGnt : Nontrivial G
k : ℕ
hk : card G = p ^ k
hk0 : k = 0
⊢ False
rw [hk0, pow_zero] at hk
no goals
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst✝ : Fintype G
hGnt : Nontrivial G
k : ℕ
hk : card G = 1
hk0 : k = 0
⊢ False
exact Fintype.one_lt_card.ne' hk