awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst : Group α
inst_1 : Group G
inst_2 : Group G'
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
⊢ k % (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ) <
    (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ)

Tactic:
Int.emod_lt_of_pos _ (Int.natCast_pos.2 (Nat.find_spec hex).1)

Premises used: Iff.mpr, And.left, Int.emod_lt_of_pos, Int.natCast_pos, Nat.find_spec
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst : Group α
inst_1 : Group G
inst_2 : Group G'
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
⊢ k % (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ) <
    (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ)

Tactic:
exact Int.emod_lt_of_pos _ (Int.natCast_pos.2 (Nat.find_spec hex).1)

Premises used: Iff.mpr, And.left, Int.emod_lt_of_pos, Int.natCast_pos, Nat.find_spec
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst : Group α
inst_1 : Group G
inst_2 : Group G'
inst_3 : IsCyclic α
H : Subgroup α
this_1 : (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
this :
  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
⊢ (↑((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) : α)

Tactic:
simpa [zpow_mul]

Premises used: zpow_mul
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst : Group α
inst_1 : Group G
inst_2 : Group G'
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
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
⊢ (↑((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) : α)

Tactic:
suffices g ^ ((Nat.find hex : ℤ) * (k / Nat.find hex : ℤ)) = x by simpa [zpow_mul]
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst : Group α
inst_1 : Group G
inst_2 : Group G'
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
rw₁ rw₂ : x = 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

Tactic:
rw [Int.mul_ediv_cancel'
                  (Int.dvd_of_emod_eq_zero (Int.natAbs_eq_zero.mp hk₆)),
                hk]

Premises used: Int.dvd_of_emod_eq_zero, Int.natAbs_eq_zero, Int.mul_ediv_cancel', Iff.mp
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst : Group α
inst_1 : Group G
inst_2 : Group G'
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
simp : ∀ (hx : ∀ x ∈ H, x = 1), x = 1
⊢ Membership.mem (γ := Subgroup α) ⊥ x

Tactic:
simp at *
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst : Group α
inst_1 : Group G
inst_2 : Group G'
inst_3 : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
x : α
h : x ∈ H
hx : ∀ x ∈ H, x = 1
⊢ x = 1

Tactic:
tauto
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst : Group α
inst_1 : Group G
inst_2 : Group G'
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
rw : 1 ∈ H
⊢ x ∈ H

Tactic:
rw [Subgroup.mem_bot.1 h]

Premises used: Iff.mp, Subgroup.mem_bot
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst : Group α
inst_1 : Group G
inst_2 : Group G'
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
⊢ 1 ∈ H

Tactic:
H.one_mem

Premises used: Subgroup.one_mem
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst : Group α
inst_1 : Group G
inst_2 : Group G'
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
⊢ 1 ∈ H

Tactic:
exact H.one_mem

Premises used: Subgroup.one_mem
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst : Group α
inst_1 : Group G
inst_2 : Group G'
inst_3 : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
hx : ¬∃ x ∈ H, x ≠ 1
⊢ 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⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst : Group α
inst_1 : Group G
inst_2 : Group G'
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 = ⊥
subst : ∀ (hx : ¬∃ (x : α), Membership.mem (γ := Subgroup α) ⊥ x ∧ x ≠ 1), IsCyclic.{u_1} ↥⊥
⊢ IsCyclic.{u_1} ↥H

Tactic:
subst this
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst : Group α
inst_1 : Group G
inst_2 : Group G'
inst_3 : IsCyclic α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
hx : ¬∃ (x : α), Membership.mem (γ := Subgroup α) ⊥ x ∧ x ≠ 1
⊢ IsCyclic.{u_1} ↥⊥

Tactic:
infer_instance
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
G' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : IsCyclic G'
f : G →* G'
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
⊢ IsCyclic G

Tactic:
isCyclic_of_surjective (MonoidHom.ofInjective hf).symm (MonoidHom.ofInjective hf).symm.surjective

Premises used: isCyclic_of_surjective, MulEquiv.surjective, MonoidHom.ofInjective, MulEquiv.symm
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
inst : Group G
H H' : Subgroup G
h : H ≤ H'
inst_1 : IsCyclic.{u_2} ↥H'
⊢ IsCyclic.{u_2} ↥H

Tactic:
isCyclic_of_injective (Subgroup.inclusion h) (Subgroup.inclusion_injective h)

Premises used: isCyclic_of_injective, Subgroup.inclusion, Subgroup.inclusion_injective
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
inst : Group G
g : G
H : Subgroup G
⊢ H ≤ zpowers g ↔ ∃ (n : ℕ), H = zpowers (g ^ n)

Tactic:
⟨fun h ↦ ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
inst : Group G
g : G
H : Subgroup G
refine_1 : ∀ (h : H ≤ zpowers g), ∃ (n : ℕ), H = zpowers (g ^ n)
refine_2 : (∃ (n : ℕ), H = zpowers (g ^ n)) → H ≤ zpowers g
⊢ H ≤ zpowers g ↔ ∃ (n : ℕ), H = zpowers (g ^ n)

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
inst : Group G
g : G
H : Subgroup G
h : H ≤ zpowers g
refine_1 :
  ∀ (x : G) (h : LE.le (α := Subgroup G) (zpowers x) (zpowers g)),
    ∃ (n : ℕ), Eq (α := Subgroup G) (zpowers x) (zpowers (g ^ n))
⊢ ∃ (n : ℕ), H = zpowers (g ^ n)

Tactic:
obtain ⟨x, rfl⟩ := (H.isCyclic_iff_exists_zpowers_eq_top).mp (isCyclic_of_le h)

Premises used: Iff.mp, Subgroup.isCyclic_iff_exists_zpowers_eq_top, Subgroup.isCyclic_of_le, rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
inst : Group G
g x : G
h : LE.le (α := Subgroup G) (zpowers x) (zpowers g)
refine_1 :
  ∀ (k : ℤ) (h : LE.le (α := Subgroup G) (zpowers (g ^ k)) (zpowers g)),
    ∃ (n : ℕ), Eq (α := Subgroup G) (zpowers (g ^ k)) (zpowers (g ^ n))
⊢ ∃ (n : ℕ), Eq (α := Subgroup G) (zpowers x) (zpowers (g ^ n))

Tactic:
obtain ⟨k, rfl⟩ := mem_zpowers_iff.mp <| h (mem_zpowers x)

Premises used: Subgroup.mem_zpowers, Iff.mp, Subgroup.mem_zpowers_iff, rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
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))
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))

Tactic:
obtain ⟨n, rfl | rfl⟩ := Int.eq_nat_or_neg k

Premises used: Int.eq_nat_or_neg, rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
inst : Group G
g : G
n : ℕ
h : LE.le (α := Subgroup G) (zpowers (HPow.hPow (β := ℤ) g (↑n : ℤ))) (zpowers g)
rw rw₁ : Eq (α := Subgroup G) (zpowers (g ^ n)) (zpowers (g ^ n))
⊢ Eq (α := Subgroup G) (zpowers (HPow.hPow (β := ℤ) g (↑n : ℤ))) (zpowers (g ^ n))

Tactic:
rw [zpow_natCast]

Premises used: zpow_natCast
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
inst : Group G
g : G
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:
exact ⟨n, by rw [zpow_natCast]⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
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))

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
inst : Group G
g : G
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:
exact ⟨n, by simp⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
inst : Group G
g : G
k : ℕ
⊢ LE.le (α := Subgroup G) (zpowers (g ^ k)) (zpowers g)

Tactic:
zpowers_le_of_mem <| npow_mem_zpowers g k

Premises used: Subgroup.zpowers_le_of_mem, Subgroup.npow_mem_zpowers
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
inst : Group G
g : G
k : ℕ
⊢ LE.le (α := Subgroup G) (zpowers (g ^ k)) (zpowers g)

Tactic:
exact zpowers_le_of_mem <| npow_mem_zpowers g k

Premises used: Subgroup.zpowers_le_of_mem, Subgroup.npow_mem_zpowers
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
inst_3 : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
a : {a : α | a ^ n = 1} ⊆ (↑(zpowers (g ^ (Fintype.card α / n.gcd (Fintype.card α)))) : Set α).toFinset
⊢ card.{u_1} (α := α) {a : α | a ^ n = 1} ≤
    #(↑(zpowers (g ^ (Fintype.card α / n.gcd (Fintype.card α)))) : Set α).toFinset

Tactic:
gcongr
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
inst_3 : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
x : α
hx : Membership.mem (γ := Finset α) {a : α | a ^ n = 1} x
a :
  ∀ (m : ℕ) (hm : (fun (x : ℕ) ↦ g ^ x) m = x),
    x ∈ (↑(zpowers (g ^ (Fintype.card α / n.gcd (Fintype.card α)))) : Set α).toFinset
⊢ 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
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
inst_3 : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
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

Tactic:
Set.mem_toFinset.2 ⟨(m / (Fintype.card α / Nat.gcd n (Fintype.card α)) : ℕ), ?_⟩

Premises used: Nat.gcd, Iff.mpr, Fintype.card, HDiv.hDiv, Nat.cast, Exists.intro, Set.mem_toFinset
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
inst_3 : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
x : α
hx : Membership.mem (γ := Finset α) {a : α | a ^ n = 1} x
m : ℕ
hm : (fun (x : ℕ) ↦ g ^ x) m = x
a :
  (fun (x : ℤ) ↦ (g ^ (Fintype.card α / n.gcd (Fintype.card α))) ^ x)
      (↑(m / (Fintype.card α / n.gcd (Fintype.card α))) : ℤ) =
    x
⊢ x ∈ (↑(zpowers (g ^ (Fintype.card α / n.gcd (Fintype.card α)))) : Set α).toFinset

Tactic:
refine Set.mem_toFinset.2 ⟨(m / (Fintype.card α / Nat.gcd n (Fintype.card α)) : ℕ), ?_⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
inst_3 : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
x : α
hx : Membership.mem (γ := Finset α) {a : α | a ^ n = 1} x
m : ℕ
hm : g ^ m = x
a : Fintype.card α / n.gcd (Fintype.card α) ∣ m
⊢ HPow.hPow (β := ℤ) (g ^ (Fintype.card α / n.gcd (Fintype.card α)))
      (↑(m / (Fintype.card α / n.gcd (Fintype.card α))) : ℤ) =
    x

Tactic:
rw [zpow_natCast, ← pow_mul, Nat.mul_div_cancel_left', hm]

Premises used: zpow_natCast, Nat.mul_div_cancel_left', pow_mul
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
inst_3 : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
x : α
hx : Membership.mem (γ := Finset α) {a : α | a ^ n = 1} x
m : ℕ
hm : g ^ m = x
⊢ Fintype.card α / n.gcd (Fintype.card α) ∣ m

Tactic:
Nat.dvd_of_mul_dvd_mul_right (gcd_pos_of_pos_left (Fintype.card α) hn0) ?_

Premises used: Nat.dvd_of_mul_dvd_mul_right, Fintype.card, Nat.gcd_pos_of_pos_left
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
inst_3 : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
x : α
hx : Membership.mem (γ := Finset α) {a : α | a ^ n = 1} x
m : ℕ
hm : g ^ m = x
a : Fintype.card α / n.gcd (Fintype.card α) * n.gcd (Fintype.card α) ∣ m * n.gcd (Fintype.card α)
⊢ Fintype.card α / n.gcd (Fintype.card α) ∣ m

Tactic:
refine Nat.dvd_of_mul_dvd_mul_right (gcd_pos_of_pos_left (Fintype.card α) hn0) ?_

Premises used: Nat.dvd_of_mul_dvd_mul_right, Fintype.card, Nat.gcd_pos_of_pos_left
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
inst_3 : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
x : α
hx : Membership.mem (γ := Finset α) {a : α | a ^ n = 1} x
m : ℕ
hm : g ^ m = x
rw : orderOf g
| Fintype.card α / n.gcd (Fintype.card α) * n.gcd (Fintype.card α)

Tactic:
rw [Nat.div_mul_cancel (Nat.gcd_dvd_right _ _), ← Nat.card_eq_fintype_card,
          ← orderOf_eq_card_of_forall_mem_zpowers hg]

Premises used: orderOf_eq_card_of_forall_mem_zpowers, Nat.div_mul_cancel, Nat.gcd_dvd_right, Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
inst_3 : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
x : α
hx : Membership.mem (γ := Finset α) {a : α | a ^ n = 1} x
m : ℕ
hm : g ^ m = x
a : orderOf g ∣ m * n.gcd (Fintype.card α)
⊢ Fintype.card α / n.gcd (Fintype.card α) * n.gcd (Fintype.card α) ∣ 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]

Premises used: orderOf_eq_card_of_forall_mem_zpowers, Nat.div_mul_cancel, Nat.gcd_dvd_right, Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
inst_3 : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
x : α
hx : Membership.mem (γ := Finset α) {a : α | a ^ n = 1} x
m : ℕ
hm : g ^ m = x
⊢ g ^ (m * n.gcd (Fintype.card α)) = 1

Tactic:
simpa [pow_mul, hm] using (mem_filter.1 hx).2

Premises used: pow_mul, And.right, Iff.mp, Finset.mem_filter
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
inst_3 : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
x : α
hx : Membership.mem (γ := Finset α) {a : α | a ^ n = 1} x
m : ℕ
hm : g ^ m = x
⊢ orderOf g ∣ m * n.gcd (Fintype.card α)

Tactic:
exact orderOf_dvd_of_pow_eq_one <| by simpa [pow_mul, hm] using (mem_filter.1 hx).2

Premises used: orderOf_dvd_of_pow_eq_one
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
inst_3 : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
let :
  ∀ (m : ℕ) (hm : Fintype.card α = n.gcd (Fintype.card α) * m),
    #(↑(zpowers (g ^ (Fintype.card α / n.gcd (Fintype.card α)))) : Set α).toFinset ≤ n
⊢ #(↑(zpowers (g ^ (Fintype.card α / n.gcd (Fintype.card α)))) : Set α).toFinset ≤ n

Tactic:
let ⟨m, hm⟩ := Nat.gcd_dvd_right n (Fintype.card α)
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
inst_3 : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
m : ℕ
hm : Fintype.card α = n.gcd (Fintype.card α) * m
hm0 : m = 0
⊢ IsEmpty α

Tactic:
rw [hm0, mul_zero, Fintype.card_eq_zero_iff] at hm

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

Tactic:
rw [hm0, mul_zero, Fintype.card_eq_zero_iff] at hm

Premises used: MulZeroClass.mul_zero, Fintype.card_eq_zero_iff