awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
inst_3 : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
m : ℕ
hm : IsEmpty α
hm0 : m = 0
⊢ False

Tactic:
hm.elim' 1

Premises used: IsEmpty.elim', OfNat.ofNat
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
inst_3 : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
m : ℕ
hm : IsEmpty α
hm0 : m = 0
⊢ False

Tactic:
exact hm.elim' 1

Premises used: IsEmpty.elim', OfNat.ofNat
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
inst_3 : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
m : ℕ
hm : Fintype.card α = n.gcd (Fintype.card α) * m
⊢ 0 < m

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
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
inst_3 : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
m : ℕ
hm : Fintype.card α = n.gcd (Fintype.card α) * m
hm0 : 0 < m
simp : Fintype.card.{u_1} ↥(zpowers (g ^ (Fintype.card α / n.gcd (Fintype.card α)))) ≤ n
⊢ #(↑(zpowers (g ^ (Fintype.card α / n.gcd (Fintype.card α)))) : Set α).toFinset ≤ n

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

Premises used: SetLike.coe_sort_coe, Set.toFinset_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
inst_3 : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
m : ℕ
hm : Fintype.card α = n.gcd (Fintype.card α) * m
hm0 : 0 < m
rw : Fintype.card α / (Fintype.card α).gcd (Fintype.card α / n.gcd (Fintype.card α)) ≤ n
⊢ Fintype.card.{u_1} ↥(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]

Premises used: orderOf_eq_card_of_forall_mem_zpowers, orderOf_pow, Fintype.card_zpowers, Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
inst_3 : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
m : ℕ
hm : Fintype.card α = n.gcd (Fintype.card α) * m
hm0 : 0 < m
nth_rw : Fintype.card α / (n.gcd (Fintype.card α) * m).gcd (Fintype.card α / n.gcd (Fintype.card α)) ≤ n
⊢ Fintype.card α / (Fintype.card α).gcd (Fintype.card α / n.gcd (Fintype.card α)) ≤ n

Tactic:
nth_rw 2 [hm]
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
inst_3 : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
m : ℕ
hm : Fintype.card α = n.gcd (Fintype.card α) * m
hm0 : 0 < m
nth_rw : Fintype.card α / (n.gcd (Fintype.card α) * m).gcd (n.gcd (Fintype.card α) * m / n.gcd (Fintype.card α)) ≤ n
⊢ Fintype.card α / (n.gcd (Fintype.card α) * m).gcd (Fintype.card α / n.gcd (Fintype.card α)) ≤ n

Tactic:
nth_rw 3 [hm]
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
inst_3 : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
m : ℕ
hm : Fintype.card α = n.gcd (Fintype.card α) * m
hm0 : 0 < m
rw : n.gcd (Fintype.card α) ≤ n
⊢ 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]

Premises used: Nat.mul_div_cancel, Nat.mul_div_cancel_left, Nat.gcd_mul_left_left, Nat.gcd_pos_of_pos_left
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
inst_3 : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
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 _ _)

Premises used: Nat.gcd_dvd_left, Nat.le_of_dvd
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
inst_1 : Finite α
inst_2 : IsCyclic α
simp_rw : ∃ (x : α), ∀ (y : α), Membership.mem (γ := Subgroup α) (zpowers x) y
⊢ ∃ (x : α), ∀ (y : α), Membership.mem (γ := Submonoid α) (Submonoid.powers x) y

Tactic:
simp_rw [mem_powers_iff_mem_zpowers]

Premises used: mem_powers_iff_mem_zpowers
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
inst_1 : Finite α
inst_2 : IsCyclic α
⊢ ∃ (x : α), ∀ (y : α), Membership.mem (γ := Subgroup α) (zpowers x) y

Tactic:
IsCyclic.exists_generator

Premises used: IsCyclic.exists_generator
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
inst_1 : Finite α
inst_2 : IsCyclic α
⊢ ∃ (x : α), ∀ (y : α), Membership.mem (γ := Subgroup α) (zpowers x) y

Tactic:
exact IsCyclic.exists_generator

Premises used: IsCyclic.exists_generator
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
h : IsCyclic α
obtain : ∀ (g : α) (hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x), ∃ (g : α), orderOf g = Nat.card α
⊢ ∃ (g : α), orderOf g = Nat.card α

Tactic:
obtain ⟨g, hg⟩ := h.exists_generator

Premises used: IsCyclic.exists_generator
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
h : IsCyclic α
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
h₁ : orderOf g = Nat.card α
⊢ ∃ (g : α), orderOf g = Nat.card α

Tactic:
use g
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
h : IsCyclic α
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
h₁ : Nat.card.{u_1} ↥⊤ = Nat.card α
⊢ orderOf g = Nat.card α

Tactic:
rw [← card_zpowers g, (eq_top_iff' (zpowers g)).mpr hg]

Premises used: Iff.mpr, Subgroup.eq_top_iff', Nat.card_zpowers, Subgroup.zpowers
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
h : IsCyclic α
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
⊢ Nat.card.{u_1} ↥⊤ = Nat.card α

Tactic:
Nat.card_congr (Equiv.Set.univ α)

Premises used: Nat.card_congr, Equiv.Set.univ
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
h : IsCyclic α
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
⊢ Nat.card.{u_1} ↥⊤ = Nat.card α

Tactic:
exact Nat.card_congr (Equiv.Set.univ α)

Premises used: Nat.card_congr, Equiv.Set.univ
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst : Group α
inst_1 : Group G
inst_2 : Group G'
M : Type u_4
inst_3 : Monoid M
inst_4 : IsCyclic G
inst_5 : MulDistribMulAction M G
n : ℕ
hn : Nat.card G = n
obtain :
  ∀ (g : G) (hg : orderOf g = Nat.card G),
    Eq (α := ZMod n)
      (↑(Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom.{u_4, u_2} (M := M) G 1 : (a : G) → G) g = g ^ m)
            ⋯) :
        ZMod n)
      1
⊢ Eq (α := ZMod n)
    (↑(Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom.{u_4, u_2} (M := M) G 1 : (a : G) → G) g = g ^ m) ⋯) :
      ZMod n)
    1

Tactic:
obtain ⟨g, hg⟩ := IsCyclic.exists_ofOrder_eq_natCard (α := G)

Premises used: IsCyclic.exists_ofOrder_eq_natCard
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst : Group α
inst_1 : Group G
inst_2 : Group G'
M : Type u_4
inst_3 : Monoid M
inst_4 : IsCyclic G
inst_5 : MulDistribMulAction M G
n : ℕ
hn : Nat.card G = n
g : G
hg : orderOf g = Nat.card G
rw :
  Eq (α := ZMod n)
    (↑(Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom.{u_4, u_2} (M := M) G 1 : (a : G) → G) g = g ^ m) ⋯) :
      ZMod n)
    (↑1 : ZMod n)
rw₁ :
  Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom.{u_4, u_2} (M := M) G 1 : (a : G) → G) g = g ^ m) ⋯ ≡
    1 [ZMOD (↑n : ℤ)]
rw₂ :
  Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom.{u_4, u_2} (M := M) G 1 : (a : G) → G) g = g ^ m) ⋯ ≡
    1 [ZMOD (↑(Nat.card G) : ℤ)]
rw₃ :
  Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom.{u_4, u_2} (M := M) G 1 : (a : G) → G) g = g ^ m) ⋯ ≡
    1 [ZMOD (↑(orderOf g) : ℤ)]
rw₄ :
  g ^ Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom.{u_4, u_2} (M := M) G 1 : (a : G) → G) g = g ^ m) ⋯ =
    HPow.hPow (β := ℤ) g 1
rw₅ :
  g ^ Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom.{u_4, u_2} (M := M) G 1 : (a : G) → G) g = g ^ m) ⋯ = g
rw₆ : (toMonoidHom.{u_4, u_2} (M := M) G 1 : (a : G) → G) g = g
rw₇ : HSMul.hSMul.{u_4, u_2, u_2} (α := M) 1 g = g
rw₈ rw₉ : g = g
⊢ Eq (α := ZMod n)
    (↑(Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom.{u_4, u_2} (M := M) G 1 : (a : G) → G) g = g ^ m) ⋯) :
      ZMod n)
    1

Tactic:
rw [← Int.cast_one, ZMod.intCast_eq_intCast_iff, ← hn, ← hg, ← zpow_eq_zpow_iff_modEq,
      zpow_one, ← (MulDistribMulAction.toMonoidHom G 1).map_cyclic.choose_spec,
      MulDistribMulAction.toMonoidHom_apply, one_smul]

Premises used: Exists.choose_spec, MonoidHom.map_cyclic, zpow_one, one_smul, ZMod.intCast_eq_intCast_iff, zpow_eq_zpow_iff_modEq, OfNat.ofNat, MulDistribMulAction.toMonoidHom, Int.cast_one, MulDistribMulAction.toMonoidHom_apply
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst : Group α
inst_1 : Group G
inst_2 : Group G'
M : Type u_4
inst_3 : Monoid M
inst_4 : IsCyclic G
inst_5 : MulDistribMulAction M G
n_1 : ℕ
hn : Nat.card G = n_1
m n : M
obtain :
  ∀ (g : G) (hg : orderOf g = Nat.card G),
    (↑(Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G (m * n) : (a : G) → G) g = g ^ m_1) ⋯) :
        ZMod n_1) =
      HMul.hMul (α := ZMod n_1)
        (↑(Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G m : (a : G) → G) g = g ^ m_1) ⋯) : ZMod n_1)
        (↑(Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom G n : (a : G) → G) g = g ^ m) ⋯) : ZMod n_1)
⊢ (↑(Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G (m * n) : (a : G) → G) g = g ^ m_1) ⋯) : ZMod n_1) =
    HMul.hMul (α := ZMod n_1)
      (↑(Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G m : (a : G) → G) g = g ^ m_1) ⋯) : ZMod n_1)
      (↑(Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom G n : (a : G) → G) g = g ^ m) ⋯) : ZMod n_1)

Tactic:
obtain ⟨g, hg⟩ := IsCyclic.exists_ofOrder_eq_natCard (α := G)

Premises used: IsCyclic.exists_ofOrder_eq_natCard
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
inst : Group G
M : Type u_4
inst_1 : Monoid M
inst_2 : IsCyclic G
inst_3 : MulDistribMulAction M G
n : ℕ
hn : Nat.card G = n
m : M
g : G
k : ℤ
h :
  Eq (α := ZMod n) (((toMonoidHomZModOfIsCyclic G M hn : M →* ZMod n) : (a : M) → ZMod n) m : ZMod n)
    ((↑k : ZMod n) : ZMod n)
rw :
  Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G m : (a : G) → G) g = g ^ m_1) ⋯ ≡ k [ZMOD
    (↑(orderOf g) : ℤ)]
⊢ m • g = g ^ k

Tactic:
rw [← MulDistribMulAction.toMonoidHom_apply,
    (MulDistribMulAction.toMonoidHom G m).map_cyclic.choose_spec g, zpow_eq_zpow_iff_modEq]

Premises used: Exists.choose_spec, MonoidHom.map_cyclic, zpow_eq_zpow_iff_modEq, MulDistribMulAction.toMonoidHom, MulDistribMulAction.toMonoidHom_apply
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
inst : Group G
M : Type u_4
inst_1 : Monoid M
inst_2 : IsCyclic G
inst_3 : MulDistribMulAction M G
n : ℕ
hn : Nat.card G = n
m : M
g : G
k : ℤ
h :
  Eq (α := ZMod n) (((toMonoidHomZModOfIsCyclic G M hn : M →* ZMod n) : (a : M) → ZMod n) m : ZMod n)
    ((↑k : ZMod n) : ZMod n)
apply :
  Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G m : (a : G) → G) g = g ^ m_1) ⋯ ≡ k [ZMOD
    (↑(Nat.card G) : ℤ)]
⊢ Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G m : (a : G) → G) g = g ^ m_1) ⋯ ≡ k [ZMOD
    (↑(orderOf g) : ℤ)]

Tactic:
apply Int.ModEq.of_dvd (Int.natCast_dvd_natCast.mpr (orderOf_dvd_natCard g))

Premises used: Iff.mpr, orderOf_dvd_natCard, Int.ModEq.of_dvd, Int.natCast_dvd_natCast
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
inst : Group G
M : Type u_4
inst_1 : Monoid M
inst_2 : IsCyclic G
inst_3 : MulDistribMulAction M G
n : ℕ
hn : Nat.card G = n
m : M
g : G
k : ℤ
h :
  Eq (α := ZMod n) (((toMonoidHomZModOfIsCyclic G M hn : M →* ZMod n) : (a : M) → ZMod n) m : ZMod n)
    ((↑k : ZMod n) : ZMod n)
rwa : Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G m : (a : G) → G) g = g ^ m_1) ⋯ ≡ k [ZMOD (↑n : ℤ)]
rwa₁ rwa₂ rwa₃ rwa₄ :
  Eq (α := ZMod n)
    (↑(Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G m : (a : G) → G) g = g ^ m_1) ⋯) : ZMod n)
    (↑k : ZMod n)
⊢ Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G m : (a : G) → G) g = g ^ m_1) ⋯ ≡ k [ZMOD
    (↑(Nat.card G) : ℤ)]

Tactic:
rwa [hn, ← ZMod.intCast_eq_intCast_iff]

Premises used: ZMod.intCast_eq_intCast_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
a : α
inst : Group α
inst_1 : Fintype α
ha : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers a) x
x : α
obtain : ∀ (n : ℤ), ∃! n_1 : ZMod (Fintype.card α), (fun (x : ℤ) ↦ a ^ x) n = a ^ n_1.val
⊢ ∃! n : ZMod (Fintype.card α), x = a ^ n.val

Tactic:
obtain ⟨n, rfl⟩ := ha x

Premises used: rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
a : α
inst : Group α
inst_1 : Fintype α
ha : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers a) x
n : ℤ
⊢ ∃! n_1 : ZMod (Fintype.card α), (fun (x : ℤ) ↦ a ^ x) n = a ^ n_1.val

Tactic:
⟨n, (?_ : a ^ n = _), fun y (hy : a ^ n = _) ↦ ?_⟩

Premises used: Int.cast, ExistsUnique, And.intro, Exists.intro
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
a : α
inst : Group α
inst_1 : Fintype α
ha : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers a) x
n : ℤ
refine_1 : a ^ n = a ^ ZMod.val (n := Fintype.card α) (↑n : ZMod (Fintype.card α))
refine_2 : ∀ (y : ZMod (Fintype.card α)) (hy : a ^ n = a ^ y.val), y = (↑n : ZMod (Fintype.card α))
⊢ ∃! n_1 : ZMod (Fintype.card α), (fun (x : ℤ) ↦ a ^ x) n = a ^ n_1.val

Tactic:
refine ⟨n, (?_ : a ^ n = _), fun y (hy : a ^ n = _) ↦ ?_⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
a : α
inst : Group α
inst_1 : Fintype α
ha : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers a) x
n : ℤ
refine_1 : a ^ n = HPow.hPow (β := ℤ) a (↑(ZMod.val (n := Fintype.card α) (↑n : ZMod (Fintype.card α))) : ℤ)
refine_1₁ : n ≡ (↑(ZMod.val (n := Fintype.card α) (↑n : ZMod (Fintype.card α))) : ℤ) [ZMOD (↑(orderOf a) : ℤ)]
refine_1₂ : n ≡ (↑(ZMod.val (n := Fintype.card α) (↑n : ZMod (Fintype.card α))) : ℤ) [ZMOD (↑(Nat.card α) : ℤ)]
refine_1₃ : (↑(ZMod.val (n := Fintype.card α) (↑n : ZMod (Fintype.card α))) : ℤ) ≡ n [ZMOD (↑(Nat.card α) : ℤ)]
refine_1₄ :
  ∃ (t : ℤ), n = (↑(ZMod.val (n := Fintype.card α) (↑n : ZMod (Fintype.card α))) : ℤ) + (↑(Nat.card α) : ℤ) * t
refine_1₅ :
  ∃ (t : ℤ), n = (↑(ZMod.val (n := Fintype.card α) (↑n : ZMod (Fintype.card α))) : ℤ) + (↑(Fintype.card α) : ℤ) * t
refine_1₆ refine_1₇ : Eq (α := ZMod (Fintype.card α)) (↑n : ZMod (Fintype.card α)) (↑n : ZMod (Fintype.card α))
⊢ a ^ n = a ^ ZMod.val (n := Fintype.card α) (↑n : ZMod (Fintype.card α))

Tactic:
rw [← zpow_natCast, zpow_eq_zpow_iff_modEq, orderOf_eq_card_of_forall_mem_zpowers ha,
      Int.modEq_comm, Int.modEq_iff_add_fac, Nat.card_eq_fintype_card, ← ZMod.intCast_eq_iff]

Premises used: zpow_natCast, orderOf_eq_card_of_forall_mem_zpowers, Int.modEq_iff_add_fac, ZMod.intCast_eq_iff, Int.modEq_comm, zpow_eq_zpow_iff_modEq, Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
a : α
inst : Group α
inst_1 : Fintype α
ha : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers a) x
n : ℤ
y : ZMod (Fintype.card α)
hy : a ^ n = a ^ y.val
⊢ Eq (α := ZMod (Fintype.card α)) (↑n : ZMod (Fintype.card α)) (↑(↑y.val : ℤ) : ZMod (Fintype.card α))

Tactic:
rw [← zpow_natCast, zpow_eq_zpow_iff_modEq, orderOf_eq_card_of_forall_mem_zpowers ha,
      Nat.card_eq_fintype_card, ← ZMod.intCast_eq_intCast_iff] at hy

Premises used: zpow_natCast, orderOf_eq_card_of_forall_mem_zpowers, ZMod.intCast_eq_intCast_iff, zpow_eq_zpow_iff_modEq, Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
a : α
inst : Group α
inst_1 : Fintype α
ha : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers a) x
n : ℤ
y : ZMod (Fintype.card α)
hy : Eq (α := ZMod (Fintype.card α)) (↑n : ZMod (Fintype.card α)) (↑(↑y.val : ℤ) : ZMod (Fintype.card α))
⊢ y = (↑n : ZMod (Fintype.card α))

Tactic:
simp [hy]
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
a : α
inst : Group α
inst_1 : Fintype α
inst_2 : DecidableEq α
ha : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers a) x
⊢ Eq.{u_1 + 1} (α := Finset α) (image (fun (i : ℕ) ↦ a ^ i) (range (orderOf a))) univ

Tactic:
simp only [_root_.image_range_orderOf, Set.eq_univ_iff_forall.mpr ha, Set.toFinset_univ]

Premises used: Iff.mpr, Set.eq_univ_iff_forall, image_range_orderOf, Set.toFinset_univ
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
a : α
inst : Group α
inst_1 : Fintype α
inst_2 : DecidableEq α
ha : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers a) x
rw : Eq.{u_1 + 1} (α := Finset α) (image (fun (i : ℕ) ↦ a ^ i) (range (orderOf a))) univ
rw₁ rw₂ : Eq.{u_1 + 1} (α := Finset α) univ univ
⊢ Eq.{u_1 + 1} (α := Finset α) (image (fun (i : ℕ) ↦ a ^ i) (range (Nat.card α))) univ

Tactic:
rw [← orderOf_eq_card_of_forall_mem_zpowers ha, IsCyclic.image_range_orderOf ha]

Premises used: IsCyclic.image_range_orderOf, orderOf_eq_card_of_forall_mem_zpowers
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
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
⊢ NeZero (Nat.card G)

Tactic:
have : NeZero (Nat.card G) := ⟨Nat.card_pos.ne'⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
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)
obtain : ∀ (g : G) (hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (zpowers g) x), a = b
⊢ a = b

Tactic:
obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := G)

Premises used: IsCyclic.exists_generator
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
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
⊢ g ^ a.val = g ^ b.val

Tactic:
specialize h g
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
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
subst : ∀ {a b : ZMod (Nat.card G)} (h : g ^ a.val = g ^ b.val), a = b
⊢ a = b

Tactic:
subst hGcard
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
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
⊢ 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

Premises used: orderOf_eq_card_of_forall_mem_zpowers, pow_eq_pow_iff_modEq, ZMod.natCast_eq_natCast_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
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 : Eq (α := ZMod (Nat.card G)) (↑a.val : ZMod (Nat.card G)) (↑b.val : ZMod (Nat.card G))
⊢ a = b

Tactic:
simpa [ZMod.natCast_val, ZMod.cast_id'] using h

Premises used: ZMod.natCast_val, ZMod.cast_id'
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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)
let : ∀ (i : ℤ) (hi : (fun (x : ℤ) ↦ a ^ x) i = (↑b : α)), (↑b : α) ^ orderOf a = 1
⊢ (↑b : α) ^ orderOf a = 1

Tactic:
let ⟨i, hi⟩ := b.2
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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
rw₇ rw₈ : Eq.{u_1 + 1} (α := α) 1 1
⊢ (↑b : α) ^ orderOf a = 1

Tactic:
rw [← hi, ← zpow_natCast, ← zpow_mul, mul_comm, zpow_mul, zpow_natCast,
                    pow_orderOf_eq_one, one_zpow]

Premises used: zpow_natCast, zpow_mul, one_zpow, pow_orderOf_eq_one, mul_comm
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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}
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
⊢ card.{u_1} (α := α) {a : α | orderOf a = d} = φ d

Tactic:
induction d using Nat.strongRec' with | _ d IH
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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
H₁ : ∀ (hd0 : d ≠ 0), card.{u_1} (α := α) {a : α | orderOf a = d} = φ d
⊢ card.{u_1} (α := α) {a : α | orderOf a = d} = φ d

Tactic:
rcases Decidable.eq_or_ne d 0 with (rfl | hd0)

Premises used: Decidable.eq_or_ne, OfNat.ofNat, rfl