simp_rw [Function.periodicPts, Function.IsPeriodicPt, Function.IsFixedPt] at hper
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
hper : Function.periodicPts f = ∅
eq : f^[n] x = x
⊢ n = 0
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
hper : {x | ∃ n > 0, f^[n] x = x} = ∅
eq : f^[n] x = x
⊢ n = 0