-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
theorem IsCyclic.card_pow_eq_one_le [DecidableEq α] [Fintype α] [IsCyclic α] {n : ℕ} (hn0 : 0 < n) :
    #{a : α | a ^ n = 1} ≤ n :=
  let ⟨g, hg⟩ := IsCyclic.exists_generator (α := α)
  calc
    #{a : α | a ^ n = 1} ≤
        #(zpowers (g ^ (Fintype.card α / Nat.gcd n (Fintype.card α))) : Set α).toFinset :=
      card_le_card fun x hx =>
        let ⟨m, hm⟩ := show x ∈ Submonoid.powers g from mem_powers_iff_mem_zpowers.2 <| hg x
        Set.mem_toFinset.2
          ⟨(m / (Fintype.card α / Nat.gcd n (Fintype.card α)) : ℕ), by
            dsimp at hm
            have hgmn : g ^ (m * Nat.gcd n (Fintype.card α)) = 1

Proof state:
α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = n.gcd (Fintype.card α) * m
hm0 : 0 < m
⊢ n.gcd (Fintype.card α) ≤ n

Tactic:
exact le_of_dvd hn0 (Nat.gcd_dvd_left _ _)

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = n.gcd (Fintype.card α) * m
hm0 : 0 < m
⊢ Fintype.card ↥(zpowers (g ^ (Fintype.card α / n.gcd (Fintype.card α)))) ≤ n

Tactic:
rw [Fintype.card_zpowers, orderOf_pow g, orderOf_eq_card_of_forall_mem_zpowers hg,
  Nat.card_eq_fintype_card]

Result:
α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = n.gcd (Fintype.card α) * m
hm0 : 0 < m
⊢ Fintype.card α / (Fintype.card α).gcd (Fintype.card α / n.gcd (Fintype.card α)) ≤ n

Proof state:
α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ filter (fun a => a ^ n = 1) univ
m : ℕ
hm : g ^ m = x
hgmn : g ^ (m * n.gcd (Fintype.card α)) = 1
⊢ orderOf g ∣ m * n.gcd (Fintype.card α)

Tactic:
exact orderOf_dvd_of_pow_eq_one hgmn

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ filter (fun a => a ^ n = 1) univ
m : ℕ
hm : g ^ m = x
hgmn : g ^ (m * n.gcd (Fintype.card α)) = 1
⊢ Fintype.card α / n.gcd (Fintype.card α) ∣ m

Tactic:
refine Nat.dvd_of_mul_dvd_mul_right (gcd_pos_of_pos_left (Fintype.card α) hn0) ?_

Result:
α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ filter (fun a => a ^ n = 1) univ
m : ℕ
hm : g ^ m = x
hgmn : g ^ (m * n.gcd (Fintype.card α)) = 1
⊢ Fintype.card α / n.gcd (Fintype.card α) * n.gcd (Fintype.card α) ∣ m * n.gcd (Fintype.card α)

Proof state:
α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ filter (fun a => a ^ n = 1) univ
m : ℕ
hm : g ^ m = x
hgmn : g ^ (m * n.gcd (Fintype.card α)) = 1
⊢ (g ^ (Fintype.card α / n.gcd (Fintype.card α))) ^ ↑(m / (Fintype.card α / n.gcd (Fintype.card α))) = x

Tactic:
rw [zpow_natCast, ← pow_mul, Nat.mul_div_cancel_left', hm]

Result:
α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ filter (fun a => a ^ n = 1) univ
m : ℕ
hm : g ^ m = x
hgmn : g ^ (m * n.gcd (Fintype.card α)) = 1
⊢ Fintype.card α / n.gcd (Fintype.card α) ∣ m

Proof state:
α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ filter (fun a => a ^ n = 1) univ
m : ℕ
hm : (fun x => g ^ x) m = x
⊢ (fun x => (g ^ (Fintype.card α / n.gcd (Fintype.card α))) ^ x) ↑(m / (Fintype.card α / n.gcd (Fintype.card α))) = x

Tactic:
dsimp at hm

Result:
α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ filter (fun a => a ^ n = 1) univ
m : ℕ
hm : g ^ m = x
⊢ (fun x => (g ^ (Fintype.card α / n.gcd (Fintype.card α))) ^ x) ↑(m / (Fintype.card α / n.gcd (Fintype.card α))) = x

Proof state:
α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ filter (fun a => a ^ n = 1) univ
m : ℕ
hm : g ^ m = x
⊢ (fun x => (g ^ (Fintype.card α / n.gcd (Fintype.card α))) ^ x) ↑(m / (Fintype.card α / n.gcd (Fintype.card α))) = x

Tactic:
have hgmn : g ^ (m * Nat.gcd n (Fintype.card α)) = 1 := by
  rw [pow_mul, hm, ← pow_gcd_card_eq_one_iff]; exact (mem_filter.1 hx).2

Result:
α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ filter (fun a => a ^ n = 1) univ
m : ℕ
hm : g ^ m = x
hgmn : g ^ (m * n.gcd (Fintype.card α)) = 1
⊢ (fun x => (g ^ (Fintype.card α / n.gcd (Fintype.card α))) ^ x) ↑(m / (Fintype.card α / n.gcd (Fintype.card α))) = x