G : Type u
A : Type v
x y : G
a b : A
n✝ m : ℕ
inst✝² : LeftCancelMonoid G
inst✝¹ : AddLeftCancelMonoid A
inst✝ : Finite G
h : orderOf x = orderOf y
n : ℕ
⊢ ↑(Fin.cast h).toEquiv { val := n % orderOf x, isLt := (_ : n % orderOf x < orderOf x) } =
    { val := n % orderOf y, isLt := (_ : n % orderOf y < orderOf y) }
G : Type u
A : Type v
x y : G
a b : A
n✝ m : ℕ
inst✝² : LeftCancelMonoid G
inst✝¹ : AddLeftCancelMonoid A
inst✝ : Finite G
h : orderOf x = orderOf y
n : ℕ
⊢ ↑(powersEquivPowers h) { val := x ^ n, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) x y = x ^ n) } =
    { val := y ^ n, property := (_ : ∃ y_1, (fun x x_1 => x ^ x_1) y y_1 = y ^ n) }
rw [powersEquivPowers, Equiv.trans_apply, Equiv.trans_apply, finEquivPowers_symm_apply, ←
  Equiv.eq_symm_apply, finEquivPowers_symm_apply]
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
h : orderOf x = orderOf y
n : ℕ
⊢ ↑(Fin.cast h).toEquiv { val := n % orderOf x, isLt := (_ : n % orderOf x < orderOf x) } =
    { val := n % orderOf y, isLt := (_ : n % orderOf y < orderOf y) }
simp [h]