awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
G' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : IsCyclic G'
f : G →* G'
hf : f.ker ≤ center G
a b : G
x : G'
y : G
hxy : (f : (a : G) → G') y = x
hx :
  ∀ (a : ↥f.range),
    Membership.mem (γ := Subgroup ↥f.range) (zpowers (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) x ⋯)) a
m : ℤ
hm_1 :
  Eq.{u_3 + 1} (α := ↥f.range)
    ((fun (x_1 : ℤ) ↦ HPow.hPow (α := ↥f.range) (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) x ⋯) x_1) m : ↥f.range)
    (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) ((f : (a : G) → G') a) ⋯ : ↥f.range)
n : ℤ
hn_1 :
  Eq.{u_3 + 1} (α := ↥f.range)
    ((fun (x_1 : ℤ) ↦ HPow.hPow (α := ↥f.range) (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) x ⋯) x_1) n : ↥f.range)
    (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) ((f : (a : G) → G') b) ⋯ : ↥f.range)
hm : x ^ m = (f : (a : G) → G') a
hn : x ^ n = (f : (a : G) → G') b
rw : Eq.{u_3 + 1} (α := G') ((f : (a : G) → G') (y ^ (-m) * a) : G') (1 : G')
rw₁ : HMul.hMul (α := G') (β := G') ((f : (a : G) → G') (y ^ (-m)) : G') ((f : (a : G) → G') a : G') = 1
rw₂ : HMul.hMul (β := G') (HPow.hPow (α := G') ((f : (a : G) → G') y : G') (-m)) ((f : (a : G) → G') a : G') = 1
rw₃ : HMul.hMul (β := G') (x ^ (-m)) ((f : (a : G) → G') a : G') = 1
rw₄ : HMul.hMul (β := G') (x ^ m)⁻¹ ((f : (a : G) → G') a : G') = 1
rw₅ : HMul.hMul (α := G') (β := G') (((f : (a : G) → G') a)⁻¹ : G') ((f : (a : G) → G') a : G') = 1
⊢ y ^ (-m) * a ∈ f.ker
have rw₆ : Eq.{u_3 + 1} (α := G') 1 1
Tactic: rw [f.mem_ker, f.map_mul, f.map_zpow, hxy, zpow_neg x m, hm, inv_mul_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
G' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : IsCyclic G'
f : G →* G'
hf : f.ker ≤ center G
a b : G
x : G'
y : G
hxy : (f : (a : G) → G') y = x
hx :
  ∀ (a : ↥f.range),
    Membership.mem (γ := Subgroup ↥f.range) (zpowers (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) x ⋯)) a
m : ℤ
hm_1 :
  Eq.{u_3 + 1} (α := ↥f.range)
    ((fun (x_1 : ℤ) ↦ HPow.hPow (α := ↥f.range) (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) x ⋯) x_1) m : ↥f.range)
    (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) ((f : (a : G) → G') a) ⋯ : ↥f.range)
n : ℤ
hn_1 :
  Eq.{u_3 + 1} (α := ↥f.range)
    ((fun (x_1 : ℤ) ↦ HPow.hPow (α := ↥f.range) (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) x ⋯) x_1) n : ↥f.range)
    (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) ((f : (a : G) → G') b) ⋯ : ↥f.range)
hm : x ^ m = (f : (a : G) → G') a
hn : x ^ n = (f : (a : G) → G') b
ha : Membership.mem (γ := Subgroup G) (center G) (y ^ (-m) * a)
⊢ y ^ (-n) * b ∈ f.ker
have rw : Eq.{u_3 + 1} (α := G') ((f : (a : G) → G') (y ^ (-n) * b) : G') (1 : G')
Tactic: rw [f.mem_ker, f.map_mul, f.map_zpow, hxy, zpow_neg x n, hn, inv_mul_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
G' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : IsCyclic G'
f : G →* G'
hf : f.ker ≤ center G
a b : G
x : G'
y : G
hxy : (f : (a : G) → G') y = x
hx :
  ∀ (a : ↥f.range),
    Membership.mem (γ := Subgroup ↥f.range) (zpowers (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) x ⋯)) a
m : ℤ
hm_1 :
  Eq.{u_3 + 1} (α := ↥f.range)
    ((fun (x_1 : ℤ) ↦ HPow.hPow (α := ↥f.range) (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) x ⋯) x_1) m : ↥f.range)
    (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) ((f : (a : G) → G') a) ⋯ : ↥f.range)
n : ℤ
hn_1 :
  Eq.{u_3 + 1} (α := ↥f.range)
    ((fun (x_1 : ℤ) ↦ HPow.hPow (α := ↥f.range) (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) x ⋯) x_1) n : ↥f.range)
    (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) ((f : (a : G) → G') b) ⋯ : ↥f.range)
hm : x ^ m = (f : (a : G) → G') a
hn : x ^ n = (f : (a : G) → G') b
ha : Membership.mem (γ := Subgroup G) (center G) (y ^ (-m) * a)
rw : Eq.{u_3 + 1} (α := G') ((f : (a : G) → G') (y ^ (-n) * b) : G') (1 : G')
⊢ y ^ (-n) * b ∈ f.ker
have rw₁ : HMul.hMul (α := G') (β := G') ((f : (a : G) → G') (y ^ (-n)) : G') ((f : (a : G) → G') b : G') = 1
Tactic: rw [f.mem_ker, f.map_mul, f.map_zpow, hxy, zpow_neg x n, hn, inv_mul_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
G' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : IsCyclic G'
f : G →* G'
hf : f.ker ≤ center G
a b : G
x : G'
y : G
hxy : (f : (a : G) → G') y = x
hx :
  ∀ (a : ↥f.range),
    Membership.mem (γ := Subgroup ↥f.range) (zpowers (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) x ⋯)) a
m : ℤ
hm_1 :
  Eq.{u_3 + 1} (α := ↥f.range)
    ((fun (x_1 : ℤ) ↦ HPow.hPow (α := ↥f.range) (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) x ⋯) x_1) m : ↥f.range)
    (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) ((f : (a : G) → G') a) ⋯ : ↥f.range)
n : ℤ
hn_1 :
  Eq.{u_3 + 1} (α := ↥f.range)
    ((fun (x_1 : ℤ) ↦ HPow.hPow (α := ↥f.range) (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) x ⋯) x_1) n : ↥f.range)
    (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) ((f : (a : G) → G') b) ⋯ : ↥f.range)
hm : x ^ m = (f : (a : G) → G') a
hn : x ^ n = (f : (a : G) → G') b
ha : Membership.mem (γ := Subgroup G) (center G) (y ^ (-m) * a)
rw : Eq.{u_3 + 1} (α := G') ((f : (a : G) → G') (y ^ (-n) * b) : G') (1 : G')
rw₁ : HMul.hMul (α := G') (β := G') ((f : (a : G) → G') (y ^ (-n)) : G') ((f : (a : G) → G') b : G') = 1
⊢ y ^ (-n) * b ∈ f.ker
have rw₂ : HMul.hMul (β := G') (HPow.hPow (α := G') ((f : (a : G) → G') y : G') (-n)) ((f : (a : G) → G') b : G') = 1
Tactic: rw [f.mem_ker, f.map_mul, f.map_zpow, hxy, zpow_neg x n, hn, inv_mul_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
G' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : IsCyclic G'
f : G →* G'
hf : f.ker ≤ center G
a b : G
x : G'
y : G
hxy : (f : (a : G) → G') y = x
hx :
  ∀ (a : ↥f.range),
    Membership.mem (γ := Subgroup ↥f.range) (zpowers (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) x ⋯)) a
m : ℤ
hm_1 :
  Eq.{u_3 + 1} (α := ↥f.range)
    ((fun (x_1 : ℤ) ↦ HPow.hPow (α := ↥f.range) (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) x ⋯) x_1) m : ↥f.range)
    (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) ((f : (a : G) → G') a) ⋯ : ↥f.range)
n : ℤ
hn_1 :
  Eq.{u_3 + 1} (α := ↥f.range)
    ((fun (x_1 : ℤ) ↦ HPow.hPow (α := ↥f.range) (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) x ⋯) x_1) n : ↥f.range)
    (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) ((f : (a : G) → G') b) ⋯ : ↥f.range)
hm : x ^ m = (f : (a : G) → G') a
hn : x ^ n = (f : (a : G) → G') b
ha : Membership.mem (γ := Subgroup G) (center G) (y ^ (-m) * a)
rw : Eq.{u_3 + 1} (α := G') ((f : (a : G) → G') (y ^ (-n) * b) : G') (1 : G')
rw₁ : HMul.hMul (α := G') (β := G') ((f : (a : G) → G') (y ^ (-n)) : G') ((f : (a : G) → G') b : G') = 1
rw₂ : HMul.hMul (β := G') (HPow.hPow (α := G') ((f : (a : G) → G') y : G') (-n)) ((f : (a : G) → G') b : G') = 1
⊢ y ^ (-n) * b ∈ f.ker
have rw₃ : HMul.hMul (β := G') (x ^ (-n)) ((f : (a : G) → G') b : G') = 1
Tactic: rw [f.mem_ker, f.map_mul, f.map_zpow, hxy, zpow_neg x n, hn, inv_mul_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
G' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : IsCyclic G'
f : G →* G'
hf : f.ker ≤ center G
a b : G
x : G'
y : G
hxy : (f : (a : G) → G') y = x
hx :
  ∀ (a : ↥f.range),
    Membership.mem (γ := Subgroup ↥f.range) (zpowers (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) x ⋯)) a
m : ℤ
hm_1 :
  Eq.{u_3 + 1} (α := ↥f.range)
    ((fun (x_1 : ℤ) ↦ HPow.hPow (α := ↥f.range) (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) x ⋯) x_1) m : ↥f.range)
    (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) ((f : (a : G) → G') a) ⋯ : ↥f.range)
n : ℤ
hn_1 :
  Eq.{u_3 + 1} (α := ↥f.range)
    ((fun (x_1 : ℤ) ↦ HPow.hPow (α := ↥f.range) (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) x ⋯) x_1) n : ↥f.range)
    (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) ((f : (a : G) → G') b) ⋯ : ↥f.range)
hm : x ^ m = (f : (a : G) → G') a
hn : x ^ n = (f : (a : G) → G') b
ha : Membership.mem (γ := Subgroup G) (center G) (y ^ (-m) * a)
rw : Eq.{u_3 + 1} (α := G') ((f : (a : G) → G') (y ^ (-n) * b) : G') (1 : G')
rw₁ : HMul.hMul (α := G') (β := G') ((f : (a : G) → G') (y ^ (-n)) : G') ((f : (a : G) → G') b : G') = 1
rw₂ : HMul.hMul (β := G') (HPow.hPow (α := G') ((f : (a : G) → G') y : G') (-n)) ((f : (a : G) → G') b : G') = 1
rw₃ : HMul.hMul (β := G') (x ^ (-n)) ((f : (a : G) → G') b : G') = 1
⊢ y ^ (-n) * b ∈ f.ker
have rw₄ : HMul.hMul (β := G') (x ^ n)⁻¹ ((f : (a : G) → G') b : G') = 1
Tactic: rw [f.mem_ker, f.map_mul, f.map_zpow, hxy, zpow_neg x n, hn, inv_mul_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
G' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : IsCyclic G'
f : G →* G'
hf : f.ker ≤ center G
a b : G
x : G'
y : G
hxy : (f : (a : G) → G') y = x
hx :
  ∀ (a : ↥f.range),
    Membership.mem (γ := Subgroup ↥f.range) (zpowers (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) x ⋯)) a
m : ℤ
hm_1 :
  Eq.{u_3 + 1} (α := ↥f.range)
    ((fun (x_1 : ℤ) ↦ HPow.hPow (α := ↥f.range) (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) x ⋯) x_1) m : ↥f.range)
    (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) ((f : (a : G) → G') a) ⋯ : ↥f.range)
n : ℤ
hn_1 :
  Eq.{u_3 + 1} (α := ↥f.range)
    ((fun (x_1 : ℤ) ↦ HPow.hPow (α := ↥f.range) (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) x ⋯) x_1) n : ↥f.range)
    (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) ((f : (a : G) → G') b) ⋯ : ↥f.range)
hm : x ^ m = (f : (a : G) → G') a
hn : x ^ n = (f : (a : G) → G') b
ha : Membership.mem (γ := Subgroup G) (center G) (y ^ (-m) * a)
rw : Eq.{u_3 + 1} (α := G') ((f : (a : G) → G') (y ^ (-n) * b) : G') (1 : G')
rw₁ : HMul.hMul (α := G') (β := G') ((f : (a : G) → G') (y ^ (-n)) : G') ((f : (a : G) → G') b : G') = 1
rw₂ : HMul.hMul (β := G') (HPow.hPow (α := G') ((f : (a : G) → G') y : G') (-n)) ((f : (a : G) → G') b : G') = 1
rw₃ : HMul.hMul (β := G') (x ^ (-n)) ((f : (a : G) → G') b : G') = 1
rw₄ : HMul.hMul (β := G') (x ^ n)⁻¹ ((f : (a : G) → G') b : G') = 1
⊢ y ^ (-n) * b ∈ f.ker
have rw₅ : HMul.hMul (α := G') (β := G') (((f : (a : G) → G') b)⁻¹ : G') ((f : (a : G) → G') b : G') = 1
Tactic: rw [f.mem_ker, f.map_mul, f.map_zpow, hxy, zpow_neg x n, hn, inv_mul_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
G' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : IsCyclic G'
f : G →* G'
hf : f.ker ≤ center G
a b : G
x : G'
y : G
hxy : (f : (a : G) → G') y = x
hx :
  ∀ (a : ↥f.range),
    Membership.mem (γ := Subgroup ↥f.range) (zpowers (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) x ⋯)) a
m : ℤ
hm_1 :
  Eq.{u_3 + 1} (α := ↥f.range)
    ((fun (x_1 : ℤ) ↦ HPow.hPow (α := ↥f.range) (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) x ⋯) x_1) m : ↥f.range)
    (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) ((f : (a : G) → G') a) ⋯ : ↥f.range)
n : ℤ
hn_1 :
  Eq.{u_3 + 1} (α := ↥f.range)
    ((fun (x_1 : ℤ) ↦ HPow.hPow (α := ↥f.range) (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) x ⋯) x_1) n : ↥f.range)
    (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) ((f : (a : G) → G') b) ⋯ : ↥f.range)
hm : x ^ m = (f : (a : G) → G') a
hn : x ^ n = (f : (a : G) → G') b
ha : Membership.mem (γ := Subgroup G) (center G) (y ^ (-m) * a)
rw : Eq.{u_3 + 1} (α := G') ((f : (a : G) → G') (y ^ (-n) * b) : G') (1 : G')
rw₁ : HMul.hMul (α := G') (β := G') ((f : (a : G) → G') (y ^ (-n)) : G') ((f : (a : G) → G') b : G') = 1
rw₂ : HMul.hMul (β := G') (HPow.hPow (α := G') ((f : (a : G) → G') y : G') (-n)) ((f : (a : G) → G') b : G') = 1
rw₃ : HMul.hMul (β := G') (x ^ (-n)) ((f : (a : G) → G') b : G') = 1
rw₄ : HMul.hMul (β := G') (x ^ n)⁻¹ ((f : (a : G) → G') b : G') = 1
rw₅ : HMul.hMul (α := G') (β := G') (((f : (a : G) → G') b)⁻¹ : G') ((f : (a : G) → G') b : G') = 1
⊢ y ^ (-n) * b ∈ f.ker
have rw₆ : Eq.{u_3 + 1} (α := G') 1 1
Tactic: rw [f.mem_ker, f.map_mul, f.map_zpow, hxy, zpow_neg x n, hn, inv_mul_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
G' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : IsCyclic G'
f : G →* G'
hf : f.ker ≤ center G
a b : G
x : G'
y : G
hxy : (f : (a : G) → G') y = x
hx :
  ∀ (a : ↥f.range),
    Membership.mem (γ := Subgroup ↥f.range) (zpowers (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) x ⋯)) a
m : ℤ
hm_1 :
  Eq.{u_3 + 1} (α := ↥f.range)
    ((fun (x_1 : ℤ) ↦ HPow.hPow (α := ↥f.range) (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) x ⋯) x_1) m : ↥f.range)
    (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) ((f : (a : G) → G') a) ⋯ : ↥f.range)
n : ℤ
hn_1 :
  Eq.{u_3 + 1} (α := ↥f.range)
    ((fun (x_1 : ℤ) ↦ HPow.hPow (α := ↥f.range) (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) x ⋯) x_1) n : ↥f.range)
    (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) ((f : (a : G) → G') b) ⋯ : ↥f.range)
hm : x ^ m = (f : (a : G) → G') a
hn : x ^ n = (f : (a : G) → G') b
ha : Membership.mem (γ := Subgroup G) (center G) (y ^ (-m) * a)
hb : Membership.mem (γ := Subgroup G) (center G) (y ^ (-n) * b)
⊢ y ^ m * (y ^ (-m) * a * y ^ n) * (y ^ (-n) * b) = y ^ m * (y ^ n * (y ^ (-m) * a)) * (y ^ (-n) * b)
have rw : y ^ m * (y ^ (-m) * a * y ^ n) * (y ^ (-n) * b) = y ^ m * (y ^ (-m) * a * y ^ n) * (y ^ (-n) * b)
Tactic: rw [mem_center_iff.1 ha]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
G' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : IsCyclic G'
f : G →* G'
hf : f.ker ≤ center G
a b : G
x : G'
y : G
hxy : (f : (a : G) → G') y = x
hx :
  ∀ (a : ↥f.range),
    Membership.mem (γ := Subgroup ↥f.range) (zpowers (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) x ⋯)) a
m : ℤ
hm_1 :
  Eq.{u_3 + 1} (α := ↥f.range)
    ((fun (x_1 : ℤ) ↦ HPow.hPow (α := ↥f.range) (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) x ⋯) x_1) m : ↥f.range)
    (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) ((f : (a : G) → G') a) ⋯ : ↥f.range)
n : ℤ
hn_1 :
  Eq.{u_3 + 1} (α := ↥f.range)
    ((fun (x_1 : ℤ) ↦ HPow.hPow (α := ↥f.range) (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) x ⋯) x_1) n : ↥f.range)
    (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) ((f : (a : G) → G') b) ⋯ : ↥f.range)
hm : x ^ m = (f : (a : G) → G') a
hn : x ^ n = (f : (a : G) → G') b
ha : Membership.mem (γ := Subgroup G) (center G) (y ^ (-m) * a)
hb : Membership.mem (γ := Subgroup G) (center G) (y ^ (-n) * b)
⊢ y ^ m * y ^ n * y ^ (-m) * (a * (y ^ (-n) * b)) = y ^ m * y ^ n * y ^ (-m) * (y ^ (-n) * b * a)
have rw : y ^ m * y ^ n * y ^ (-m) * (y ^ (-n) * b * a) = y ^ m * y ^ n * y ^ (-m) * (y ^ (-n) * b * a)
Tactic: rw [mem_center_iff.1 hb]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
G' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : IsCyclic G'
f : G →* G'
hf : f.ker ≤ center G
a b : G
x : G'
y : G
hxy : (f : (a : G) → G') y = x
hx :
  ∀ (a : ↥f.range),
    Membership.mem (γ := Subgroup ↥f.range) (zpowers (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) x ⋯)) a
m : ℤ
hm_1 :
  Eq.{u_3 + 1} (α := ↥f.range)
    ((fun (x_1 : ℤ) ↦ HPow.hPow (α := ↥f.range) (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) x ⋯) x_1) m : ↥f.range)
    (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) ((f : (a : G) → G') a) ⋯ : ↥f.range)
n : ℤ
hn_1 :
  Eq.{u_3 + 1} (α := ↥f.range)
    ((fun (x_1 : ℤ) ↦ HPow.hPow (α := ↥f.range) (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) x ⋯) x_1) n : ↥f.range)
    (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) ((f : (a : G) → G') b) ⋯ : ↥f.range)
hm : x ^ m = (f : (a : G) → G') a
hn : x ^ n = (f : (a : G) → G') b
ha : Membership.mem (γ := Subgroup G) (center G) (y ^ (-m) * a)
hb : Membership.mem (γ := Subgroup G) (center G) (y ^ (-n) * b)
⊢ y ^ m * y ^ n * y ^ (-m) * (y ^ (-n) * b * a) = b * a
have group : y ^ (m + n + -m + -n) * b * a = b * a
Tactic: group
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
G' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : IsCyclic G'
f : G →* G'
hf : f.ker ≤ center G
a b : G
x : G'
y : G
hxy : (f : (a : G) → G') y = x
hx :
  ∀ (a : ↥f.range),
    Membership.mem (γ := Subgroup ↥f.range) (zpowers (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) x ⋯)) a
m : ℤ
hm_1 :
  Eq.{u_3 + 1} (α := ↥f.range)
    ((fun (x_1 : ℤ) ↦ HPow.hPow (α := ↥f.range) (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) x ⋯) x_1) m : ↥f.range)
    (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) ((f : (a : G) → G') a) ⋯ : ↥f.range)
n : ℤ
hn_1 :
  Eq.{u_3 + 1} (α := ↥f.range)
    ((fun (x_1 : ℤ) ↦ HPow.hPow (α := ↥f.range) (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) x ⋯) x_1) n : ↥f.range)
    (Subtype.mk (p := fun (x : G') ↦ x ∈ f.range) ((f : (a : G) → G') b) ⋯ : ↥f.range)
hm : x ^ m = (f : (a : G) → G') a
hn : x ^ n = (f : (a : G) → G') b
ha : Membership.mem (γ := Subgroup G) (center G) (y ^ (-m) * a)
hb : Membership.mem (γ := Subgroup G) (center G) (y ^ (-n) * b)
group group₁ group₂ group₃ : y ^ (m + n + -m + -n) * b * a = b * a
⊢ y ^ m * y ^ n * y ^ (-m) * (y ^ (-n) * b * a) = b * a
have group₄ : HPow.hPow (β := ℤ) y 0 * b * a = b * a
Tactic: group
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst : CommGroup α
inst_1 : IsSimpleGroup α
⊢ IsCyclic α
have inst : Nontrivial α
Tactic: nontriviality α
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst : CommGroup α
inst_1 : IsSimpleGroup α
inst_2 : Nontrivial α
⊢ IsCyclic α
have obtain : ∀ (g : α) (hg : g ≠ 1), IsCyclic α
Tactic: obtain ⟨g, hg⟩ := exists_ne (1 : α)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst : CommGroup α
inst_1 : IsSimpleGroup α
inst_2 : Nontrivial α
g : α
hg : g ≠ 1
⊢ IsCyclic α
have this : Eq (α := Subgroup α) (Subgroup.zpowers g) ⊤
Tactic: have : Subgroup.zpowers g = ⊤ :=
    (eq_bot_or_eq_top (Subgroup.zpowers g)).resolve_left (Subgroup.zpowers_ne_bot.2 hg)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : IsSimpleGroup α
⊢ Nat.Prime (Nat.card α)
have hα : Nontrivial α
Tactic: have hα : Nontrivial α := IsSimpleGroup.toNontrivial
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : IsSimpleGroup α
hα : Nontrivial α
⊢ Nat.Prime (Nat.card α)
have obtain : ∀ (g : α) (hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (Subgroup.zpowers g) x), Nat.Prime (Nat.card α)
Tactic: obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := α)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : IsSimpleGroup α
hα : Nontrivial α
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (Subgroup.zpowers g) x
⊢ Nat.card α ≠ 1
have contrapose! : ∀ (hα : Nat.card α = 1), Subsingleton α
Tactic: contrapose! hα
Cleared hypotheses: hα
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : IsSimpleGroup α
hα : Nontrivial α
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (Subgroup.zpowers g) x
⊢ Nat.Prime (Nat.card α)
have hα₁ : Nat.card α ≠ 1
Tactic: replace hα : Nat.card α ≠ 1 := by contrapose! hα; exact (Nat.card_eq_one_iff_unique.mp hα).1
Cleared hypotheses: hα
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : IsSimpleGroup α
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (Subgroup.zpowers g) x
hα : Nat.card α ≠ 1
⊢ Nat.Prime (Nat.card α)
have rw : ∀ (hα : orderOf g ≠ 1), Nat.Prime (orderOf g)
Tactic: rw [← orderOf_eq_card_of_forall_mem_zpowers hg] at hα ⊢
Cleared hypotheses: hα
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : IsSimpleGroup α
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (Subgroup.zpowers g) x
hα : orderOf g ≠ 1
n : ℕ
⊢ orderOf g ∣ n ∨ n.Coprime (orderOf g)
have refine_1 : Eq (α := Subgroup α) (Subgroup.zpowers (g ^ n)) ⊥ → orderOf g ∣ n
Tactic: refine (IsSimpleOrder.eq_bot_or_eq_top (Subgroup.zpowers (g ^ n))).imp ?_ fun h ↦ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : IsSimpleGroup α
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (Subgroup.zpowers g) x
hα : orderOf g ≠ 1
n : ℕ
refine_1 : Eq (α := Subgroup α) (Subgroup.zpowers (g ^ n)) ⊥ → orderOf g ∣ n
⊢ orderOf g ∣ n ∨ n.Coprime (orderOf g)
have refine_2 : ∀ (h : Eq (α := Subgroup α) (Subgroup.zpowers (g ^ n)) ⊤), n.Coprime (orderOf g)
Tactic: refine (IsSimpleOrder.eq_bot_or_eq_top (Subgroup.zpowers (g ^ n))).imp ?_ fun h ↦ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : IsSimpleGroup α
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (Subgroup.zpowers g) x
hα : orderOf g ≠ 1
n : ℕ
h : Eq (α := Subgroup α) (Subgroup.zpowers (g ^ n)) ⊤
⊢ n.gcd (orderOf g) = 1
have hgn : Membership.mem (γ := Subgroup α) (Subgroup.zpowers (g ^ n)) g
Tactic: have hgn : g ∈ Subgroup.zpowers (g ^ n) := by simp_all only [ne_eq, orderOf_eq_one_iff,
        Subgroup.mem_top]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : IsSimpleGroup α
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (Subgroup.zpowers g) x
hα : orderOf g ≠ 1
⊢ Nat.Prime (orderOf g)
have h : ∀ (n : ℕ), orderOf g ∣ n ∨ n.Coprime (orderOf g)
Tactic: have h (n : ℕ) : orderOf g ∣ n ∨ n.Coprime (orderOf g) := by
    refine (IsSimpleOrder.eq_bot_or_eq_top (Subgroup.zpowers (g ^ n))).imp ?_ fun h ↦ ?_
    · simp [orderOf_dvd_iff_pow_eq_one]
    · simp only [Nat.coprime_iff_gcd_eq_one]
      have hgn : g ∈ Subgroup.zpowers (g ^ n) := by simp_all only [ne_eq, orderOf_eq_one_iff,
        Subgroup.mem_top]
      exact mem_zpowers_pow_iff.mp hgn
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : IsSimpleGroup α
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (Subgroup.zpowers g) x
hα : orderOf g ≠ 1
h : ∀ (n : ℕ), orderOf g ∣ n ∨ n.Coprime (orderOf g)
⊢ Nat.Prime (orderOf g)
have h1 : 1 < orderOf g
Tactic: apply Nat.prime_of_coprime
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : IsSimpleGroup α
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (Subgroup.zpowers g) x
hα : orderOf g ≠ 1
h : ∀ (n : ℕ), orderOf g ∣ n ∨ n.Coprime (orderOf g)
h1 : 1 < orderOf g
⊢ Nat.Prime (orderOf g)
have h₁ : ∀ m < orderOf g, m ≠ 0 → (orderOf g).Coprime m
Tactic: apply Nat.prime_of_coprime
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : IsSimpleGroup α
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (Subgroup.zpowers g) x
hα : orderOf g ≠ 1
h : ∀ (n : ℕ), orderOf g ∣ n ∨ n.Coprime (orderOf g)
⊢ 1 < orderOf g
have h1 : orderOf g ≠ 0
Tactic: refine Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨?_, hα⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : IsSimpleGroup α
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (Subgroup.zpowers g) x
hα : orderOf g ≠ 1
h : ∀ (n : ℕ), orderOf g ∣ n ∨ n.Coprime (orderOf g)
⊢ orderOf g ≠ 0
have h1 : ∀ (h : orderOf g = 0), ∃ (n : ℕ), ¬orderOf g ∣ n ∧ n.gcd (orderOf g) ≠ 1
Tactic: contrapose! h
Cleared hypotheses: h
-- 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
⊢ IsAddCyclic A ↔ Nonempty.{max 1 (u_4 + 1)} (A ≃+o ℤ)
have refine : IsAddCyclic A → Nonempty.{max 1 (u_4 + 1)} (A ≃+o ℤ)
Tactic: refine ⟨?_, fun ⟨e⟩ ↦ e.isAddCyclic.mpr inferInstance⟩
-- 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
⊢ g ≠ 0
have obtain : ∀ (a : A) (ha : a ≠ 0), g ≠ 0
Tactic: obtain ⟨a, ha⟩ := exists_ne (0 : A)