awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
G : Type u_2
inst : Group G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card G
this : Finite G
a : G
ha : Function.Surjective.{1, u_2 + 1} (β := G) fun (x : ℤ) ↦ a ^ x
⊢ ∃ (a : G), a ^ k ≠ 1
have h : a ^ k ≠ 1
Tactic: use a
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
G : Type u_2
inst : Group G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card G
this : Finite G
a : G
ha : Function.Surjective.{1, u_2 + 1} (β := G) fun (x : ℤ) ↦ a ^ x
⊢ a ^ k ≠ 1
have h : ∀ (k_lt_card_G : a ^ k = 1), Nat.card G ≤ k
Tactic: contrapose! k_lt_card_G
Cleared hypotheses: k_lt_card_G
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
G : Type u_2
inst : Group G
k : ℕ
k_pos : k ≠ 0
this : Finite G
a : G
ha : Function.Surjective.{1, u_2 + 1} (β := G) fun (x : ℤ) ↦ a ^ x
k_lt_card_G : a ^ k = 1
⊢ Nat.card G ≤ k
have h : Nat.card G = orderOf a
Tactic: convert! orderOf_le_of_pow_eq_one k_pos.bot_lt k_lt_card_G
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
G : Type u_2
inst : Group G
k : ℕ
k_pos : k ≠ 0
this : Finite G
a : G
ha : Function.Surjective.{1, u_2 + 1} (β := G) fun (x : ℤ) ↦ a ^ x
k_lt_card_G : a ^ k = 1
⊢ Nat.card G = orderOf a
have h : LE.le (α := Subgroup G) ⊤ (zpowers a)
Tactic: rw [← Nat.card_zpowers, eq_comm, card_eq_iff_eq_top, eq_top_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : Infinite α
g : α
h : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
⊢ orderOf g = 0
have rw : Nat.card α = 0
Tactic: rw [orderOf_eq_card_of_forall_mem_zpowers h, Nat.card_eq_zero_of_infinite]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : Infinite α
g : α
h : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
rw : Nat.card α = 0
⊢ orderOf g = 0
have rw₁ : Eq (α := ℕ) 0 0
Tactic: rw [orderOf_eq_card_of_forall_mem_zpowers h, Nat.card_eq_zero_of_infinite]
-- 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'
inst_3 : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
hx : ∃ x ∈ H, x ≠ 1
x : α
hx₁ : x ∈ H
hx₂ : x ≠ 1
k : ℤ
hk_1 : (fun (x : ℤ) ↦ g ^ x) k = x
hk : g ^ k = x
h : k.natAbs = 0
⊢ x = 1
have rw : g ^ k = 1
Tactic: rw [← hk, Int.natAbs_eq_zero.mp h, zpow_zero]
-- 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'
inst_3 : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
hx : ∃ x ∈ H, x ≠ 1
x : α
hx₁ : x ∈ H
hx₂ : x ≠ 1
k : ℤ
hk_1 : (fun (x : ℤ) ↦ g ^ x) k = x
hk : g ^ k = x
h : k.natAbs = 0
rw : g ^ k = 1
⊢ x = 1
have rw₁ : HPow.hPow (β := ℤ) g 0 = 1
Tactic: rw [← hk, Int.natAbs_eq_zero.mp h, zpow_zero]
-- 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'
inst_3 : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
hx : ∃ x ∈ H, x ≠ 1
x : α
hx₁ : x ∈ H
hx₂ : x ≠ 1
k : ℤ
hk_1 : (fun (x : ℤ) ↦ g ^ x) k = x
hk : g ^ k = x
h : k.natAbs = 0
rw : g ^ k = 1
rw₁ : HPow.hPow (β := ℤ) g 0 = 1
⊢ x = 1
have rw₂ : Eq.{u_1 + 1} (α := α) 1 1
Tactic: rw [← hk, Int.natAbs_eq_zero.mp h, zpow_zero]
-- 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'
inst_3 : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
hx : ∃ x ∈ H, x ≠ 1
x : α
hx₁ : x ∈ H
hx₂ : x ≠ 1
k : ℤ
hk_1 : (fun (x : ℤ) ↦ g ^ x) k = x
hk : g ^ k = x
⊢ g ^ k.natAbs ∈ H
have ofNat : ∀ (k : ℕ) (hk : (fun (x : ℤ) ↦ g ^ x) (Int.ofNat k) = x) (hk : g ^ Int.ofNat k = x), g ^ (Int.ofNat k).natAbs ∈ H
Tactic: rcases k with k | k
Cleared hypotheses: k, hk_1, hk
-- 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'
inst_3 : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
hx : ∃ x ∈ H, x ≠ 1
x : α
hx₁ : x ∈ H
hx₂ : x ≠ 1
k : ℤ
hk_1 : (fun (x : ℤ) ↦ g ^ x) k = x
hk : g ^ k = x
ofNat :
  ∀ (k : ℕ) (hk : (fun (x : ℤ) ↦ g ^ x) (Int.ofNat k) = x) (hk : g ^ Int.ofNat k = x), g ^ (Int.ofNat k).natAbs ∈ H
⊢ g ^ k.natAbs ∈ H
have negSucc : ∀ (k : ℕ) (hk : (fun (x : ℤ) ↦ g ^ x) (Int.negSucc k) = x) (hk : g ^ Int.negSucc k = x), g ^ (Int.negSucc k).natAbs ∈ H
Tactic: rcases k with k | k
Cleared hypotheses: k, hk_1, hk
-- 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'
inst_3 : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
hx : ∃ x ∈ H, x ≠ 1
x : α
hx₁ : x ∈ H
hx₂ : x ≠ 1
k : ℕ
hk_1 : (fun (x : ℤ) ↦ g ^ x) (Int.negSucc k) = x
hk : g ^ Int.negSucc k = x
⊢ g ^ (Int.negSucc k).natAbs ∈ H
have negSucc : (g ^ k.succ)⁻¹ ∈ H
Tactic: rw [Int.natAbs_negSucc, ← Subgroup.inv_mem_iff H]
-- 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'
inst_3 : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
hx_1 : ∃ x ∈ H, x ≠ 1
x_1 : α
hx₁ : x_1 ∈ H
hx₂ : x_1 ≠ 1
k_1 : ℤ
hk_1 : (fun (x : ℤ) ↦ g ^ x) k_1 = x_1
hk_2 : g ^ k_1 = x_1
hex : ∃ (n : ℕ), 0 < n ∧ g ^ n ∈ H
x_2 : ↥H
x : α
hx : x ∈ H
k : ℤ
hk_3 : (fun (x : ℤ) ↦ g ^ x) k = x
hk : g ^ k = x
⊢ g ^
      ((↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ) *
        (k / (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ))) ∈
    H
have rw : HPow.hPow (β := ℤ) g (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ) ^
    (k / (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ)) ∈
  H
Tactic: rw [zpow_mul]
-- 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'
inst_3 : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
hx_1 : ∃ x ∈ H, x ≠ 1
x_1 : α
hx₁ : x_1 ∈ H
hx₂ : x_1 ≠ 1
k_1 : ℤ
hk_1 : (fun (x : ℤ) ↦ g ^ x) k_1 = x_1
hk_2 : g ^ k_1 = x_1
hex : ∃ (n : ℕ), 0 < n ∧ g ^ n ∈ H
x_2 : ↥H
x : α
hx : x ∈ H
k : ℤ
hk_3 : (fun (x : ℤ) ↦ g ^ x) k = x
hk : g ^ k = x
⊢ HPow.hPow (β := ℤ) g (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ) ^
      (k / (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ)) ∈
    H
have hx₃ : HPow.hPow (β := ℤ) g (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ) ∈ H
Tactic: apply H.zpow_mem
-- 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'
inst_3 : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
hx_1 : ∃ x ∈ H, x ≠ 1
x_1 : α
hx₁ : x_1 ∈ H
hx₂ : x_1 ≠ 1
k_1 : ℤ
hk_1 : (fun (x : ℤ) ↦ g ^ x) k_1 = x_1
hk_2 : g ^ k_1 = x_1
hex : ∃ (n : ℕ), 0 < n ∧ g ^ n ∈ H
x_2 : ↥H
x : α
hx : x ∈ H
k : ℤ
hk_3 : (fun (x : ℤ) ↦ g ^ x) k = x
hk : g ^ k = x
hk₂ :
  g ^
      ((↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ) *
        (k / (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ))) ∈
    H
hk₃ : g ^ (k % (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ)) ∈ H
⊢ k % (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ) =
    (↑(k % (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ)).natAbs : ℤ)
have rw : k % (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ) =
  k % (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ)
Tactic: rw [Int.natAbs_of_nonneg
              (Int.emod_nonneg _ (Int.natCast_ne_zero_iff_pos.2 (Nat.find_spec hex).1))]
-- 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'
inst_3 : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
hx_1 : ∃ x ∈ H, x ≠ 1
x_1 : α
hx₁ : x_1 ∈ H
hx₂ : x_1 ≠ 1
k_1 : ℤ
hk_1 : (fun (x : ℤ) ↦ g ^ x) k_1 = x_1
hk_2 : g ^ k_1 = x_1
hex : ∃ (n : ℕ), 0 < n ∧ g ^ n ∈ H
x_2 : ↥H
x : α
hx : x ∈ H
k : ℤ
hk_3 : (fun (x : ℤ) ↦ g ^ x) k = x
hk : g ^ k = x
hk₂ :
  g ^
      ((↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ) *
        (k / (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ))) ∈
    H
hk₃ : g ^ (k % (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ)) ∈ H
hk₄ :
  k % (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ) =
    (↑(k % (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ)).natAbs : ℤ)
⊢ g ^ (k % (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ)).natAbs ∈ H
have rwa : HPow.hPow (β := ℤ) g (↑(k % (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ)).natAbs : ℤ) ∈ H
Tactic: rwa [← zpow_natCast, ← hk₄]
-- 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'
inst_3 : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
hx_1 : ∃ x ∈ H, x ≠ 1
x_1 : α
hx₁ : x_1 ∈ H
hx₂ : x_1 ≠ 1
k_1 : ℤ
hk_1 : (fun (x : ℤ) ↦ g ^ x) k_1 = x_1
hk_2 : g ^ k_1 = x_1
hex : ∃ (n : ℕ), 0 < n ∧ g ^ n ∈ H
x_2 : ↥H
x : α
hx : x ∈ H
k : ℤ
hk_3 : (fun (x : ℤ) ↦ g ^ x) k = x
hk : g ^ k = x
hk₂ :
  g ^
      ((↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ) *
        (k / (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ))) ∈
    H
hk₃ : g ^ (k % (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ)) ∈ H
hk₄ :
  k % (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ) =
    (↑(k % (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ)).natAbs : ℤ)
hk₅ : g ^ (k % (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ)).natAbs ∈ H
h : ¬(k % (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ)).natAbs = 0
⊢ LT.lt (α := ℤ) (↑(k % (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ)).natAbs : ℤ)
    (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ)
have rw : k % (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ) <
  (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ)
Tactic: rw [← hk₄]
-- 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'
inst_3 : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
hx_1 : ∃ x ∈ H, x ≠ 1
x_1 : α
hx₁ : x_1 ∈ H
hx₂ : x_1 ≠ 1
k_1 : ℤ
hk_1 : (fun (x : ℤ) ↦ g ^ x) k_1 = x_1
hk_2 : g ^ k_1 = x_1
hex : ∃ (n : ℕ), 0 < n ∧ g ^ n ∈ H
x_2 : ↥H
x : α
hx : x ∈ H
k : ℤ
hk_3 : (fun (x : ℤ) ↦ g ^ x) k = x
hk : g ^ k = x
hk₂ :
  g ^
      ((↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ) *
        (k / (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ))) ∈
    H
hk₃ : g ^ (k % (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ)) ∈ H
hk₄ :
  k % (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ) =
    (↑(k % (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ)).natAbs : ℤ)
hk₅ : g ^ (k % (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ)).natAbs ∈ H
hk₆ : (k % (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ)).natAbs = 0
⊢ (↑((fun (x : ℤ) ↦
            Subtype.mk (p := fun (x : α) ↦ x ∈ H) (g ^ Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) ⋯ ^ x)
          (k / (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ))) :
      α) =
    (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ H) x hx) : α)
have suffices : g ^
    ((↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ) *
      (k / (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ))) =
  x
Tactic: suffices g ^ ((Nat.find hex : ℤ) * (k / Nat.find hex : ℤ)) = x by simpa [zpow_mul]
-- 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'
inst_3 : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
hx_1 : ∃ x ∈ H, x ≠ 1
x_1 : α
hx₁ : x_1 ∈ H
hx₂ : x_1 ≠ 1
k_1 : ℤ
hk_1 : (fun (x : ℤ) ↦ g ^ x) k_1 = x_1
hk_2 : g ^ k_1 = x_1
hex : ∃ (n : ℕ), 0 < n ∧ g ^ n ∈ H
x_2 : ↥H
x : α
hx : x ∈ H
k : ℤ
hk_3 : (fun (x : ℤ) ↦ g ^ x) k = x
hk : g ^ k = x
hk₂ :
  g ^
      ((↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ) *
        (k / (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ))) ∈
    H
hk₃ : g ^ (k % (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ)) ∈ H
hk₄ :
  k % (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ) =
    (↑(k % (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ)).natAbs : ℤ)
hk₅ : g ^ (k % (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ)).natAbs ∈ H
hk₆ : (k % (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ)).natAbs = 0
rw : g ^ k = x
⊢ g ^
      ((↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ) *
        (k / (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ))) =
    x
have rw₁ : x = x
Tactic: rw [Int.mul_ediv_cancel'
                  (Int.dvd_of_emod_eq_zero (Int.natAbs_eq_zero.mp hk₆)),
                hk]
-- 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'
inst_3 : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
hx : ¬∃ x ∈ H, x ≠ 1
x : α
h : x ∈ H
⊢ Membership.mem (γ := Subgroup α) ⊥ x
have simp : ∀ (hx : ∀ x ∈ H, x = 1), x = 1
Tactic: simp at *
Cleared hypotheses: hx
-- 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'
inst_3 : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
hx : ¬∃ x ∈ H, x ≠ 1
x : α
h : Membership.mem (γ := Subgroup α) ⊥ x
⊢ x ∈ H
have rw : 1 ∈ H
Tactic: rw [Subgroup.mem_bot.1 h]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (hypothesis)
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst : Group α
inst_1 : Group G
inst_2 : Group G'
inst_3 : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
hx : ¬∃ x ∈ H, x ≠ 1
⊢ IsCyclic.{u_1} ↥H
have this₁ : H = ⊥
Tactic: have : H = (⊥ : Subgroup α) :=
      Subgroup.ext fun x =>
        ⟨fun h => by simp at *; tauto, fun h => by rw [Subgroup.mem_bot.1 h]; exact H.one_mem⟩
-- 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'
inst_3 : IsCyclic α
H : Subgroup α
this_1 : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
hx : ¬∃ x ∈ H, x ≠ 1
this : H = ⊥
⊢ IsCyclic.{u_1} ↥H
have subst : ∀ (hx : ¬∃ (x : α), Membership.mem (γ := Subgroup α) ⊥ x ∧ x ≠ 1), IsCyclic.{u_1} ↥⊥
Tactic: subst this
Cleared hypotheses: H, hx, this
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
G : Type u_2
inst : Group G
g : G
H : Subgroup G
⊢ H ≤ zpowers g ↔ ∃ (n : ℕ), H = zpowers (g ^ n)
have refine_1 : ∀ (h : H ≤ zpowers g), ∃ (n : ℕ), H = zpowers (g ^ n)
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
G : Type u_2
inst : Group G
g : G
H : Subgroup G
refine_1 : ∀ (h : H ≤ zpowers g), ∃ (n : ℕ), H = zpowers (g ^ n)
⊢ H ≤ zpowers g ↔ ∃ (n : ℕ), H = zpowers (g ^ n)
have refine_2 : (∃ (n : ℕ), H = zpowers (g ^ n)) → H ≤ zpowers g
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
G : Type u_2
inst : Group G
g : G
H : Subgroup G
h : H ≤ zpowers g
⊢ ∃ (n : ℕ), H = zpowers (g ^ n)
have refine_1 : ∀ (x : G) (h : LE.le (α := Subgroup G) (zpowers x) (zpowers g)),
  ∃ (n : ℕ), Eq (α := Subgroup G) (zpowers x) (zpowers (g ^ n))
Tactic: obtain ⟨x, rfl⟩ := (H.isCyclic_iff_exists_zpowers_eq_top).mp (isCyclic_of_le h)
Cleared hypotheses: H, h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
G : Type u_2
inst : Group G
g x : G
h : LE.le (α := Subgroup G) (zpowers x) (zpowers g)
⊢ ∃ (n : ℕ), Eq (α := Subgroup G) (zpowers x) (zpowers (g ^ n))
have refine_1 : ∀ (k : ℤ) (h : LE.le (α := Subgroup G) (zpowers (g ^ k)) (zpowers g)),
  ∃ (n : ℕ), Eq (α := Subgroup G) (zpowers (g ^ k)) (zpowers (g ^ n))
Tactic: obtain ⟨k, rfl⟩ := mem_zpowers_iff.mp <| h (mem_zpowers x)
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
G : Type u_2
inst : Group G
g : G
k : ℤ
h : LE.le (α := Subgroup G) (zpowers (g ^ k)) (zpowers g)
⊢ ∃ (n : ℕ), Eq (α := Subgroup G) (zpowers (g ^ k)) (zpowers (g ^ n))
have refine_1 : ∀ (n : ℕ) (h : LE.le (α := Subgroup G) (zpowers (HPow.hPow (β := ℤ) g (↑n : ℤ))) (zpowers g)),
  ∃ (n_1 : ℕ), Eq (α := Subgroup G) (zpowers (HPow.hPow (β := ℤ) g (↑n : ℤ))) (zpowers (g ^ n_1))
Tactic: obtain ⟨n, rfl | rfl⟩ := Int.eq_nat_or_neg k
Cleared hypotheses: k, h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
G : Type u_2
inst : Group G
g : G
k : ℤ
h : LE.le (α := Subgroup G) (zpowers (g ^ k)) (zpowers g)
refine_1 :
  ∀ (n : ℕ) (h : LE.le (α := Subgroup G) (zpowers (HPow.hPow (β := ℤ) g (↑n : ℤ))) (zpowers g)),
    ∃ (n_1 : ℕ), Eq (α := Subgroup G) (zpowers (HPow.hPow (β := ℤ) g (↑n : ℤ))) (zpowers (g ^ n_1))
⊢ ∃ (n : ℕ), Eq (α := Subgroup G) (zpowers (g ^ k)) (zpowers (g ^ n))
have refine_1₁ : ∀ (n : ℕ) (h : LE.le (α := Subgroup G) (zpowers (HPow.hPow (β := ℤ) g (-(↑n : ℤ)))) (zpowers g)),
  ∃ (n_1 : ℕ), Eq (α := Subgroup G) (zpowers (HPow.hPow (β := ℤ) g (-(↑n : ℤ)))) (zpowers (g ^ n_1))
Tactic: obtain ⟨n, rfl | rfl⟩ := Int.eq_nat_or_neg k
Cleared hypotheses: k, h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
G : Type u_2
inst : Group G
g : G
n : ℕ
h : LE.le (α := Subgroup G) (zpowers (HPow.hPow (β := ℤ) g (↑n : ℤ))) (zpowers g)
⊢ Eq (α := Subgroup G) (zpowers (HPow.hPow (β := ℤ) g (↑n : ℤ))) (zpowers (g ^ n))
have rw : Eq (α := Subgroup G) (zpowers (g ^ n)) (zpowers (g ^ n))
Tactic: rw [zpow_natCast]
-- 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
⊢ card.{u_1} (α := α) {a : α | a ^ n = 1} ≤
    #(↑(zpowers (g ^ (Fintype.card α / n.gcd (Fintype.card α)))) : Set α).toFinset
have a : {a : α | a ^ n = 1} ⊆ (↑(zpowers (g ^ (Fintype.card α / n.gcd (Fintype.card α)))) : Set α).toFinset
Tactic: gcongr
-- 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
x : α
hx : Membership.mem (γ := Finset α) {a : α | a ^ n = 1} x
⊢ x ∈ (↑(zpowers (g ^ (Fintype.card α / n.gcd (Fintype.card α)))) : Set α).toFinset
have a : ∀ (m : ℕ) (hm : (fun (x : ℕ) ↦ g ^ x) m = x),
  x ∈ (↑(zpowers (g ^ (Fintype.card α / n.gcd (Fintype.card α)))) : Set α).toFinset
Tactic: let ⟨m, hm⟩ := show x ∈ Submonoid.powers g from mem_powers_iff_mem_zpowers.2 <| hg x
-- 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
x : α
hx : Membership.mem (γ := Finset α) {a : α | a ^ n = 1} x
m : ℕ
hm : (fun (x : ℕ) ↦ g ^ x) m = x
⊢ x ∈ (↑(zpowers (g ^ (Fintype.card α / n.gcd (Fintype.card α)))) : Set α).toFinset
have a : (fun (x : ℤ) ↦ (g ^ (Fintype.card α / n.gcd (Fintype.card α))) ^ x)
    (↑(m / (Fintype.card α / n.gcd (Fintype.card α))) : ℤ) =
  x
Tactic: refine Set.mem_toFinset.2 ⟨(m / (Fintype.card α / Nat.gcd n (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
x : α
hx : Membership.mem (γ := Finset α) {a : α | a ^ n = 1} x
m : ℕ
hm : g ^ m = x
⊢ HPow.hPow (β := ℤ) (g ^ (Fintype.card α / n.gcd (Fintype.card α)))
      (↑(m / (Fintype.card α / n.gcd (Fintype.card α))) : ℤ) =
    x
have a : Fintype.card α / n.gcd (Fintype.card α) ∣ m
Tactic: rw [zpow_natCast, ← pow_mul, Nat.mul_div_cancel_left', 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
x : α
hx : Membership.mem (γ := Finset α) {a : α | a ^ n = 1} x
m : ℕ
hm : g ^ m = x
⊢ Fintype.card α / n.gcd (Fintype.card α) ∣ m
have a : Fintype.card α / n.gcd (Fintype.card α) * n.gcd (Fintype.card α) ∣ m * n.gcd (Fintype.card α)
Tactic: refine Nat.dvd_of_mul_dvd_mul_right (gcd_pos_of_pos_left (Fintype.card α) hn0) ?_
-- 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
x : α
hx : Membership.mem (γ := Finset α) {a : α | a ^ n = 1} x
m : ℕ
hm : g ^ m = x
| Fintype.card α / n.gcd (Fintype.card α) * n.gcd (Fintype.card α)
have rw : orderOf g
Tactic: rw [Nat.div_mul_cancel (Nat.gcd_dvd_right _ _), ← Nat.card_eq_fintype_card,
          ← orderOf_eq_card_of_forall_mem_zpowers hg]
-- 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
x : α
hx : Membership.mem (γ := Finset α) {a : α | a ^ n = 1} x
m : ℕ
hm : g ^ m = x
⊢ Fintype.card α / n.gcd (Fintype.card α) * n.gcd (Fintype.card α) ∣ m * n.gcd (Fintype.card α)
have a : orderOf g ∣ m * n.gcd (Fintype.card α)
Tactic: conv_lhs =>
        rw [Nat.div_mul_cancel (Nat.gcd_dvd_right _ _), ← Nat.card_eq_fintype_card,
          ← orderOf_eq_card_of_forall_mem_zpowers hg]