awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k
t : ℕ
ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ
⊢ orderOf (g ^ k) = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
have inr : orderOf (g ^ k) = p ^ t.succ
Tactic: rw [ht]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k
t : ℕ
ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ
⊢ orderOf (g ^ k) = p ^ t.succ
have inr : ¬(g ^ k) ^ p ^ t = 1
Tactic: apply orderOf_eq_prime_pow
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k
t : ℕ
ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ
inr : ¬(g ^ k) ^ p ^ t = 1
⊢ orderOf (g ^ k) = p ^ t.succ
have inr₁ : (g ^ k) ^ p ^ (t + 1) = 1
Tactic: apply orderOf_eq_prime_pow
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k
t : ℕ
ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ
⊢ ¬(g ^ k) ^ p ^ t = 1
have inr : ∀ (hg : g ^ (HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k / p) ≠ 1)
  (hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k) (t : ℕ)
  (ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ), ¬(g ^ k) ^ p ^ t = 1
Tactic: rwa [hk, mul_comm, ht, pow_succ, ← mul_assoc, Nat.mul_div_cancel _ hp.pos, pow_mul] at hg
Cleared hypotheses: hg, hk, t, ht
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k
t : ℕ
ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ
inr :
  ∀ (hg : g ^ (HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k / p) ≠ 1)
    (hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k) (t : ℕ)
    (ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ), ¬(g ^ k) ^ p ^ t = 1
⊢ ¬(g ^ k) ^ p ^ t = 1
have inr₁ : ∀ (hg : g ^ (k * HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) / p) ≠ 1)
  (hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k) (t : ℕ)
  (ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ), ¬(g ^ k) ^ p ^ t = 1
Tactic: rwa [hk, mul_comm, ht, pow_succ, ← mul_assoc, Nat.mul_div_cancel _ hp.pos, pow_mul] at hg
Cleared hypotheses: hg, hk, t, ht
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k
t : ℕ
ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ
inr :
  ∀ (hg : g ^ (HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k / p) ≠ 1)
    (hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k) (t : ℕ)
    (ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ), ¬(g ^ k) ^ p ^ t = 1
inr₁ :
  ∀ (hg : g ^ (k * HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) / p) ≠ 1)
    (hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k) (t : ℕ)
    (ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ), ¬(g ^ k) ^ p ^ t = 1
⊢ ¬(g ^ k) ^ p ^ t = 1
have inr₂ : ∀ (hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k) (t : ℕ)
  (hg : g ^ (k * p ^ t.succ / p) ≠ 1) (ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ), ¬(g ^ k) ^ p ^ t = 1
Tactic: rwa [hk, mul_comm, ht, pow_succ, ← mul_assoc, Nat.mul_div_cancel _ hp.pos, pow_mul] at hg
Cleared hypotheses: hg, hk, t, ht
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k
t : ℕ
ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ
inr :
  ∀ (hg : g ^ (HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k / p) ≠ 1)
    (hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k) (t : ℕ)
    (ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ), ¬(g ^ k) ^ p ^ t = 1
inr₁ :
  ∀ (hg : g ^ (k * HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) / p) ≠ 1)
    (hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k) (t : ℕ)
    (ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ), ¬(g ^ k) ^ p ^ t = 1
inr₂ :
  ∀ (hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k) (t : ℕ)
    (hg : g ^ (k * p ^ t.succ / p) ≠ 1) (ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ),
    ¬(g ^ k) ^ p ^ t = 1
⊢ ¬(g ^ k) ^ p ^ t = 1
have inr₃ : ∀ (hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k) (t : ℕ)
  (hg : g ^ (k * (p ^ t * p) / p) ≠ 1) (ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ),
  ¬(g ^ k) ^ p ^ t = 1
Tactic: rwa [hk, mul_comm, ht, pow_succ, ← mul_assoc, Nat.mul_div_cancel _ hp.pos, pow_mul] at hg
Cleared hypotheses: hg, hk, t, ht
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k
t : ℕ
ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ
inr :
  ∀ (hg : g ^ (HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k / p) ≠ 1)
    (hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k) (t : ℕ)
    (ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ), ¬(g ^ k) ^ p ^ t = 1
inr₁ :
  ∀ (hg : g ^ (k * HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) / p) ≠ 1)
    (hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k) (t : ℕ)
    (ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ), ¬(g ^ k) ^ p ^ t = 1
inr₂ :
  ∀ (hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k) (t : ℕ)
    (hg : g ^ (k * p ^ t.succ / p) ≠ 1) (ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ),
    ¬(g ^ k) ^ p ^ t = 1
inr₃ :
  ∀ (hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k) (t : ℕ)
    (hg : g ^ (k * (p ^ t * p) / p) ≠ 1) (ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ),
    ¬(g ^ k) ^ p ^ t = 1
⊢ ¬(g ^ k) ^ p ^ t = 1
have inr₄ : ∀ (hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k) (t : ℕ)
  (hg : g ^ (k * p ^ t * p / p) ≠ 1) (ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ), ¬(g ^ k) ^ p ^ t = 1
Tactic: rwa [hk, mul_comm, ht, pow_succ, ← mul_assoc, Nat.mul_div_cancel _ hp.pos, pow_mul] at hg
Cleared hypotheses: hg, hk, t, ht
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k
t : ℕ
ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ
inr :
  ∀ (hg : g ^ (HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k / p) ≠ 1)
    (hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k) (t : ℕ)
    (ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ), ¬(g ^ k) ^ p ^ t = 1
inr₁ :
  ∀ (hg : g ^ (k * HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) / p) ≠ 1)
    (hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k) (t : ℕ)
    (ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ), ¬(g ^ k) ^ p ^ t = 1
inr₂ :
  ∀ (hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k) (t : ℕ)
    (hg : g ^ (k * p ^ t.succ / p) ≠ 1) (ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ),
    ¬(g ^ k) ^ p ^ t = 1
inr₃ :
  ∀ (hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k) (t : ℕ)
    (hg : g ^ (k * (p ^ t * p) / p) ≠ 1) (ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ),
    ¬(g ^ k) ^ p ^ t = 1
inr₄ :
  ∀ (hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k) (t : ℕ)
    (hg : g ^ (k * p ^ t * p / p) ≠ 1) (ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ),
    ¬(g ^ k) ^ p ^ t = 1
⊢ ¬(g ^ k) ^ p ^ t = 1
have inr₅ : ∀ (hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k) (t : ℕ)
  (hg : g ^ (k * p ^ t) ≠ 1) (ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ), ¬(g ^ k) ^ p ^ t = 1
Tactic: rwa [hk, mul_comm, ht, pow_succ, ← mul_assoc, Nat.mul_div_cancel _ hp.pos, pow_mul] at hg
Cleared hypotheses: hg, hk, t, ht
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k
t : ℕ
ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ
inr :
  ∀ (hg : g ^ (HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k / p) ≠ 1)
    (hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k) (t : ℕ)
    (ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ), ¬(g ^ k) ^ p ^ t = 1
inr₁ :
  ∀ (hg : g ^ (k * HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) / p) ≠ 1)
    (hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k) (t : ℕ)
    (ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ), ¬(g ^ k) ^ p ^ t = 1
inr₂ :
  ∀ (hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k) (t : ℕ)
    (hg : g ^ (k * p ^ t.succ / p) ≠ 1) (ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ),
    ¬(g ^ k) ^ p ^ t = 1
inr₃ :
  ∀ (hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k) (t : ℕ)
    (hg : g ^ (k * (p ^ t * p) / p) ≠ 1) (ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ),
    ¬(g ^ k) ^ p ^ t = 1
inr₄ :
  ∀ (hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k) (t : ℕ)
    (hg : g ^ (k * p ^ t * p / p) ≠ 1) (ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ),
    ¬(g ^ k) ^ p ^ t = 1
inr₅ :
  ∀ (hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k) (t : ℕ)
    (hg : g ^ (k * p ^ t) ≠ 1) (ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ), ¬(g ^ k) ^ p ^ t = 1
⊢ ¬(g ^ k) ^ p ^ t = 1
have inr₆ : ∀ (hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k) (t : ℕ)
  (hg : (g ^ k) ^ p ^ t ≠ 1) (ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ), ¬(g ^ k) ^ p ^ t = 1
Tactic: rwa [hk, mul_comm, ht, pow_succ, ← mul_assoc, Nat.mul_div_cancel _ hp.pos, pow_mul] at hg
Cleared hypotheses: hg, hk, t, ht
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k
t : ℕ
ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ
⊢ (g ^ k) ^ p ^ (t + 1) = 1
have inr : g ^ exponent G = 1
Tactic: rw [← Nat.succ_eq_add_one, ← ht, ← pow_mul, mul_comm, ← hk]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ orderOf
      (x ^ (orderOf x / (orderOf x).factorizationLCMLeft (orderOf y)) *
        y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))) =
    (orderOf x).lcm (orderOf y)
have rw : orderOf (x ^ (orderOf x / (orderOf x).factorizationLCMLeft (orderOf y))) *
    orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))) =
  (orderOf x).lcm (orderOf y)
Tactic: rw [(h.pow_pow _ _).orderOf_mul_eq_mul_orderOf_of_coprime]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
rw :
  orderOf (x ^ (orderOf x / (orderOf x).factorizationLCMLeft (orderOf y))) *
      orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))) =
    (orderOf x).lcm (orderOf y)
⊢ orderOf
      (x ^ (orderOf x / (orderOf x).factorizationLCMLeft (orderOf y)) *
        y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))) =
    (orderOf x).lcm (orderOf y)
have rw₁ : (orderOf (x ^ (orderOf x / (orderOf x).factorizationLCMLeft (orderOf y)))).Coprime
  (orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))))
Tactic: rw [(h.pow_pow _ _).orderOf_mul_eq_mul_orderOf_of_coprime]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ orderOf (x ^ (orderOf x / (orderOf x).factorizationLCMLeft (orderOf y))) *
      orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))) =
    (orderOf x).lcm (orderOf y)
have rw : (orderOf x).factorizationLCMLeft (orderOf y) *
    orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))) =
  (orderOf x).lcm (orderOf y)
Tactic: rw [orderOf_pow_orderOf_div]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
rw :
  (orderOf x).factorizationLCMLeft (orderOf y) *
      orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))) =
    (orderOf x).lcm (orderOf y)
hx₁ : orderOf x ≠ 0
⊢ orderOf (x ^ (orderOf x / (orderOf x).factorizationLCMLeft (orderOf y))) *
      orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))) =
    (orderOf x).lcm (orderOf y)
have hn : (orderOf x).factorizationLCMLeft (orderOf y) ∣ orderOf x
Tactic: rw [orderOf_pow_orderOf_div]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ (orderOf x).factorizationLCMLeft (orderOf y) *
      orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))) =
    (orderOf x).lcm (orderOf y)
have rw : (orderOf x).factorizationLCMLeft (orderOf y) * (orderOf x).factorizationLCMRight (orderOf y) =
  (orderOf x).lcm (orderOf y)
Tactic: rw [orderOf_pow_orderOf_div]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
rw :
  (orderOf x).factorizationLCMLeft (orderOf y) * (orderOf x).factorizationLCMRight (orderOf y) =
    (orderOf x).lcm (orderOf y)
hx₁ : orderOf y ≠ 0
⊢ (orderOf x).factorizationLCMLeft (orderOf y) *
      orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))) =
    (orderOf x).lcm (orderOf y)
have hn : (orderOf x).factorizationLCMRight (orderOf y) ∣ orderOf y
Tactic: rw [orderOf_pow_orderOf_div]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ orderOf (x ^ (orderOf x / (orderOf x).factorizationLCMLeft (orderOf y))) *
      orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))) =
    (orderOf x).lcm (orderOf y)
have iterate : (orderOf x).factorizationLCMLeft (orderOf y) * (orderOf x).factorizationLCMRight (orderOf y) =
  (orderOf x).lcm (orderOf y)
Tactic: iterate 2 rw [orderOf_pow_orderOf_div]; try rw [Coprime]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
iterate :
  (orderOf x).factorizationLCMLeft (orderOf y) * (orderOf x).factorizationLCMRight (orderOf y) =
    (orderOf x).lcm (orderOf y)
hx₁ : orderOf y ≠ 0
⊢ orderOf (x ^ (orderOf x / (orderOf x).factorizationLCMLeft (orderOf y))) *
      orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))) =
    (orderOf x).lcm (orderOf y)
have hn : (orderOf x).factorizationLCMRight (orderOf y) ∣ orderOf y
Tactic: iterate 2 rw [orderOf_pow_orderOf_div]; try rw [Coprime]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
iterate :
  (orderOf x).factorizationLCMLeft (orderOf y) * (orderOf x).factorizationLCMRight (orderOf y) =
    (orderOf x).lcm (orderOf y)
hx₁ : orderOf y ≠ 0
hn : (orderOf x).factorizationLCMRight (orderOf y) ∣ orderOf y
hx₂ : orderOf x ≠ 0
⊢ orderOf (x ^ (orderOf x / (orderOf x).factorizationLCMLeft (orderOf y))) *
      orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))) =
    (orderOf x).lcm (orderOf y)
have hn₁ : (orderOf x).factorizationLCMLeft (orderOf y) ∣ orderOf x
Tactic: iterate 2 rw [orderOf_pow_orderOf_div]; try rw [Coprime]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ (orderOf (x ^ (orderOf x / (orderOf x).factorizationLCMLeft (orderOf y)))).Coprime
    (orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))))
have rw : ((orderOf x).factorizationLCMLeft (orderOf y)).Coprime
  (orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))))
Tactic: rw [orderOf_pow_orderOf_div]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
rw :
  ((orderOf x).factorizationLCMLeft (orderOf y)).Coprime
    (orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))))
hx₁ : orderOf x ≠ 0
⊢ (orderOf (x ^ (orderOf x / (orderOf x).factorizationLCMLeft (orderOf y)))).Coprime
    (orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))))
have hn : (orderOf x).factorizationLCMLeft (orderOf y) ∣ orderOf x
Tactic: rw [orderOf_pow_orderOf_div]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ ((orderOf x).factorizationLCMLeft (orderOf y)).gcd
      (orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y)))) =
    1
have rw : ((orderOf x).factorizationLCMLeft (orderOf y)).gcd ((orderOf x).factorizationLCMRight (orderOf y)) = 1
Tactic: rw [orderOf_pow_orderOf_div]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
rw : ((orderOf x).factorizationLCMLeft (orderOf y)).gcd ((orderOf x).factorizationLCMRight (orderOf y)) = 1
hx₁ : orderOf y ≠ 0
⊢ ((orderOf x).factorizationLCMLeft (orderOf y)).gcd
      (orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y)))) =
    1
have hn : (orderOf x).factorizationLCMRight (orderOf y) ∣ orderOf y
Tactic: rw [orderOf_pow_orderOf_div]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ (orderOf (x ^ (orderOf x / (orderOf x).factorizationLCMLeft (orderOf y)))).Coprime
    (orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))))
have iterate : ((orderOf x).factorizationLCMLeft (orderOf y)).gcd ((orderOf x).factorizationLCMRight (orderOf y)) = 1
Tactic: iterate 2 rw [orderOf_pow_orderOf_div]; try rw [Coprime]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
iterate : ((orderOf x).factorizationLCMLeft (orderOf y)).gcd ((orderOf x).factorizationLCMRight (orderOf y)) = 1
hx₁ : orderOf y ≠ 0
⊢ (orderOf (x ^ (orderOf x / (orderOf x).factorizationLCMLeft (orderOf y)))).Coprime
    (orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))))
have hn : (orderOf x).factorizationLCMRight (orderOf y) ∣ orderOf y
Tactic: iterate 2 rw [orderOf_pow_orderOf_div]; try rw [Coprime]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
iterate : ((orderOf x).factorizationLCMLeft (orderOf y)).gcd ((orderOf x).factorizationLCMRight (orderOf y)) = 1
hx₁ : orderOf y ≠ 0
hn : (orderOf x).factorizationLCMRight (orderOf y) ∣ orderOf y
hx₂ : orderOf x ≠ 0
⊢ (orderOf (x ^ (orderOf x / (orderOf x).factorizationLCMLeft (orderOf y)))).Coprime
    (orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))))
have hn₁ : (orderOf x).factorizationLCMLeft (orderOf y) ∣ orderOf x
Tactic: iterate 2 rw [orderOf_pow_orderOf_div]; try rw [Coprime]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
⊢ ∃ (z : G), Membership.mem (γ := Submonoid G) (closure {x, y}) z ∧ orderOf z = (orderOf x).lcm (orderOf y)
have pos : ∀ (hx : orderOf x = 0),
  ∃ (z : G), Membership.mem (γ := Submonoid G) (closure {x, y}) z ∧ orderOf z = (orderOf x).lcm (orderOf y)
Tactic: by_cases hx : orderOf x = 0
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
pos :
  ∀ (hx : orderOf x = 0),
    ∃ (z : G), Membership.mem (γ := Submonoid G) (closure {x, y}) z ∧ orderOf z = (orderOf x).lcm (orderOf y)
⊢ ∃ (z : G), Membership.mem (γ := Submonoid G) (closure {x, y}) z ∧ orderOf z = (orderOf x).lcm (orderOf y)
have neg : ∀ (hx : ¬orderOf x = 0),
  ∃ (z : G), Membership.mem (γ := Submonoid G) (closure {x, y}) z ∧ orderOf z = (orderOf x).lcm (orderOf y)
Tactic: by_cases hx : orderOf x = 0
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : orderOf x = 0
⊢ ∃ (z : G), Membership.mem (γ := Submonoid G) (closure {x, y}) z ∧ orderOf z = (orderOf x).lcm (orderOf y)
have pos : ∀ (hy : orderOf y = 0),
  ∃ (z : G), Membership.mem (γ := Submonoid G) (closure {x, y}) z ∧ orderOf z = (orderOf x).lcm (orderOf y)
Tactic: by_cases hy : orderOf y = 0