α : Type u_1
β : Type ?u.23216
f fa : α → α
fb : β → β
x y : α
m n✝ : ℕ
hx : x ∈ periodicPts f
n : ℕ
⊢ IsPeriodicPt f (minimalPeriod f x) ((f^[n]) x)

α : Type u_1
β : Type ?u.23216
f fa : α → α
fb : β → β
x y : α
m n✝ : ℕ
hx : x ∈ periodicPts f
n : ℕ
⊢ (f^[n]) x ∈ periodicPts f
α : Type u_1
β : Type ?u.23216
f fa : α → α
fb : β → β
x y : α
m n✝ : ℕ
hx : x ∈ periodicPts f
n : ℕ
⊢ minimalPeriod f ((f^[n]) x) = minimalPeriod f x
apply
  (IsPeriodicPt.minimalPeriod_le (minimalPeriod_pos_of_mem_periodicPts hx) _).antisymm
    ((isPeriodicPt_of_mem_periodicPts_of_isPeriodicPt_iterate hx
          (isPeriodicPt_minimalPeriod f _)).minimalPeriod_le
      (minimalPeriod_pos_of_mem_periodicPts _))
no goals
α : Type u_1
β : Type ?u.23216
f fa : α → α
fb : β → β
x y : α
m n✝ : ℕ
hx : x ∈ periodicPts f
n : ℕ
⊢ IsPeriodicPt f (minimalPeriod f x) ((f^[n]) x)
exact (isPeriodicPt_minimalPeriod f x).apply_iterate n
case intro.intro
α : Type u_1
β : Type ?u.23216
f fa : α → α
fb : β → β
x y : α
m✝ n✝ n m : ℕ
hm : m > 0
hx : IsPeriodicPt f m x
⊢ (f^[n]) x ∈ periodicPts f
α : Type u_1
β : Type ?u.23216
f fa : α → α
fb : β → β
x y : α
m n✝ : ℕ
hx : x ∈ periodicPts f
n : ℕ
⊢ (f^[n]) x ∈ periodicPts f
rcases hx with ⟨m, hm, hx⟩
no goals
case intro.intro
α : Type u_1
β : Type ?u.23216
f fa : α → α
fb : β → β
x y : α
m✝ n✝ n m : ℕ
hm : m > 0
hx : IsPeriodicPt f m x
⊢ (f^[n]) x ∈ periodicPts f
exact ⟨m, hm, hx.apply_iterate n⟩