awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
⊢ orderOf.{u_1} (G := G) 1 = 1
have rw : minimalPeriod (fun (x : G) ↦ 1 * x) 1 = 1
Tactic: rw [orderOf, ← minimalPeriod_id (x := (1 : G)), ← one_mul_eq_id]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
rw : minimalPeriod (fun (x : G) ↦ 1 * x) 1 = 1
⊢ orderOf.{u_1} (G := G) 1 = 1
have rw₁ : minimalPeriod (fun (x : G) ↦ 1 * x) 1 = minimalPeriod.{u_1} (α := G) id 1
Tactic: rw [orderOf, ← minimalPeriod_id (x := (1 : G)), ← one_mul_eq_id]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
rw : minimalPeriod (fun (x : G) ↦ 1 * x) 1 = 1
rw₁ : minimalPeriod (fun (x : G) ↦ 1 * x) 1 = minimalPeriod.{u_1} (α := G) id 1
⊢ orderOf.{u_1} (G := G) 1 = 1
have rw₂ : minimalPeriod (fun (x : G) ↦ 1 * x) 1 = minimalPeriod (fun (x : G) ↦ 1 * x) 1
Tactic: rw [orderOf, ← minimalPeriod_id (x := (1 : G)), ← one_mul_eq_id]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
⊢ orderOf x = 1 ↔ x = 1
have rw : minimalPeriod (fun (x_1 : G) ↦ x * x_1) 1 = 1 ↔ x = 1
Tactic: rw [orderOf, minimalPeriod_eq_one_iff_isFixedPt, IsFixedPt, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
rw : minimalPeriod (fun (x_1 : G) ↦ x * x_1) 1 = 1 ↔ x = 1
⊢ orderOf x = 1 ↔ x = 1
have rw₁ : IsFixedPt (fun (x_1 : G) ↦ x * x_1) 1 ↔ x = 1
Tactic: rw [orderOf, minimalPeriod_eq_one_iff_isFixedPt, IsFixedPt, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
rw : minimalPeriod (fun (x_1 : G) ↦ x * x_1) 1 = 1 ↔ x = 1
rw₁ : IsFixedPt (fun (x_1 : G) ↦ x * x_1) 1 ↔ x = 1
⊢ orderOf x = 1 ↔ x = 1
have rw₂ : x * 1 = 1 ↔ x = 1
Tactic: rw [orderOf, minimalPeriod_eq_one_iff_isFixedPt, IsFixedPt, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
rw : minimalPeriod (fun (x_1 : G) ↦ x * x_1) 1 = 1 ↔ x = 1
rw₁ : IsFixedPt (fun (x_1 : G) ↦ x * x_1) 1 ↔ x = 1
rw₂ : x * 1 = 1 ↔ x = 1
⊢ orderOf x = 1 ↔ x = 1
have rw₃ : x = 1 ↔ x = 1
Tactic: rw [orderOf, minimalPeriod_eq_one_iff_isFixedPt, IsFixedPt, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
⊢ x ^ (n % orderOf x + orderOf x * (n / orderOf x)) = x ^ n
have rw : x ^ n = x ^ n
Tactic: rw [Nat.mod_add_div]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : orderOf x ∣ n
⊢ x ^ n = 1
have rw : x ^ (n % orderOf x) = 1
Tactic: rw [← pow_mod_orderOf, Nat.mod_eq_zero_of_dvd h, _root_.pow_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : orderOf x ∣ n
rw : x ^ (n % orderOf x) = 1
⊢ x ^ n = 1
have rw₁ : HPow.hPow (β := ℕ) x 0 = 1
Tactic: rw [← pow_mod_orderOf, Nat.mod_eq_zero_of_dvd h, _root_.pow_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : orderOf x ∣ n
rw : x ^ (n % orderOf x) = 1
rw₁ : HPow.hPow (β := ℕ) x 0 = 1
⊢ x ^ n = 1
have rw₂ : Eq.{u_1 + 1} (α := G) 1 1
Tactic: rw [← pow_mod_orderOf, Nat.mod_eq_zero_of_dvd h, _root_.pow_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
⊢ orderOf (x ^ n) ∣ orderOf x
have rw : (x ^ n) ^ orderOf x = 1
Tactic: rw [orderOf_dvd_iff_pow_eq_one, pow_right_comm, pow_orderOf_eq_one, one_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
rw : (x ^ n) ^ orderOf x = 1
⊢ orderOf (x ^ n) ∣ orderOf x
have rw₁ : (x ^ orderOf x) ^ n = 1
Tactic: rw [orderOf_dvd_iff_pow_eq_one, pow_right_comm, pow_orderOf_eq_one, one_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
rw : (x ^ n) ^ orderOf x = 1
rw₁ : (x ^ orderOf x) ^ n = 1
⊢ orderOf (x ^ n) ∣ orderOf x
have rw₂ : HPow.hPow (α := G) 1 n = 1
Tactic: rw [orderOf_dvd_iff_pow_eq_one, pow_right_comm, pow_orderOf_eq_one, one_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
rw : (x ^ n) ^ orderOf x = 1
rw₁ : (x ^ orderOf x) ^ n = 1
rw₂ : HPow.hPow (α := G) 1 n = 1
⊢ orderOf (x ^ n) ∣ orderOf x
have rw₃ : Eq.{u_1 + 1} (α := G) 1 1
Tactic: rw [orderOf_dvd_iff_pow_eq_one, pow_right_comm, pow_orderOf_eq_one, one_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n a b : ℕ
h : a ≡ b [MOD n]
hx : x ^ n = 1
⊢ x ^ a = x ^ b
have inl : ∀ (hle : a ≤ b), x ^ a = x ^ b
Tactic: obtain hle | hle := le_total a b
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n a b : ℕ
h : a ≡ b [MOD n]
hx : x ^ n = 1
inl : ∀ (hle : a ≤ b), x ^ a = x ^ b
⊢ x ^ a = x ^ b
have inr : ∀ (hle : b ≤ a), x ^ a = x ^ b
Tactic: obtain hle | hle := le_total a b
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n a b : ℕ
h : a ≡ b [MOD n]
hx : x ^ n = 1
hle : a ≤ b
⊢ x ^ a = x ^ b
have inl : ∀ (c : ℕ) (h : a ≡ a + c [MOD n]) (hle : a ≤ a + c), x ^ a = x ^ (a + c)
Tactic: obtain ⟨c, rfl⟩ := le_iff_exists_add.mp hle
Cleared hypotheses: b, h, hle
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n a : ℕ
hx : x ^ n = 1
c : ℕ
h : a ≡ a + c [MOD n]
hle : a ≤ a + c
⊢ x ^ a = x ^ (a + c)
have inl : ∀ (c : ℕ) (h : a ≡ a + n * c [MOD n]) (hle : a ≤ a + n * c), x ^ a = x ^ (a + n * c)
Tactic: obtain ⟨c, rfl⟩ : n ∣ c := by simpa using h
Cleared hypotheses: c, h, hle
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n a b : ℕ
h : a ≡ b [MOD n]
hx : x ^ n = 1
hle : b ≤ a
⊢ x ^ a = x ^ b
have inr : ∀ (c : ℕ) (h : b + c ≡ b [MOD n]) (hle : b ≤ b + c), x ^ (b + c) = x ^ b
Tactic: obtain ⟨c, rfl⟩ := le_iff_exists_add.mp hle
Cleared hypotheses: a, h, hle
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n b : ℕ
hx : x ^ n = 1
c : ℕ
h : b + c ≡ b [MOD n]
hle : b ≤ b + c
⊢ x ^ (b + c) = x ^ b
have inr : ∀ (c : ℕ) (h : b + n * c ≡ b [MOD n]) (hle : b ≤ b + n * c), x ^ (b + n * c) = x ^ b
Tactic: obtain ⟨c, rfl⟩ : n ∣ c := by simpa using h
Cleared hypotheses: c, h, hle
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
⊢ x ^ n = 1 ↔ n ≡ 0 [MOD orderOf x]
have rw : x ^ n = 1 ↔ orderOf x ∣ n
Tactic: rw [modEq_zero_iff_dvd, orderOf_dvd_iff_pow_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
rw : x ^ n = 1 ↔ orderOf x ∣ n
⊢ x ^ n = 1 ↔ n ≡ 0 [MOD orderOf x]
have rw₁ : x ^ n = 1 ↔ x ^ n = 1
Tactic: rw [modEq_zero_iff_dvd, orderOf_dvd_iff_pow_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
H : Type u_6
inst_1 : Monoid H
ψ : G →* H
x : G
⊢ orderOf.{u_6} (G := H) ((ψ : (a : G) → H) x : H) ∣ orderOf x
have h : HPow.hPow (α := H) ((ψ : (a : G) → H) x : H) (orderOf x) = 1
Tactic: apply orderOf_dvd_of_pow_eq_one
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
H : Type u_6
inst_1 : Monoid H
ψ : G →* H
x : G
⊢ HPow.hPow (α := H) ((ψ : (a : G) → H) x : H) (orderOf x) = 1
have h : Eq.{u_6 + 1} (α := H) ((ψ : (a : G) → H) 1 : H) (1 : H)
Tactic: rw [← map_pow, 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.Coprime (orderOf x)
⊢ ∃ (m : ℕ), (x ^ n) ^ m = x
have pos : ∀ (h0 : orderOf x = 0), ∃ (m : ℕ), (x ^ n) ^ m = x
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 : G
n : ℕ
h : n.Coprime (orderOf x)
pos : ∀ (h0 : orderOf x = 0), ∃ (m : ℕ), (x ^ n) ^ m = x
⊢ ∃ (m : ℕ), (x ^ n) ^ m = x
have neg : ∀ (h0 : ¬orderOf x = 0), ∃ (m : ℕ), (x ^ n) ^ m = x
Tactic: by_cases h0 : orderOf x = 0
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (hypothesis)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
h0 : orderOf x = 0
⊢ ∃ (m : ℕ), (x ^ n) ^ m = x
have h₁ : n = 1
Tactic: rw [h0, coprime_zero_right] at h
Cleared hypotheses: h, h0
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : n = 1
h0 : orderOf x = 0
⊢ HPow.hPow (β := ℕ) (x ^ n) 1 = x
have rw : HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) x 1) 1 = x
Tactic: rw [h, pow_one, pow_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : n = 1
h0 : orderOf x = 0
rw : HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) x 1) 1 = x
⊢ HPow.hPow (β := ℕ) (x ^ n) 1 = x
have rw₁ : HPow.hPow (β := ℕ) x 1 = x
Tactic: rw [h, pow_one, pow_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : n = 1
h0 : orderOf x = 0
rw : HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) x 1) 1 = x
rw₁ : HPow.hPow (β := ℕ) x 1 = x
⊢ HPow.hPow (β := ℕ) (x ^ n) 1 = x
have rw₂ : x = x
Tactic: rw [h, pow_one, pow_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
⊢ ∃ (m : ℕ), (x ^ n) ^ m = x
have pos : ∀ (h1 : orderOf x = 1), ∃ (m : ℕ), (x ^ n) ^ m = x
Tactic: by_cases h1 : orderOf x = 1
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
pos : ∀ (h1 : orderOf x = 1), ∃ (m : ℕ), (x ^ n) ^ m = x
⊢ ∃ (m : ℕ), (x ^ n) ^ m = x
have neg : ∀ (h1 : ¬orderOf x = 1), ∃ (m : ℕ), (x ^ n) ^ m = x
Tactic: by_cases h1 : orderOf x = 1
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : orderOf x = 1
⊢ HPow.hPow (β := ℕ) (x ^ n) 0 = x
have rw : HPow.hPow (β := ℕ) (HPow.hPow (α := G) 1 n) 0 = 1
Tactic: rw [orderOf_eq_one_iff.mp h1, one_pow, one_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : orderOf x = 1
rw : HPow.hPow (β := ℕ) (HPow.hPow (α := G) 1 n) 0 = 1
⊢ HPow.hPow (β := ℕ) (x ^ n) 0 = x
have rw₁ : HPow.hPow (α := G) (β := ℕ) 1 0 = 1
Tactic: rw [orderOf_eq_one_iff.mp h1, one_pow, one_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : orderOf x = 1
rw : HPow.hPow (β := ℕ) (HPow.hPow (α := G) 1 n) 0 = 1
rw₁ : HPow.hPow (α := G) (β := ℕ) 1 0 = 1
⊢ HPow.hPow (β := ℕ) (x ^ n) 0 = x
have rw₂ : Eq.{u_1 + 1} (α := G) 1 1
Tactic: rw [orderOf_eq_one_iff.mp h1, one_pow, one_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : ¬orderOf x = 1
⊢ ∃ (m : ℕ), (x ^ n) ^ m = x
have neg : ∀ (m : ℕ) (h : n * m % orderOf x = 1), ∃ (m : ℕ), (x ^ n) ^ m = x
Tactic: obtain ⟨m, -, h⟩ := exists_mul_mod_eq_one_of_coprime h (by lia)
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h_1 : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : ¬orderOf x = 1
m : ℕ
h : n * m % orderOf x = 1
⊢ (x ^ n) ^ m = x
have rw : x ^ (n * m) = x
Tactic: rw [← pow_mul, ← pow_mod_orderOf, h, pow_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h_1 : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : ¬orderOf x = 1
m : ℕ
h : n * m % orderOf x = 1
rw : x ^ (n * m) = x
⊢ (x ^ n) ^ m = x
have rw₁ : x ^ (n * m % orderOf x) = x
Tactic: rw [← pow_mul, ← pow_mod_orderOf, h, pow_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h_1 : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : ¬orderOf x = 1
m : ℕ
h : n * m % orderOf x = 1
rw : x ^ (n * m) = x
rw₁ : x ^ (n * m % orderOf x) = x
⊢ (x ^ n) ^ m = x
have rw₂ : HPow.hPow (β := ℕ) x 1 = x
Tactic: rw [← pow_mul, ← pow_mod_orderOf, h, pow_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h_1 : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : ¬orderOf x = 1
m : ℕ
h : n * m % orderOf x = 1
rw : x ^ (n * m) = x
rw₁ : x ^ (n * m % orderOf x) = x
rw₂ : HPow.hPow (β := ℕ) x 1 = x
⊢ (x ^ n) ^ m = x
have rw₃ : x = x
Tactic: rw [← pow_mul, ← pow_mod_orderOf, h, pow_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
⊢ orderOf x = n
have obtain : ∀ (a : ℕ) (ha : n = orderOf x * a), orderOf x = n
Tactic: obtain ⟨a, ha⟩ := exists_eq_mul_right_of_dvd (orderOf_dvd_of_pow_eq_one hx)
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
⊢ orderOf x = n
have suffices : a = 1
Tactic: suffices a = 1 by simp [this, ha]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
⊢ a = 1
have by_contra : ∀ (h : ¬a = 1), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
⊢ a.minFac ∣ n
have obtain : ∀ (b : ℕ) (hb : a = b * a.minFac), a.minFac ∣ n
Tactic: obtain ⟨b, hb⟩ : ∃ b : ℕ, a = b * a.minFac := exists_eq_mul_left_of_dvd a.minFac_dvd
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (hypothesis)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
b : ℕ
hb : a = b * a.minFac
⊢ a.minFac ∣ n
have ha₁ : n = orderOf x * b * a.minFac
Tactic: rw [hb, ← mul_assoc] at ha
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (hypothesis)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
⊢ False
have a_min_fac_dvd_p_sub_one : a.minFac ∣ n
Tactic: have a_min_fac_dvd_p_sub_one : a.minFac ∣ n := by
    obtain ⟨b, hb⟩ : ∃ b : ℕ, a = b * a.minFac := exists_eq_mul_left_of_dvd a.minFac_dvd
    rw [hb, ← mul_assoc] at ha
    exact Dvd.intro_left (orderOf x * b) ha.symm
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : a.minFac ∣ n
⊢ False
have refine : x ^ (n / a.minFac) = 1
Tactic: refine hd a.minFac (Nat.minFac_prime h) a_min_fac_dvd_p_sub_one ?_
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : a.minFac ∣ n
⊢ x ^ (n / a.minFac) = 1
have rw : a.minFac ∣ a
Tactic: rw [← orderOf_dvd_iff_pow_eq_one, Nat.dvd_div_iff_mul_dvd a_min_fac_dvd_p_sub_one, ha, mul_comm,
    Nat.mul_dvd_mul_iff_left (IsOfFinOrder.orderOf_pos _)]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : a.minFac ∣ n
rw : a.minFac ∣ a
⊢ x ^ (n / a.minFac) = 1
have rw₁ : IsOfFinOrder x
Tactic: rw [← orderOf_dvd_iff_pow_eq_one, Nat.dvd_div_iff_mul_dvd a_min_fac_dvd_p_sub_one, ha, mul_comm,
    Nat.mul_dvd_mul_iff_left (IsOfFinOrder.orderOf_pos _)]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : a.minFac ∣ n
⊢ IsOfFinOrder x
have rw : ∃ (n : ℕ), 0 < n ∧ x ^ n = 1
Tactic: rw [isOfFinOrder_iff_pow_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
H : Type u_6
inst_1 : Monoid H
y : H
⊢ orderOf x = orderOf y ↔ ∀ (n : ℕ), x ^ n = 1 ↔ y ^ n = 1
have simp_rw : orderOf x = orderOf y ↔ ∀ (n : ℕ), IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) n 1 ↔ IsPeriodicPt (fun (x : H) ↦ y * x) n 1
Tactic: simp_rw [← isPeriodicPt_mul_iff_pow_eq_one, ← minimalPeriod_eq_minimalPeriod_iff, orderOf]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
H : Type u_6
inst_1 : Monoid H
y : H
simp_rw :
  orderOf x = orderOf y ↔ ∀ (n : ℕ), IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) n 1 ↔ IsPeriodicPt (fun (x : H) ↦ y * x) n 1
⊢ orderOf x = orderOf y ↔ ∀ (n : ℕ), x ^ n = 1 ↔ y ^ n = 1
have simp_rw₁ : orderOf x = orderOf y ↔ minimalPeriod (fun (x_1 : G) ↦ x * x_1) 1 = minimalPeriod (fun (x : H) ↦ y * x) 1
Tactic: simp_rw [← isPeriodicPt_mul_iff_pow_eq_one, ← minimalPeriod_eq_minimalPeriod_iff, orderOf]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
H : Type u_6
inst_1 : Monoid H
f : G →* H
hf : Injective.{u_1 + 1, u_6 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
x : G
⊢ orderOf.{u_6} (G := H) ((f : (a : G) → H) x : H) = orderOf x
have simp_rw : ∀ (n : ℕ), HPow.hPow (α := H) ((f : (a : G) → H) x : H) n = 1 ↔ x ^ n = 1
Tactic: simp_rw [orderOf_eq_orderOf_iff, ← f.map_pow, ← f.map_one, hf.eq_iff, forall_const]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
H : Type u_6
inst_1 : Monoid H
f : G →* H
hf : Injective.{u_1 + 1, u_6 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
x : G
simp_rw : ∀ (n : ℕ), HPow.hPow (α := H) ((f : (a : G) → H) x : H) n = 1 ↔ x ^ n = 1
⊢ orderOf.{u_6} (G := H) ((f : (a : G) → H) x : H) = orderOf x
have simp_rw₁ : ∀ (n : ℕ), Eq.{u_6 + 1} (α := H) ((f : (a : G) → H) (x ^ n) : H) (1 : H) ↔ x ^ n = 1
Tactic: simp_rw [orderOf_eq_orderOf_iff, ← f.map_pow, ← f.map_one, hf.eq_iff, forall_const]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
H : Type u_6
inst_1 : Monoid H
f : G →* H
hf : Injective.{u_1 + 1, u_6 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
x : G
simp_rw : ∀ (n : ℕ), HPow.hPow (α := H) ((f : (a : G) → H) x : H) n = 1 ↔ x ^ n = 1
simp_rw₁ : ∀ (n : ℕ), Eq.{u_6 + 1} (α := H) ((f : (a : G) → H) (x ^ n) : H) (1 : H) ↔ x ^ n = 1
⊢ orderOf.{u_6} (G := H) ((f : (a : G) → H) x : H) = orderOf x
have simp_rw₂ : ∀ (n : ℕ), Eq.{u_6 + 1} (α := H) ((f : (a : G) → H) (x ^ n) : H) ((f : (a : G) → H) 1 : H) ↔ x ^ n = 1
Tactic: simp_rw [orderOf_eq_orderOf_iff, ← f.map_pow, ← f.map_one, hf.eq_iff, forall_const]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
H : Type u_6
inst_1 : Monoid H
f : G →* H
hf : Injective.{u_1 + 1, u_6 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
x : G
simp_rw : ∀ (n : ℕ), HPow.hPow (α := H) ((f : (a : G) → H) x : H) n = 1 ↔ x ^ n = 1
simp_rw₁ : ∀ (n : ℕ), Eq.{u_6 + 1} (α := H) ((f : (a : G) → H) (x ^ n) : H) (1 : H) ↔ x ^ n = 1
simp_rw₂ : ∀ (n : ℕ), Eq.{u_6 + 1} (α := H) ((f : (a : G) → H) (x ^ n) : H) ((f : (a : G) → H) 1 : H) ↔ x ^ n = 1
⊢ orderOf.{u_6} (G := H) ((f : (a : G) → H) x : H) = orderOf x
have simp_rw₃ : ∀ (n : ℕ), True
Tactic: simp_rw [orderOf_eq_orderOf_iff, ← f.map_pow, ← f.map_one, hf.eq_iff, forall_const]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Monoid G
x : G
inst_1 : Monoid H
f : G →* H
hf : Injective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
⊢ IsOfFinOrder.{u_2} (G := H) ((f : (a : G) → H) x : H) ↔ IsOfFinOrder x
have rw : 0 < orderOf.{u_2} (G := H) ((f : (a : G) → H) x : H) ↔ IsOfFinOrder x
Tactic: rw [← orderOf_pos_iff, orderOf_injective f hf x, ← orderOf_pos_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Monoid G
x : G
inst_1 : Monoid H
f : G →* H
hf : Injective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
rw : 0 < orderOf.{u_2} (G := H) ((f : (a : G) → H) x : H) ↔ IsOfFinOrder x
⊢ IsOfFinOrder.{u_2} (G := H) ((f : (a : G) → H) x : H) ↔ IsOfFinOrder x
have rw₁ : 0 < orderOf x ↔ IsOfFinOrder x
Tactic: rw [← orderOf_pos_iff, orderOf_injective f hf x, ← orderOf_pos_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Monoid G
x : G
inst_1 : Monoid H
f : G →* H
hf : Injective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
rw : 0 < orderOf.{u_2} (G := H) ((f : (a : G) → H) x : H) ↔ IsOfFinOrder x
rw₁ : 0 < orderOf x ↔ IsOfFinOrder x
⊢ IsOfFinOrder.{u_2} (G := H) ((f : (a : G) → H) x : H) ↔ IsOfFinOrder x
have rw₂ : 0 < orderOf x ↔ 0 < orderOf x
Tactic: rw [← orderOf_pos_iff, orderOf_injective f hf x, ← orderOf_pos_iff]
-- 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
⊢ x * x ^ (orderOf x - 1) = 1
have rw : x ^ (orderOf x - 1 + 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
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
⊢ x * x ^ (orderOf x - 1) = 1
have rw₁ : x ^ orderOf x = 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
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 * x ^ (orderOf x - 1) = 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
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
⊢ x ^ (orderOf x - 1) * x = 1
have rw : x ^ (orderOf x - 1 + 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
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
⊢ x ^ (orderOf x - 1) * x = 1
have rw₁ : x ^ orderOf x = 1
Tactic: rw [← _root_.pow_succ, tsub_add_cancel_of_le (by exact hx.orderOf_pos), pow_orderOf_eq_one]