case intro
G : Type u
A : Type v
y : G
a✝ b : A
n m : ℕ
inst✝² : Group G
inst✝¹ : AddGroup A
i : ℤ
α : Type u_1
inst✝ : MulAction G α
a : α
hs : y • a = a
k : ℤ
hx : y ^ k ∈ Subgroup.zpowers y
⊢ y ^ k • a = a
G : Type u
A : Type v
x y : G
a✝ b : A
n m : ℕ
inst✝² : Group G
inst✝¹ : AddGroup A
i : ℤ
α : Type u_1
inst✝ : MulAction G α
hx : x ∈ Subgroup.zpowers y
a : α
hs : y • a = a
⊢ x • a = a
obtain ⟨k, rfl⟩ := Subgroup.mem_zpowers_iff.mp hx
case intro
G : Type u
A : Type v
y : G
a✝ b : A
n m : ℕ
inst✝² : Group G
inst✝¹ : AddGroup A
i : ℤ
α : Type u_1
inst✝ : MulAction G α
a : α
hs : y • a = a
k : ℤ
hx : y ^ k ∈ Subgroup.zpowers y
⊢ ↑(MulAction.toPerm y ^ k) a = a
case intro
G : Type u
A : Type v
y : G
a✝ b : A
n m : ℕ
inst✝² : Group G
inst✝¹ : AddGroup A
i : ℤ
α : Type u_1
inst✝ : MulAction G α
a : α
hs : y • a = a
k : ℤ
hx : y ^ k ∈ Subgroup.zpowers y
⊢ y ^ k • a = a
rw [← MulAction.toPerm_apply, ← MulAction.toPermHom_apply, MonoidHom.map_zpow _ y k,
  MulAction.toPermHom_apply]
no goals
case intro
G : Type u
A : Type v
y : G
a✝ b : A
n m : ℕ
inst✝² : Group G
inst✝¹ : AddGroup A
i : ℤ
α : Type u_1
inst✝ : MulAction G α
a : α
hs : y • a = a
k : ℤ
hx : y ^ k ∈ Subgroup.zpowers y
⊢ ↑(MulAction.toPerm y ^ k) a = a
exact Function.IsFixedPt.perm_zpow (by exact hs) k
no goals
G : Type u
A : Type v
y : G
a✝ b : A
n m : ℕ
inst✝² : Group G
inst✝¹ : AddGroup A
i : ℤ
α : Type u_1
inst✝ : MulAction G α
a : α
hs : y • a = a
k : ℤ
hx : y ^ k ∈ Subgroup.zpowers y
⊢ IsFixedPt (↑(MulAction.toPerm y)) a
exact hs