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

State before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
h : EventuallyEqual (fun x => ⌊f^[x] r⌋) fun x => 0
⊢ EventuallyEqual (fun x => f^[x] r) fun x => 0
Tactic:
rw [EventuallyEqual.const_right_iff] at h ⊢
State after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
h : ∃ N, ∀ (k : ℕ), ⌊f^[k + N] r⌋ = 0
⊢ ∃ N, ∀ (k : ℕ), f^[k + N] r = 0

State before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
h : ∃ N, ∀ (k : ℕ), ⌊f^[k + N] r⌋ = 0
⊢ ∃ N, ∀ (k : ℕ), f^[k + N] r = 0
Tactic:
rcases h with ⟨N, h⟩
State after:
case intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = 0
⊢ ∃ N, ∀ (k : ℕ), f^[k + N] r = 0

State before:
case intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = 0
⊢ ∃ N, ∀ (k : ℕ), f^[k + N] r = 0
Tactic:
refine ⟨N + 1, λ k ↦ ?_⟩
State after:
case intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = 0
k : ℕ
⊢ f^[k + (N + 1)] r = 0

State before:
case intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋ = 0
k : ℕ
⊢ f^[k + (N + 1)] r = 0
Tactic:
rw [← Nat.add_assoc, f.iterate_succ_apply', f, h, Int.cast_zero, zero_mul]
State after:
no goals