no goals
G : Type u
A : Type v
x✝ y : G
a b : A
n✝ m : ℕ
inst✝² : LeftCancelMonoid G
inst✝¹ : AddLeftCancelMonoid A
inst✝ : Finite G
x : G
n : ℕ
hn : ∃ m, x ^ m = x ^ n
⊢ ↑(finEquivPowers x).symm { val := x ^ n, property := hn } =
    { val := n % orderOf x, isLt := (_ : n % orderOf x < orderOf x) }
rw [Equiv.symm_apply_eq, finEquivPowers_apply, Subtype.mk_eq_mk, pow_eq_mod_orderOf, Fin.val_mk]