-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
/-- A group of order `p ^ 2` is not cyclic if and only if its exponent is `p`. -/
@[to_additive]
lemma not_isCyclic_iff_exponent_eq_prime [Group α] {p : ℕ} (hp : p.Prime)
    (hα : Nat.card α = p ^ 2) : ¬ IsCyclic α ↔ Monoid.exponent α = p

Proof state:
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this✝ : Finite α
this : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
a : ℕ
ha : 2 < 3
ha' : p ^ 2 = orderOf g
⊢ orderOf g = Nat.card α

Tactic:
aesop

Result:
no goals

Proof state:
case intro.intro.«0»
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this✝ : Finite α
this : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
a : ℕ
ha : 0 < 3
ha' : p ^ 0 = orderOf g
⊢ orderOf g = p

Tactic:
exact False.elim <| hg <| orderOf_eq_one_iff.mp <| by aesop

Result:
no goals

Proof state:
case intro.intro.«2»
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this✝ : Finite α
this : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
a : ℕ
ha : 2 < 3
ha' : p ^ 2 = orderOf g
⊢ orderOf g = p

Tactic:
exact False.elim <| h_cyc <| isCyclic_of_orderOf_eq_card g <| by aesop

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this✝ : Finite α
this : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
⊢ p ^ 2 ≠ 0

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this✝ : Finite α
this : Nontrivial α
h_exp : exponent α = p
h_cyc : IsCyclic α
⊢ False

Tactic:
obtain (rfl|rfl) := eq_zero_or_one_of_sq_eq_self <| hα ▸ h_exp ▸ (h_cyc.exponent_eq_card).symm

Result:
case inl
α : Type u_1
inst✝ : Group α
this✝ : Finite α
this : Nontrivial α
h_cyc : IsCyclic α
hp : Nat.Prime 0
hα : Nat.card α = 0 ^ 2
h_exp : exponent α = 0
⊢ False

case inr
α : Type u_1
inst✝ : Group α
this✝ : Finite α
this : Nontrivial α
h_cyc : IsCyclic α
hp : Nat.Prime 1
hα : Nat.card α = 1 ^ 2
h_exp : exponent α = 1
⊢ False

Proof state:
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this✝¹ : Finite α
this✝ : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
this : orderOf g ∈ (p ^ 2).divisors
⊢ orderOf g = p

Tactic:
simp only [Nat.divisors_prime_pow hp 2, Nat.reduceAdd, Finset.mem_map, Finset.mem_range,
  Function.Embedding.coeFn_mk] at this

Result:
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this✝¹ : Finite α
this✝ : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
this : ∃ a < 3, p ^ a = orderOf g
⊢ orderOf g = p

Proof state:
case intro.intro.«1»
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this✝ : Finite α
this : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
a : ℕ
ha : 1 < 3
ha' : p ^ 1 = orderOf g
⊢ orderOf g = p

Tactic:
aesop

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝ : Group α
this✝ : Finite α
this : Nontrivial α
h_cyc : IsCyclic α
hp : Nat.Prime 0
hα : Nat.card α = 0 ^ 2
h_exp : exponent α = 0
⊢ False

Tactic:
exact Nat.not_prime_zero hp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this✝ : Finite α
this : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
a : ℕ
ha : 0 < 3
ha' : p ^ 0 = orderOf g
⊢ orderOf g = 1

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this✝¹ : Finite α
this✝ : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
this : orderOf g ∈ (p ^ 2).divisors
⊢ orderOf g = p

Tactic:
simp? [Nat.divisors_prime_pow hp 2] at this says
  simp only [Nat.divisors_prime_pow hp 2, Nat.reduceAdd, Finset.mem_map, Finset.mem_range,
    Function.Embedding.coeFn_mk] at this

Result:
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this✝¹ : Finite α
this✝ : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
this : ∃ a < 3, p ^ a = orderOf g
⊢ orderOf g = p

Proof state:
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this✝ : Finite α
this : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
⊢ orderOf g = p

Tactic:
have := (Nat.mem_divisors (m := p ^ 2)).mpr ⟨hα ▸ orderOf_dvd_natCard (x := g), by aesop⟩

Result:
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this✝¹ : Finite α
this✝ : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
this : orderOf g ∈ (p ^ 2).divisors
⊢ orderOf g = p

Proof state:
case intro.intro
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this✝ : Finite α
this : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
a : ℕ
ha : a < 3
ha' : p ^ a = orderOf g
⊢ orderOf g = p

Tactic:
interval_cases a

Result:
case intro.intro.«0»
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this✝ : Finite α
this : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
a : ℕ
ha : 0 < 3
ha' : p ^ 0 = orderOf g
⊢ orderOf g = p

case intro.intro.«1»
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this✝ : Finite α
this : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
a : ℕ
ha : 1 < 3
ha' : p ^ 1 = orderOf g
⊢ orderOf g = p

case intro.intro.«2»
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this✝ : Finite α
this : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
a : ℕ
ha : 2 < 3
ha' : p ^ 2 = orderOf g
⊢ orderOf g = p

Proof state:
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
⊢ ¬IsCyclic α ↔ exponent α = p

Tactic:
have : Finite α := Nat.finite_of_card_ne_zero (hα ▸ pow_ne_zero 2 hp.ne_zero)

Result:
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this : Finite α
⊢ ¬IsCyclic α ↔ exponent α = p

Proof state:
case inr
α : Type u_1
inst✝ : Group α
this✝ : Finite α
this : Nontrivial α
h_cyc : IsCyclic α
hp : Nat.Prime 1
hα : Nat.card α = 1 ^ 2
h_exp : exponent α = 1
⊢ False

Tactic:
exact Nat.not_prime_one hp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this✝¹ : Finite α
this✝ : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
this : ∃ a < 3, p ^ a = orderOf g
⊢ orderOf g = p

Tactic:
obtain ⟨a, ha, ha'⟩ := this

Result:
case intro.intro
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this✝ : Finite α
this : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
a : ℕ
ha : a < 3
ha' : p ^ a = orderOf g
⊢ orderOf g = p

Proof state:
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this : Finite α
⊢ ¬IsCyclic α ↔ exponent α = p

Tactic:
have : Nontrivial α := Finite.one_lt_card_iff_nontrivial.mp
  (hα ▸ one_lt_pow₀ hp.one_lt two_ne_zero)

Result:
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this✝ : Finite α
this : Nontrivial α
⊢ ¬IsCyclic α ↔ exponent α = p