-- 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
⊢ #(↑(zpowers (g ^ (Fintype.card α / n.gcd (Fintype.card α))))).toFinset ≤ n

Tactic:
let ⟨m, hm⟩ := Nat.gcd_dvd_right n (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
⊢ #(↑(zpowers (g ^ (Fintype.card α / n.gcd (Fintype.card α))))).toFinset ≤ n

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 : IsEmpty α
hm0 : m = 0
⊢ False

Tactic:
exact hm.elim' 1

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
⊢ (fun x => (g ^ (Fintype.card α / n.gcd (Fintype.card α))) ^ x) ↑(m / (Fintype.card α / n.gcd (Fintype.card α))) = x

Tactic:
dsimp only

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
⊢ (g ^ (Fintype.card α / n.gcd (Fintype.card α))) ^ ↑(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
hgmn : g ^ (m * n.gcd (Fintype.card α)) = 1
⊢ Fintype.card α / n.gcd (Fintype.card α) * n.gcd (Fintype.card α) ∣ m * n.gcd (Fintype.card α)

Tactic:
conv_lhs =>
  rw [Nat.div_mul_cancel (Nat.gcd_dvd_right _ _), ← Nat.card_eq_fintype_card,
    ← orderOf_eq_card_of_forall_mem_zpowers hg]

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
⊢ orderOf g ∣ 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
⊢ x ^ n = 1

Tactic:
exact (mem_filter.1 hx).2

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 α / (Fintype.card α).gcd (Fintype.card α / n.gcd (Fintype.card α)) ≤ n

Tactic:
nth_rw 2 [hm]

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 α / (n.gcd (Fintype.card α) * m).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
m : ℕ
hm : Fintype.card α = n.gcd (Fintype.card α) * m
hm0 : 0 < m
⊢ Fintype.card α / (n.gcd (Fintype.card α) * m).gcd (n.gcd (Fintype.card α) * m / n.gcd (Fintype.card α)) ≤ n

Tactic:
rw [Nat.mul_div_cancel_left _ (gcd_pos_of_pos_left _ hn0), gcd_mul_left_left, hm,
  Nat.mul_div_cancel _ hm0]

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
⊢ 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
⊢ g ^ (m * n.gcd (Fintype.card α)) = 1

Tactic:
rw [pow_mul, hm, ← pow_gcd_card_eq_one_iff]

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
⊢ x ^ n = 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 : m = 0
⊢ False

Tactic:
rw [hm0, mul_zero, Fintype.card_eq_zero_iff] at hm

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

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 α / (n.gcd (Fintype.card α) * m).gcd (Fintype.card α / n.gcd (Fintype.card α)) ≤ n

Tactic:
nth_rw 3 [hm]

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 α / (n.gcd (Fintype.card α) * m).gcd (n.gcd (Fintype.card α) * m / 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
m : ℕ
hm : Fintype.card α = n.gcd (Fintype.card α) * m
⊢ #(↑(zpowers (g ^ (Fintype.card α / n.gcd (Fintype.card α))))).toFinset ≤ n

Tactic:
have hm0 : 0 < m :=
  Nat.pos_of_ne_zero fun hm0 => by
    rw [hm0, mul_zero, Fintype.card_eq_zero_iff] at hm
    exact hm.elim' 1

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
⊢ #(↑(zpowers (g ^ (Fintype.card α / n.gcd (Fintype.card α))))).toFinset ≤ n

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
⊢ #(↑(zpowers (g ^ (Fintype.card α / n.gcd (Fintype.card α))))).toFinset ≤ n

Tactic:
simp only [Set.toFinset_card, SetLike.coe_sort_coe]

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 ↥(zpowers (g ^ (Fintype.card α / n.gcd (Fintype.card α)))) ≤ n