-- Mathlib/GroupTheory/Exponent.lean
/-- If two commuting elements `x` and `y` of a monoid have order `n` and `m`, there is an element
of order `lcm n m`. The result actually gives an explicit (computable) element, written as the
product of a power of `x` and a power of `y`. See also the result below if you don't need the
explicit formula. -/
@[to_additive "If two commuting elements `x` and `y` of an additive monoid have order `n` and `m`,
there is an element of order `lcm n m`. The result actually gives an explicit (computable) element,
written as the sum of a multiple of `x` and a multiple of `y`. See also the result below if you
don't need the explicit formula."]
lemma _root_.Commute.orderOf_mul_pow_eq_lcm {x y : G} (h : Commute x y) (hx : orderOf x ≠ 0)
    (hy : orderOf y ≠ 0) :
    orderOf (x ^ (orderOf x / (factorizationLCMLeft (orderOf x) (orderOf y))) *
      y ^ (orderOf y / factorizationLCMRight (orderOf x) (orderOf y))) =
      Nat.lcm (orderOf x) (orderOf y)

Proof state:
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)).Coprime
    (orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))))

case hx
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ orderOf x ≠ 0

case hn
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 x

Tactic:
try rw [Coprime]

Result:
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

case hx
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ orderOf x ≠ 0

case hn
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 x

Proof state:
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)).Coprime
    (orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))))

case hx
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ orderOf x ≠ 0

case hn
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 x

Tactic:
rw [Coprime]

Result:
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

case hx
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ orderOf x ≠ 0

case hn
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 x

Proof state:
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

case hx
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ orderOf x ≠ 0

case hn
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 x

Tactic:
rw [orderOf_pow_orderOf_div]

Result:
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 x).factorizationLCMRight (orderOf y)) = 1

case hx
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ orderOf y ≠ 0

case hn
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ (orderOf x).factorizationLCMRight (orderOf y) ∣ orderOf y

case hx
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ orderOf x ≠ 0

case hn
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 x