awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
A : Type u_4
inst : AddCommGroup A
inst_1 : LinearOrder A
inst_2 : IsOrderedAddMonoid A
inst_3 : Nontrivial A
g : A
hs : Function.Surjective.{1, u_4 + 1} (β := A) fun (x : ℤ) ↦ x • g
a : A
ha : a ≠ 0
⊢ g ≠ 0
have obtain : ∀ (m : ℤ) (ha : Ne.{u_4 + 1} (α := A) ((fun (x : ℤ) ↦ x • g) m) 0), g ≠ 0
Tactic: obtain ⟨m, rfl⟩ := hs a
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
Goal:
A : Type u_4
inst : AddCommGroup A
inst_1 : LinearOrder A
inst_2 : IsOrderedAddMonoid A
inst_3 : Nontrivial A
g : A
hs : Function.Surjective.{1, u_4 + 1} (β := A) fun (x : ℤ) ↦ x • g
⊢ Nonempty.{max 1 (u_4 + 1)} (A ≃+o ℤ)
have h_ne : g ≠ 0
Tactic: have h_ne : g ≠ 0 := by
    obtain ⟨a, ha⟩ := exists_ne (0 : A)
    obtain ⟨m, rfl⟩ := hs a
    aesop
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
A : Type u_4
inst : AddCommGroup A
inst_1 : LinearOrder A
inst_2 : IsOrderedAddMonoid A
inst_3 : Nontrivial A
g : A
hs : Function.Surjective.{1, u_4 + 1} (β := A) fun (x : ℤ) ↦ x • g
h_ne : g ≠ 0
⊢ Nonempty.{max 1 (u_4 + 1)} (A ≃+o ℤ)
have inr : ∀
  (this :
    ∀ {A : Type u_4} [inst : AddCommGroup A] [inst_4 : LinearOrder A] [IsOrderedAddMonoid A] [Nontrivial A] (g : A)
      (hs : Function.Surjective.{1, u_4 + 1} (β := A) fun (x : ℤ) ↦ x • g) (h_ne : g ≠ 0) (hg' : 0 < g),
      Nonempty.{max 1 (u_4 + 1)} (A ≃+o ℤ))
  (hg' : ¬0 < g), Nonempty.{max 1 (u_4 + 1)} (A ≃+o ℤ)
Tactic: wlog hg' : 0 < g
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
A : Type u_4
inst : AddCommGroup A
inst_1 : LinearOrder A
inst_2 : IsOrderedAddMonoid A
inst_3 : Nontrivial A
g : A
hs : Function.Surjective.{1, u_4 + 1} (β := A) fun (x : ℤ) ↦ x • g
h_ne : g ≠ 0
inr :
  ∀
    (this :
      ∀ {A : Type u_4} [inst : AddCommGroup A] [inst_4 : LinearOrder A] [IsOrderedAddMonoid A] [Nontrivial A] (g : A)
        (hs : Function.Surjective.{1, u_4 + 1} (β := A) fun (x : ℤ) ↦ x • g) (h_ne : g ≠ 0) (hg' : 0 < g),
        Nonempty.{max 1 (u_4 + 1)} (A ≃+o ℤ))
    (hg' : ¬0 < g), Nonempty.{max 1 (u_4 + 1)} (A ≃+o ℤ)
⊢ Nonempty.{max 1 (u_4 + 1)} (A ≃+o ℤ)
have wlog : ∀ {A : Type u_4} [inst : AddCommGroup A] [inst_4 : LinearOrder A] [IsOrderedAddMonoid A] [Nontrivial A] (g : A)
  (hs : Function.Surjective.{1, u_4 + 1} (β := A) fun (x : ℤ) ↦ x • g) (h_ne : g ≠ 0) (hg' : 0 < g),
  Nonempty.{max 1 (u_4 + 1)} (A ≃+o ℤ)
Tactic: wlog hg' : 0 < g
Cleared hypotheses: A, inst, inst_1, inst_2, inst_3, g, hs, h_ne
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
Goal:
A : Type u_4
inst : AddCommGroup A
inst_1 : LinearOrder A
inst_2 : IsOrderedAddMonoid A
inst_3 : Nontrivial A
g : A
hs : Function.Surjective.{1, u_4 + 1} (β := A) fun (x : ℤ) ↦ x • g
h_ne : g ≠ 0
hg' : 0 < g
⊢ Nonempty.{max 1 (u_4 + 1)} (A ≃+o ℤ)
have hi : Function.Injective.{1, u_4 + 1} (β := A) fun (n : ℤ) ↦ n • g
Tactic: have hi : (fun n : ℤ ↦ n • g).Injective := injective_zsmul_iff_not_isOfFinAddOrder.mpr
      <| not_isOfFinAddOrder_of_isAddTorsionFree h_ne
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_4
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : Nontrivial G
⊢ IsCyclic G ↔ Nonempty.{max 1 (u_4 + 1)} (G ≃*o Multiplicative ℤ)
have rw : IsAddCyclic.{u_4} (Additive G) ↔ Nonempty.{max 1 (u_4 + 1)} (G ≃*o Multiplicative ℤ)
Tactic: rw [← isAddCyclic_additive_iff, LinearOrderedAddCommGroup.isAddCyclic_iff_nonempty_equiv_int,
    OrderAddMonoidIso.toMultiplicativeRight.nonempty_congr]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_4
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : Nontrivial G
rw : IsAddCyclic.{u_4} (Additive G) ↔ Nonempty.{max 1 (u_4 + 1)} (G ≃*o Multiplicative ℤ)
⊢ IsCyclic G ↔ Nonempty.{max 1 (u_4 + 1)} (G ≃*o Multiplicative ℤ)
have rw₁ : Nonempty.{u_4 + 1} (Additive G ≃+o ℤ) ↔ Nonempty.{max 1 (u_4 + 1)} (G ≃*o Multiplicative ℤ)
Tactic: rw [← isAddCyclic_additive_iff, LinearOrderedAddCommGroup.isAddCyclic_iff_nonempty_equiv_int,
    OrderAddMonoidIso.toMultiplicativeRight.nonempty_congr]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_4
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : Nontrivial G
rw : IsAddCyclic.{u_4} (Additive G) ↔ Nonempty.{max 1 (u_4 + 1)} (G ≃*o Multiplicative ℤ)
rw₁ : Nonempty.{u_4 + 1} (Additive G ≃+o ℤ) ↔ Nonempty.{max 1 (u_4 + 1)} (G ≃*o Multiplicative ℤ)
⊢ IsCyclic G ↔ Nonempty.{max 1 (u_4 + 1)} (G ≃*o Multiplicative ℤ)
have rw₂ : Nonempty.{max 1 (u_4 + 1)} (G ≃*o Multiplicative ℤ) ↔ Nonempty.{max 1 (u_4 + 1)} (G ≃*o Multiplicative ℤ)
Tactic: rw [← isAddCyclic_additive_iff, LinearOrderedAddCommGroup.isAddCyclic_iff_nonempty_equiv_int,
    OrderAddMonoidIso.toMultiplicativeRight.nonempty_congr]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : IsCyclic α
⊢ exponent α = Nat.card α
have obtain : ∀ (g : α) (hg : orderOf g = Nat.card α), exponent α = Nat.card α
Tactic: obtain ⟨g, hg⟩ := IsCyclic.exists_ofOrder_eq_natCard (α := α)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : IsCyclic α
g : α
hg : orderOf g = Nat.card α
⊢ exponent α = Nat.card α
have apply : Nat.card α ∣ exponent α
Tactic: apply Nat.dvd_antisymm Group.exponent_dvd_nat_card
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : IsCyclic α
g : α
hg : orderOf g = Nat.card α
⊢ Nat.card α ∣ exponent α
have rw : orderOf g ∣ exponent α
Tactic: rw [← hg]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
n : ℕ
⊢ AddMonoid.exponent (ZMod n) = n
have rw : Nat.card (ZMod n) = n
Tactic: rw [IsAddCyclic.exponent_eq_card, Nat.card_zmod]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
n : ℕ
rw : Nat.card (ZMod n) = n
⊢ AddMonoid.exponent (ZMod n) = n
have rw₁ : n = n
Tactic: rw [IsAddCyclic.exponent_eq_card, Nat.card_zmod]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = HPow.hPow (β := ℕ) p 2
⊢ ¬IsCyclic α ↔ exponent α = p
have this : Finite α
Tactic: have : Finite α := Nat.finite_of_card_ne_zero (hα ▸ pow_ne_zero 2 hp.ne_zero)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = HPow.hPow (β := ℕ) p 2
this : Finite α
⊢ ¬IsCyclic α ↔ exponent α = p
have this₁ : Nontrivial α
Tactic: have : Nontrivial α := Finite.one_lt_card_iff_nontrivial.mp
    (hα ▸ one_lt_pow₀ hp.one_lt two_ne_zero)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = HPow.hPow (β := ℕ) p 2
this_1 : Finite α
this : Nontrivial α
h_exp : exponent α = p
h_cyc : IsCyclic α
⊢ False
have inl : ∀ (hp : Nat.Prime 0) (hα : Nat.card α = HPow.hPow (α := ℕ) (β := ℕ) 0 2) (h_exp : exponent α = 0), False
Tactic: obtain (rfl | rfl) := eq_zero_or_one_of_sq_eq_self <| hα ▸ h_exp ▸ (h_cyc.exponent_eq_card).symm
Cleared hypotheses: p, hp, hα, h_exp
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = HPow.hPow (β := ℕ) p 2
this_1 : Finite α
this : Nontrivial α
h_exp : exponent α = p
h_cyc : IsCyclic α
inl : ∀ (hp : Nat.Prime 0) (hα : Nat.card α = HPow.hPow (α := ℕ) (β := ℕ) 0 2) (h_exp : exponent α = 0), False
⊢ False
have inr : ∀ (hp : Nat.Prime 1) (hα : Nat.card α = HPow.hPow (α := ℕ) (β := ℕ) 1 2) (h_exp : exponent α = 1), False
Tactic: obtain (rfl | rfl) := eq_zero_or_one_of_sq_eq_self <| hα ▸ h_exp ▸ (h_cyc.exponent_eq_card).symm
Cleared hypotheses: p, hp, hα, h_exp
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = HPow.hPow (β := ℕ) p 2
this_1 : Finite α
this : Nontrivial α
⊢ ¬IsCyclic α ↔ exponent α = p
have refine : ∀ (h_cyc : ¬IsCyclic α) (g : α) (hg : g ≠ 1), orderOf g = p
Tactic: refine ⟨fun h_cyc ↦ (Monoid.exponent_eq_prime_iff hp).mpr fun g hg ↦ ?_, fun h_exp h_cyc ↦ by
    obtain (rfl | rfl) := eq_zero_or_one_of_sq_eq_self <| hα ▸ h_exp ▸ (h_cyc.exponent_eq_card).symm
    · exact Nat.not_prime_zero hp
    · exact Nat.not_prime_one hp⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = HPow.hPow (β := ℕ) p 2
this_1 : Finite α
this : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
⊢ orderOf g = p
have this₁ : orderOf g ∈ (HPow.hPow (β := ℕ) p 2).divisors
Tactic: have := (Nat.mem_divisors (m := p ^ 2)).mpr ⟨hα ▸ orderOf_dvd_natCard (x := g), by aesop⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = HPow.hPow (β := ℕ) p 2
this_1 : Finite α
this_2 : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
this : orderOf g ∈ (HPow.hPow (β := ℕ) p 2).divisors
⊢ orderOf g = p
have this₁ : ∃ a < 3, p ^ a = orderOf g
Tactic: have : ∃ a < 3, p ^ a = orderOf g := by
    simpa [Nat.divisors_prime_pow hp 2] using this
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = HPow.hPow (β := ℕ) p 2
this_1 : Finite α
this_2 : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
this_3 : orderOf g ∈ (HPow.hPow (β := ℕ) p 2).divisors
this : ∃ a < 3, p ^ a = orderOf g
⊢ orderOf g = p
have obtain : ∀ (a : ℕ) (ha : a < 3) (ha' : p ^ a = orderOf g), orderOf g = p
Tactic: obtain ⟨a, ha, ha'⟩ := by simpa using this
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = HPow.hPow (β := ℕ) p 2
this_1 : Finite α
this_2 : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
this_3 : orderOf g ∈ (HPow.hPow (β := ℕ) p 2).divisors
this : ∃ a < 3, p ^ a = orderOf g
a : ℕ
ha : a < 3
ha' : p ^ a = orderOf g
⊢ orderOf g = p
have 0 : ∀ (ha : LT.lt (α := ℕ) 0 3) (ha' : HPow.hPow (β := ℕ) p 0 = orderOf g), orderOf g = p
Tactic: interval_cases a
Cleared hypotheses: ha, ha'
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = HPow.hPow (β := ℕ) p 2
this_1 : Finite α
this_2 : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
this_3 : orderOf g ∈ (HPow.hPow (β := ℕ) p 2).divisors
this : ∃ a < 3, p ^ a = orderOf g
a : ℕ
ha : a < 3
ha' : p ^ a = orderOf g
0 : ∀ (ha : LT.lt (α := ℕ) 0 3) (ha' : HPow.hPow (β := ℕ) p 0 = orderOf g), orderOf g = p
⊢ orderOf g = p
have 1 : ∀ (ha : LT.lt (α := ℕ) 1 3) (ha' : HPow.hPow (β := ℕ) p 1 = orderOf g), orderOf g = p
Tactic: interval_cases a
Cleared hypotheses: ha, ha'
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = HPow.hPow (β := ℕ) p 2
this_1 : Finite α
this_2 : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
this_3 : orderOf g ∈ (HPow.hPow (β := ℕ) p 2).divisors
this : ∃ a < 3, p ^ a = orderOf g
a : ℕ
ha : a < 3
ha' : p ^ a = orderOf g
0 : ∀ (ha : LT.lt (α := ℕ) 0 3) (ha' : HPow.hPow (β := ℕ) p 0 = orderOf g), orderOf g = p
1 : ∀ (ha : LT.lt (α := ℕ) 1 3) (ha' : HPow.hPow (β := ℕ) p 1 = orderOf g), orderOf g = p
⊢ orderOf g = p
have 2 : ∀ (ha : LT.lt (α := ℕ) 2 3) (ha' : HPow.hPow (β := ℕ) p 2 = orderOf g), orderOf g = p
Tactic: interval_cases a
Cleared hypotheses: ha, ha'
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : AddGroup G
g : G
⊢ Eq (α := AddSubgroup ℤ) (AddMonoidHom.ker.{0, u_2} (M := G) ((zmultiplesHom G : (a : G) → ℤ →+ G) g))
    (zmultiples (↑(addOrderOf g) : ℤ))
have h : ∀ (x : ℤ),
  Membership.mem (γ := AddSubgroup ℤ) (AddMonoidHom.ker.{0, u_2} (M := G) ((zmultiplesHom G : (a : G) → ℤ →+ G) g)) x ↔
    Membership.mem (γ := AddSubgroup ℤ) (zmultiples (↑(addOrderOf g) : ℤ)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : AddGroup G
g : G
x : ℤ
⊢ Membership.mem (γ := AddSubgroup ℤ) (AddMonoidHom.ker.{0, u_2} (M := G) ((zmultiplesHom G : (a : G) → ℤ →+ G) g)) x ↔
    Membership.mem (γ := AddSubgroup ℤ) (zmultiples (↑(addOrderOf g) : ℤ)) x
have h : Eq (α := G) ((((zmultiplesHom G : (a : G) → ℤ →+ G) g : ℤ →+ G) : (a : ℤ) → G) x : G) (0 : G) ↔
  Membership.mem (γ := AddSubgroup ℤ) (zmultiples (↑(addOrderOf g) : ℤ)) x
Tactic: simp_rw [AddMonoidHom.mem_ker, mem_zmultiples_iff, zmultiplesHom_apply,
    ← addOrderOf_dvd_iff_zsmul_eq_zero, zsmul_eq_mul', Int.cast_id, dvd_def, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : AddGroup G
g : G
x : ℤ
h :
  Eq (α := G) ((((zmultiplesHom G : (a : G) → ℤ →+ G) g : ℤ →+ G) : (a : ℤ) → G) x : G) (0 : G) ↔
    Membership.mem (γ := AddSubgroup ℤ) (zmultiples (↑(addOrderOf g) : ℤ)) x
⊢ Membership.mem (γ := AddSubgroup ℤ) (AddMonoidHom.ker.{0, u_2} (M := G) ((zmultiplesHom G : (a : G) → ℤ →+ G) g)) x ↔
    Membership.mem (γ := AddSubgroup ℤ) (zmultiples (↑(addOrderOf g) : ℤ)) x
have h₁ : Eq (α := G) ((((zmultiplesHom G : (a : G) → ℤ →+ G) g : ℤ →+ G) : (a : ℤ) → G) x : G) (0 : G) ↔
  ∃ (k : ℤ), HSMul.hSMul (β := ℤ) k (↑(addOrderOf g) : ℤ) = x
Tactic: simp_rw [AddMonoidHom.mem_ker, mem_zmultiples_iff, zmultiplesHom_apply,
    ← addOrderOf_dvd_iff_zsmul_eq_zero, zsmul_eq_mul', Int.cast_id, dvd_def, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : AddGroup G
g : G
x : ℤ
h :
  Eq (α := G) ((((zmultiplesHom G : (a : G) → ℤ →+ G) g : ℤ →+ G) : (a : ℤ) → G) x : G) (0 : G) ↔
    Membership.mem (γ := AddSubgroup ℤ) (zmultiples (↑(addOrderOf g) : ℤ)) x
h₁ :
  Eq (α := G) ((((zmultiplesHom G : (a : G) → ℤ →+ G) g : ℤ →+ G) : (a : ℤ) → G) x : G) (0 : G) ↔
    ∃ (k : ℤ), HSMul.hSMul (β := ℤ) k (↑(addOrderOf g) : ℤ) = x
⊢ Membership.mem (γ := AddSubgroup ℤ) (AddMonoidHom.ker.{0, u_2} (M := G) ((zmultiplesHom G : (a : G) → ℤ →+ G) g)) x ↔
    Membership.mem (γ := AddSubgroup ℤ) (zmultiples (↑(addOrderOf g) : ℤ)) x
have h₂ : x • g = 0 ↔ ∃ (k : ℤ), HSMul.hSMul (β := ℤ) k (↑(addOrderOf g) : ℤ) = x
Tactic: simp_rw [AddMonoidHom.mem_ker, mem_zmultiples_iff, zmultiplesHom_apply,
    ← addOrderOf_dvd_iff_zsmul_eq_zero, zsmul_eq_mul', Int.cast_id, dvd_def, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : AddGroup G
g : G
x : ℤ
h :
  Eq (α := G) ((((zmultiplesHom G : (a : G) → ℤ →+ G) g : ℤ →+ G) : (a : ℤ) → G) x : G) (0 : G) ↔
    Membership.mem (γ := AddSubgroup ℤ) (zmultiples (↑(addOrderOf g) : ℤ)) x
h₁ :
  Eq (α := G) ((((zmultiplesHom G : (a : G) → ℤ →+ G) g : ℤ →+ G) : (a : ℤ) → G) x : G) (0 : G) ↔
    ∃ (k : ℤ), HSMul.hSMul (β := ℤ) k (↑(addOrderOf g) : ℤ) = x
h₂ : x • g = 0 ↔ ∃ (k : ℤ), HSMul.hSMul (β := ℤ) k (↑(addOrderOf g) : ℤ) = x
⊢ Membership.mem (γ := AddSubgroup ℤ) (AddMonoidHom.ker.{0, u_2} (M := G) ((zmultiplesHom G : (a : G) → ℤ →+ G) g)) x ↔
    Membership.mem (γ := AddSubgroup ℤ) (zmultiples (↑(addOrderOf g) : ℤ)) x
have h₃ : (↑(addOrderOf g) : ℤ) ∣ x ↔ ∃ (k : ℤ), HSMul.hSMul (β := ℤ) k (↑(addOrderOf g) : ℤ) = x
Tactic: simp_rw [AddMonoidHom.mem_ker, mem_zmultiples_iff, zmultiplesHom_apply,
    ← addOrderOf_dvd_iff_zsmul_eq_zero, zsmul_eq_mul', Int.cast_id, dvd_def, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : AddGroup G
g : G
x : ℤ
h :
  Eq (α := G) ((((zmultiplesHom G : (a : G) → ℤ →+ G) g : ℤ →+ G) : (a : ℤ) → G) x : G) (0 : G) ↔
    Membership.mem (γ := AddSubgroup ℤ) (zmultiples (↑(addOrderOf g) : ℤ)) x
h₁ :
  Eq (α := G) ((((zmultiplesHom G : (a : G) → ℤ →+ G) g : ℤ →+ G) : (a : ℤ) → G) x : G) (0 : G) ↔
    ∃ (k : ℤ), HSMul.hSMul (β := ℤ) k (↑(addOrderOf g) : ℤ) = x
h₂ : x • g = 0 ↔ ∃ (k : ℤ), HSMul.hSMul (β := ℤ) k (↑(addOrderOf g) : ℤ) = x
h₃ : (↑(addOrderOf g) : ℤ) ∣ x ↔ ∃ (k : ℤ), HSMul.hSMul (β := ℤ) k (↑(addOrderOf g) : ℤ) = x
⊢ Membership.mem (γ := AddSubgroup ℤ) (AddMonoidHom.ker.{0, u_2} (M := G) ((zmultiplesHom G : (a : G) → ℤ →+ G) g)) x ↔
    Membership.mem (γ := AddSubgroup ℤ) (zmultiples (↑(addOrderOf g) : ℤ)) x
have h₄ : (↑(addOrderOf g) : ℤ) ∣ x ↔ ∃ (k : ℤ), HMul.hMul (α := ℤ) (↑(addOrderOf g) : ℤ) (↑k : ℤ) = x
Tactic: simp_rw [AddMonoidHom.mem_ker, mem_zmultiples_iff, zmultiplesHom_apply,
    ← addOrderOf_dvd_iff_zsmul_eq_zero, zsmul_eq_mul', Int.cast_id, dvd_def, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : AddGroup G
g : G
x : ℤ
h :
  Eq (α := G) ((((zmultiplesHom G : (a : G) → ℤ →+ G) g : ℤ →+ G) : (a : ℤ) → G) x : G) (0 : G) ↔
    Membership.mem (γ := AddSubgroup ℤ) (zmultiples (↑(addOrderOf g) : ℤ)) x
h₁ :
  Eq (α := G) ((((zmultiplesHom G : (a : G) → ℤ →+ G) g : ℤ →+ G) : (a : ℤ) → G) x : G) (0 : G) ↔
    ∃ (k : ℤ), HSMul.hSMul (β := ℤ) k (↑(addOrderOf g) : ℤ) = x
h₂ : x • g = 0 ↔ ∃ (k : ℤ), HSMul.hSMul (β := ℤ) k (↑(addOrderOf g) : ℤ) = x
h₃ : (↑(addOrderOf g) : ℤ) ∣ x ↔ ∃ (k : ℤ), HSMul.hSMul (β := ℤ) k (↑(addOrderOf g) : ℤ) = x
h₄ : (↑(addOrderOf g) : ℤ) ∣ x ↔ ∃ (k : ℤ), HMul.hMul (α := ℤ) (↑(addOrderOf g) : ℤ) (↑k : ℤ) = x
⊢ Membership.mem (γ := AddSubgroup ℤ) (AddMonoidHom.ker.{0, u_2} (M := G) ((zmultiplesHom G : (a : G) → ℤ →+ G) g)) x ↔
    Membership.mem (γ := AddSubgroup ℤ) (zmultiples (↑(addOrderOf g) : ℤ)) x
have h₅ : (↑(addOrderOf g) : ℤ) ∣ x ↔ ∃ (k : ℤ), (↑(addOrderOf g) : ℤ) * k = x
Tactic: simp_rw [AddMonoidHom.mem_ker, mem_zmultiples_iff, zmultiplesHom_apply,
    ← addOrderOf_dvd_iff_zsmul_eq_zero, zsmul_eq_mul', Int.cast_id, dvd_def, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : AddGroup G
g : G
x : ℤ
h :
  Eq (α := G) ((((zmultiplesHom G : (a : G) → ℤ →+ G) g : ℤ →+ G) : (a : ℤ) → G) x : G) (0 : G) ↔
    Membership.mem (γ := AddSubgroup ℤ) (zmultiples (↑(addOrderOf g) : ℤ)) x
h₁ :
  Eq (α := G) ((((zmultiplesHom G : (a : G) → ℤ →+ G) g : ℤ →+ G) : (a : ℤ) → G) x : G) (0 : G) ↔
    ∃ (k : ℤ), HSMul.hSMul (β := ℤ) k (↑(addOrderOf g) : ℤ) = x
h₂ : x • g = 0 ↔ ∃ (k : ℤ), HSMul.hSMul (β := ℤ) k (↑(addOrderOf g) : ℤ) = x
h₃ : (↑(addOrderOf g) : ℤ) ∣ x ↔ ∃ (k : ℤ), HSMul.hSMul (β := ℤ) k (↑(addOrderOf g) : ℤ) = x
h₄ : (↑(addOrderOf g) : ℤ) ∣ x ↔ ∃ (k : ℤ), HMul.hMul (α := ℤ) (↑(addOrderOf g) : ℤ) (↑k : ℤ) = x
h₅ : (↑(addOrderOf g) : ℤ) ∣ x ↔ ∃ (k : ℤ), (↑(addOrderOf g) : ℤ) * k = x
⊢ Membership.mem (γ := AddSubgroup ℤ) (AddMonoidHom.ker.{0, u_2} (M := G) ((zmultiplesHom G : (a : G) → ℤ →+ G) g)) x ↔
    Membership.mem (γ := AddSubgroup ℤ) (zmultiples (↑(addOrderOf g) : ℤ)) x
have h₆ : (∃ (c : ℤ), x = (↑(addOrderOf g) : ℤ) * c) ↔ ∃ (k : ℤ), (↑(addOrderOf g) : ℤ) * k = x
Tactic: simp_rw [AddMonoidHom.mem_ker, mem_zmultiples_iff, zmultiplesHom_apply,
    ← addOrderOf_dvd_iff_zsmul_eq_zero, zsmul_eq_mul', Int.cast_id, dvd_def, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst : AddGroup G
g : G
hg : ∀ (x : G), Membership.mem (γ := AddSubgroup G) (zmultiples g) x
n : ℕ
hn : Nat.card G = n
⊢ Eq (α := AddSubgroup ℤ) (zmultiples (↑n : ℤ))
    (AddMonoidHom.ker.{0, u_2} (M := G) ((zmultiplesHom G : (a : G) → ℤ →+ G) g))
have rw : Eq (α := AddSubgroup ℤ) (zmultiples (↑n : ℤ)) (zmultiples (↑(addOrderOf g) : ℤ))
Tactic: rw [zmultiplesHom_ker_eq, ← Nat.card_zmultiples, ← hn,
      Nat.card_congr (Equiv.subtypeUnivEquiv hg)]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst : AddGroup G
g : G
hg : ∀ (x : G), Membership.mem (γ := AddSubgroup G) (zmultiples g) x
n : ℕ
hn : Nat.card G = n
rw : Eq (α := AddSubgroup ℤ) (zmultiples (↑n : ℤ)) (zmultiples (↑(addOrderOf g) : ℤ))
⊢ Eq (α := AddSubgroup ℤ) (zmultiples (↑n : ℤ))
    (AddMonoidHom.ker.{0, u_2} (M := G) ((zmultiplesHom G : (a : G) → ℤ →+ G) g))
have rw₁ : Eq (α := AddSubgroup ℤ) (zmultiples (↑n : ℤ)) (zmultiples (↑(Nat.card.{u_2} ↥(zmultiples g)) : ℤ))
Tactic: rw [zmultiplesHom_ker_eq, ← Nat.card_zmultiples, ← hn,
      Nat.card_congr (Equiv.subtypeUnivEquiv hg)]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst : AddGroup G
g : G
hg : ∀ (x : G), Membership.mem (γ := AddSubgroup G) (zmultiples g) x
n : ℕ
hn : Nat.card G = n
rw : Eq (α := AddSubgroup ℤ) (zmultiples (↑n : ℤ)) (zmultiples (↑(addOrderOf g) : ℤ))
rw₁ : Eq (α := AddSubgroup ℤ) (zmultiples (↑n : ℤ)) (zmultiples (↑(Nat.card.{u_2} ↥(zmultiples g)) : ℤ))
⊢ Eq (α := AddSubgroup ℤ) (zmultiples (↑n : ℤ))
    (AddMonoidHom.ker.{0, u_2} (M := G) ((zmultiplesHom G : (a : G) → ℤ →+ G) g))
have rw₂ : Eq (α := AddSubgroup ℤ) (zmultiples (↑(Nat.card G) : ℤ)) (zmultiples (↑(Nat.card.{u_2} ↥(zmultiples g)) : ℤ))
Tactic: rw [zmultiplesHom_ker_eq, ← Nat.card_zmultiples, ← hn,
      Nat.card_congr (Equiv.subtypeUnivEquiv hg)]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst : AddGroup G
g : G
hg : ∀ (x : G), Membership.mem (γ := AddSubgroup G) (zmultiples g) x
n : ℕ
hn : Nat.card G = n
rw : Eq (α := AddSubgroup ℤ) (zmultiples (↑n : ℤ)) (zmultiples (↑(addOrderOf g) : ℤ))
rw₁ : Eq (α := AddSubgroup ℤ) (zmultiples (↑n : ℤ)) (zmultiples (↑(Nat.card.{u_2} ↥(zmultiples g)) : ℤ))
rw₂ : Eq (α := AddSubgroup ℤ) (zmultiples (↑(Nat.card G) : ℤ)) (zmultiples (↑(Nat.card.{u_2} ↥(zmultiples g)) : ℤ))
⊢ Eq (α := AddSubgroup ℤ) (zmultiples (↑n : ℤ))
    (AddMonoidHom.ker.{0, u_2} (M := G) ((zmultiplesHom G : (a : G) → ℤ →+ G) g))
have rw₃ : Eq (α := AddSubgroup ℤ) (zmultiples (↑(Nat.card G) : ℤ)) (zmultiples (↑(Nat.card G) : ℤ))
Tactic: rw [zmultiplesHom_ker_eq, ← Nat.card_zmultiples, ← hn,
      Nat.card_congr (Equiv.subtypeUnivEquiv hg)]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : AddGroup G
g : G
hg : ∀ (x : G), Membership.mem (γ := AddSubgroup G) (zmultiples g) x
n : ℕ
hn : Nat.card G = n
i : ℤ
⊢ (zmodAddEquivOfGenerator hg hn : (a : ZMod n) → G) (↑i : ZMod n) = i • g
have change : HSMul.hSMul (α := ℤ) (ZMod.cast (n := n) (↑i : ZMod n)) g = i • g
Tactic: change (ZMod.cast (i : ZMod n) : ℤ) • g = i • g
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : AddGroup G
g : G
hg : ∀ (x : G), Membership.mem (γ := AddSubgroup G) (zmultiples g) x
n : ℕ
hn : Nat.card G = n
i : ℤ
⊢ HSMul.hSMul (α := ℤ) (ZMod.cast (n := n) (↑i : ZMod n)) g = i • g
have rw : (i % (↑n : ℤ)) • g = i • g
Tactic: rw [ZMod.coe_intCast, Int.emod_def, eq_comm, ← sub_eq_zero, sub_eq_add_neg, ← sub_zsmul,
    Int.sub_sub_self, mul_zsmul', natCast_zsmul, ← hn, card_nsmul_eq_zero', zsmul_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : AddGroup G
g : G
hg : ∀ (x : G), Membership.mem (γ := AddSubgroup G) (zmultiples g) x
n : ℕ
hn : Nat.card G = n
i : ℤ
rw : (i % (↑n : ℤ)) • g = i • g
⊢ HSMul.hSMul (α := ℤ) (ZMod.cast (n := n) (↑i : ZMod n)) g = i • g
have rw₁ : (i - (↑n : ℤ) * (i / (↑n : ℤ))) • g = i • g
Tactic: rw [ZMod.coe_intCast, Int.emod_def, eq_comm, ← sub_eq_zero, sub_eq_add_neg, ← sub_zsmul,
    Int.sub_sub_self, mul_zsmul', natCast_zsmul, ← hn, card_nsmul_eq_zero', zsmul_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : AddGroup G
g : G
hg : ∀ (x : G), Membership.mem (γ := AddSubgroup G) (zmultiples g) x
n : ℕ
hn : Nat.card G = n
i : ℤ
rw : (i % (↑n : ℤ)) • g = i • g
rw₁ : (i - (↑n : ℤ) * (i / (↑n : ℤ))) • g = i • g
⊢ HSMul.hSMul (α := ℤ) (ZMod.cast (n := n) (↑i : ZMod n)) g = i • g
have rw₂ : i • g = (i - (↑n : ℤ) * (i / (↑n : ℤ))) • g
Tactic: rw [ZMod.coe_intCast, Int.emod_def, eq_comm, ← sub_eq_zero, sub_eq_add_neg, ← sub_zsmul,
    Int.sub_sub_self, mul_zsmul', natCast_zsmul, ← hn, card_nsmul_eq_zero', zsmul_zero]