α : Type u_1
β : Type ?u.36142
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ (∀ (n : ℕ), n < minimalPeriod f x → r ((f^[n]) x) ((f^[n + 1]) x)) ↔ ∀ (n : ℕ), r ((f^[n]) x) ((f^[n + 1]) x)
α : Type u_1
β : Type ?u.36142
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ (n : ℕ), r ((f^[n]) x) ((f^[n + 1]) x)
rw [periodicOrbit_chain r]
α : Type u_1
β : Type ?u.36142
f✝ fa : α → α
fb : β → β
x✝ y : α
m n✝ : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
H : ∀ (n : ℕ), n < minimalPeriod f x → r ((f^[n]) x) ((f^[n + 1]) x)
n : ℕ
⊢ r ((f^[n]) x) ((f^[n + 1]) x)
α : Type u_1
β : Type ?u.36142
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ (∀ (n : ℕ), n < minimalPeriod f x → r ((f^[n]) x) ((f^[n + 1]) x)) ↔ ∀ (n : ℕ), r ((f^[n]) x) ((f^[n + 1]) x)
refine' ⟨fun H n => _, fun H n _ => H n⟩
α : Type u_1
β : Type ?u.36142
f✝ fa : α → α
fb : β → β
x✝ y : α
m n✝ : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
H : ∀ (n : ℕ), n < minimalPeriod f x → r ((f^[n]) x) ((f^[n + 1]) x)
n : ℕ
⊢ r ((f^[n % minimalPeriod f x]) x) ((f^[succ (n % minimalPeriod f x)]) x)
α : Type u_1
β : Type ?u.36142
f✝ fa : α → α
fb : β → β
x✝ y : α
m n✝ : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
H : ∀ (n : ℕ), n < minimalPeriod f x → r ((f^[n]) x) ((f^[n + 1]) x)
n : ℕ
⊢ r ((f^[n]) x) ((f^[n + 1]) x)
rw [iterate_succ_apply, ← iterate_mod_minimalPeriod_eq, ← iterate_mod_minimalPeriod_eq (n := n),
  ← iterate_succ_apply, minimalPeriod_apply hx]
no goals
α : Type u_1
β : Type ?u.36142
f✝ fa : α → α
fb : β → β
x✝ y : α
m n✝ : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
H : ∀ (n : ℕ), n < minimalPeriod f x → r ((f^[n]) x) ((f^[n + 1]) x)
n : ℕ
⊢ r ((f^[n % minimalPeriod f x]) x) ((f^[succ (n % minimalPeriod f x)]) x)
exact H _ (mod_lt _ (minimalPeriod_pos_of_mem_periodicPts hx))