case intro.intro
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
hG : card G = p ^ 2
k : ℕ
hk0 : k > 0
hk : card { x // x ∈ center G } = p ^ k
⊢ IsCyclic (G ⧸ center G)
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
hG : card G = p ^ 2
⊢ IsCyclic (G ⧸ center G)
rcases card_center_eq_prime_pow hG zero_lt_two with ⟨k, hk0, hk⟩
case intro.intro
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
k : ℕ
hG : p ^ k * card (G ⧸ center G) = p ^ 2
hk0 : k > 0
hk : card { x // x ∈ center G } = p ^ k
⊢ IsCyclic (G ⧸ center G)
case intro.intro
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
hG : card G = p ^ 2
k : ℕ
hk0 : k > 0
hk : card { x // x ∈ center G } = p ^ k
⊢ IsCyclic (G ⧸ center G)
rw [card_eq_card_quotient_mul_card_subgroup (center G), mul_comm, hk] at hG
case intro.intro
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
k : ℕ
hG : p ^ k * card (G ⧸ center G) = p ^ 2
hk0 : k > 0
hk : card { x // x ∈ center G } = p ^ k
hk2 : k ≤ 2
⊢ IsCyclic (G ⧸ center G)
case intro.intro
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
k : ℕ
hG : p ^ k * card (G ⧸ center G) = p ^ 2
hk0 : k > 0
hk : card { x // x ∈ center G } = p ^ k
⊢ IsCyclic (G ⧸ center G)
have hk2 := (Nat.pow_dvd_pow_iff_le_right (Fact.out (p := p.Prime)).one_lt).1 ⟨_, hG.symm⟩
case intro.intro.«1»
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
k : ℕ
hG : p ^ 1 * card (G ⧸ center G) = p ^ 2
hk0 : 1 > 0
hk : card { x // x ∈ center G } = p ^ 1
hk2 : 1 ≤ 2
⊢ IsCyclic (G ⧸ center G)

case intro.intro.«2»
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
k : ℕ
hG : p ^ 2 * card (G ⧸ center G) = p ^ 2
hk0 : 2 > 0
hk : card { x // x ∈ center G } = p ^ 2
hk2 : 2 ≤ 2
⊢ IsCyclic (G ⧸ center G)
case intro.intro
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
k : ℕ
hG : p ^ k * card (G ⧸ center G) = p ^ 2
hk0 : k > 0
hk : card { x // x ∈ center G } = p ^ k
hk2 : k ≤ 2
⊢ IsCyclic (G ⧸ center G)
interval_cases k
case intro.intro.«1»
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
k : ℕ
hG : card (G ⧸ center G) = p
hk0 : 1 > 0
hk : card { x // x ∈ center G } = p ^ 1
hk2 : 1 ≤ 2
⊢ IsCyclic (G ⧸ center G)
case intro.intro.«1»
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
k : ℕ
hG : p ^ 1 * card (G ⧸ center G) = p ^ 2
hk0 : 1 > 0
hk : card { x // x ∈ center G } = p ^ 1
hk2 : 1 ≤ 2
⊢ IsCyclic (G ⧸ center G)
rw [sq, pow_one, mul_right_inj' (Fact.out (p := p.Prime)).ne_zero] at hG
no goals
case intro.intro.«1»
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
k : ℕ
hG : card (G ⧸ center G) = p
hk0 : 1 > 0
hk : card { x // x ∈ center G } = p ^ 1
hk2 : 1 ≤ 2
⊢ IsCyclic (G ⧸ center G)
exact isCyclic_of_prime_card hG
no goals
case intro.intro.«2»
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
k : ℕ
hG : p ^ 2 * card (G ⧸ center G) = p ^ 2
hk0 : 2 > 0
hk : card { x // x ∈ center G } = p ^ 2
hk2 : 2 ≤ 2
⊢ IsCyclic (G ⧸ center G)
exact
  @isCyclic_of_subsingleton _ _
    ⟨Fintype.card_le_one_iff.1
        (mul_right_injective₀ (pow_ne_zero 2 (NeZero.ne p))
            (hG.trans (mul_one (p ^ 2)).symm)).le⟩