-- Mathlib/GroupTheory/PGroup.lean
theorem iff_card [Fact p.Prime] [Finite G] : IsPGroup p G ↔ ∃ n : ℕ, Nat.card G = p ^ n

Proof state:
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite G
hG : Nat.card G ≠ 0
h : IsPGroup p G
⊢ ∃ n, Nat.card G = p ^ n

Tactic:
suffices ∀ q ∈ (Nat.card G).primeFactorsList, q = p by
  use (Nat.card G).primeFactorsList.length
  rw [← List.prod_replicate, ← List.eq_replicate_of_mem this, Nat.prod_primeFactorsList hG]

Result:
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite G
hG : Nat.card G ≠ 0
h : IsPGroup p G
⊢ ∀ q ∈ (Nat.card G).primeFactorsList, q = p

Proof state:
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite G
hG : Nat.card G ≠ 0
⊢ IsPGroup p G ↔ ∃ n, Nat.card G = p ^ n

Tactic:
refine ⟨fun h => ?_, fun ⟨n, hn⟩ => of_card hn⟩

Result:
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite G
hG : Nat.card G ≠ 0
h : IsPGroup p G
⊢ ∃ n, Nat.card G = p ^ n

Proof state:
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite G
⊢ IsPGroup p G ↔ ∃ n, Nat.card G = p ^ n

Tactic:
have hG : Nat.card G ≠ 0 := Nat.card_pos.ne'

Result:
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite G
hG : Nat.card G ≠ 0
⊢ IsPGroup p G ↔ ∃ n, Nat.card G = p ^ n

Proof state:
case intro.intro.intro
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite G
hG : Nat.card G ≠ 0
h : IsPGroup p G
q : ℕ
hq : q ∈ (Nat.card G).primeFactorsList
hq1 : Nat.Prime q
hq2 : q ∣ Nat.card G
this : Fact (Nat.Prime q)
g : G
hg : orderOf g = q
k : ℕ
hk : orderOf g = p ^ k
⊢ q = p

Tactic:
exact (hq1.pow_eq_iff.mp (hg.symm.trans hk).symm).1.symm

Result:
no goals

Proof state:
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite G
hG : Nat.card G ≠ 0
h : IsPGroup p G
⊢ ∀ q ∈ (Nat.card G).primeFactorsList, q = p

Tactic:
intro q hq

Result:
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite G
hG : Nat.card G ≠ 0
h : IsPGroup p G
q : ℕ
hq : q ∈ (Nat.card G).primeFactorsList
⊢ q = p

Proof state:
case intro
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite G
hG : Nat.card G ≠ 0
h : IsPGroup p G
q : ℕ
hq : q ∈ (Nat.card G).primeFactorsList
hq1 : Nat.Prime q
hq2 : q ∣ Nat.card G
this : Fact (Nat.Prime q)
⊢ q = p

Tactic:
obtain ⟨g, hg⟩ := exists_prime_orderOf_dvd_card' q hq2

Result:
case intro.intro
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite G
hG : Nat.card G ≠ 0
h : IsPGroup p G
q : ℕ
hq : q ∈ (Nat.card G).primeFactorsList
hq1 : Nat.Prime q
hq2 : q ∣ Nat.card G
this : Fact (Nat.Prime q)
g : G
hg : orderOf g = q
⊢ q = p

Proof state:
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite G
hG : Nat.card G ≠ 0
h : IsPGroup p G
q : ℕ
hq : q ∈ (Nat.card G).primeFactorsList
⊢ q = p

Tactic:
obtain ⟨hq1, hq2⟩ := (Nat.mem_primeFactorsList hG).mp hq

Result:
case intro
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite G
hG : Nat.card G ≠ 0
h : IsPGroup p G
q : ℕ
hq : q ∈ (Nat.card G).primeFactorsList
hq1 : Nat.Prime q
hq2 : q ∣ Nat.card G
⊢ q = p

Proof state:
case intro
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite G
hG : Nat.card G ≠ 0
h : IsPGroup p G
q : ℕ
hq : q ∈ (Nat.card G).primeFactorsList
hq1 : Nat.Prime q
hq2 : q ∣ Nat.card G
⊢ q = p

Tactic:
haveI : Fact q.Prime := ⟨hq1⟩

Result:
case intro
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite G
hG : Nat.card G ≠ 0
h : IsPGroup p G
q : ℕ
hq : q ∈ (Nat.card G).primeFactorsList
hq1 : Nat.Prime q
hq2 : q ∣ Nat.card G
this : Fact (Nat.Prime q)
⊢ q = p

Proof state:
case h
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite G
hG : Nat.card G ≠ 0
h : IsPGroup p G
this : ∀ q ∈ (Nat.card G).primeFactorsList, q = p
⊢ Nat.card G = p ^ (Nat.card G).primeFactorsList.length

Tactic:
rw [← List.prod_replicate, ← List.eq_replicate_of_mem this, Nat.prod_primeFactorsList hG]

Result:
no goals

Proof state:
case intro.intro
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite G
hG : Nat.card G ≠ 0
h : IsPGroup p G
q : ℕ
hq : q ∈ (Nat.card G).primeFactorsList
hq1 : Nat.Prime q
hq2 : q ∣ Nat.card G
this : Fact (Nat.Prime q)
g : G
hg : orderOf g = q
⊢ q = p

Tactic:
obtain ⟨k, hk⟩ := (iff_orderOf.mp h) g

Result:
case intro.intro.intro
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite G
hG : Nat.card G ≠ 0
h : IsPGroup p G
q : ℕ
hq : q ∈ (Nat.card G).primeFactorsList
hq1 : Nat.Prime q
hq2 : q ∣ Nat.card G
this : Fact (Nat.Prime q)
g : G
hg : orderOf g = q
k : ℕ
hk : orderOf g = p ^ k
⊢ q = p

Proof state:
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite G
hG : Nat.card G ≠ 0
h : IsPGroup p G
this : ∀ q ∈ (Nat.card G).primeFactorsList, q = p
⊢ ∃ n, Nat.card G = p ^ n

Tactic:
use (Nat.card G).primeFactorsList.length

Result:
case h
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite G
hG : Nat.card G ≠ 0
h : IsPGroup p G
this : ∀ q ∈ (Nat.card G).primeFactorsList, q = p
⊢ Nat.card G = p ^ (Nat.card G).primeFactorsList.length