G : Type u
A : Type v
x✝ y : G
a b : A
n✝ m : ℕ
inst✝² : Group G
inst✝¹ : AddGroup A
inst✝ : Finite G
x : G
n : ℕ
hn : ∃ m, x ^ m = x ^ n
⊢ ↑(finEquivPowers x).symm
      (↑(Equiv.Set.ofEq (_ : ↑(Submonoid.powers x) = ↑(zpowers x))).symm { val := x ^ n, property := hn }) =
    { val := n % orderOf x, isLt := (_ : n % orderOf x < orderOf x) }
G : Type u
A : Type v
x✝ y : G
a b : A
n✝ m : ℕ
inst✝² : Group G
inst✝¹ : AddGroup A
inst✝ : Finite G
x : G
n : ℕ
hn : ∃ m, x ^ m = x ^ n
⊢ ↑(finEquivZpowers x).symm { val := x ^ n, property := hn } =
    { val := n % orderOf x, isLt := (_ : n % orderOf x < orderOf x) }
rw [finEquivZpowers, Equiv.symm_trans_apply]
no goals
G : Type u
A : Type v
x✝ y : G
a b : A
n✝ m : ℕ
inst✝² : Group G
inst✝¹ : AddGroup A
inst✝ : Finite G
x : G
n : ℕ
hn : ∃ m, x ^ m = x ^ n
⊢ ↑(finEquivPowers x).symm
      (↑(Equiv.Set.ofEq (_ : ↑(Submonoid.powers x) = ↑(zpowers x))).symm { val := x ^ n, property := hn }) =
    { val := n % orderOf x, isLt := (_ : n % orderOf x < orderOf x) }
exact finEquivPowers_symm_apply x n