awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
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
⊢ #(↑(zpowers (g ^ (Fintype.card α / n.gcd (Fintype.card α)))) : Set α).toFinset ≤ n
have let : ∀ (m : ℕ) (hm : Fintype.card α = n.gcd (Fintype.card α) * m),
  #(↑(zpowers (g ^ (Fintype.card α / n.gcd (Fintype.card α)))) : Set α).toFinset ≤ n
Tactic: let ⟨m, hm⟩ := Nat.gcd_dvd_right n (Fintype.card α)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (hypothesis)
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 : m = 0
⊢ False
have hm₁ : IsEmpty α
Tactic: rw [hm0, mul_zero, Fintype.card_eq_zero_iff] at hm
Cleared hypotheses: hm, hm0
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (hypothesis)
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
⊢ #(↑(zpowers (g ^ (Fintype.card α / n.gcd (Fintype.card α)))) : Set α).toFinset ≤ n
have hm0 : 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
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
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
⊢ #(↑(zpowers (g ^ (Fintype.card α / n.gcd (Fintype.card α)))) : Set α).toFinset ≤ n
have simp : Fintype.card.{u_1} ↥(zpowers (g ^ (Fintype.card α / n.gcd (Fintype.card α)))) ≤ n
Tactic: simp only [Set.toFinset_card, SetLike.coe_sort_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
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
⊢ Fintype.card.{u_1} ↥(zpowers (g ^ (Fintype.card α / n.gcd (Fintype.card α)))) ≤ n
have rw : Fintype.card α / (Fintype.card α).gcd (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]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
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
⊢ Fintype.card α / (Fintype.card α).gcd (Fintype.card α / n.gcd (Fintype.card α)) ≤ n
have nth_rw : Fintype.card α / (n.gcd (Fintype.card α) * m).gcd (Fintype.card α / n.gcd (Fintype.card α)) ≤ n
Tactic: nth_rw 2 [hm]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
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
⊢ Fintype.card α / (n.gcd (Fintype.card α) * m).gcd (Fintype.card α / n.gcd (Fintype.card α)) ≤ n
have nth_rw : Fintype.card α / (n.gcd (Fintype.card α) * m).gcd (n.gcd (Fintype.card α) * m / n.gcd (Fintype.card α)) ≤ n
Tactic: nth_rw 3 [hm]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
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
⊢ Fintype.card α / (n.gcd (Fintype.card α) * m).gcd (n.gcd (Fintype.card α) * m / n.gcd (Fintype.card α)) ≤ n
have rw : 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]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : Finite α
inst_2 : IsCyclic α
⊢ ∃ (x : α), ∀ (y : α), Membership.mem (γ := Submonoid α) (Submonoid.powers x) y
have simp_rw : ∃ (x : α), ∀ (y : α), Membership.mem (γ := Subgroup α) (zpowers x) y
Tactic: simp_rw [mem_powers_iff_mem_zpowers]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
α : Type u_1
inst : Group α
h : IsCyclic α
⊢ ∃ (g : α), orderOf g = Nat.card α
have obtain : ∀ (g : α) (hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x), ∃ (g : α), orderOf g = Nat.card α
Tactic: obtain ⟨g, hg⟩ := h.exists_generator
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
α : Type u_1
inst : Group α
h : IsCyclic α
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
⊢ ∃ (g : α), orderOf g = Nat.card α
have h₁ : orderOf g = Nat.card α
Tactic: use g
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
α : Type u_1
inst : Group α
h : IsCyclic α
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
⊢ orderOf g = Nat.card α
have h₁ : Nat.card.{u_1} ↥⊤ = Nat.card α
Tactic: rw [← card_zpowers g, (eq_top_iff' (zpowers g)).mpr hg]
-- 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 : ℕ
hn : Nat.card G = n
⊢ 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
have 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) sorry) :
      ZMod n)
    1
Tactic: obtain ⟨g, hg⟩ := IsCyclic.exists_ofOrder_eq_natCard (α := G)
-- 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 : ℕ
hn : Nat.card G = n
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
have 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) sorry) :
    ZMod n)
  (↑1 : ZMod n)
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]
-- 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 : ℕ
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)
⊢ 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
have rw₁ : Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom.{u_4, u_2} (M := M) G 1 : (a : G) → G) g = g ^ m) sorry ≡ 1 [ZMOD
  (↑n : ℤ)]
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]
-- 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 : ℕ
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 : ℤ)]
⊢ 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
have rw₂ : Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom.{u_4, u_2} (M := M) G 1 : (a : G) → G) g = g ^ m) sorry ≡ 1 [ZMOD
  (↑(Nat.card G) : ℤ)]
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]
-- 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 : ℕ
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) : ℤ)]
⊢ 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
have rw₃ : Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom.{u_4, u_2} (M := M) G 1 : (a : G) → G) g = g ^ m) sorry ≡ 1 [ZMOD
  (↑(orderOf g) : ℤ)]
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]
-- 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 : ℕ
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) : ℤ)]
⊢ 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
have rw₄ : g ^ Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom.{u_4, u_2} (M := M) G 1 : (a : G) → G) g = g ^ m) sorry =
  HPow.hPow (β := ℤ) g 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]
-- 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 : ℕ
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
⊢ 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
have rw₅ : g ^ Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom.{u_4, u_2} (M := M) G 1 : (a : G) → G) g = g ^ m) sorry = g
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]
-- 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 : ℕ
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
⊢ 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
have rw₆ : (toMonoidHom.{u_4, u_2} (M := M) G 1 : (a : G) → G) g = g
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]
-- 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 : ℕ
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
⊢ 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
have rw₇ : HSMul.hSMul.{u_4, u_2, u_2} (α := M) 1 g = g
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]
-- 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 : ℕ
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
⊢ 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
have rw₈ : g = g
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]
-- 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
⊢ (↑(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 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) sorry) : 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) sorry) : ZMod n_1)
      (↑(Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom G n : (a : G) → G) g = g ^ m) sorry) : ZMod n_1)
Tactic: obtain ⟨g, hg⟩ := IsCyclic.exists_ofOrder_eq_natCard (α := G)
-- 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
⊢ (↑(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 : Eq (α := ZMod n_1)
  (↑(Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G (m * n) : (a : G) → G) g = g ^ m_1) sorry) : ZMod n_1)
  (↑(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 n_1)
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)
⊢ (↑(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
  (↑n_1 : ℤ)]
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]