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

State before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
⊢ (EventuallyEqual (fun x => f^[x] r) fun x => 0) ∨
    (∃ s, (0 < s ∧ s < 1) ∧ EventuallyEqual (fun x => f^[x] r) (NatSeq_ofList [-s, s - 1])) ∨
      ∃ C, 1 < C ∧ ∃ ε, Infinitesimal ε ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2 + (-↑C) ^ x * ε
Tactic:
rcases floor_f_iter_eventually_const r with ⟨C, h⟩
State after:
case intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
h : EventuallyEqual (fun x => ⌊f^[x] r⌋) fun x => -↑C
⊢ (EventuallyEqual (fun x => f^[x] r) fun x => 0) ∨
    (∃ s, (0 < s ∧ s < 1) ∧ EventuallyEqual (fun x => f^[x] r) (NatSeq_ofList [-s, s - 1])) ∨
      ∃ C, 1 < C ∧ ∃ ε, Infinitesimal ε ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2 + (-↑C) ^ x * ε

State before:
case intro
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
h : EventuallyEqual (fun x => ⌊f^[x] r⌋) fun x => -↑C
⊢ (EventuallyEqual (fun x => f^[x] r) fun x => 0) ∨
    (∃ s, (0 < s ∧ s < 1) ∧ EventuallyEqual (fun x => f^[x] r) (NatSeq_ofList [-s, s - 1])) ∨
      ∃ C, 1 < C ∧ ∃ ε, Infinitesimal ε ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2 + (-↑C) ^ x * ε
Tactic:
refine C.eq_zero_or_pos.imp ?_ (λ h0 ↦ (h0 : 1 ≤ C).eq_or_lt.imp ?_ ?_)
State after:
case intro.refine_1
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
h : EventuallyEqual (fun x => ⌊f^[x] r⌋) fun x => -↑C
⊢ C = 0 → EventuallyEqual (fun x => f^[x] r) fun x => 0

case intro.refine_2
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
h : EventuallyEqual (fun x => ⌊f^[x] r⌋) fun x => -↑C
h0 : 1 ≤ C
⊢ 1 = C → ∃ s, (0 < s ∧ s < 1) ∧ EventuallyEqual (fun x => f^[x] r) (NatSeq_ofList [-s, s - 1])

case intro.refine_3
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
h : EventuallyEqual (fun x => ⌊f^[x] r⌋) fun x => -↑C
h0 : 1 ≤ C
⊢ 1 < C →
    ∃ C, 1 < C ∧ ∃ ε, Infinitesimal ε ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2 + (-↑C) ^ x * ε

State before:
case intro.refine_1
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
h : EventuallyEqual (fun x => ⌊f^[x] r⌋) fun x => -↑C
⊢ C = 0 → EventuallyEqual (fun x => f^[x] r) fun x => 0
Tactic:
rintro rfl
State after:
case intro.refine_1
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

State before:
case intro.refine_1
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:
exact case_floor_eventually_zero h
State after:
no goals

State before:
case intro.refine_2
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
h : EventuallyEqual (fun x => ⌊f^[x] r⌋) fun x => -↑C
h0 : 1 ≤ C
⊢ 1 = C → ∃ s, (0 < s ∧ s < 1) ∧ EventuallyEqual (fun x => f^[x] r) (NatSeq_ofList [-s, s - 1])
Tactic:
rintro rfl
State after:
case intro.refine_2
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
h : EventuallyEqual (fun x => ⌊f^[x] r⌋) fun x => -↑1
h0 : 1 ≤ 1
⊢ ∃ s, (0 < s ∧ s < 1) ∧ EventuallyEqual (fun x => f^[x] r) (NatSeq_ofList [-s, s - 1])

State before:
case intro.refine_2
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
h : EventuallyEqual (fun x => ⌊f^[x] r⌋) fun x => -↑1
h0 : 1 ≤ 1
⊢ ∃ s, (0 < s ∧ s < 1) ∧ EventuallyEqual (fun x => f^[x] r) (NatSeq_ofList [-s, s - 1])
Tactic:
exact case_floor_eventually_neg_one h
State after:
no goals

State before:
case intro.refine_3
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
h : EventuallyEqual (fun x => ⌊f^[x] r⌋) fun x => -↑C
h0 : 1 ≤ C
⊢ 1 < C →
    ∃ C, 1 < C ∧ ∃ ε, Infinitesimal ε ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2 + (-↑C) ^ x * ε
Tactic:
intro h0
State after:
case intro.refine_3
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
h : EventuallyEqual (fun x => ⌊f^[x] r⌋) fun x => -↑C
h0✝ : 1 ≤ C
h0 : 1 < C
⊢ ∃ C, 1 < C ∧ ∃ ε, Infinitesimal ε ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2 + (-↑C) ^ x * ε

State before:
case intro.refine_3
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
C : ℕ
h : EventuallyEqual (fun x => ⌊f^[x] r⌋) fun x => -↑C
h0✝ : 1 ≤ C
h0 : 1 < C
⊢ ∃ C, 1 < C ∧ ∃ ε, Infinitesimal ε ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2 + (-↑C) ^ x * ε
Tactic:
exact ⟨C, h0, case_floor_eventually_neg_of_one_lt h0 h⟩
State after:
no goals