have h2 : x ^ m = x ^ ((n : ℤ) * (m / (n : ℤ)) + m % (n : ℤ)) :=
  congr_arg (fun a => x ^ a) ((Int.add_comm _ _).trans (Int.emod_add_ediv _ _)).symm
L : Type u
inst✝¹ : Field L
n✝ : ℕ+
G : Type u_1
inst✝ : Group G
x : G
m : ℤ
n : ℕ
h : x ^ n = 1
⊢ x ^ m = x ^ (m % ↑n)
L : Type u
inst✝¹ : Field L
n✝ : ℕ+
G : Type u_1
inst✝ : Group G
x : G
m : ℤ
n : ℕ
h : x ^ n = 1
h2 : x ^ m = x ^ (↑n * (m / ↑n) + m % ↑n)
⊢ x ^ m = x ^ (m % ↑n)