awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
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
g : G
hg : orderOf g = Nat.card G
rw :
  Eq (α := 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)
    (↑(Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G m : (a : G) → G) g = g ^ m_1) ⋯ *
          Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom G n : (a : G) → G) g = g ^ m) ⋯) :
      ZMod n_1)
rw₁ :
  Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G (m * n) : (a : G) → G) g = g ^ m_1) ⋯ ≡
    Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G m : (a : G) → G) g = g ^ m_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)
have rw₂ : Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G (m * n) : (a : G) → G) g = g ^ m_1) sorry ≡
  Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G m : (a : G) → G) g = g ^ m_1) sorry *
    Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom G n : (a : G) → G) g = g ^ m) sorry [ZMOD
  (↑(Nat.card G) : ℤ)]
Tactic: rw [← Int.cast_mul, ZMod.intCast_eq_intCast_iff, ← hn, ← hg, ← zpow_eq_zpow_iff_modEq,
      zpow_mul', ← (MulDistribMulAction.toMonoidHom G m).map_cyclic.choose_spec,
      ← (MulDistribMulAction.toMonoidHom G n).map_cyclic.choose_spec,
      ← (MulDistribMulAction.toMonoidHom G (m * n)).map_cyclic.choose_spec,
      MulDistribMulAction.toMonoidHom_apply, MulDistribMulAction.toMonoidHom_apply,
      MulDistribMulAction.toMonoidHom_apply, mul_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
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
g : G
hg : orderOf g = Nat.card G
rw :
  Eq (α := 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)
    (↑(Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G m : (a : G) → G) g = g ^ m_1) ⋯ *
          Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom G n : (a : G) → G) g = g ^ m) ⋯) :
      ZMod n_1)
rw₁ :
  Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G (m * n) : (a : G) → G) g = g ^ m_1) ⋯ ≡
    Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G m : (a : G) → G) g = g ^ m_1) ⋯ *
      Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom G n : (a : G) → G) g = g ^ m) ⋯ [ZMOD
    (↑n_1 : ℤ)]
rw₂ :
  Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G (m * n) : (a : G) → G) g = g ^ m_1) ⋯ ≡
    Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G m : (a : G) → G) g = g ^ m_1) ⋯ *
      Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom G n : (a : G) → G) g = g ^ m) ⋯ [ZMOD
    (↑(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)
have rw₃ : Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G (m * n) : (a : G) → G) g = g ^ m_1) sorry ≡
  Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G m : (a : G) → G) g = g ^ m_1) sorry *
    Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom G n : (a : G) → G) g = g ^ m) sorry [ZMOD
  (↑(orderOf g) : ℤ)]
Tactic: rw [← Int.cast_mul, ZMod.intCast_eq_intCast_iff, ← hn, ← hg, ← zpow_eq_zpow_iff_modEq,
      zpow_mul', ← (MulDistribMulAction.toMonoidHom G m).map_cyclic.choose_spec,
      ← (MulDistribMulAction.toMonoidHom G n).map_cyclic.choose_spec,
      ← (MulDistribMulAction.toMonoidHom G (m * n)).map_cyclic.choose_spec,
      MulDistribMulAction.toMonoidHom_apply, MulDistribMulAction.toMonoidHom_apply,
      MulDistribMulAction.toMonoidHom_apply, mul_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
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
g : G
hg : orderOf g = Nat.card G
rw :
  Eq (α := 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)
    (↑(Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G m : (a : G) → G) g = g ^ m_1) ⋯ *
          Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom G n : (a : G) → G) g = g ^ m) ⋯) :
      ZMod n_1)
rw₁ :
  Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G (m * n) : (a : G) → G) g = g ^ m_1) ⋯ ≡
    Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G m : (a : G) → G) g = g ^ m_1) ⋯ *
      Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom G n : (a : G) → G) g = g ^ m) ⋯ [ZMOD
    (↑n_1 : ℤ)]
rw₂ :
  Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G (m * n) : (a : G) → G) g = g ^ m_1) ⋯ ≡
    Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G m : (a : G) → G) g = g ^ m_1) ⋯ *
      Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom G n : (a : G) → G) g = g ^ m) ⋯ [ZMOD
    (↑(Nat.card G) : ℤ)]
rw₃ :
  Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G (m * n) : (a : G) → G) g = g ^ m_1) ⋯ ≡
    Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G m : (a : G) → G) g = g ^ m_1) ⋯ *
      Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom G n : (a : G) → G) g = g ^ m) ⋯ [ZMOD
    (↑(orderOf 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)
have rw₄ : g ^ Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G (m * n) : (a : G) → G) g = g ^ m_1) sorry =
  g ^
    (Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G m : (a : G) → G) g = g ^ m_1) sorry *
      Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom G n : (a : G) → G) g = g ^ m) sorry)
Tactic: rw [← Int.cast_mul, ZMod.intCast_eq_intCast_iff, ← hn, ← hg, ← zpow_eq_zpow_iff_modEq,
      zpow_mul', ← (MulDistribMulAction.toMonoidHom G m).map_cyclic.choose_spec,
      ← (MulDistribMulAction.toMonoidHom G n).map_cyclic.choose_spec,
      ← (MulDistribMulAction.toMonoidHom G (m * n)).map_cyclic.choose_spec,
      MulDistribMulAction.toMonoidHom_apply, MulDistribMulAction.toMonoidHom_apply,
      MulDistribMulAction.toMonoidHom_apply, mul_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
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
g : G
hg : orderOf g = Nat.card G
rw :
  Eq (α := 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)
    (↑(Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G m : (a : G) → G) g = g ^ m_1) ⋯ *
          Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom G n : (a : G) → G) g = g ^ m) ⋯) :
      ZMod n_1)
rw₁ :
  Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G (m * n) : (a : G) → G) g = g ^ m_1) ⋯ ≡
    Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G m : (a : G) → G) g = g ^ m_1) ⋯ *
      Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom G n : (a : G) → G) g = g ^ m) ⋯ [ZMOD
    (↑n_1 : ℤ)]
rw₂ :
  Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G (m * n) : (a : G) → G) g = g ^ m_1) ⋯ ≡
    Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G m : (a : G) → G) g = g ^ m_1) ⋯ *
      Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom G n : (a : G) → G) g = g ^ m) ⋯ [ZMOD
    (↑(Nat.card G) : ℤ)]
rw₃ :
  Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G (m * n) : (a : G) → G) g = g ^ m_1) ⋯ ≡
    Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G m : (a : G) → G) g = g ^ m_1) ⋯ *
      Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom G n : (a : G) → G) g = g ^ m) ⋯ [ZMOD
    (↑(orderOf g) : ℤ)]
rw₄ :
  g ^ Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G (m * n) : (a : G) → G) g = g ^ m_1) ⋯ =
    g ^
      (Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G m : (a : G) → G) g = g ^ m_1) ⋯ *
        Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom G n : (a : G) → G) g = g ^ m) ⋯)
⊢ (↑(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)
have rw₅ : g ^ Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G (m * n) : (a : G) → G) g = g ^ m_1) sorry =
  (g ^ Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom G n : (a : G) → G) g = g ^ m) sorry) ^
    Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G m : (a : G) → G) g = g ^ m_1) sorry
Tactic: rw [← Int.cast_mul, ZMod.intCast_eq_intCast_iff, ← hn, ← hg, ← zpow_eq_zpow_iff_modEq,
      zpow_mul', ← (MulDistribMulAction.toMonoidHom G m).map_cyclic.choose_spec,
      ← (MulDistribMulAction.toMonoidHom G n).map_cyclic.choose_spec,
      ← (MulDistribMulAction.toMonoidHom G (m * n)).map_cyclic.choose_spec,
      MulDistribMulAction.toMonoidHom_apply, MulDistribMulAction.toMonoidHom_apply,
      MulDistribMulAction.toMonoidHom_apply, mul_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
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)
⊢ m • g = g ^ k
have rw : Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G m : (a : G) → G) g = g ^ m_1) sorry ≡ k [ZMOD
  (↑(orderOf g) : ℤ)]
Tactic: rw [← MulDistribMulAction.toMonoidHom_apply,
    (MulDistribMulAction.toMonoidHom G m).map_cyclic.choose_spec g, zpow_eq_zpow_iff_modEq]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
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)
⊢ Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G m : (a : G) → G) g = g ^ m_1) ⋯ ≡ k [ZMOD
    (↑(orderOf g) : ℤ)]
have apply : Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G m : (a : G) → G) g = g ^ m_1) sorry ≡ k [ZMOD
  (↑(Nat.card G) : ℤ)]
Tactic: apply Int.ModEq.of_dvd (Int.natCast_dvd_natCast.mpr (orderOf_dvd_natCard g))
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
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)
⊢ Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G m : (a : G) → G) g = g ^ m_1) ⋯ ≡ k [ZMOD
    (↑(Nat.card G) : ℤ)]
have rwa : Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G m : (a : G) → G) g = g ^ m_1) sorry ≡ k [ZMOD (↑n : ℤ)]
Tactic: rwa [hn, ← ZMod.intCast_eq_intCast_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
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 : ℤ)]
⊢ Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G m : (a : G) → G) g = g ^ m_1) ⋯ ≡ k [ZMOD
    (↑(Nat.card G) : ℤ)]
have rwa₁ : Eq (α := ZMod n)
  (↑(Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G m : (a : G) → G) g = g ^ m_1) sorry) : ZMod n)
  (↑k : ZMod n)
Tactic: rwa [hn, ← ZMod.intCast_eq_intCast_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
α : Type u_1
a : α
inst : Group α
inst_1 : Fintype α
ha : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers a) x
x : α
⊢ ∃! n : ZMod (Fintype.card α), x = a ^ n.val
have obtain : ∀ (n : ℤ), ∃! n_1 : ZMod (Fintype.card α), (fun (x : ℤ) ↦ a ^ x) n = a ^ n_1.val
Tactic: obtain ⟨n, rfl⟩ := ha x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
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
have refine_1 : a ^ n = a ^ ZMod.val (n := Fintype.card α) (↑n : ZMod (Fintype.card α))
Tactic: refine ⟨n, (?_ : a ^ n = _), fun y (hy : a ^ n = _) ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
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 α))
⊢ ∃! n_1 : ZMod (Fintype.card α), (fun (x : ℤ) ↦ a ^ x) n = a ^ n_1.val
have refine_2 : ∀ (y : ZMod (Fintype.card α)) (hy : a ^ n = a ^ y.val), y = (↑n : ZMod (Fintype.card α))
Tactic: refine ⟨n, (?_ : a ^ n = _), fun y (hy : a ^ n = _) ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
α : Type u_1
a : α
inst : Group α
inst_1 : Fintype α
ha : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers a) x
n : ℤ
⊢ a ^ n = a ^ ZMod.val (n := Fintype.card α) (↑n : ZMod (Fintype.card α))
have refine_1 : a ^ n = HPow.hPow (β := ℤ) 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]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
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 α))) : ℤ)
⊢ a ^ n = a ^ ZMod.val (n := Fintype.card α) (↑n : ZMod (Fintype.card α))
have refine_1₁ : n ≡ (↑(ZMod.val (n := Fintype.card α) (↑n : ZMod (Fintype.card α))) : ℤ) [ZMOD (↑(orderOf a) : ℤ)]
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]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
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) : ℤ)]
⊢ a ^ n = a ^ ZMod.val (n := Fintype.card α) (↑n : ZMod (Fintype.card α))
have refine_1₂ : n ≡ (↑(ZMod.val (n := Fintype.card α) (↑n : ZMod (Fintype.card α))) : ℤ) [ZMOD (↑(Nat.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]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
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 α) : ℤ)]
⊢ a ^ n = a ^ ZMod.val (n := Fintype.card α) (↑n : ZMod (Fintype.card α))
have refine_1₃ : (↑(ZMod.val (n := Fintype.card α) (↑n : ZMod (Fintype.card α))) : ℤ) ≡ n [ZMOD (↑(Nat.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]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
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 α) : ℤ)]
⊢ a ^ n = a ^ ZMod.val (n := Fintype.card α) (↑n : ZMod (Fintype.card α))
have refine_1₄ : ∃ (t : ℤ), n = (↑(ZMod.val (n := Fintype.card α) (↑n : ZMod (Fintype.card α))) : ℤ) + (↑(Nat.card α) : ℤ) * t
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]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
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
⊢ a ^ n = a ^ ZMod.val (n := Fintype.card α) (↑n : ZMod (Fintype.card α))
have refine_1₅ : ∃ (t : ℤ), n = (↑(ZMod.val (n := Fintype.card α) (↑n : ZMod (Fintype.card α))) : ℤ) + (↑(Fintype.card α) : ℤ) * t
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]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
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
⊢ a ^ n = a ^ ZMod.val (n := Fintype.card α) (↑n : ZMod (Fintype.card α))
have refine_1₆ : Eq (α := ZMod (Fintype.card α)) (↑n : ZMod (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]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (hypothesis)
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
⊢ y = (↑n : ZMod (Fintype.card α))
have hy₁ : 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
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
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 (Nat.card α))) univ
have rw : Eq.{u_1 + 1} (α := Finset α) (image (fun (i : ℕ) ↦ a ^ i) (range (orderOf a))) univ
Tactic: rw [← orderOf_eq_card_of_forall_mem_zpowers ha, IsCyclic.image_range_orderOf ha]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
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
⊢ Eq.{u_1 + 1} (α := Finset α) (image (fun (i : ℕ) ↦ a ^ i) (range (Nat.card α))) univ
have rw₁ : Eq.{u_1 + 1} (α := Finset α) univ univ
Tactic: rw [← orderOf_eq_card_of_forall_mem_zpowers ha, IsCyclic.image_range_orderOf ha]
-- 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
⊢ a = b
have this : NeZero (Nat.card G)
Tactic: have : NeZero (Nat.card G) := ⟨Nat.card_pos.ne'⟩
-- 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
h : ∀ (t : G), t ^ a.val = t ^ b.val
this : NeZero (Nat.card G)
⊢ a = b
have obtain : ∀ (g : G) (hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (zpowers g) x), a = b
Tactic: obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := G)