α : Type u_1
β : Type ?u.32376
f fa : α → α
fb : β → β
x y : α
m n✝ : ℕ
hx : x ∈ periodicPts f
n : ℕ
⊢ List.length (List.rotate (List.map (fun n => (f^[n]) x) (List.range (minimalPeriod f x))) n) =
    List.length (List.map (fun n_1 => (f^[n_1]) ((f^[n]) x)) (List.range (minimalPeriod f ((f^[n]) x))))

α : Type u_1
β : Type ?u.32376
f fa : α → α
fb : β → β
x y : α
m n✝ : ℕ
hx : x ∈ periodicPts f
n : ℕ
⊢ ∀ (m : ℕ) (x_1 : m < List.length (List.rotate (List.map (fun n => (f^[n]) x) (List.range (minimalPeriod f x))) n))
    (x_2 : m < List.length (List.map (fun n_1 => (f^[n_1]) ((f^[n]) x)) (List.range (minimalPeriod f ((f^[n]) x))))),
    List.nthLe (List.rotate (List.map (fun n => (f^[n]) x) (List.range (minimalPeriod f x))) n) m x_1 =
      List.nthLe (List.map (fun n_1 => (f^[n_1]) ((f^[n]) x)) (List.range (minimalPeriod f ((f^[n]) x)))) m x_2
α : Type u_1
β : Type ?u.32376
f fa : α → α
fb : β → β
x y : α
m n✝ : ℕ
hx : x ∈ periodicPts f
n : ℕ
⊢ List.rotate (List.map (fun n => (f^[n]) x) (List.range (minimalPeriod f x))) n =
    List.map (fun n_1 => (f^[n_1]) ((f^[n]) x)) (List.range (minimalPeriod f ((f^[n]) x)))
apply List.ext_nthLe _ fun m _ _ => _
no goals
α : Type u_1
β : Type ?u.32376
f fa : α → α
fb : β → β
x y : α
m n✝ : ℕ
hx : x ∈ periodicPts f
n : ℕ
⊢ List.length (List.rotate (List.map (fun n => (f^[n]) x) (List.range (minimalPeriod f x))) n) =
    List.length (List.map (fun n_1 => (f^[n_1]) ((f^[n]) x)) (List.range (minimalPeriod f ((f^[n]) x))))
simp [minimalPeriod_apply_iterate hx]
no goals
α : Type u_1
β : Type ?u.32376
f fa : α → α
fb : β → β
x y : α
m n✝ : ℕ
hx : x ∈ periodicPts f
n : ℕ
⊢ ∀ (m : ℕ) (x_1 : m < List.length (List.rotate (List.map (fun n => (f^[n]) x) (List.range (minimalPeriod f x))) n))
    (x_2 : m < List.length (List.map (fun n_1 => (f^[n_1]) ((f^[n]) x)) (List.range (minimalPeriod f ((f^[n]) x))))),
    List.nthLe (List.rotate (List.map (fun n => (f^[n]) x) (List.range (minimalPeriod f x))) n) m x_1 =
      List.nthLe (List.map (fun n_1 => (f^[n_1]) ((f^[n]) x)) (List.range (minimalPeriod f ((f^[n]) x)))) m x_2
simp [List.nthLe_rotate, iterate_add_apply]