Theorem: IMOSL.IMO2006A1.floor_f_iter_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⌋) fun x => -↑C
Tactic:
rcases floor_f_iter_natAbs_eventually_const r with ⟨C, N, K, h⟩
State after:
case intro.intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C N K : ℕ
h : ∀ (k : ℕ), (fun x => ⌊f^[x] r⌋.natAbs) (k + N) = (fun x => C) (k + K)
⊢ ∃ C, EventuallyEqual (fun x => ⌊f^[x] r⌋) fun x => -↑C

State before:
case intro.intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C N K : ℕ
h : ∀ (k : ℕ), (fun x => ⌊f^[x] r⌋.natAbs) (k + N) = (fun x => C) (k + K)
⊢ ∃ C, EventuallyEqual (fun x => ⌊f^[x] r⌋) fun x => -↑C
Tactic:
refine ⟨C, N, K, λ n ↦ (Int.natAbs_eq_iff.mp (h n)).elim (λ h0 ↦ h0.trans ?_) id⟩
State after:
case intro.intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C N K : ℕ
h : ∀ (k : ℕ), (fun x => ⌊f^[x] r⌋.natAbs) (k + N) = (fun x => C) (k + K)
n : ℕ
h0 : ⌊f^[n + N] r⌋ = ↑((fun x => C) (n + K))
⊢ ↑((fun x => C) (n + K)) = (fun x => -↑C) (n + K)

State before:
case intro.intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C N K : ℕ
h : ∀ (k : ℕ), (fun x => ⌊f^[x] r⌋.natAbs) (k + N) = (fun x => C) (k + K)
n : ℕ
h0 : ⌊f^[n + N] r⌋ = ↑((fun x => C) (n + K))
⊢ ↑((fun x => C) (n + K)) = (fun x => -↑C) (n + K)
Tactic:
simp only at h h0 ⊢
State after:
case intro.intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C N K : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋.natAbs = C
n : ℕ
h0 : ⌊f^[n + N] r⌋ = ↑C
⊢ ↑C = -↑C

State before:
case intro.intro.intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C N K : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋.natAbs = C
n : ℕ
h0 : ⌊f^[n + N] r⌋ = ↑C
⊢ ↑C = -↑C
Tactic:
rcases C.eq_zero_or_pos with rfl | h1
State after:
case intro.intro.intro.inl
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N K n : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋.natAbs = 0
h0 : ⌊f^[n + N] r⌋ = ↑0
⊢ ↑0 = -↑0

case intro.intro.intro.inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C N K : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋.natAbs = C
n : ℕ
h0 : ⌊f^[n + N] r⌋ = ↑C
h1 : C > 0
⊢ ↑C = -↑C

State before:
case intro.intro.intro.inl
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
N K n : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋.natAbs = 0
h0 : ⌊f^[n + N] r⌋ = ↑0
⊢ ↑0 = -↑0

case intro.intro.intro.inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C N K : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋.natAbs = C
n : ℕ
h0 : ⌊f^[n + N] r⌋ = ↑C
h1 : C > 0
⊢ ↑C = -↑C
Tactic:
rfl
State after:
case intro.intro.intro.inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C N K : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋.natAbs = C
n : ℕ
h0 : ⌊f^[n + N] r⌋ = ↑C
h1 : C > 0
⊢ ↑C = -↑C

State before:
case intro.intro.intro.inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C N K : ℕ
h : ∀ (k : ℕ), ⌊f^[k + N] r⌋.natAbs = C
n : ℕ
h0 : ⌊f^[n + N] r⌋ = ↑C
h1 : C > 0
⊢ ↑C = -↑C
Tactic:
specialize h (n + 1)
State after:
case intro.intro.intro.inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C N K n : ℕ
h0 : ⌊f^[n + N] r⌋ = ↑C
h1 : C > 0
h : ⌊f^[n + 1 + N] r⌋.natAbs = C
⊢ ↑C = -↑C

State before:
case intro.intro.intro.inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C N K n : ℕ
h0 : ⌊f^[n + N] r⌋ = ↑C
h1 : C > 0
h : ⌊f^[n + 1 + N] r⌋.natAbs = C
⊢ ↑C = -↑C
Tactic:
rw [Nat.add_right_comm, f.iterate_succ_apply'] at h
State after:
case intro.intro.intro.inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C N K n : ℕ
h0 : ⌊f^[n + N] r⌋ = ↑C
h1 : C > 0
h : ⌊f (f^[n + N] r)⌋.natAbs = C
⊢ ↑C = -↑C

State before:
case intro.intro.intro.inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C N K n : ℕ
h0 : ⌊f^[n + N] r⌋ = ↑C
h1 : C > 0
h : ⌊f (f^[n + N] r)⌋.natAbs = C
⊢ ↑C = -↑C
Tactic:
replace h1 : 0 < ⌊f^[n + N] r⌋ := by rwa [h0, Nat.cast_pos]
State after:
case intro.intro.intro.inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C N K n : ℕ
h0 : ⌊f^[n + N] r⌋ = ↑C
h : ⌊f (f^[n + N] r)⌋.natAbs = C
h1 : 0 < ⌊f^[n + N] r⌋
⊢ ↑C = -↑C

State before:
case intro.intro.intro.inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C N K n : ℕ
h0 : ⌊f^[n + N] r⌋ = ↑C
h : ⌊f (f^[n + N] r)⌋.natAbs = C
h1 : 0 < ⌊f^[n + N] r⌋
⊢ ↑C = -↑C
Tactic:
rw [← h, Int.natCast_natAbs, abs_eq_self.mpr (floor_f_nonneg h1.le)] at h0
State after:
case intro.intro.intro.inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C N K n : ℕ
h0 : ⌊f^[n + N] r⌋ = ⌊f (f^[n + N] r)⌋
h : ⌊f (f^[n + N] r)⌋.natAbs = C
h1 : 0 < ⌊f^[n + N] r⌋
⊢ ↑C = -↑C

State before:
case intro.intro.intro.inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C N K n : ℕ
h0 : ⌊f^[n + N] r⌋ = ⌊f (f^[n + N] r)⌋
h : ⌊f (f^[n + N] r)⌋.natAbs = C
h1 : 0 < ⌊f^[n + N] r⌋
⊢ ↑C = -↑C
Tactic:
exact absurd h0.symm (floor_f_lt_of_floor_pos h1).ne
State after:
no goals

State before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C N K n : ℕ
h0 : ⌊f^[n + N] r⌋ = ↑C
h1 : C > 0
h : ⌊f (f^[n + N] r)⌋.natAbs = C
⊢ 0 < ⌊f^[n + N] r⌋
Tactic:
rwa [h0, Nat.cast_pos]
State after:
no goals