case intro.intro
α : Type u_1
β : Type ?u.6665
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m ((f^[n]) x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
⊢ IsPeriodicPt f m x
α : Type u_1
β : Type ?u.6665
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hx : x ∈ periodicPts f
hm : IsPeriodicPt f m ((f^[n]) x)
⊢ IsPeriodicPt f m x
rcases hx with ⟨r, hr, hr'⟩
case intro.intro
α : Type u_1
β : Type ?u.6665
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m ((f^[n]) x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
⊢ n ≤ (n / r + 1) * r
case intro.intro
α : Type u_1
β : Type ?u.6665
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m ((f^[n]) x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
⊢ IsPeriodicPt f m x
suffices n ≤ (n / r + 1) * r by
  change _ = _
  convert (hm.apply_iterate ((n / r + 1) * r - n)).eq <;>
    rw [← iterate_add_apply, Nat.sub_add_cancel this, iterate_mul, (hr'.iterate _).eq]
case intro.intro
α : Type u_1
β : Type ?u.6665
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m ((f^[n]) x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
⊢ n ≤ n / r * r + r
case intro.intro
α : Type u_1
β : Type ?u.6665
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m ((f^[n]) x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
⊢ n ≤ (n / r + 1) * r
rw [add_mul, one_mul]
no goals
case intro.intro
α : Type u_1
β : Type ?u.6665
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m ((f^[n]) x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
⊢ n ≤ n / r * r + r
exact (Nat.lt_div_mul_add hr).le
α : Type u_1
β : Type ?u.6665
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m ((f^[n]) x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
this : n ≤ (n / r + 1) * r
⊢ (f^[m]) x = x
α : Type u_1
β : Type ?u.6665
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m ((f^[n]) x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
this : n ≤ (n / r + 1) * r
⊢ IsPeriodicPt f m x
change _ = _
no goals
α : Type u_1
β : Type ?u.6665
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hm : IsPeriodicPt f m ((f^[n]) x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
this : n ≤ (n / r + 1) * r
⊢ (f^[m]) x = x
convert (hm.apply_iterate ((n / r + 1) * r - n)).eq <;>
  rw [← iterate_add_apply, Nat.sub_add_cancel this, iterate_mul, (hr'.iterate _).eq]