awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
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 : ℕ
IH :
  ∀ m < d,
    ∀ (hd : m ∣ Fintype.card α) (hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = m}),
      card.{u_1} (α := α) {a : α | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : Membership.mem (γ := Finset α) {a : α | orderOf a = d} a
ha : orderOf a = d
h1 : Eq (α := ℕ) (∑ m ∈ d.properDivisors, card.{u_1} (α := α) {a : α | orderOf a = m}) (∑ m ∈ d.properDivisors, φ m)
⊢ card.{u_1} (α := α) {a : α | orderOf a = d} = φ d
have h2 : Eq (α := ℕ) (∑ m ∈ d.divisors, card.{u_1} (α := α) {a : α | orderOf a = m}) (∑ m ∈ d.divisors, φ m)
Tactic: have h2 :
    (∑ m ∈ d.divisors, #{a : α | orderOf a = m}) =
      ∑ m ∈ d.divisors, φ m := by
    rw [sum_card_orderOf_eq_card_pow_eq_one hd0, sum_totient,
      ← ha, card_pow_eq_one_eq_orderOf_aux hn a]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
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 α
⊢ card.{u_1} (α := α) {a : α | orderOf a = d} = φ d
have hc0 : 0 < c
Tactic: have hc0 : 0 < c := Fintype.card_pos_iff.2 ⟨1⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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
⊢ card.{u_1} (α := α) {a : α | orderOf a = d} = φ d
have apply : 0 < card.{u_1} (α := α) {a : α | orderOf a = d}
Tactic: apply card_orderOf_eq_totient_aux₁ hn hd
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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
⊢ 0 < card.{u_1} (α := α) {a : α | orderOf a = d}
have by_contra : ∀ (h0 : ¬0 < card.{u_1} (α := α) {a : α | orderOf a = d}), False
Tactic: by_contra h0
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
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 : ¬0 < card.{u_1} (α := α) {a : α | orderOf a = d}
⊢ False
have h0₁ : Eq.{u_1 + 1} (α := Finset α) {a : α | orderOf a = d} ∅
Tactic: simp_rw [not_lt, Nat.le_zero, Finset.card_eq_zero] at h0
Cleared hypotheses: h0
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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} ∅
⊢ False
have apply : c < c
Tactic: apply lt_irrefl c
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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 = ∑ m ∈ c.divisors, card.{u_1} (α := α) {a : α | orderOf a = m}
have simp : c = card.{u_1} (α := α) {x : α | x ^ c = 1}
Tactic: simp only [sum_card_orderOf_eq_card_pow_eq_one hc0.ne']
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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 = card.{u_1} (α := α) {x : α | x ^ c = 1}
have apply : Eq.{u_1 + 1} (α := Finset α) univ {x : α | x ^ c = 1}
Tactic: apply congr_arg card
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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} ∅
⊢ Eq (α := ℕ) (∑ m ∈ c.divisors, card.{u_1} (α := α) {a : α | orderOf a = m})
    (∑ m ∈ c.divisors.erase d, card.{u_1} (α := α) {a : α | orderOf a = m})
have rw : Eq (α := ℕ) (∑ m ∈ c.divisors.erase d, card.{u_1} (α := α) {a : α | orderOf a = m})
  (∑ m ∈ c.divisors, card.{u_1} (α := α) {a : α | orderOf a = m})
Tactic: rw [eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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} ∅
⊢ Eq (α := ℕ) (∑ m ∈ c.divisors.erase d, card.{u_1} (α := α) {a : α | orderOf a = m})
    (∑ m ∈ c.divisors, card.{u_1} (α := α) {a : α | orderOf a = m})
have refine : ∀ (m : ℕ) (hm₁ : m ∈ c.divisors) (hm₂ : m ∉ c.divisors.erase d), card.{u_1} (α := α) {a : α | orderOf a = m} = 0
Tactic: refine sum_subset (erase_subset _ _) fun m hm₁ hm₂ => ?_
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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} ∅
m : ℕ
hm₁ : m ∈ c.divisors
hm₂ : m ∉ c.divisors.erase d
⊢ m = d
have contrapose! : ∀ (hm₂ : m ≠ d), m ∈ c.divisors.erase d
Tactic: contrapose! hm₂
Cleared hypotheses: hm₂
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
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} ∅
m : ℕ
hm₁ : m ∈ c.divisors
hm₂ : m ∉ c.divisors.erase d
⊢ card.{u_1} (α := α) {a : α | orderOf a = m} = 0
have this : m = d
Tactic: have : m = d := by
        contrapose! hm₂
        exact mem_erase_of_ne_of_mem hm₂ hm₁
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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} ∅
⊢ LE.le (α := ℕ) (∑ m ∈ c.divisors.erase d, card.{u_1} (α := α) {a : α | orderOf a = m}) (∑ m ∈ c.divisors.erase d, φ m)
have h : ∀ (m : ℕ) (hm : m ∈ c.divisors.erase d), card.{u_1} (α := α) {a : α | orderOf a = m} ≤ φ m
Tactic: gcongr with m hm
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
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} ∅
m : ℕ
hm : m ∈ c.divisors.erase d
⊢ m ∣ c
have hm₁ : m ≠ d ∧ m ∣ c ∧ c ≠ 0
Tactic: simp only [mem_erase, mem_divisors] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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} ∅
m : ℕ
hm : m ≠ d ∧ m ∣ c ∧ c ≠ 0
⊢ m ∣ c
have tauto : m ≠ d → m ∣ c → c ≠ 0 → m ∣ c
Tactic: tauto
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
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} ∅
m : ℕ
hm : m ∈ c.divisors.erase d
⊢ card.{u_1} (α := α) {a : α | orderOf a = m} ≤ φ m
have hmc : m ∣ c
Tactic: have hmc : m ∣ c := by
        simp only [mem_erase, mem_divisors] at hm
        tauto
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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} ∅
m : ℕ
hm : m ∈ c.divisors.erase d
hmc : m ∣ c
⊢ card.{u_1} (α := α) {a : α | orderOf a = m} ≤ φ m
have h : ∀ (h1 : card.{u_1} (α := α) {a : α | orderOf a = m} = 0), card.{u_1} (α := α) {a : α | orderOf a = m} ≤ φ m
Tactic: obtain h1 | h1 := (#{a : α | orderOf a = m}).eq_zero_or_pos
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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} ∅
m : ℕ
hm : m ∈ c.divisors.erase d
hmc : m ∣ c
h : ∀ (h1 : card.{u_1} (α := α) {a : α | orderOf a = m} = 0), card.{u_1} (α := α) {a : α | orderOf a = m} ≤ φ m
⊢ card.{u_1} (α := α) {a : α | orderOf a = m} ≤ φ m
have h₁ : ∀ (h1 : card.{u_1} (α := α) {a : α | orderOf a = m} > 0), card.{u_1} (α := α) {a : α | orderOf a = m} ≤ φ m
Tactic: obtain h1 | h1 := (#{a : α | orderOf a = m}).eq_zero_or_pos
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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
have c₁ : c = ∑ m ∈ c.divisors, card.{u_1} (α := α) {a : α | orderOf a = m}
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 _
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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 < c
have c₂ : Eq (α := ℕ) (∑ m ∈ c.divisors, card.{u_1} (α := α) {a : α | orderOf a = m})
  (∑ m ∈ c.divisors.erase d, card.{u_1} (α := α) {a : α | orderOf a = m})
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 _
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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 < c
have c₃ : LE.le (α := ℕ) (∑ m ∈ c.divisors.erase d, card.{u_1} (α := α) {a : α | orderOf a = m}) (∑ m ∈ c.divisors.erase d, φ m)
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 _
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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 < card.{u_1} (α := α) {a : α | orderOf a = Nat.card α}
have rw : 0 < Fintype.card α
Tactic: rw [Nat.card_eq_fintype_card, card_orderOf_eq_totient_aux₂ hn dvd_rfl, totient_pos]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
Goal:
α : Type u_1
inst : Group α
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card α = p
⊢ IsSimpleGroup α
have hp₁ : Fact (Nat.Prime (Nat.card α))
Tactic: subst h
Cleared hypotheses: p, hp, h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
Goal:
α : Type u_1
inst : Group α
hp : Fact (Nat.Prime (Nat.card α))
⊢ IsSimpleGroup α
have this : Finite α
Tactic: have : Finite α := Nat.finite_of_card_ne_zero hp.1.ne_zero
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
Goal:
α : Type u_1
inst : Group α
hp : Fact (Nat.Prime (Nat.card α))
this : Finite α
⊢ IsSimpleGroup α
have this₁ : Nontrivial α
Tactic: have : Nontrivial α := Finite.one_lt_card_iff_nontrivial.mp hp.1.one_lt
-- 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
⊢ y ^ (-m) * a ∈ f.ker
have rw : Eq.{u_3 + 1} (α := G') ((f : (a : G) → G') (y ^ (-m) * a) : G') (1 : G')
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
rw : Eq.{u_3 + 1} (α := G') ((f : (a : G) → G') (y ^ (-m) * a) : G') (1 : G')
⊢ y ^ (-m) * a ∈ f.ker
have rw₁ : HMul.hMul (α := G') (β := G') ((f : (a : G) → G') (y ^ (-m)) : G') ((f : (a : G) → G') a : G') = 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
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
⊢ y ^ (-m) * a ∈ f.ker
have rw₂ : HMul.hMul (β := G') (HPow.hPow (α := G') ((f : (a : G) → G') y : G') (-m)) ((f : (a : G) → G') a : G') = 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
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
⊢ y ^ (-m) * a ∈ f.ker
have rw₃ : HMul.hMul (β := G') (x ^ (-m)) ((f : (a : G) → G') a : G') = 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
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
⊢ y ^ (-m) * a ∈ f.ker
have rw₄ : HMul.hMul (β := G') (x ^ m)⁻¹ ((f : (a : G) → G') a : G') = 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
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
⊢ y ^ (-m) * a ∈ f.ker
have rw₅ : HMul.hMul (α := G') (β := G') (((f : (a : G) → G') a)⁻¹ : G') ((f : (a : G) → G') a : G') = 1
Tactic: rw [f.mem_ker, f.map_mul, f.map_zpow, hxy, zpow_neg x m, hm, inv_mul_cancel]