α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
⊢ Nat.Prime (Fintype.card α)
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
⊢ Nat.Prime (Fintype.card α)
have h0 : 0 < Fintype.card α := Fintype.card_pos_iff.2 (by infer_instance)
case intro
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
⊢ Nat.Prime (Fintype.card α)
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
⊢ Nat.Prime (Fintype.card α)
obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := α)
case intro
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
⊢ 2 ≤ Fintype.card α ∧ ∀ (m : ℕ), m ∣ Fintype.card α → m = 1 ∨ m = Fintype.card α
case intro
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
⊢ Nat.Prime (Fintype.card α)
rw [Nat.prime_def_lt'']
case intro
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
⊢ n = 1 ∨ n = Fintype.card α
case intro
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
⊢ 2 ≤ Fintype.card α ∧ ∀ (m : ℕ), m ∣ Fintype.card α → m = 1 ∨ m = Fintype.card α
refine' ⟨Fintype.one_lt_card_iff_nontrivial.2 inferInstance, fun n hn => _⟩
case intro.refine'_1
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
⊢ Subgroup.zpowers (g ^ n) = ⊤ → n = 1

case intro.refine'_2
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
⊢ Subgroup.zpowers (g ^ n) = ⊥ → n = Fintype.card α
case intro
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
⊢ n = 1 ∨ n = Fintype.card α
refine' (IsSimpleOrder.eq_bot_or_eq_top (Subgroup.zpowers (g ^ n))).symm.imp _ _
no goals
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
⊢ Nonempty α
infer_instance
case intro.refine'_1
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
h : Subgroup.zpowers (g ^ n) = ⊤
⊢ n = 1
case intro.refine'_1
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
⊢ Subgroup.zpowers (g ^ n) = ⊤ → n = 1
intro h
case intro.refine'_1
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
h : Subgroup.zpowers (g ^ n) = ⊤
hgo : orderOf (g ^ n) = orderOf g / Nat.gcd (orderOf g) n
⊢ n = 1
case intro.refine'_1
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
h : Subgroup.zpowers (g ^ n) = ⊤
⊢ n = 1
have hgo := orderOf_pow (n := n) g
case intro.refine'_1
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
h : Subgroup.zpowers (g ^ n) = ⊤
hgo✝ : orderOf (g ^ n) = Fintype.card α / n
hgo : Fintype.card α = Fintype.card α * n
⊢ n = 1

case intro.refine'_1
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
h : Subgroup.zpowers (g ^ n) = ⊤
hgo : orderOf (g ^ n) = Fintype.card α / n
⊢ ∀ (x : α), x ∈ Subgroup.zpowers (g ^ n)
case intro.refine'_1
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
h : Subgroup.zpowers (g ^ n) = ⊤
hgo : orderOf (g ^ n) = orderOf g / Nat.gcd (orderOf g) n
⊢ n = 1
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
no goals
case intro.refine'_1
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
h : Subgroup.zpowers (g ^ n) = ⊤
hgo✝ : orderOf (g ^ n) = Fintype.card α / n
hgo : Fintype.card α = Fintype.card α * n
⊢ n = 1
exact (mul_left_cancel₀ (ne_of_gt h0) ((mul_one (Fintype.card α)).trans hgo)).symm
case intro.refine'_1
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
h : Subgroup.zpowers (g ^ n) = ⊤
hgo : orderOf (g ^ n) = Fintype.card α / n
x : α
⊢ x ∈ Subgroup.zpowers (g ^ n)
case intro.refine'_1
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
h : Subgroup.zpowers (g ^ n) = ⊤
hgo : orderOf (g ^ n) = Fintype.card α / n
⊢ ∀ (x : α), x ∈ Subgroup.zpowers (g ^ n)
intro x
case intro.refine'_1
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
h : Subgroup.zpowers (g ^ n) = ⊤
hgo : orderOf (g ^ n) = Fintype.card α / n
x : α
⊢ x ∈ ⊤
case intro.refine'_1
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
h : Subgroup.zpowers (g ^ n) = ⊤
hgo : orderOf (g ^ n) = Fintype.card α / n
x : α
⊢ x ∈ Subgroup.zpowers (g ^ n)
rw [h]
no goals
case intro.refine'_1
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
h : Subgroup.zpowers (g ^ n) = ⊤
hgo : orderOf (g ^ n) = Fintype.card α / n
x : α
⊢ x ∈ ⊤
exact Subgroup.mem_top _
case intro.refine'_2
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
h : Subgroup.zpowers (g ^ n) = ⊥
⊢ n = Fintype.card α
case intro.refine'_2
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
⊢ Subgroup.zpowers (g ^ n) = ⊥ → n = Fintype.card α
intro h
case intro.refine'_2
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
h : Subgroup.zpowers (g ^ n) = ⊥
⊢ Fintype.card α ≤ n
case intro.refine'_2
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
h : Subgroup.zpowers (g ^ n) = ⊥
⊢ n = Fintype.card α
apply le_antisymm (Nat.le_of_dvd h0 hn)
case intro.refine'_2
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
h : Subgroup.zpowers (g ^ n) = ⊥
⊢ orderOf g ≤ n
case intro.refine'_2
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
h : Subgroup.zpowers (g ^ n) = ⊥
⊢ Fintype.card α ≤ n
rw [← orderOf_eq_card_of_forall_mem_zpowers hg]
case intro.refine'_2
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
h : Subgroup.zpowers (g ^ n) = ⊥
⊢ g ^ n = 1
case intro.refine'_2
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
h : Subgroup.zpowers (g ^ n) = ⊥
⊢ orderOf g ≤ n
apply orderOf_le_of_pow_eq_one (Nat.pos_of_dvd_of_pos hn h0)
case intro.refine'_2
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
h : Subgroup.zpowers (g ^ n) = ⊥
⊢ g ^ n ∈ Subgroup.zpowers (g ^ n)
case intro.refine'_2
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
h : Subgroup.zpowers (g ^ n) = ⊥
⊢ g ^ n = 1
rw [← Subgroup.mem_bot, ← h]
no goals
case intro.refine'_2
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
h : Subgroup.zpowers (g ^ n) = ⊥
⊢ g ^ n ∈ Subgroup.zpowers (g ^ n)
exact Subgroup.mem_zpowers _