n : ℕ
A : Type ?u.232055
R : Type ?u.232058
inst✝³ : AddGroup A
inst✝² : Ring R
α : Type u_2
β : Type u_1
inst✝¹ : Group α
a : α
inst✝ : MulAction α β
b : β
k : ℤ
⊢ { val := a, property := (_ : a ∈ zpowers a) } ^ (k % ↑(minimalPeriod ((fun x x_1 => x • x_1) a) b)) •
      { val := b, property := (_ : b ∈ orbit { x // x ∈ zpowers a } b) } =
    { val := a, property := (_ : a ∈ zpowers a) } ^ k •
      { val := b, property := (_ : b ∈ orbit { x // x ∈ zpowers a } b) }
n : ℕ
A : Type ?u.232055
R : Type ?u.232058
inst✝³ : AddGroup A
inst✝² : Ring R
α : Type u_2
β : Type u_1
inst✝¹ : Group α
a : α
inst✝ : MulAction α β
b : β
k : ℤ
⊢ ↑(orbitZpowersEquiv a b).symm ↑k =
    { val := a, property := (_ : a ∈ zpowers a) } ^ k •
      { val := b, property := (_ : b ∈ orbit { x // x ∈ zpowers a } b) }
rw [orbitZpowersEquiv_symm_apply, ZMod.coe_int_cast]
no goals
n : ℕ
A : Type ?u.232055
R : Type ?u.232058
inst✝³ : AddGroup A
inst✝² : Ring R
α : Type u_2
β : Type u_1
inst✝¹ : Group α
a : α
inst✝ : MulAction α β
b : β
k : ℤ
⊢ { val := a, property := (_ : a ∈ zpowers a) } ^ (k % ↑(minimalPeriod ((fun x x_1 => x • x_1) a) b)) •
      { val := b, property := (_ : b ∈ orbit { x // x ∈ zpowers a } b) } =
    { val := a, property := (_ : a ∈ zpowers a) } ^ k •
      { val := b, property := (_ : b ∈ orbit { x // x ∈ zpowers a } b) }
exact Subtype.ext (zpow_smul_mod_minimalPeriod _ _ k)