-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem pow_mul_pow_lcm {ζ' : M} {k' : ℕ} (hζ : IsPrimitiveRoot ζ k) (hζ' : IsPrimitiveRoot ζ' k')
    (hk : k ≠ 0) (hk' : k' ≠ 0) :
    IsPrimitiveRoot
      (ζ ^ (k / Nat.factorizationLCMLeft k k') * ζ' ^ (k' / Nat.factorizationLCMRight k k'))
      (Nat.lcm k k')

Proof state:
case h.e'_3.h.e'_3
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ ζ' : M
k' : ℕ
hζ : IsPrimitiveRoot ζ k
hζ' : IsPrimitiveRoot ζ' k'
hk : k ≠ 0
hk' : k' ≠ 0
⊢ ζ ^ (k / k.factorizationLCMLeft k') * ζ' ^ (k' / k.factorizationLCMRight k') =
    ζ ^ (orderOf ζ / (orderOf ζ).factorizationLCMLeft (orderOf ζ')) *
      ζ' ^ (orderOf ζ' / (orderOf ζ).factorizationLCMRight (orderOf ζ'))

Tactic:
simp [hζ.eq_orderOf, hζ'.eq_orderOf]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ ζ' : M
k' : ℕ
hζ : IsPrimitiveRoot ζ k
hζ' : IsPrimitiveRoot ζ' k'
hk : k ≠ 0
hk' : k' ≠ 0
⊢ orderOf ζ ≠ 0

Tactic:
simpa [← hζ.eq_orderOf]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ ζ' : M
k' : ℕ
hζ : IsPrimitiveRoot ζ k
hζ' : IsPrimitiveRoot ζ' k'
hk : k ≠ 0
hk' : k' ≠ 0
⊢ orderOf ζ' ≠ 0

Tactic:
simpa [← hζ'.eq_orderOf]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ ζ' : M
k' : ℕ
hζ : IsPrimitiveRoot ζ k
hζ' : IsPrimitiveRoot ζ' k'
hk : k ≠ 0
hk' : k' ≠ 0
⊢ IsPrimitiveRoot (ζ ^ (k / k.factorizationLCMLeft k') * ζ' ^ (k' / k.factorizationLCMRight k')) (k.lcm k')

Tactic:
convert IsPrimitiveRoot.orderOf _

Result:
case h.e'_1
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ ζ' : M
k' : ℕ
hζ : IsPrimitiveRoot ζ k
hζ' : IsPrimitiveRoot ζ' k'
hk : k ≠ 0
hk' : k' ≠ 0
⊢ k.lcm k' = orderOf (ζ ^ (k / k.factorizationLCMLeft k') * ζ' ^ (k' / k.factorizationLCMRight k'))

Proof state:
case h.e'_1
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ ζ' : M
k' : ℕ
hζ : IsPrimitiveRoot ζ k
hζ' : IsPrimitiveRoot ζ' k'
hk : k ≠ 0
hk' : k' ≠ 0
⊢ k.lcm k' = orderOf (ζ ^ (k / k.factorizationLCMLeft k') * ζ' ^ (k' / k.factorizationLCMRight k'))

Tactic:
convert ((Commute.all ζ ζ').orderOf_mul_pow_eq_lcm
  (by simpa [← hζ.eq_orderOf]) (by simpa [← hζ'.eq_orderOf])).symm using 2

Result:
case h.e'_2.h.e'_1
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ ζ' : M
k' : ℕ
hζ : IsPrimitiveRoot ζ k
hζ' : IsPrimitiveRoot ζ' k'
hk : k ≠ 0
hk' : k' ≠ 0
⊢ k = orderOf ζ

case h.e'_2.h.e'_2
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ ζ' : M
k' : ℕ
hζ : IsPrimitiveRoot ζ k
hζ' : IsPrimitiveRoot ζ' k'
hk : k ≠ 0
hk' : k' ≠ 0
⊢ k' = orderOf ζ'

case h.e'_3.h.e'_3
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ ζ' : M
k' : ℕ
hζ : IsPrimitiveRoot ζ k
hζ' : IsPrimitiveRoot ζ' k'
hk : k ≠ 0
hk' : k' ≠ 0
⊢ ζ ^ (k / k.factorizationLCMLeft k') * ζ' ^ (k' / k.factorizationLCMRight k') =
    ζ ^ (orderOf ζ / (orderOf ζ).factorizationLCMLeft (orderOf ζ')) *
      ζ' ^ (orderOf ζ' / (orderOf ζ).factorizationLCMRight (orderOf ζ'))

Proof state:
case h.e'_2.h.e'_1
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ ζ' : M
k' : ℕ
hζ : IsPrimitiveRoot ζ k
hζ' : IsPrimitiveRoot ζ' k'
hk : k ≠ 0
hk' : k' ≠ 0
⊢ k = orderOf ζ

case h.e'_2.h.e'_2
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ ζ' : M
k' : ℕ
hζ : IsPrimitiveRoot ζ k
hζ' : IsPrimitiveRoot ζ' k'
hk : k ≠ 0
hk' : k' ≠ 0
⊢ k' = orderOf ζ'

case h.e'_3.h.e'_3
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ ζ' : M
k' : ℕ
hζ : IsPrimitiveRoot ζ k
hζ' : IsPrimitiveRoot ζ' k'
hk : k ≠ 0
hk' : k' ≠ 0
⊢ ζ ^ (k / k.factorizationLCMLeft k') * ζ' ^ (k' / k.factorizationLCMRight k') =
    ζ ^ (orderOf ζ / (orderOf ζ).factorizationLCMLeft (orderOf ζ')) *
      ζ' ^ (orderOf ζ' / (orderOf ζ).factorizationLCMRight (orderOf ζ'))

Tactic:
all_goals simp [hζ.eq_orderOf, hζ'.eq_orderOf]

Result:
no goals