awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : Eq.{u_1 + 1} (α := Finset α) {a : α | orderOf a = d} ∅
c₁ : c = ∑ m ∈ c.divisors, card.{u_1} (α := α) {a : α | orderOf a = m}
c₂ :
  Eq (α := ℕ) (∑ m ∈ c.divisors, card.{u_1} (α := α) {a : α | orderOf a = m})
    (∑ m ∈ c.divisors.erase d, card.{u_1} (α := α) {a : α | orderOf a = m})
c₃ :
  LE.le (α := ℕ) (∑ m ∈ c.divisors.erase d, card.{u_1} (α := α) {a : α | orderOf a = m}) (∑ m ∈ c.divisors.erase d, φ m)
⊢ c < c

Tactic:
calc
    c = ∑ m ∈ c.divisors, #{a : α | orderOf a = m} := by
      simp only [sum_card_orderOf_eq_card_pow_eq_one hc0.ne']
      apply congr_arg card
      simp [c]
    _ = ∑ m ∈ c.divisors.erase d, #{a : α | orderOf a = m} := by
      rw [eq_comm]
      refine sum_subset (erase_subset _ _) fun m hm₁ hm₂ => ?_
      have : m = d := by
        contrapose! hm₂
        exact mem_erase_of_ne_of_mem hm₂ hm₁
      simp [this, h0]
    _ ≤ ∑ m ∈ c.divisors.erase d, φ m := by
      gcongr with m hm
      have hmc : m ∣ c := by
        simp only [mem_erase, mem_divisors] at hm
        tauto
      obtain h1 | h1 := (#{a : α | orderOf a = m}).eq_zero_or_pos
      · simp [h1]
      · simp [card_orderOf_eq_totient_aux₁ hn hmc h1]
    _ < ∑ m ∈ c.divisors, φ m :=
      sum_erase_lt_of_pos (mem_divisors.2 ⟨hd, hc0.ne'⟩) (totient_pos.2 (pos_of_dvd_of_pos hd hc0))
    _ = c := sum_totient _

Premises used: Iff.mpr, Nat.mem_divisors, Nat.sum_totient, LT.lt.ne', Nat.divisors, And.intro, Nat.pos_of_dvd_of_pos, Nat.totient_pos, Finset.erase, Finset.sum_erase_lt_of_pos
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
rw : 0 < Fintype.card α
⊢ 0 < card.{u_1} (α := α) {a : α | orderOf a = Nat.card α}

Tactic:
rw [Nat.card_eq_fintype_card, card_orderOf_eq_totient_aux₂ hn dvd_rfl, totient_pos]

Premises used: card_orderOf_eq_totient_aux₂, dvd_rfl, Nat.totient_pos, Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
⊢ 0 < Fintype.card α

Tactic:
apply Fintype.card_pos

Premises used: Fintype.card_pos
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : IsCyclic α
inst_2 : Fintype α
d : ℕ
hd : d ∣ Fintype.card α
⊢ card.{u_1} (α := α) {a : α | orderOf a = d} = φ d

Tactic:
apply card_orderOf_eq_totient_aux₂ (fun n => IsCyclic.card_pow_eq_one_le) hd

Premises used: IsCyclic.card_pow_eq_one_le, card_orderOf_eq_totient_aux₂
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : IsCyclic α
inst_2 : Fintype α
d : ℕ
hd : d ∣ Fintype.card α
⊢ card.{u_1} (α := α) {a : α | orderOf a = d} = φ d

Tactic:
classical apply card_orderOf_eq_totient_aux₂ (fun n => IsCyclic.card_pow_eq_one_le) hd
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card α = p
⊢ Fact (Nat.Prime (Nat.card α))

Tactic:
subst h
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
hp : Fact (Nat.Prime (Nat.card α))
⊢ Finite α

Tactic:
have : Finite α := Nat.finite_of_card_ne_zero hp.1.ne_zero
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
hp : Fact (Nat.Prime (Nat.card α))
this : Finite α
⊢ Nontrivial α

Tactic:
have : Nontrivial α := Finite.one_lt_card_iff_nontrivial.mp hp.1.one_lt
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
hp : Fact (Nat.Prime (Nat.card α))
this_1 : Finite α
this : Nontrivial α
⊢ IsSimpleGroup α

Tactic:
⟨fun H _ => H.eq_bot_or_eq_top_of_prime_card⟩

Premises used: IsSimpleGroup.mk, Subgroup.eq_bot_or_eq_top_of_prime_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
hp : Fact (Nat.Prime (Nat.card α))
this_1 : Finite α
this : Nontrivial α
⊢ IsSimpleGroup α

Tactic:
exact ⟨fun H _ => H.eq_bot_or_eq_top_of_prime_card⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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 :
  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 :
  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)
⊢ x ^ m = (f : (a : G) → G') a

Tactic:
simpa [Subtype.ext_iff] using hm

Premises used: Subtype.ext_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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 :
  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
⊢ x ^ n = (f : (a : G) → G') b

Tactic:
simpa [Subtype.ext_iff] using hn

Premises used: Subtype.ext_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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
rw₆ rw₇ : Eq.{u_3 + 1} (α := G') 1 1
⊢ y ^ (-m) * a ∈ f.ker

Tactic:
rw [f.mem_ker, f.map_mul, f.map_zpow, hxy, zpow_neg x m, hm, inv_mul_cancel]

Premises used: inv_mul_cancel, MonoidHom.mem_ker, zpow_neg, MonoidHom.map_mul, MonoidHom.map_zpow
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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
rw₆ rw₇ : Eq.{u_3 + 1} (α := G') 1 1
⊢ y ^ (-n) * b ∈ f.ker

Tactic:
rw [f.mem_ker, f.map_mul, f.map_zpow, hxy, zpow_neg x n, hn, inv_mul_cancel]

Premises used: inv_mul_cancel, MonoidHom.mem_ker, zpow_neg, MonoidHom.map_mul, MonoidHom.map_zpow
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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)
⊢ a * b = y ^ m * (y ^ (-m) * a * y ^ n) * (y ^ (-n) * b)

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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)
rw rw₁ : y ^ m * (y ^ (-m) * a * y ^ n) * (y ^ (-n) * b) = y ^ m * (y ^ (-m) * a * y ^ n) * (y ^ (-n) * b)
⊢ y ^ m * (y ^ (-m) * a * y ^ n) * (y ^ (-n) * b) = y ^ m * (y ^ n * (y ^ (-m) * a)) * (y ^ (-n) * b)

Tactic:
rw [mem_center_iff.1 ha]

Premises used: Subgroup.mem_center_iff, Iff.mp
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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) * (a * (y ^ (-n) * b))

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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)
rw rw₁ : y ^ m * y ^ n * y ^ (-m) * (y ^ (-n) * b * a) = y ^ m * y ^ n * y ^ (-m) * (y ^ (-n) * b * a)
⊢ y ^ m * y ^ n * y ^ (-m) * (a * (y ^ (-n) * b)) = y ^ m * y ^ n * y ^ (-m) * (y ^ (-n) * b * a)

Tactic:
rw [mem_center_iff.1 hb]

Premises used: Subgroup.mem_center_iff, Iff.mp
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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
group₄ group₅ : HPow.hPow (β := ℤ) y 0 * b * a = b * a
⊢ y ^ m * y ^ n * y ^ (-m) * (y ^ (-n) * b * a) = b * a

Tactic:
group
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst : CommGroup α
inst_1 : IsSimpleGroup α
⊢ Nontrivial α

Tactic:
nontriviality α
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst : CommGroup α
inst_1 : IsSimpleGroup α
inst_2 : Nontrivial α
obtain : ∀ (g : α) (hg : g ≠ 1), IsCyclic α
⊢ IsCyclic α

Tactic:
obtain ⟨g, hg⟩ := exists_ne (1 : α)

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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
⊢ 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)
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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
this : Eq (α := Subgroup α) (Subgroup.zpowers g) ⊤
⊢ IsCyclic α

Tactic:
⟨⟨g, (Subgroup.eq_top_iff' _).1 this⟩⟩

Premises used: Subgroup.eq_top_iff', Exists.intro, Iff.mp, IsCyclic.mk
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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
this : Eq (α := Subgroup α) (Subgroup.zpowers g) ⊤
⊢ IsCyclic α

Tactic:
exact ⟨⟨g, (Subgroup.eq_top_iff' _).1 this⟩⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : IsSimpleGroup α
⊢ Nontrivial α

Tactic:
have hα : Nontrivial α := IsSimpleGroup.toNontrivial
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : IsSimpleGroup α
hα : Nontrivial α
obtain : ∀ (g : α) (hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (Subgroup.zpowers g) x), Nat.Prime (Nat.card α)
⊢ Nat.Prime (Nat.card α)

Tactic:
obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := α)

Premises used: IsCyclic.exists_generator
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : IsSimpleGroup α
hα : Nontrivial α
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (Subgroup.zpowers g) x
contrapose! : ∀ (hα : Nat.card α = 1), Subsingleton α
⊢ Nat.card α ≠ 1

Tactic:
contrapose! hα
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : IsSimpleGroup α
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (Subgroup.zpowers g) x
hα : Nat.card α = 1
⊢ Subsingleton α

Tactic:
(Nat.card_eq_one_iff_unique.mp hα).1

Premises used: Nat.card_eq_one_iff_unique, And.left, Iff.mp
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : IsSimpleGroup α
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (Subgroup.zpowers g) x
hα : Nat.card α = 1
⊢ Subsingleton α

Tactic:
exact (Nat.card_eq_one_iff_unique.mp hα).1

Premises used: Nat.card_eq_one_iff_unique, And.left, Iff.mp
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : IsSimpleGroup α
hα : Nontrivial α
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (Subgroup.zpowers g) x
⊢ Nat.card α ≠ 1

Tactic:
replace hα : Nat.card α ≠ 1 := by contrapose! hα; exact (Nat.card_eq_one_iff_unique.mp hα).1
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : IsSimpleGroup α
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (Subgroup.zpowers g) x
hα : Nat.card α ≠ 1
rw : ∀ (hα : orderOf g ≠ 1), Nat.Prime (orderOf g)
⊢ Nat.Prime (Nat.card α)

Tactic:
rw [← orderOf_eq_card_of_forall_mem_zpowers hg] at hα ⊢

Premises used: orderOf_eq_card_of_forall_mem_zpowers
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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)

Tactic:
(IsSimpleOrder.eq_bot_or_eq_top (Subgroup.zpowers (g ^ n))).imp ?_ fun h ↦ ?_

Premises used: HPow.hPow, Subgroup.zpowers, Or.imp, IsSimpleOrder.eq_bot_or_eq_top
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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
refine_2 : ∀ (h : Eq (α := Subgroup α) (Subgroup.zpowers (g ^ n)) ⊤), n.Coprime (orderOf g)
⊢ orderOf g ∣ n ∨ n.Coprime (orderOf g)

Tactic:
refine (IsSimpleOrder.eq_bot_or_eq_top (Subgroup.zpowers (g ^ n))).imp ?_ fun h ↦ ?_

Premises used: HPow.hPow, Subgroup.zpowers, Or.imp, IsSimpleOrder.eq_bot_or_eq_top
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : IsSimpleGroup α
g : α
hg : ∀ (x : α), Membership.mem (γ := Subgroup α) (Subgroup.zpowers g) x
hα : orderOf g ≠ 1
n : ℕ
⊢ Eq (α := Subgroup α) (Subgroup.zpowers (g ^ n)) ⊥ → orderOf g ∣ n

Tactic:
simp [orderOf_dvd_iff_pow_eq_one]

Premises used: orderOf_dvd_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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)) ⊤
⊢ Membership.mem (γ := Subgroup α) (Subgroup.zpowers (g ^ n)) g

Tactic:
simp_all only [ne_eq, orderOf_eq_one_iff,
        Subgroup.mem_top]

Premises used: ne_eq, Subgroup.mem_top, orderOf_eq_one_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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)) ⊤
⊢ 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]
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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)) ⊤
hgn : Membership.mem (γ := Subgroup α) (Subgroup.zpowers (g ^ n)) g
⊢ n.gcd (orderOf g) = 1

Tactic:
mem_zpowers_pow_iff.mp hgn

Premises used: mem_zpowers_pow_iff, Iff.mp
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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)) ⊤
hgn : Membership.mem (γ := Subgroup α) (Subgroup.zpowers (g ^ n)) g
⊢ n.gcd (orderOf g) = 1

Tactic:
exact mem_zpowers_pow_iff.mp hgn

Premises used: mem_zpowers_pow_iff, Iff.mp
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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)

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
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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
h₁ : ∀ m < orderOf g, m ≠ 0 → (orderOf g).Coprime m
⊢ Nat.Prime (orderOf g)

Tactic:
apply Nat.prime_of_coprime

Premises used: Nat.prime_of_coprime