case inl
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
val✝ : Fintype G
⊢ Nat.card G = 1 ∨ p ∣ Nat.card G

case inr
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
val✝ : Infinite G
⊢ Nat.card G = 1 ∨ p ∣ Nat.card G
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
⊢ Nat.card G = 1 ∨ p ∣ Nat.card G
cases fintypeOrInfinite G
case inl.intro
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
val✝ : Fintype G
n : ℕ
hn : card G = p ^ n
⊢ Nat.card G = 1 ∨ p ∣ Nat.card G
case inl
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
val✝ : Fintype G
⊢ Nat.card G = 1 ∨ p ∣ Nat.card G
obtain ⟨n, hn⟩ := iff_card.mp hG
case inl.intro
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
val✝ : Fintype G
n : ℕ
hn : card G = p ^ n
⊢ p ^ n = 1 ∨ p ∣ p ^ n
case inl.intro
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
val✝ : Fintype G
n : ℕ
hn : card G = p ^ n
⊢ Nat.card G = 1 ∨ p ∣ Nat.card G
rw [Nat.card_eq_fintype_card, hn]
case inl.intro.zero
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
val✝ : Fintype G
hn : card G = p ^ Nat.zero
⊢ p ^ Nat.zero = 1 ∨ p ∣ p ^ Nat.zero

case inl.intro.succ
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
val✝ : Fintype G
n : ℕ
hn : card G = p ^ Nat.succ n
⊢ p ^ Nat.succ n = 1 ∨ p ∣ p ^ Nat.succ n
case inl.intro
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
val✝ : Fintype G
n : ℕ
hn : card G = p ^ n
⊢ p ^ n = 1 ∨ p ∣ p ^ n
cases' n with n n
no goals
case inl.intro.zero
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
val✝ : Fintype G
hn : card G = p ^ Nat.zero
⊢ p ^ Nat.zero = 1 ∨ p ∣ p ^ Nat.zero
exact Or.inl rfl
no goals
case inl.intro.succ
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
val✝ : Fintype G
n : ℕ
hn : card G = p ^ Nat.succ n
⊢ p ^ Nat.succ n = 1 ∨ p ∣ p ^ Nat.succ n
exact Or.inr ⟨p ^ n, by rw [pow_succ]⟩
no goals
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
val✝ : Fintype G
n : ℕ
hn : card G = p ^ Nat.succ n
⊢ p ^ Nat.succ n = p * p ^ n
rw [pow_succ]
case inr
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
val✝ : Infinite G
⊢ 0 = 1 ∨ p ∣ 0
case inr
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
val✝ : Infinite G
⊢ Nat.card G = 1 ∨ p ∣ Nat.card G
rw [Nat.card_eq_zero_of_infinite]
no goals
case inr
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
val✝ : Infinite G
⊢ 0 = 1 ∨ p ∣ 0
exact Or.inr ⟨0, rfl⟩