awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst : Monoid G
a b x_1 y : G
n m : ℕ
M : Type u_6
inst_1 : Monoid M
x : M
hx : IsOfFinOrder x
rw : x ^ (orderOf x - 1 + 1) = 1
rw₁ : x ^ orderOf x = 1
⊢ x ^ (orderOf x - 1) * x = 1
have rw₂ : Eq.{u_6 + 1} (α := M) 1 1
Tactic: rw [← _root_.pow_succ, tsub_add_cancel_of_le (by exact hx.orderOf_pos), pow_orderOf_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : n ≠ 0
⊢ minimalPeriod (fun (x_1 : G) ↦ x ^ n * x_1) 1 =
    minimalPeriod (fun (x_1 : G) ↦ x * x_1) 1 / (minimalPeriod (fun (x_1 : G) ↦ x * x_1) 1).gcd n
have rw : minimalPeriod (fun (x_1 : G) ↦ x ^ n * x_1) 1 = minimalPeriod.{u_1} (α := G) (fun (x_1 : G) ↦ x * x_1)^[n] 1
Tactic: rw [← minimalPeriod_iterate_eq_div_gcd h, mul_left_iterate]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : n ≠ 0
rw : minimalPeriod (fun (x_1 : G) ↦ x ^ n * x_1) 1 = minimalPeriod.{u_1} (α := G) (fun (x_1 : G) ↦ x * x_1)^[n] 1
⊢ minimalPeriod (fun (x_1 : G) ↦ x ^ n * x_1) 1 =
    minimalPeriod (fun (x_1 : G) ↦ x * x_1) 1 / (minimalPeriod (fun (x_1 : G) ↦ x * x_1) 1).gcd n
have rw₁ : minimalPeriod (fun (x_1 : G) ↦ x ^ n * x_1) 1 = minimalPeriod (fun (x_1 : G) ↦ x ^ n * x_1) 1
Tactic: rw [← minimalPeriod_iterate_eq_div_gcd h, mul_left_iterate]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
hn : n ≠ 0
dvd : n ∣ orderOf x
⊢ orderOf (x ^ n) = orderOf x / n
have rw : orderOf x / (orderOf x).gcd n = orderOf x / n
Tactic: rw [orderOf_pow' _ hn, Nat.gcd_eq_right dvd]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
hn : n ≠ 0
dvd : n ∣ orderOf x
rw : orderOf x / (orderOf x).gcd n = orderOf x / n
⊢ orderOf (x ^ n) = orderOf x / n
have rw₁ : orderOf x / n = orderOf x / n
Tactic: rw [orderOf_pow' _ hn, Nat.gcd_eq_right dvd]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
hx : orderOf x ≠ 0
hn : n ∣ orderOf x
⊢ orderOf (x ^ (orderOf x / n)) = n
have rw : orderOf x / n ≠ 0
Tactic: rw [orderOf_pow_of_dvd _ (Nat.div_dvd_of_dvd hn), Nat.div_div_self hn hx]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (hypothesis)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
hx : orderOf x ≠ 0
hn : n ∣ orderOf x
⊢ orderOf x / n ≠ 0
have hx₁ : orderOf x / n * n ≠ 0
Tactic: rw [← Nat.div_mul_cancel hn] at hx
Cleared hypotheses: hx, hn
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : IsOfFinOrder x
⊢ minimalPeriod (fun (x_1 : G) ↦ x ^ n * x_1) 1 =
    minimalPeriod (fun (x_1 : G) ↦ x * x_1) 1 / (minimalPeriod (fun (x_1 : G) ↦ x * x_1) 1).gcd n
have rw : minimalPeriod (fun (x_1 : G) ↦ x ^ n * x_1) 1 = minimalPeriod.{u_1} (α := G) (fun (x_1 : G) ↦ x * x_1)^[n] 1
Tactic: rw [← minimalPeriod_iterate_eq_div_gcd' h, mul_left_iterate]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : IsOfFinOrder x
rw : minimalPeriod (fun (x_1 : G) ↦ x ^ n * x_1) 1 = minimalPeriod.{u_1} (α := G) (fun (x_1 : G) ↦ x * x_1)^[n] 1
⊢ minimalPeriod (fun (x_1 : G) ↦ x ^ n * x_1) 1 =
    minimalPeriod (fun (x_1 : G) ↦ x * x_1) 1 / (minimalPeriod (fun (x_1 : G) ↦ x * x_1) 1).gcd n
have rw₁ : minimalPeriod (fun (x_1 : G) ↦ x ^ n * x_1) 1 = minimalPeriod (fun (x_1 : G) ↦ x ^ n * x_1) 1
Tactic: rw [← minimalPeriod_iterate_eq_div_gcd' h, mul_left_iterate]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
y : G
m : ℕ
h : (orderOf y).Coprime m
⊢ orderOf (y ^ m) = orderOf y
have pos : ∀ (hg : IsOfFinOrder y), orderOf (y ^ m) = orderOf y
Tactic: by_cases hg : IsOfFinOrder y
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
y : G
m : ℕ
h : (orderOf y).Coprime m
pos : ∀ (hg : IsOfFinOrder y), orderOf (y ^ m) = orderOf y
⊢ orderOf (y ^ m) = orderOf y
have neg : ∀ (hg : ¬IsOfFinOrder y), orderOf (y ^ m) = orderOf y
Tactic: by_cases hg : IsOfFinOrder y
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
y : G
m : ℕ
h : (orderOf y).Coprime m
hg : IsOfFinOrder y
⊢ orderOf (y ^ m) = orderOf y
have pos : orderOf y / (orderOf y).gcd m = orderOf y
Tactic: rw [hg.orderOf_pow y m, h.gcd_eq_one, Nat.div_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
y : G
m : ℕ
h : (orderOf y).Coprime m
hg : IsOfFinOrder y
pos : orderOf y / (orderOf y).gcd m = orderOf y
⊢ orderOf (y ^ m) = orderOf y
have pos₁ : orderOf y / 1 = orderOf y
Tactic: rw [hg.orderOf_pow y m, h.gcd_eq_one, Nat.div_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
y : G
m : ℕ
h : (orderOf y).Coprime m
hg : IsOfFinOrder y
pos : orderOf y / (orderOf y).gcd m = orderOf y
pos₁ : orderOf y / 1 = orderOf y
⊢ orderOf (y ^ m) = orderOf y
have pos₂ : orderOf y = orderOf y
Tactic: rw [hg.orderOf_pow y m, h.gcd_eq_one, Nat.div_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
y : G
m : ℕ
h : (orderOf y).Coprime m
hg : ¬IsOfFinOrder y
⊢ orderOf (y ^ m) = orderOf y
have neg : orderOf (HPow.hPow (β := ℕ) y 1) = orderOf y
Tactic: rw [m.coprime_zero_left.1 (orderOf_eq_zero hg ▸ h), pow_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
y : G
m : ℕ
h : (orderOf y).Coprime m
hg : ¬IsOfFinOrder y
neg : orderOf (HPow.hPow (β := ℕ) y 1) = orderOf y
⊢ orderOf (y ^ m) = orderOf y
have neg₁ : orderOf y = orderOf y
Tactic: rw [m.coprime_zero_left.1 (orderOf_eq_zero hg ▸ h), pow_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
a : G
ha : IsOfFinOrder a
⊢ (↑(powers a) : Set G).Finite
have rw : (↑(Finset.image (fun (x : ℕ) ↦ a ^ x) (Finset.range (orderOf a))) : Set G).Finite
Tactic: rw [ha.powers_eq_image_range_orderOf]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
a : G
ha : IsOfFinOrder a
⊢ (↑(powers a) : Set G).Finite
have classical : (↑(Finset.image (fun (x : ℕ) ↦ a ^ x) (Finset.range (orderOf a))) : Set G).Finite
Tactic: classical rw [ha.powers_eq_image_range_orderOf]; exact Finset.finite_toSet _
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
⊢ orderOf (x * y) ∣ (orderOf x).lcm (orderOf y)
have rw : minimalPeriod.{u_1} (α := G) ((fun (x_1 : G) ↦ x * x_1) ∘ fun (x : G) ↦ y * x) 1 ∣ (orderOf x).lcm (orderOf y)
Tactic: rw [orderOf, ← comp_mul_left]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
⊢ orderOf y ∣ (orderOf x).lcm (orderOf (x * y))
have pos : ∀ (h0 : orderOf x = 0), orderOf y ∣ (orderOf x).lcm (orderOf (x * y))
Tactic: by_cases h0 : orderOf x = 0
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
pos : ∀ (h0 : orderOf x = 0), orderOf y ∣ (orderOf x).lcm (orderOf (x * y))
⊢ orderOf y ∣ (orderOf x).lcm (orderOf (x * y))
have neg : ∀ (h0 : ¬orderOf x = 0), orderOf y ∣ (orderOf x).lcm (orderOf (x * y))
Tactic: by_cases h0 : orderOf x = 0
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
h0 : orderOf x = 0
⊢ orderOf y ∣ (orderOf x).lcm (orderOf (x * y))
have pos : orderOf y ∣ 0
Tactic: rw [h0, lcm_zero_left]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
h0 : ¬orderOf x = 0
| orderOf y
have rw : orderOf (x ^ (orderOf x).pred * (x * y))
Tactic: rw [← one_mul y, ← pow_orderOf_eq_one x, ← succ_pred_eq_of_pos (Nat.pos_of_ne_zero h0),
      _root_.pow_succ, mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
h0 : ¬orderOf x = 0
⊢ orderOf y ∣ (orderOf x).lcm (orderOf (x * y))
have neg : orderOf (x ^ (orderOf x).pred * (x * y)) ∣ (orderOf x).lcm (orderOf (x * y))
Tactic: conv_lhs =>
    rw [← one_mul y, ← pow_orderOf_eq_one x, ← succ_pred_eq_of_pos (Nat.pos_of_ne_zero h0),
      _root_.pow_succ, mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
hco : (orderOf x).Coprime (orderOf y)
⊢ orderOf (x * y) = orderOf x * orderOf y
have rw : minimalPeriod.{u_1} (α := G) ((fun (x_1 : G) ↦ x * x_1) ∘ fun (x : G) ↦ y * x) 1 = orderOf x * orderOf y
Tactic: rw [orderOf, ← comp_mul_left]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (hypothesis)
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
⊢ orderOf (x * y) = orderOf y
have hoy : 0 < orderOf y
Tactic: have hoy := hy.orderOf_pos
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (hypothesis)
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
⊢ orderOf (x * y) = orderOf y
have hxy : orderOf x ∣ orderOf y
Tactic: have hxy := dvd_of_forall_prime_mul_dvd hdvd
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
⊢ orderOf (x * y) = orderOf y
have hx : (x * y) ^ orderOf y = 1
Tactic: apply orderOf_eq_of_pow_and_pow_div_prime hoy
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
hx : (x * y) ^ orderOf y = 1
⊢ orderOf (x * y) = orderOf y
have hd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf y → (x * y) ^ (orderOf y / p) ≠ 1
Tactic: apply orderOf_eq_of_pow_and_pow_div_prime hoy
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
⊢ (x * y) ^ orderOf y = 1
have hx : orderOf (x * y) ∣ orderOf y
Tactic: simp only [Ne, ← orderOf_dvd_iff_pow_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
⊢ ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf y → (x * y) ^ (orderOf y / p) ≠ 1
have hd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf y → ¬orderOf (x * y) ∣ orderOf y / p
Tactic: simp only [Ne, ← orderOf_dvd_iff_pow_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
⊢ ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf y → ¬orderOf (x * y) ∣ orderOf y / p
have hd : ∀ (p : ℕ) (hp : Nat.Prime p) (hpy : p ∣ orderOf y) (hd : orderOf (x * y) ∣ orderOf y / p), p = 1
Tactic: refine fun p hp hpy hd => hp.ne_one ?_
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
p : ℕ
hp : Nat.Prime p
hpy : p ∣ orderOf y
hd : orderOf (x * y) ∣ orderOf y / p
⊢ p = 1
have hd₁ : orderOf y ∣ orderOf y / p
Tactic: rw [← Nat.dvd_one, ← mul_dvd_mul_iff_right hoy.ne', one_mul, ← dvd_div_iff_mul_dvd hpy]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
p : ℕ
hp : Nat.Prime p
hpy : p ∣ orderOf y
hd : orderOf (x * y) ∣ orderOf y / p
⊢ orderOf y ∣ orderOf y / p
have hd₁ : p * orderOf x ∣ orderOf y
Tactic: refine (orderOf_dvd_lcm_mul h).trans (Nat.lcm_dvd ((dvd_div_iff_mul_dvd hpy).2 ?_) hd)
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
p : ℕ
hp : Nat.Prime p
hpy : p ∣ orderOf y
hd : orderOf (x * y) ∣ orderOf y / p
⊢ p * orderOf x ∣ orderOf y
have pos : ∀ (h : p ∣ orderOf x), p * orderOf x ∣ orderOf y
Tactic: by_cases h : p ∣ orderOf x
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
p : ℕ
hp : Nat.Prime p
hpy : p ∣ orderOf y
hd : orderOf (x * y) ∣ orderOf y / p
pos : ∀ (h : p ∣ orderOf x), p * orderOf x ∣ orderOf y
⊢ p * orderOf x ∣ orderOf y
have neg : ∀ (h : ¬p ∣ orderOf x), p * orderOf x ∣ orderOf y
Tactic: by_cases h : p ∣ orderOf x
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
p : ℕ
hp : Fact (Nat.Prime p)
⊢ orderOf x = p ↔ x ^ p = 1 ∧ x ≠ 1
have rw : minimalPeriod (fun (x_1 : G) ↦ x * x_1) 1 = p ↔ x ^ p = 1 ∧ x ≠ 1
Tactic: rw [orderOf, minimalPeriod_eq_prime_iff, isPeriodicPt_mul_iff_pow_eq_one, IsFixedPt, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
p : ℕ
hp : Fact (Nat.Prime p)
rw : minimalPeriod (fun (x_1 : G) ↦ x * x_1) 1 = p ↔ x ^ p = 1 ∧ x ≠ 1
⊢ orderOf x = p ↔ x ^ p = 1 ∧ x ≠ 1
have rw₁ : IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) p 1 ∧ ¬IsFixedPt (fun (x_1 : G) ↦ x * x_1) 1 ↔ x ^ p = 1 ∧ x ≠ 1
Tactic: rw [orderOf, minimalPeriod_eq_prime_iff, isPeriodicPt_mul_iff_pow_eq_one, IsFixedPt, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
p : ℕ
hp : Fact (Nat.Prime p)
rw : minimalPeriod (fun (x_1 : G) ↦ x * x_1) 1 = p ↔ x ^ p = 1 ∧ x ≠ 1
rw₁ : IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) p 1 ∧ ¬IsFixedPt (fun (x_1 : G) ↦ x * x_1) 1 ↔ x ^ p = 1 ∧ x ≠ 1
⊢ orderOf x = p ↔ x ^ p = 1 ∧ x ≠ 1
have rw₂ : x ^ p = 1 ∧ ¬IsFixedPt (fun (x_1 : G) ↦ x * x_1) 1 ↔ x ^ p = 1 ∧ x ≠ 1
Tactic: rw [orderOf, minimalPeriod_eq_prime_iff, isPeriodicPt_mul_iff_pow_eq_one, IsFixedPt, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
p : ℕ
hp : Fact (Nat.Prime p)
rw : minimalPeriod (fun (x_1 : G) ↦ x * x_1) 1 = p ↔ x ^ p = 1 ∧ x ≠ 1
rw₁ : IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) p 1 ∧ ¬IsFixedPt (fun (x_1 : G) ↦ x * x_1) 1 ↔ x ^ p = 1 ∧ x ≠ 1
rw₂ : x ^ p = 1 ∧ ¬IsFixedPt (fun (x_1 : G) ↦ x * x_1) 1 ↔ x ^ p = 1 ∧ x ≠ 1
⊢ orderOf x = p ↔ x ^ p = 1 ∧ x ≠ 1
have rw₃ : x ^ p = 1 ∧ ¬x * 1 = 1 ↔ x ^ p = 1 ∧ x ≠ 1
Tactic: rw [orderOf, minimalPeriod_eq_prime_iff, isPeriodicPt_mul_iff_pow_eq_one, IsFixedPt, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
p : ℕ
hp : Fact (Nat.Prime p)
rw : minimalPeriod (fun (x_1 : G) ↦ x * x_1) 1 = p ↔ x ^ p = 1 ∧ x ≠ 1
rw₁ : IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) p 1 ∧ ¬IsFixedPt (fun (x_1 : G) ↦ x * x_1) 1 ↔ x ^ p = 1 ∧ x ≠ 1
rw₂ : x ^ p = 1 ∧ ¬IsFixedPt (fun (x_1 : G) ↦ x * x_1) 1 ↔ x ^ p = 1 ∧ x ≠ 1
rw₃ : x ^ p = 1 ∧ ¬x * 1 = 1 ↔ x ^ p = 1 ∧ x ≠ 1
⊢ orderOf x = p ↔ x ^ p = 1 ∧ x ≠ 1
have rw₄ : x ^ p = 1 ∧ ¬x = 1 ↔ x ^ p = 1 ∧ x ≠ 1
Tactic: rw [orderOf, minimalPeriod_eq_prime_iff, isPeriodicPt_mul_iff_pow_eq_one, IsFixedPt, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n p : ℕ
hp : Fact (Nat.Prime p)
hnot : ¬x ^ p ^ n = 1
hfin : x ^ p ^ (n + 1) = 1
⊢ orderOf x = p ^ (n + 1)
have hk : ¬IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) (p ^ n) 1
Tactic: apply minimalPeriod_eq_prime_pow
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n p : ℕ
hp : Fact (Nat.Prime p)
hnot : ¬x ^ p ^ n = 1
hfin : x ^ p ^ (n + 1) = 1
hk : ¬IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) (p ^ n) 1
⊢ orderOf x = p ^ (n + 1)
have hk1 : IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) (p ^ (n + 1)) 1
Tactic: apply minimalPeriod_eq_prime_pow
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
p : ℕ
hp : Fact (Nat.Prime p)
h : ∃ (k : ℕ), orderOf x = p ^ k
k : ℕ
hk : orderOf x = p ^ k
⊢ x ^ p ^ k = 1
have rw : x ^ orderOf x = 1
Tactic: rw [← hk, pow_orderOf_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
p : ℕ
hp : Fact (Nat.Prime p)
h : ∃ (k : ℕ), orderOf x = p ^ k
k : ℕ
hk : orderOf x = p ^ k
rw : x ^ orderOf x = 1
⊢ x ^ p ^ k = 1
have rw₁ : Eq.{u_1 + 1} (α := G) 1 1
Tactic: rw [← hk, pow_orderOf_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
p : ℕ
hp : Fact (Nat.Prime p)
h : ∃ (m : ℕ), x ^ p ^ m = 1
w : ℕ
hm : x ^ p ^ w = 1
⊢ ∃ (k : ℕ), orderOf x = p ^ k
have obtain : ∀ k ≤ w, ∀ (hk : orderOf x = p ^ k), ∃ (k : ℕ), orderOf x = p ^ k
Tactic: obtain ⟨k, _, hk⟩ := (Nat.dvd_prime_pow hp.elim).mp (orderOf_dvd_of_pow_eq_one hm)
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
R : Type u_6
inst : Ring R
inst_1 : Nontrivial R
⊢ orderOf.{u_6} (G := R) (-1) = if ringChar R = 2 then 1 else 2
have pos : ∀ (h : ringChar R = 2), orderOf.{u_6} (G := R) (-1) = 1
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
R : Type u_6
inst : Ring R
inst_1 : Nontrivial R
pos : ∀ (h : ringChar R = 2), orderOf.{u_6} (G := R) (-1) = 1
⊢ orderOf.{u_6} (G := R) (-1) = if ringChar R = 2 then 1 else 2
have neg : ∀ (h : ¬ringChar R = 2), orderOf.{u_6} (G := R) (-1) = 2
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
R : Type u_6
inst : Ring R
inst_1 : Nontrivial R
h : ringChar R = 2
⊢ orderOf.{u_6} (G := R) (-1) = 1
have pos : orderOf.{u_6} (G := R) 1 = 1
Tactic: rw [neg_one_eq_one_iff.2 h, orderOf_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
R : Type u_6
inst : Ring R
inst_1 : Nontrivial R
h : ringChar R = 2
pos : orderOf.{u_6} (G := R) 1 = 1
⊢ orderOf.{u_6} (G := R) (-1) = 1
have pos₁ : Eq (α := ℕ) 1 1
Tactic: rw [neg_one_eq_one_iff.2 h, orderOf_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
R : Type u_6
inst : Ring R
inst_1 : Nontrivial R
h : ¬ringChar R = 2
⊢ orderOf.{u_6} (G := R) (-1) = 2
have neg : HPow.hPow (α := R) (β := ℕ) (-1) 2 = 1
Tactic: apply orderOf_eq_prime
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
R : Type u_6
inst : Ring R
inst_1 : Nontrivial R
h : ¬ringChar R = 2
neg : HPow.hPow (α := R) (β := ℕ) (-1) 2 = 1
⊢ orderOf.{u_6} (G := R) (-1) = 2
have neg₁ : Ne.{u_6 + 1} (α := R) (-1) 1
Tactic: apply orderOf_eq_prime
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
R : Type u_6
inst : Ring R
inst_1 : Nontrivial R
inst_2 : NoZeroDivisors R
p : ℕ
hp : p ≠ 2
inst_3 : CharP R p
x : R
⊢ orderOf x = 2 ↔ x = -1
have simp : x = -1 → ¬x = 1
Tactic: simp only [orderOf_eq_prime_iff, sq_eq_one_iff, ne_eq, or_and_right, and_not_self, false_or,
    and_iff_left_iff_imp]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
hx : IsOfFinOrder x
n : ℕ
⊢ ((finEquivPowers hx).symm : (a : ↥(powers x)) → Fin (orderOf x))
      (Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Submonoid G) (powers x) x_1) (x ^ n) ⋯) =
    (⟨n % orderOf x, ⋯⟩ : Fin (orderOf x))
have rw : Eq (α := ↥(powers x)) (Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Submonoid G) (powers x) x_1) (x ^ n) sorry)
  ((finEquivPowers hx : (a : Fin (orderOf x)) → ↥(powers x)) (⟨n % orderOf x, sorry⟩ : Fin (orderOf x)))
Tactic: rw [Equiv.symm_apply_eq, finEquivPowers_apply, Subtype.mk_eq_mk, ← pow_mod_orderOf, Fin.val_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
hx : IsOfFinOrder x
n : ℕ
rw :
  Eq (α := ↥(powers x)) (Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Submonoid G) (powers x) x_1) (x ^ n) ⋯)
    ((finEquivPowers hx : (a : Fin (orderOf x)) → ↥(powers x)) (⟨n % orderOf x, ⋯⟩ : Fin (orderOf x)))
⊢ ((finEquivPowers hx).symm : (a : ↥(powers x)) → Fin (orderOf x))
      (Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Submonoid G) (powers x) x_1) (x ^ n) ⋯) =
    (⟨n % orderOf x, ⋯⟩ : Fin (orderOf x))
have rw₁ : Eq (α := ↥(powers x)) (Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Submonoid G) (powers x) x_1) (x ^ n) sorry)
  (Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Submonoid G) (powers x) x_1)
    (x ^ (↑(⟨n % orderOf x, sorry⟩ : Fin (orderOf x)) : ℕ)) sorry)
Tactic: rw [Equiv.symm_apply_eq, finEquivPowers_apply, Subtype.mk_eq_mk, ← pow_mod_orderOf, Fin.val_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
hx : IsOfFinOrder x
n : ℕ
rw :
  Eq (α := ↥(powers x)) (Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Submonoid G) (powers x) x_1) (x ^ n) ⋯)
    ((finEquivPowers hx : (a : Fin (orderOf x)) → ↥(powers x)) (⟨n % orderOf x, ⋯⟩ : Fin (orderOf x)))
rw₁ :
  Eq (α := ↥(powers x)) (Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Submonoid G) (powers x) x_1) (x ^ n) ⋯)
    (Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Submonoid G) (powers x) x_1)
      (x ^ (↑(⟨n % orderOf x, ⋯⟩ : Fin (orderOf x)) : ℕ)) ⋯)
⊢ ((finEquivPowers hx).symm : (a : ↥(powers x)) → Fin (orderOf x))
      (Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Submonoid G) (powers x) x_1) (x ^ n) ⋯) =
    (⟨n % orderOf x, ⋯⟩ : Fin (orderOf x))
have rw₂ : x ^ n = x ^ (↑(⟨n % orderOf x, sorry⟩ : Fin (orderOf x)) : ℕ)
Tactic: rw [Equiv.symm_apply_eq, finEquivPowers_apply, Subtype.mk_eq_mk, ← pow_mod_orderOf, Fin.val_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
hx : IsOfFinOrder x
n : ℕ
rw :
  Eq (α := ↥(powers x)) (Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Submonoid G) (powers x) x_1) (x ^ n) ⋯)
    ((finEquivPowers hx : (a : Fin (orderOf x)) → ↥(powers x)) (⟨n % orderOf x, ⋯⟩ : Fin (orderOf x)))
rw₁ :
  Eq (α := ↥(powers x)) (Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Submonoid G) (powers x) x_1) (x ^ n) ⋯)
    (Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Submonoid G) (powers x) x_1)
      (x ^ (↑(⟨n % orderOf x, ⋯⟩ : Fin (orderOf x)) : ℕ)) ⋯)
rw₂ : x ^ n = x ^ (↑(⟨n % orderOf x, ⋯⟩ : Fin (orderOf x)) : ℕ)
⊢ ((finEquivPowers hx).symm : (a : ↥(powers x)) → Fin (orderOf x))
      (Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Submonoid G) (powers x) x_1) (x ^ n) ⋯) =
    (⟨n % orderOf x, ⋯⟩ : Fin (orderOf x))
have rw₃ : x ^ (n % orderOf x) = x ^ (↑(⟨n % orderOf x, sorry⟩ : Fin (orderOf x)) : ℕ)
Tactic: rw [Equiv.symm_apply_eq, finEquivPowers_apply, Subtype.mk_eq_mk, ← pow_mod_orderOf, Fin.val_mk]