p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
hG : card G ≠ 0
⊢ IsPGroup p G ↔ ∃ n, card G = p ^ n
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
⊢ IsPGroup p G ↔ ∃ n, card G = p ^ n
have hG : card G ≠ 0 := card_ne_zero
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
hG : card G ≠ 0
h : IsPGroup p G
⊢ ∃ n, card G = p ^ n
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
hG : card G ≠ 0
⊢ IsPGroup p G ↔ ∃ n, card G = p ^ n
refine' ⟨fun h => _, fun ⟨n, hn⟩ => of_card hn⟩
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
hG : card G ≠ 0
h : IsPGroup p G
⊢ ∀ (q : ℕ), q ∈ Nat.factors (card G) → q = p
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
hG : card G ≠ 0
h : IsPGroup p G
⊢ ∃ n, card G = p ^ n
suffices ∀ q ∈ Nat.factors (card G), q = p by
  use (card G).factors.length
  rw [← List.prod_replicate, ← List.eq_replicate_of_mem this, Nat.prod_factors hG]
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
hG : card G ≠ 0
h : IsPGroup p G
q : ℕ
hq : q ∈ Nat.factors (card G)
⊢ q = p
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
hG : card G ≠ 0
h : IsPGroup p G
⊢ ∀ (q : ℕ), q ∈ Nat.factors (card G) → q = p
intro q hq
case intro
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
hG : card G ≠ 0
h : IsPGroup p G
q : ℕ
hq : q ∈ Nat.factors (card G)
hq1 : Nat.Prime q
hq2 : q ∣ card G
⊢ q = p
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
hG : card G ≠ 0
h : IsPGroup p G
q : ℕ
hq : q ∈ Nat.factors (card G)
⊢ q = p
obtain ⟨hq1, hq2⟩ := (Nat.mem_factors hG).mp hq
case intro
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
hG : card G ≠ 0
h : IsPGroup p G
q : ℕ
hq : q ∈ Nat.factors (card G)
hq1 : Nat.Prime q
hq2 : q ∣ card G
this : Fact (Nat.Prime q)
⊢ q = p
case intro
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
hG : card G ≠ 0
h : IsPGroup p G
q : ℕ
hq : q ∈ Nat.factors (card G)
hq1 : Nat.Prime q
hq2 : q ∣ card G
⊢ q = p
haveI : Fact q.Prime := ⟨hq1⟩
case intro.intro
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
hG : card G ≠ 0
h : IsPGroup p G
q : ℕ
hq : q ∈ Nat.factors (card G)
hq1 : Nat.Prime q
hq2 : q ∣ card G
this : Fact (Nat.Prime q)
g : G
hg : orderOf g = q
⊢ q = p
case intro
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
hG : card G ≠ 0
h : IsPGroup p G
q : ℕ
hq : q ∈ Nat.factors (card G)
hq1 : Nat.Prime q
hq2 : q ∣ card G
this : Fact (Nat.Prime q)
⊢ q = p
obtain ⟨g, hg⟩ := exists_prime_orderOf_dvd_card q hq2
case intro.intro.intro
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
hG : card G ≠ 0
h : IsPGroup p G
q : ℕ
hq : q ∈ Nat.factors (card G)
hq1 : Nat.Prime q
hq2 : q ∣ card G
this : Fact (Nat.Prime q)
g : G
hg : orderOf g = q
k : ℕ
hk : orderOf g = p ^ k
⊢ q = p
case intro.intro
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
hG : card G ≠ 0
h : IsPGroup p G
q : ℕ
hq : q ∈ Nat.factors (card G)
hq1 : Nat.Prime q
hq2 : q ∣ card G
this : Fact (Nat.Prime q)
g : G
hg : orderOf g = q
⊢ q = p
obtain ⟨k, hk⟩ := (iff_orderOf.mp h) g
no goals
case intro.intro.intro
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
hG : card G ≠ 0
h : IsPGroup p G
q : ℕ
hq : q ∈ Nat.factors (card G)
hq1 : Nat.Prime q
hq2 : q ∣ card G
this : Fact (Nat.Prime q)
g : G
hg : orderOf g = q
k : ℕ
hk : orderOf g = p ^ k
⊢ q = p
exact (hq1.pow_eq_iff.mp (hg.symm.trans hk).symm).1.symm
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
hG : card G ≠ 0
h : IsPGroup p G
this : ∀ (q : ℕ), q ∈ Nat.factors (card G) → q = p
⊢ card G = p ^ List.length (Nat.factors (card G))
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
hG : card G ≠ 0
h : IsPGroup p G
this : ∀ (q : ℕ), q ∈ Nat.factors (card G) → q = p
⊢ ∃ n, card G = p ^ n
use (card G).factors.length
no goals
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
hG : card G ≠ 0
h : IsPGroup p G
this : ∀ (q : ℕ), q ∈ Nat.factors (card G) → q = p
⊢ card G = p ^ List.length (Nat.factors (card G))
rw [← List.prod_replicate, ← List.eq_replicate_of_mem this, Nat.prod_factors hG]