awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (hypothesis)
Goal:
G : Type u_2
inst : Group G
inst_1 : Finite G
inst_2 : IsCyclic G
d : ℕ
a b : ZMod d
hGcard : Nat.card G = d
h : ∀ (t : G), t ^ a.val = t ^ b.val
this : NeZero (Nat.card G)
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (zpowers g) x
⊢ a = b
have h₁ : g ^ a.val = g ^ b.val
Tactic: specialize h g
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
G : Type u_2
inst : Group G
inst_1 : Finite G
inst_2 : IsCyclic G
d : ℕ
a b : ZMod d
hGcard : Nat.card G = d
this : NeZero (Nat.card G)
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (zpowers g) x
h : g ^ a.val = g ^ b.val
⊢ a = b
have subst : ∀ {a b : ZMod (Nat.card G)} (h : g ^ a.val = g ^ b.val), a = b
Tactic: subst hGcard
Cleared hypotheses: d, a, b, hGcard, h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (hypothesis)
Goal:
G : Type u_2
inst : Group G
inst_1 : Finite G
inst_2 : IsCyclic G
this : NeZero (Nat.card G)
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (zpowers g) x
a b : ZMod (Nat.card G)
h : g ^ a.val = g ^ b.val
⊢ a = b
have h₁ : Eq (α := ZMod (Nat.card G)) (↑a.val : ZMod (Nat.card G)) (↑b.val : ZMod (Nat.card G))
Tactic: rw [pow_eq_pow_iff_modEq, orderOf_eq_card_of_forall_mem_zpowers hg,
    ← ZMod.natCast_eq_natCast_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
a : α
b : ↥(zpowers a)
⊢ (↑b : α) ^ orderOf a = 1
have let : ∀ (i : ℤ) (hi : (fun (x : ℤ) ↦ a ^ x) i = (↑b : α)), (↑b : α) ^ orderOf a = 1
Tactic: let ⟨i, hi⟩ := b.2
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
a : α
b : ↥(zpowers a)
i : ℤ
hi : (fun (x : ℤ) ↦ a ^ x) i = (↑b : α)
⊢ (↑b : α) ^ orderOf a = 1
have rw : HPow.hPow (α := α) ((fun (x : ℤ) ↦ a ^ x) i) (orderOf a) = 1
Tactic: rw [← hi, ← zpow_natCast, ← zpow_mul, mul_comm, zpow_mul, zpow_natCast,
                    pow_orderOf_eq_one, one_zpow]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
a : α
b : ↥(zpowers a)
i : ℤ
hi : (fun (x : ℤ) ↦ a ^ x) i = (↑b : α)
rw : HPow.hPow (α := α) ((fun (x : ℤ) ↦ a ^ x) i) (orderOf a) = 1
⊢ (↑b : α) ^ orderOf a = 1
have rw₁ : HPow.hPow (α := α) (β := ℤ) ((fun (x : ℤ) ↦ a ^ x) i) (↑(orderOf a) : ℤ) = 1
Tactic: rw [← hi, ← zpow_natCast, ← zpow_mul, mul_comm, zpow_mul, zpow_natCast,
                    pow_orderOf_eq_one, one_zpow]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
a : α
b : ↥(zpowers a)
i : ℤ
hi : (fun (x : ℤ) ↦ a ^ x) i = (↑b : α)
rw : HPow.hPow (α := α) ((fun (x : ℤ) ↦ a ^ x) i) (orderOf a) = 1
rw₁ : HPow.hPow (α := α) (β := ℤ) ((fun (x : ℤ) ↦ a ^ x) i) (↑(orderOf a) : ℤ) = 1
⊢ (↑b : α) ^ orderOf a = 1
have rw₂ : a ^ (i * (↑(orderOf a) : ℤ)) = 1
Tactic: rw [← hi, ← zpow_natCast, ← zpow_mul, mul_comm, zpow_mul, zpow_natCast,
                    pow_orderOf_eq_one, one_zpow]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
a : α
b : ↥(zpowers a)
i : ℤ
hi : (fun (x : ℤ) ↦ a ^ x) i = (↑b : α)
rw : HPow.hPow (α := α) ((fun (x : ℤ) ↦ a ^ x) i) (orderOf a) = 1
rw₁ : HPow.hPow (α := α) (β := ℤ) ((fun (x : ℤ) ↦ a ^ x) i) (↑(orderOf a) : ℤ) = 1
rw₂ : a ^ (i * (↑(orderOf a) : ℤ)) = 1
⊢ (↑b : α) ^ orderOf a = 1
have rw₃ : a ^ ((↑(orderOf a) : ℤ) * i) = 1
Tactic: rw [← hi, ← zpow_natCast, ← zpow_mul, mul_comm, zpow_mul, zpow_natCast,
                    pow_orderOf_eq_one, one_zpow]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
a : α
b : ↥(zpowers a)
i : ℤ
hi : (fun (x : ℤ) ↦ a ^ x) i = (↑b : α)
rw : HPow.hPow (α := α) ((fun (x : ℤ) ↦ a ^ x) i) (orderOf a) = 1
rw₁ : HPow.hPow (α := α) (β := ℤ) ((fun (x : ℤ) ↦ a ^ x) i) (↑(orderOf a) : ℤ) = 1
rw₂ : a ^ (i * (↑(orderOf a) : ℤ)) = 1
rw₃ : a ^ ((↑(orderOf a) : ℤ) * i) = 1
⊢ (↑b : α) ^ orderOf a = 1
have rw₄ : HPow.hPow (β := ℤ) a (↑(orderOf a) : ℤ) ^ i = 1
Tactic: rw [← hi, ← zpow_natCast, ← zpow_mul, mul_comm, zpow_mul, zpow_natCast,
                    pow_orderOf_eq_one, one_zpow]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
a : α
b : ↥(zpowers a)
i : ℤ
hi : (fun (x : ℤ) ↦ a ^ x) i = (↑b : α)
rw : HPow.hPow (α := α) ((fun (x : ℤ) ↦ a ^ x) i) (orderOf a) = 1
rw₁ : HPow.hPow (α := α) (β := ℤ) ((fun (x : ℤ) ↦ a ^ x) i) (↑(orderOf a) : ℤ) = 1
rw₂ : a ^ (i * (↑(orderOf a) : ℤ)) = 1
rw₃ : a ^ ((↑(orderOf a) : ℤ) * i) = 1
rw₄ : HPow.hPow (β := ℤ) a (↑(orderOf a) : ℤ) ^ i = 1
⊢ (↑b : α) ^ orderOf a = 1
have rw₅ : (a ^ orderOf a) ^ i = 1
Tactic: rw [← hi, ← zpow_natCast, ← zpow_mul, mul_comm, zpow_mul, zpow_natCast,
                    pow_orderOf_eq_one, one_zpow]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
a : α
b : ↥(zpowers a)
i : ℤ
hi : (fun (x : ℤ) ↦ a ^ x) i = (↑b : α)
rw : HPow.hPow (α := α) ((fun (x : ℤ) ↦ a ^ x) i) (orderOf a) = 1
rw₁ : HPow.hPow (α := α) (β := ℤ) ((fun (x : ℤ) ↦ a ^ x) i) (↑(orderOf a) : ℤ) = 1
rw₂ : a ^ (i * (↑(orderOf a) : ℤ)) = 1
rw₃ : a ^ ((↑(orderOf a) : ℤ) * i) = 1
rw₄ : HPow.hPow (β := ℤ) a (↑(orderOf a) : ℤ) ^ i = 1
rw₅ : (a ^ orderOf a) ^ i = 1
⊢ (↑b : α) ^ orderOf a = 1
have rw₆ : HPow.hPow (α := α) 1 i = 1
Tactic: rw [← hi, ← zpow_natCast, ← zpow_mul, mul_comm, zpow_mul, zpow_natCast,
                    pow_orderOf_eq_one, one_zpow]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
a : α
b : ↥(zpowers a)
i : ℤ
hi : (fun (x : ℤ) ↦ a ^ x) i = (↑b : α)
rw : HPow.hPow (α := α) ((fun (x : ℤ) ↦ a ^ x) i) (orderOf a) = 1
rw₁ : HPow.hPow (α := α) (β := ℤ) ((fun (x : ℤ) ↦ a ^ x) i) (↑(orderOf a) : ℤ) = 1
rw₂ : a ^ (i * (↑(orderOf a) : ℤ)) = 1
rw₃ : a ^ ((↑(orderOf a) : ℤ) * i) = 1
rw₄ : HPow.hPow (β := ℤ) a (↑(orderOf a) : ℤ) ^ i = 1
rw₅ : (a ^ orderOf a) ^ i = 1
rw₆ : HPow.hPow (α := α) 1 i = 1
⊢ (↑b : α) ^ orderOf a = 1
have rw₇ : Eq.{u_1 + 1} (α := α) 1 1
Tactic: rw [← hi, ← zpow_natCast, ← zpow_mul, mul_comm, zpow_mul, zpow_natCast,
                    pow_orderOf_eq_one, one_zpow]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = d}
⊢ card.{u_1} (α := α) {a : α | orderOf a = d} = φ d
have H : ∀ (d : ℕ)
  (IH :
    ∀ m < d,
      ∀ (hd : m ∣ Fintype.card α) (hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = m}),
        card.{u_1} (α := α) {a : α | orderOf a = m} = φ m)
  (hd : d ∣ Fintype.card α) (hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = d}),
  card.{u_1} (α := α) {a : α | orderOf a = d} = φ d
Tactic: induction d using Nat.strongRec' with | _ d IH
Cleared hypotheses: d, hd, hpos
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
IH :
  ∀ m < d,
    ∀ (hd : m ∣ Fintype.card α) (hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = m}),
      card.{u_1} (α := α) {a : α | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = d}
⊢ card.{u_1} (α := α) {a : α | orderOf a = d} = φ d
have H : ∀
  (IH :
    ∀ m < 0,
      ∀ (hd : m ∣ Fintype.card α) (hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = m}),
        card.{u_1} (α := α) {a : α | orderOf a = m} = φ m)
  (hd : 0 ∣ Fintype.card α) (hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = 0}),
  card.{u_1} (α := α) {a : α | orderOf a = 0} = φ 0
Tactic: rcases Decidable.eq_or_ne d 0 with (rfl | hd0)
Cleared hypotheses: d, IH, hd, hpos
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
IH :
  ∀ m < d,
    ∀ (hd : m ∣ Fintype.card α) (hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = m}),
      card.{u_1} (α := α) {a : α | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = d}
H :
  ∀
    (IH :
      ∀ m < 0,
        ∀ (hd : m ∣ Fintype.card α) (hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = m}),
          card.{u_1} (α := α) {a : α | orderOf a = m} = φ m)
    (hd : 0 ∣ Fintype.card α) (hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = 0}),
    card.{u_1} (α := α) {a : α | orderOf a = 0} = φ 0
⊢ card.{u_1} (α := α) {a : α | orderOf a = d} = φ d
have H₁ : ∀ (hd0 : d ≠ 0), card.{u_1} (α := α) {a : α | orderOf a = d} = φ d
Tactic: rcases Decidable.eq_or_ne d 0 with (rfl | hd0)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
IH :
  ∀ m < d,
    ∀ (hd : m ∣ Fintype.card α) (hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = m}),
      card.{u_1} (α := α) {a : α | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = d}
hd0 : d ≠ 0
⊢ card.{u_1} (α := α) {a : α | orderOf a = d} = φ d
have H : ∀ (a : α) (ha' : Membership.mem (γ := Finset α) {a : α | orderOf a = d} a),
  card.{u_1} (α := α) {a : α | orderOf a = d} = φ d
Tactic: rcases Finset.card_pos.1 hpos with ⟨a, ha'⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
IH :
  ∀ m < d,
    ∀ (hd : m ∣ Fintype.card α) (hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = m}),
      card.{u_1} (α := α) {a : α | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : Membership.mem (γ := Finset α) {a : α | orderOf a = d} a
⊢ card.{u_1} (α := α) {a : α | orderOf a = d} = φ d
have ha : orderOf a = d
Tactic: have ha : orderOf a = d := (mem_filter.1 ha').2
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
IH :
  ∀ m < d,
    ∀ (hd : m ∣ Fintype.card α) (hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = m}),
      card.{u_1} (α := α) {a : α | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : Membership.mem (γ := Finset α) {a : α | orderOf a = d} a
ha : orderOf a = d
⊢ Eq (α := ℕ) (∑ m ∈ d.properDivisors, card.{u_1} (α := α) {a : α | orderOf a = m}) (∑ m ∈ d.properDivisors, φ m)
have refine : ∀ (m : ℕ) (hm : m ∈ d.properDivisors), card.{u_1} (α := α) {a : α | orderOf a = m} = φ m
Tactic: refine Finset.sum_congr rfl fun m hm => ?_
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
IH :
  ∀ m < d,
    ∀ (hd : m ∣ Fintype.card α) (hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = m}),
      card.{u_1} (α := α) {a : α | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : Membership.mem (γ := Finset α) {a : α | orderOf a = d} a
ha : orderOf a = d
m : ℕ
hm : m ∈ d.properDivisors
⊢ card.{u_1} (α := α) {a : α | orderOf a = m} = φ m
have hm₁ : m ∣ d ∧ m < d
Tactic: simp only [mem_properDivisors] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
IH :
  ∀ m < d,
    ∀ (hd : m ∣ Fintype.card α) (hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = m}),
      card.{u_1} (α := α) {a : α | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : Membership.mem (γ := Finset α) {a : α | orderOf a = d} a
ha : orderOf a = d
m : ℕ
hm : m ∣ d ∧ m < d
⊢ card.{u_1} (α := α) {a : α | orderOf a = m} = φ m
have refine : Membership.mem (γ := Finset α) {a : α | orderOf a = m} (a ^ (d / m))
Tactic: refine IH m hm.2 (hm.1.trans hd) (Finset.card_pos.2 ⟨a ^ (d / m), ?_⟩)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
IH :
  ∀ m < d,
    ∀ (hd : m ∣ Fintype.card α) (hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = m}),
      card.{u_1} (α := α) {a : α | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : Membership.mem (γ := Finset α) {a : α | orderOf a = d} a
ha : orderOf a = d
m : ℕ
hm : m ∣ d ∧ m < d
⊢ Membership.mem (γ := Finset α) {a : α | orderOf a = m} (a ^ (d / m))
have rw : orderOf (a ^ (d / m)) = m
Tactic: rw [mem_filter_univ, orderOf_pow a, ha, Nat.gcd_eq_right (div_dvd_of_dvd hm.1),
      Nat.div_div_self hm.1 hd0]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
IH :
  ∀ m < d,
    ∀ (hd : m ∣ Fintype.card α) (hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = m}),
      card.{u_1} (α := α) {a : α | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : Membership.mem (γ := Finset α) {a : α | orderOf a = d} a
ha : orderOf a = d
m : ℕ
hm : m ∣ d ∧ m < d
rw : orderOf (a ^ (d / m)) = m
⊢ Membership.mem (γ := Finset α) {a : α | orderOf a = m} (a ^ (d / m))
have rw₁ : orderOf a / (orderOf a).gcd (d / m) = m
Tactic: rw [mem_filter_univ, orderOf_pow a, ha, Nat.gcd_eq_right (div_dvd_of_dvd hm.1),
      Nat.div_div_self hm.1 hd0]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
IH :
  ∀ m < d,
    ∀ (hd : m ∣ Fintype.card α) (hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = m}),
      card.{u_1} (α := α) {a : α | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : Membership.mem (γ := Finset α) {a : α | orderOf a = d} a
ha : orderOf a = d
m : ℕ
hm : m ∣ d ∧ m < d
rw : orderOf (a ^ (d / m)) = m
rw₁ : orderOf a / (orderOf a).gcd (d / m) = m
⊢ Membership.mem (γ := Finset α) {a : α | orderOf a = m} (a ^ (d / m))
have rw₂ : d / d.gcd (d / m) = m
Tactic: rw [mem_filter_univ, orderOf_pow a, ha, Nat.gcd_eq_right (div_dvd_of_dvd hm.1),
      Nat.div_div_self hm.1 hd0]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
IH :
  ∀ m < d,
    ∀ (hd : m ∣ Fintype.card α) (hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = m}),
      card.{u_1} (α := α) {a : α | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : Membership.mem (γ := Finset α) {a : α | orderOf a = d} a
ha : orderOf a = d
m : ℕ
hm : m ∣ d ∧ m < d
rw : orderOf (a ^ (d / m)) = m
rw₁ : orderOf a / (orderOf a).gcd (d / m) = m
rw₂ : d / d.gcd (d / m) = m
⊢ Membership.mem (γ := Finset α) {a : α | orderOf a = m} (a ^ (d / m))
have rw₃ : d / (d / m) = m
Tactic: rw [mem_filter_univ, orderOf_pow a, ha, Nat.gcd_eq_right (div_dvd_of_dvd hm.1),
      Nat.div_div_self hm.1 hd0]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
IH :
  ∀ m < d,
    ∀ (hd : m ∣ Fintype.card α) (hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = m}),
      card.{u_1} (α := α) {a : α | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : Membership.mem (γ := Finset α) {a : α | orderOf a = d} a
ha : orderOf a = d
m : ℕ
hm : m ∣ d ∧ m < d
rw : orderOf (a ^ (d / m)) = m
rw₁ : orderOf a / (orderOf a).gcd (d / m) = m
rw₂ : d / d.gcd (d / m) = m
rw₃ : d / (d / m) = m
⊢ Membership.mem (γ := Finset α) {a : α | orderOf a = m} (a ^ (d / m))
have rw₄ : m = m
Tactic: rw [mem_filter_univ, orderOf_pow a, ha, Nat.gcd_eq_right (div_dvd_of_dvd hm.1),
      Nat.div_div_self hm.1 hd0]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
IH :
  ∀ m < d,
    ∀ (hd : m ∣ Fintype.card α) (hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = m}),
      card.{u_1} (α := α) {a : α | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : Membership.mem (γ := Finset α) {a : α | orderOf a = d} a
ha : orderOf a = d
⊢ card.{u_1} (α := α) {a : α | orderOf a = d} = φ d
have h1 : Eq (α := ℕ) (∑ m ∈ d.properDivisors, card.{u_1} (α := α) {a : α | orderOf a = m}) (∑ m ∈ d.properDivisors, φ m)
Tactic: have h1 :
    (∑ m ∈ d.properDivisors, #{a : α | orderOf a = m}) =
      ∑ m ∈ d.properDivisors, φ m := by
    refine Finset.sum_congr rfl fun m hm => ?_
    simp only [mem_properDivisors] at hm
    refine IH m hm.2 (hm.1.trans hd) (Finset.card_pos.2 ⟨a ^ (d / m), ?_⟩)
    rw [mem_filter_univ, orderOf_pow a, ha, Nat.gcd_eq_right (div_dvd_of_dvd hm.1),
      Nat.div_div_self hm.1 hd0]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
IH :
  ∀ m < d,
    ∀ (hd : m ∣ Fintype.card α) (hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = m}),
      card.{u_1} (α := α) {a : α | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : Membership.mem (γ := Finset α) {a : α | orderOf a = d} a
ha : orderOf a = d
h1 : Eq (α := ℕ) (∑ m ∈ d.properDivisors, card.{u_1} (α := α) {a : α | orderOf a = m}) (∑ m ∈ d.properDivisors, φ m)
⊢ Eq (α := ℕ) (∑ m ∈ d.divisors, card.{u_1} (α := α) {a : α | orderOf a = m}) (∑ m ∈ d.divisors, φ m)
have rw : card.{u_1} (α := α) {x : α | x ^ d = 1} = ∑ m ∈ d.divisors, φ m
Tactic: rw [sum_card_orderOf_eq_card_pow_eq_one hd0, sum_totient,
      ← ha, card_pow_eq_one_eq_orderOf_aux hn a]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
IH :
  ∀ m < d,
    ∀ (hd : m ∣ Fintype.card α) (hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = m}),
      card.{u_1} (α := α) {a : α | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : Membership.mem (γ := Finset α) {a : α | orderOf a = d} a
ha : orderOf a = d
h1 : Eq (α := ℕ) (∑ m ∈ d.properDivisors, card.{u_1} (α := α) {a : α | orderOf a = m}) (∑ m ∈ d.properDivisors, φ m)
rw : card.{u_1} (α := α) {x : α | x ^ d = 1} = ∑ m ∈ d.divisors, φ m
⊢ Eq (α := ℕ) (∑ m ∈ d.divisors, card.{u_1} (α := α) {a : α | orderOf a = m}) (∑ m ∈ d.divisors, φ m)
have rw₁ : card.{u_1} (α := α) {x : α | x ^ d = 1} = d
Tactic: rw [sum_card_orderOf_eq_card_pow_eq_one hd0, sum_totient,
      ← ha, card_pow_eq_one_eq_orderOf_aux hn a]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
IH :
  ∀ m < d,
    ∀ (hd : m ∣ Fintype.card α) (hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = m}),
      card.{u_1} (α := α) {a : α | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : Membership.mem (γ := Finset α) {a : α | orderOf a = d} a
ha : orderOf a = d
h1 : Eq (α := ℕ) (∑ m ∈ d.properDivisors, card.{u_1} (α := α) {a : α | orderOf a = m}) (∑ m ∈ d.properDivisors, φ m)
rw : card.{u_1} (α := α) {x : α | x ^ d = 1} = ∑ m ∈ d.divisors, φ m
rw₁ : card.{u_1} (α := α) {x : α | x ^ d = 1} = d
⊢ Eq (α := ℕ) (∑ m ∈ d.divisors, card.{u_1} (α := α) {a : α | orderOf a = m}) (∑ m ∈ d.divisors, φ m)
have rw₂ : card.{u_1} (α := α) {x : α | x ^ orderOf a = 1} = orderOf a
Tactic: rw [sum_card_orderOf_eq_card_pow_eq_one hd0, sum_totient,
      ← ha, card_pow_eq_one_eq_orderOf_aux hn a]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
IH :
  ∀ m < d,
    ∀ (hd : m ∣ Fintype.card α) (hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = m}),
      card.{u_1} (α := α) {a : α | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : Membership.mem (γ := Finset α) {a : α | orderOf a = d} a
ha : orderOf a = d
h1 : Eq (α := ℕ) (∑ m ∈ d.properDivisors, card.{u_1} (α := α) {a : α | orderOf a = m}) (∑ m ∈ d.properDivisors, φ m)
rw : card.{u_1} (α := α) {x : α | x ^ d = 1} = ∑ m ∈ d.divisors, φ m
rw₁ : card.{u_1} (α := α) {x : α | x ^ d = 1} = d
rw₂ : card.{u_1} (α := α) {x : α | x ^ orderOf a = 1} = orderOf a
⊢ Eq (α := ℕ) (∑ m ∈ d.divisors, card.{u_1} (α := α) {a : α | orderOf a = m}) (∑ m ∈ d.divisors, φ m)
have rw₃ : orderOf a = orderOf a
Tactic: rw [sum_card_orderOf_eq_card_pow_eq_one hd0, sum_totient,
      ← ha, card_pow_eq_one_eq_orderOf_aux hn a]