awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Fact (Nat.Prime p)
h_1 : Nat.card α ∣ p
h : Nat.card α = p
⊢ IsCyclic α

Tactic:
exact isCyclic_of_prime_card h

Premises used: isCyclic_of_prime_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
G' : Type u_3
inst : Group G
inst_1 : Group G'
F : Type u_4
hH : IsCyclic G'
inst_2 : FunLike F G' G
inst_3 : MonoidHomClass F G' G
f : F
hf : Function.Surjective.{u_3 + 1, u_2 + 1} (α := G') (β := G) (⇑f : (a : G') → G)
obtain : ∀ (x : G') (hx : Function.Surjective.{1, u_3 + 1} (β := G') fun (x_1 : ℤ) ↦ x ^ x_1), IsCyclic G
⊢ IsCyclic G

Tactic:
obtain ⟨x, hx⟩ := hH
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
G' : Type u_3
inst : Group G
inst_1 : Group G'
F : Type u_4
inst_2 : FunLike F G' G
inst_3 : MonoidHomClass F G' G
f : F
hf : Function.Surjective.{u_3 + 1, u_2 + 1} (α := G') (β := G) (⇑f : (a : G') → G)
x : G'
hx : Function.Surjective.{1, u_3 + 1} (β := G') fun (x_1 : ℤ) ↦ x ^ x_1
⊢ IsCyclic G

Tactic:
⟨f x, fun a ↦ ?_⟩

Premises used: Exists.intro, IsCyclic.mk, DFunLike.coe
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
G' : Type u_3
inst : Group G
inst_1 : Group G'
F : Type u_4
inst_2 : FunLike F G' G
inst_3 : MonoidHomClass F G' G
f : F
hf : Function.Surjective.{u_3 + 1, u_2 + 1} (α := G') (β := G) (⇑f : (a : G') → G)
x : G'
hx : Function.Surjective.{1, u_3 + 1} (β := G') fun (x_1 : ℤ) ↦ x ^ x_1
refine : ∀ (a : G), ∃ (a_1 : ℤ), (fun (x_1 : ℤ) ↦ HPow.hPow (α := G) ((f : (a : G') → G) x : G) x_1) a_1 = a
⊢ IsCyclic G

Tactic:
refine ⟨f x, fun a ↦ ?_⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
G' : Type u_3
inst : Group G
inst_1 : Group G'
F : Type u_4
inst_2 : FunLike F G' G
inst_3 : MonoidHomClass F G' G
f : F
hf : Function.Surjective.{u_3 + 1, u_2 + 1} (α := G') (β := G) (⇑f : (a : G') → G)
x : G'
hx : Function.Surjective.{1, u_3 + 1} (β := G') fun (x_1 : ℤ) ↦ x ^ x_1
a : G
obtain :
  ∀ (a : G'),
    ∃ (a_1 : ℤ),
      Eq.{u_2 + 1} (α := G) ((fun (x_1 : ℤ) ↦ HPow.hPow (α := G) ((f : (a : G') → G) x : G) x_1) a_1 : G)
        ((f : (a : G') → G) a : G)
⊢ ∃ (a_1 : ℤ), (fun (x_1 : ℤ) ↦ HPow.hPow (α := G) ((f : (a : G') → G) x : G) x_1) a_1 = a

Tactic:
obtain ⟨a, rfl⟩ := hf a

Premises used: rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
G' : Type u_3
inst : Group G
inst_1 : Group G'
F : Type u_4
inst_2 : FunLike F G' G
inst_3 : MonoidHomClass F G' G
f : F
hf : Function.Surjective.{u_3 + 1, u_2 + 1} (α := G') (β := G) (⇑f : (a : G') → G)
x : G'
hx : Function.Surjective.{1, u_3 + 1} (β := G') fun (x_1 : ℤ) ↦ x ^ x_1
a : G'
obtain :
  ∀ (n : ℤ),
    ∃ (a : ℤ),
      Eq.{u_2 + 1} (α := G) ((fun (x_1 : ℤ) ↦ HPow.hPow (α := G) ((f : (a : G') → G) x : G) x_1) a : G)
        ((f : (a : G') → G) ((fun (x_1 : ℤ) ↦ x ^ x_1) n) : G)
⊢ ∃ (a_1 : ℤ),
    Eq.{u_2 + 1} (α := G) ((fun (x_1 : ℤ) ↦ HPow.hPow (α := G) ((f : (a : G') → G) x : G) x_1) a_1 : G)
      ((f : (a : G') → G) a : G)

Tactic:
obtain ⟨n, rfl⟩ := hx a

Premises used: rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
G' : Type u_3
inst : Group G
inst_1 : Group G'
F : Type u_4
inst_2 : FunLike F G' G
inst_3 : MonoidHomClass F G' G
f : F
hf : Function.Surjective.{u_3 + 1, u_2 + 1} (α := G') (β := G) (⇑f : (a : G') → G)
x : G'
hx : Function.Surjective.{1, u_3 + 1} (β := G') fun (x_1 : ℤ) ↦ x ^ x_1
n : ℤ
⊢ ∃ (a : ℤ),
    Eq.{u_2 + 1} (α := G) ((fun (x_1 : ℤ) ↦ HPow.hPow (α := G) ((f : (a : G') → G) x : G) x_1) a : G)
      ((f : (a : G') → G) ((fun (x_1 : ℤ) ↦ x ^ x_1) n) : G)

Tactic:
⟨n, (map_zpow _ _ _).symm⟩

Premises used: map_zpow, Exists.intro, Eq.symm
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
G' : Type u_3
inst : Group G
inst_1 : Group G'
F : Type u_4
inst_2 : FunLike F G' G
inst_3 : MonoidHomClass F G' G
f : F
hf : Function.Surjective.{u_3 + 1, u_2 + 1} (α := G') (β := G) (⇑f : (a : G') → G)
x : G'
hx : Function.Surjective.{1, u_3 + 1} (β := G') fun (x_1 : ℤ) ↦ x ^ x_1
n : ℤ
⊢ ∃ (a : ℤ),
    Eq.{u_2 + 1} (α := G) ((fun (x_1 : ℤ) ↦ HPow.hPow (α := G) ((f : (a : G') → G) x : G) x_1) a : G)
      ((f : (a : G') → G) ((fun (x_1 : ℤ) ↦ x ^ x_1) n) : G)

Tactic:
exact ⟨n, (map_zpow _ _ _).symm⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
G' : Type u_3
inst : Group G
inst_1 : Group G'
e : G ≃* G'
⊢ IsCyclic G ↔ IsCyclic G'

Tactic:
⟨fun _ ↦ isCyclic_of_surjective e e.surjective,
    fun _ ↦ isCyclic_of_surjective e.symm e.symm.surjective⟩

Premises used: isCyclic_of_surjective, MulEquiv.surjective, Iff.intro, MulEquiv.symm
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
g : α
hx : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
rw : Nat.card.{u_1} ↥(zpowers g) = Nat.card α
rw₁ : Nat.card.{u_1} ↥⊤ = Nat.card α
rw₂ rw₃ : Nat.card α = Nat.card α
⊢ orderOf g = Nat.card α

Tactic:
rw [← Nat.card_zpowers, (zpowers g).eq_top_iff'.mpr hx, card_top]

Premises used: Iff.mpr, Subgroup.card_top, Subgroup.eq_top_iff', Nat.card_zpowers, Subgroup.zpowers
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
g : α
hx : ∀ (x : α), Membership.mem (γ := Submonoid α) (Submonoid.powers g) x
rw : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
⊢ orderOf g = Nat.card α

Tactic:
rw [orderOf_eq_card_of_forall_mem_zpowers]

Premises used: orderOf_eq_card_of_forall_mem_zpowers
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
g : α
hx : ∀ (x : α), Membership.mem (γ := Submonoid α) (Submonoid.powers g) x
⊢ ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x

Tactic:
fun x ↦ Submonoid.powers_le_zpowers _ (hx _)

Premises used: Set.Mem, Submonoid.powers_le_zpowers
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
g : α
hx : ∀ (x : α), Membership.mem (γ := Submonoid α) (Submonoid.powers g) x
⊢ ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x

Tactic:
exact fun x ↦ Submonoid.powers_le_zpowers _ (hx _)

Premises used: Submonoid.powers_le_zpowers
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
inst : Group G
g : G
h : Eq (α := Subgroup G) (zpowers g) ⊤
⊢ orderOf g = Nat.card G

Tactic:
orderOf_eq_card_of_forall_mem_zpowers fun _ ↦ h.ge (Subgroup.mem_top _)

Premises used: orderOf_eq_card_of_forall_mem_zpowers, Eq.ge, Subgroup.mem_top
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
inst : Group G
G_cyclic : IsCyclic G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card G
⊢ Finite G

Tactic:
have : Finite G := Nat.finite_of_card_ne_zero (Nat.ne_zero_of_lt k_lt_card_G)
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
G : Type u_2
inst : Group G
G_cyclic : IsCyclic G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card G
this : Finite G
rcases : ∀ (a : G) (ha : Function.Surjective.{1, u_2 + 1} (β := G) fun (x : ℤ) ↦ a ^ x), ∃ (a : G), a ^ k ≠ 1
⊢ ∃ (a : G), a ^ k ≠ 1

Tactic:
rcases G_cyclic with ⟨a, ha⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
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
h : a ^ k ≠ 1
⊢ ∃ (a : G), a ^ k ≠ 1

Tactic:
use a
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
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
h : ∀ (k_lt_card_G : a ^ k = 1), Nat.card G ≤ k
⊢ a ^ k ≠ 1

Tactic:
contrapose! k_lt_card_G
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
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
⊢ orderOf a ≤ k

Tactic:
orderOf_le_of_pow_eq_one k_pos.bot_lt k_lt_card_G

Premises used: orderOf_le_of_pow_eq_one, Ne.bot_lt
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
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
h : Nat.card G = orderOf a
⊢ Nat.card G ≤ k

Tactic:
convert! orderOf_le_of_pow_eq_one k_pos.bot_lt k_lt_card_G

Premises used: orderOf_le_of_pow_eq_one, Ne.bot_lt
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
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
h : LE.le (α := Subgroup G) ⊤ (zpowers a)
⊢ Nat.card G = orderOf a

Tactic:
rw [← Nat.card_zpowers, eq_comm, card_eq_iff_eq_top, eq_top_iff]

Premises used: eq_top_iff, eq_comm, Nat.card_zpowers, Subgroup.card_eq_iff_eq_top
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
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
⊢ LE.le (α := Subgroup G) ⊤ (zpowers a)

Tactic:
fun x _ ↦ ha x

Premises used: Set.Mem, setOf, Set.range
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
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
⊢ LE.le (α := Subgroup G) ⊤ (zpowers a)

Tactic:
exact fun x _ ↦ ha x
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Goal:
α : Type u_1
inst : Group α
inst_1 : Infinite α
g : α
h : ∀ (x : α), Membership.mem (γ := Subgroup α) (zpowers g) x
rw : Nat.card α = 0
rw₁ rw₂ : Eq (α := ℕ) 0 0
⊢ orderOf g = 0

Tactic:
rw [orderOf_eq_card_of_forall_mem_zpowers h, Nat.card_eq_zero_of_infinite]

Premises used: orderOf_eq_card_of_forall_mem_zpowers, Nat.card_eq_zero_of_infinite
-- 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'
⊢ IsCyclic.{u_1} ↥⊥

Tactic:
⟨⟨1, fun x => ⟨0, Subtype.ext <| (zpow_zero (1 : α)).trans <| Eq.symm (Subgroup.mem_bot.1 x.2)⟩⟩⟩

Premises used: zpow_zero, Exists.intro, Iff.mp, IsCyclic.mk, OfNat.ofNat, Eq.symm, Subgroup.mem_bot, Eq.trans, Subtype.property, Subtype.ext
-- 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 : α
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
rw₂ rw₃ : Eq.{u_1 + 1} (α := α) 1 1
⊢ x = 1

Tactic:
rw [← hk, Int.natAbs_eq_zero.mp h, zpow_zero]

Premises used: zpow_zero, Int.natAbs_eq_zero, 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 : α
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
negSucc :
  ∀ (k : ℕ) (hk : (fun (x : ℤ) ↦ g ^ x) (Int.negSucc k) = x) (hk : g ^ Int.negSucc k = x),
    g ^ (Int.negSucc k).natAbs ∈ H
⊢ g ^ k.natAbs ∈ H

Tactic:
rcases k with k | k
-- 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 : α
hx₁ : x ∈ H
hx₂ : x ≠ 1
k : ℕ
hk_1 : (fun (x : ℤ) ↦ g ^ x) (Int.ofNat k) = x
hk : g ^ Int.ofNat k = x
ofNat : x ∈ H
⊢ g ^ (Int.ofNat k).natAbs ∈ H

Tactic:
rw [Int.ofNat_eq_natCast, Int.natAbs_natCast k, ← zpow_natCast,
                ← Int.ofNat_eq_natCast, hk]

Premises used: zpow_natCast, Int.ofNat_eq_natCast, Int.natAbs_natCast
-- 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 : α
hx₁ : x ∈ H
hx₂ : x ≠ 1
k : ℕ
hk_1 : (fun (x : ℤ) ↦ g ^ x) (Int.ofNat k) = x
hk : g ^ Int.ofNat k = x
⊢ x ∈ H

Tactic:
hx₁
-- 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 : α
hx₁ : x ∈ H
hx₂ : x ≠ 1
k : ℕ
hk_1 : (fun (x : ℤ) ↦ g ^ x) (Int.ofNat k) = x
hk : g ^ Int.ofNat k = x
⊢ x ∈ H

Tactic:
exact hx₁
-- 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 : α
hx₁ : x ∈ H
hx₂ : x ≠ 1
k : ℕ
hk_1 : (fun (x : ℤ) ↦ g ^ x) (Int.negSucc k) = x
hk : g ^ Int.negSucc k = x
negSucc : (g ^ k.succ)⁻¹ ∈ H
⊢ g ^ (Int.negSucc k).natAbs ∈ H

Tactic:
rw [Int.natAbs_negSucc, ← Subgroup.inv_mem_iff H]

Premises used: Subgroup.inv_mem_iff, Int.natAbs_negSucc
-- 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 : α
hx₁ : x ∈ H
hx₂ : x ≠ 1
k : ℕ
hk_1 : (fun (x : ℤ) ↦ g ^ x) (Int.negSucc k) = x
hk : g ^ Int.negSucc k = x
⊢ (g ^ k.succ)⁻¹ ∈ H

Tactic:
simp_all
-- 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
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
⊢ 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]

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
hx₃ : HPow.hPow (β := ℤ) g (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ) ∈ H
⊢ 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:
apply H.zpow_mem

Premises used: Subgroup.zpow_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_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) : ℤ) ∈ H

Tactic:
mod_cast (Nat.find_spec hex).2

Premises used: zpow_natCast, congrArg, cast, Membership.mem, And.right, Nat.find, Eq.symm, 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
⊢ HPow.hPow (β := ℤ) g (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ) ∈ H

Tactic:
exact mod_cast (Nat.find_spec hex).2

Premises used: And.right, 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
rw : x ∈ H
⊢ g ^ (k % (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ)) *
      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_add, Int.emod_add_mul_ediv, hk]

Premises used: zpow_add, Int.emod_add_mul_ediv
-- 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
⊢ x ∈ H

Tactic:
hx
-- 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
⊢ x ∈ H

Tactic:
exact hx
-- 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
rw 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) : ℤ)
⊢ 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 : ℤ)

Tactic:
rw [Int.natAbs_of_nonneg
              (Int.emod_nonneg _ (Int.natCast_ne_zero_iff_pos.2 (Nat.find_spec hex).1))]

Premises used: Iff.mpr, Int.natCast_ne_zero_iff_pos, Int.natAbs_of_nonneg, And.left, Int.emod_nonneg, 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 : ℤ)
rwa : HPow.hPow (β := ℤ) g (↑(k % (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ)).natAbs : ℤ) ∈ H
rwa₁ rwa₂ rwa₃ rwa₄ : g ^ (k % (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ)) ∈ H
⊢ g ^ (k % (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ)).natAbs ∈ H

Tactic:
rwa [← zpow_natCast, ← hk₄]

Premises used: zpow_natCast
-- 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
rw :
  k % (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ) <
    (↑(Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ g ^ n ∈ H) hex) : ℤ)
⊢ 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) : ℤ)

Tactic:
rw [← hk₄]