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✝ : y ∈ Submonoid.powers x
n : ℕ
hn : (fun x x_1 => x ^ x_1) x n = y
⊢ (fun x x_1 => x ^ x_1) x ↑n = y
simp_all
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝² : Group G
inst✝¹ : AddGroup A
inst✝ : Finite G
x✝ : y ∈ zpowers x
i : ℤ
hi : (fun x x_1 => x ^ x_1) x i = y
⊢ x ^ Int.natAbs (i % ↑(orderOf x)) = y
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝² : Group G
inst✝¹ : AddGroup A
inst✝ : Finite G
x✝ : y ∈ zpowers x
i : ℤ
hi : (fun x x_1 => x ^ x_1) x i = y
⊢ (fun x x_1 => x ^ x_1) x (Int.natAbs (i % ↑(orderOf x))) = y
dsimp only
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✝ : y ∈ zpowers x
i : ℤ
hi : (fun x x_1 => x ^ x_1) x i = y
⊢ x ^ Int.natAbs (i % ↑(orderOf x)) = y
rwa [← zpow_ofNat,
  Int.natAbs_of_nonneg (Int.emod_nonneg _ (Int.coe_nat_ne_zero_iff_pos.2 (orderOf_pos x))), ←
  zpow_eq_mod_orderOf]