-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
theorem prime_card [Finite α] : (Nat.card α).Prime

Proof state:
case intro.refine_1
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Finite α
h0 : 0 < Nat.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Nat.card α
h : Subgroup.zpowers (g ^ n) = ⊤
hgo : orderOf (g ^ n) = orderOf g / (orderOf g).gcd n
⊢ n = 1

Tactic:
rw [orderOf_eq_card_of_forall_mem_zpowers hg, Nat.gcd_eq_right_iff_dvd.1 hn,
  orderOf_eq_card_of_forall_mem_zpowers, eq_comm,
  Nat.div_eq_iff_eq_mul_left (Nat.pos_of_dvd_of_pos hn h0) hn] at hgo

Result:
case intro.refine_1
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Finite α
h0 : 0 < Nat.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Nat.card α
h : Subgroup.zpowers (g ^ n) = ⊤
hgo : Nat.card α = Nat.card α * n
⊢ n = 1

case intro.refine_1
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Finite α
h0 : 0 < Nat.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Nat.card α
h : Subgroup.zpowers (g ^ n) = ⊤
hgo : orderOf (g ^ n) = Nat.card α / n
⊢ ∀ (x : α), x ∈ Subgroup.zpowers (g ^ n)

Proof state:
case intro.refine_1
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Finite α
h0 : 0 < Nat.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Nat.card α
h : Subgroup.zpowers (g ^ n) = ⊤
⊢ n = 1

Tactic:
have hgo := orderOf_pow (n := n) g

Result:
case intro.refine_1
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Finite α
h0 : 0 < Nat.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Nat.card α
h : Subgroup.zpowers (g ^ n) = ⊤
hgo : orderOf (g ^ n) = orderOf g / (orderOf g).gcd n
⊢ n = 1

Proof state:
case intro.refine_1
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Finite α
h0 : 0 < Nat.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Nat.card α
h : Subgroup.zpowers (g ^ n) = ⊤
hgo : orderOf (g ^ n) = Nat.card α / n
x : α
⊢ x ∈ Subgroup.zpowers (g ^ n)

Tactic:
rw [h]

Result:
case intro.refine_1
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Finite α
h0 : 0 < Nat.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Nat.card α
h : Subgroup.zpowers (g ^ n) = ⊤
hgo : orderOf (g ^ n) = Nat.card α / n
x : α
⊢ x ∈ ⊤

Proof state:
case intro
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Finite α
h0 : 0 < Nat.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Nat.card α
⊢ n = 1 ∨ n = Nat.card α

Tactic:
refine (IsSimpleOrder.eq_bot_or_eq_top (Subgroup.zpowers (g ^ n))).symm.imp ?_ ?_

Result:
case intro.refine_1
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Finite α
h0 : 0 < Nat.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Nat.card α
⊢ Subgroup.zpowers (g ^ n) = ⊤ → n = 1

case intro.refine_2
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Finite α
h0 : 0 < Nat.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Nat.card α
⊢ Subgroup.zpowers (g ^ n) = ⊥ → n = Nat.card α

Proof state:
case intro.refine_2
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Finite α
h0 : 0 < Nat.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Nat.card α
h : Subgroup.zpowers (g ^ n) = ⊥
⊢ Nat.card α ≤ n

Tactic:
rw [← orderOf_eq_card_of_forall_mem_zpowers hg]

Result:
case intro.refine_2
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Finite α
h0 : 0 < Nat.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Nat.card α
h : Subgroup.zpowers (g ^ n) = ⊥
⊢ orderOf g ≤ n

Proof state:
case intro.refine_2
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Finite α
h0 : 0 < Nat.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Nat.card α
⊢ Subgroup.zpowers (g ^ n) = ⊥ → n = Nat.card α

Tactic:
intro h

Result:
case intro.refine_2
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Finite α
h0 : 0 < Nat.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Nat.card α
h : Subgroup.zpowers (g ^ n) = ⊥
⊢ n = Nat.card α

Proof state:
case intro.refine_1
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Finite α
h0 : 0 < Nat.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Nat.card α
h : Subgroup.zpowers (g ^ n) = ⊤
hgo : orderOf (g ^ n) = Nat.card α / n
x : α
⊢ x ∈ ⊤

Tactic:
exact Subgroup.mem_top _

Result:
no goals

Proof state:
case intro
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Finite α
h0 : 0 < Nat.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
⊢ 2 ≤ Nat.card α ∧ ∀ (m : ℕ), m ∣ Nat.card α → m = 1 ∨ m = Nat.card α

Tactic:
refine ⟨Finite.one_lt_card_iff_nontrivial.2 inferInstance, fun n hn => ?_⟩

Result:
case intro
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Finite α
h0 : 0 < Nat.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Nat.card α
⊢ n = 1 ∨ n = Nat.card α

Proof state:
case intro
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Finite α
h0 : 0 < Nat.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
⊢ Nat.Prime (Nat.card α)

Tactic:
rw [Nat.prime_def]

Result:
case intro
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Finite α
h0 : 0 < Nat.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
⊢ 2 ≤ Nat.card α ∧ ∀ (m : ℕ), m ∣ Nat.card α → m = 1 ∨ m = Nat.card α

Proof state:
case intro.refine_2
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Finite α
h0 : 0 < Nat.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Nat.card α
h : Subgroup.zpowers (g ^ n) = ⊥
⊢ g ^ n = 1

Tactic:
rw [← Subgroup.mem_bot, ← h]

Result:
case intro.refine_2
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Finite α
h0 : 0 < Nat.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Nat.card α
h : Subgroup.zpowers (g ^ n) = ⊥
⊢ g ^ n ∈ Subgroup.zpowers (g ^ n)

Proof state:
case intro.refine_2
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Finite α
h0 : 0 < Nat.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Nat.card α
h : Subgroup.zpowers (g ^ n) = ⊥
⊢ g ^ n ∈ Subgroup.zpowers (g ^ n)

Tactic:
exact Subgroup.mem_zpowers _

Result:
no goals

Proof state:
case intro.refine_2
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Finite α
h0 : 0 < Nat.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Nat.card α
h : Subgroup.zpowers (g ^ n) = ⊥
⊢ n = Nat.card α

Tactic:
apply le_antisymm (Nat.le_of_dvd h0 hn)

Result:
case intro.refine_2
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Finite α
h0 : 0 < Nat.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Nat.card α
h : Subgroup.zpowers (g ^ n) = ⊥
⊢ Nat.card α ≤ n

Proof state:
case intro.refine_2
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Finite α
h0 : 0 < Nat.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Nat.card α
h : Subgroup.zpowers (g ^ n) = ⊥
⊢ orderOf g ≤ n

Tactic:
apply orderOf_le_of_pow_eq_one (Nat.pos_of_dvd_of_pos hn h0)

Result:
case intro.refine_2
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Finite α
h0 : 0 < Nat.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Nat.card α
h : Subgroup.zpowers (g ^ n) = ⊥
⊢ g ^ n = 1

Proof state:
case intro.refine_1
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Finite α
h0 : 0 < Nat.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Nat.card α
⊢ Subgroup.zpowers (g ^ n) = ⊤ → n = 1

Tactic:
intro h

Result:
case intro.refine_1
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Finite α
h0 : 0 < Nat.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Nat.card α
h : Subgroup.zpowers (g ^ n) = ⊤
⊢ n = 1