Theorem: IMOSL.IMO2006A1.floor_f_iter_natAbs_eventually_const (IMOSLLean4/IMO2006/A1/A1.lean)

State before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
⊢ ∃ C, EventuallyEqual (fun x => ⌊f^[x] r⌋.natAbs) fun x => C
Tactic:
have ha : Antitone (λ k ↦ ⌊f^[k] r⌋.natAbs) := λ k m h0 ↦ by
  rcases Nat.exists_eq_add_of_le h0 with ⟨c, rfl⟩; simp only
  rw [Nat.add_comm, f.iterate_add_apply]
  exact floor_f_iter_natAbs_le _ c
State after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
ha : Antitone fun k => ⌊f^[k] r⌋.natAbs
⊢ ∃ C, EventuallyEqual (fun x => ⌊f^[x] r⌋.natAbs) fun x => C

State before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
ha : Antitone fun k => ⌊f^[k] r⌋.natAbs
⊢ ∃ C, EventuallyEqual (fun x => ⌊f^[x] r⌋.natAbs) fun x => C
Tactic:
rcases NatSeq_antitone_imp_const ha with ⟨C, N, ha⟩
State after:
case intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
ha✝ : Antitone fun k => ⌊f^[k] r⌋.natAbs
C N : ℕ
ha : ∀ (n : ℕ), ⌊f^[n + N] r⌋.natAbs = C
⊢ ∃ C, EventuallyEqual (fun x => ⌊f^[x] r⌋.natAbs) fun x => C

State before:
case intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
ha✝ : Antitone fun k => ⌊f^[k] r⌋.natAbs
C N : ℕ
ha : ∀ (n : ℕ), ⌊f^[n + N] r⌋.natAbs = C
⊢ ∃ C, EventuallyEqual (fun x => ⌊f^[x] r⌋.natAbs) fun x => C
Tactic:
exact ⟨C, N, 0, ha⟩
State after:
no goals

State before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
k m : ℕ
h0 : k ≤ m
⊢ (fun k => ⌊f^[k] r⌋.natAbs) m ≤ (fun k => ⌊f^[k] r⌋.natAbs) k
Tactic:
rcases Nat.exists_eq_add_of_le h0 with ⟨c, rfl⟩
State after:
case intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
k c : ℕ
h0 : k ≤ k + c
⊢ (fun k => ⌊f^[k] r⌋.natAbs) (k + c) ≤ (fun k => ⌊f^[k] r⌋.natAbs) k

State before:
case intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
k c : ℕ
h0 : k ≤ k + c
⊢ (fun k => ⌊f^[k] r⌋.natAbs) (k + c) ≤ (fun k => ⌊f^[k] r⌋.natAbs) k
Tactic:
simp only
State after:
case intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
k c : ℕ
h0 : k ≤ k + c
⊢ ⌊f^[k + c] r⌋.natAbs ≤ ⌊f^[k] r⌋.natAbs

State before:
case intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
k c : ℕ
h0 : k ≤ k + c
⊢ ⌊f^[k + c] r⌋.natAbs ≤ ⌊f^[k] r⌋.natAbs
Tactic:
rw [Nat.add_comm, f.iterate_add_apply]
State after:
case intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
k c : ℕ
h0 : k ≤ k + c
⊢ ⌊f^[c] (f^[k] r)⌋.natAbs ≤ ⌊f^[k] r⌋.natAbs

State before:
case intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
k c : ℕ
h0 : k ≤ k + c
⊢ ⌊f^[c] (f^[k] r)⌋.natAbs ≤ ⌊f^[k] r⌋.natAbs
Tactic:
exact floor_f_iter_natAbs_le _ c
State after:
no goals