α : Type u_1
β : Type ?u.19001
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
f : α → α
x : α
⊢ IsPeriodicPt f (if h : x ∈ periodicPts f then Nat.find h else 0) x
α : Type u_1
β : Type ?u.19001
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
f : α → α
x : α
⊢ IsPeriodicPt f (minimalPeriod f x) x
delta minimalPeriod
case inl
α : Type u_1
β : Type ?u.19001
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ IsPeriodicPt f (Nat.find hx) x

case inr
α : Type u_1
β : Type ?u.19001
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
f : α → α
x : α
hx : ¬x ∈ periodicPts f
⊢ IsPeriodicPt f 0 x
α : Type u_1
β : Type ?u.19001
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
f : α → α
x : α
⊢ IsPeriodicPt f (if h : x ∈ periodicPts f then Nat.find h else 0) x
split_ifs with hx
no goals
case inl
α : Type u_1
β : Type ?u.19001
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ IsPeriodicPt f (Nat.find hx) x
exact (Nat.find_spec hx).2
no goals
case inr
α : Type u_1
β : Type ?u.19001
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
f : α → α
x : α
hx : ¬x ∈ periodicPts f
⊢ IsPeriodicPt f 0 x
exact isPeriodicPt_zero f x