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

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

State before:
case intro.intro.intro.intro
R : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Archimedean R
r : R
C : ℕ
h : 1 < C
ε : R
h0 : Infinitesimal ε
h1 : EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2 + (-↑C) ^ x * ε
⊢ ∃ C, 1 < C ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2
Tactic:
simp only [h0.zero_of_Archimedean, mul_zero, add_zero] at h1
State after:
case intro.intro.intro.intro
R : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Archimedean R
r : R
C : ℕ
h : 1 < C
ε : R
h0 : Infinitesimal ε
h1 : EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2
⊢ ∃ C, 1 < C ∧ EventuallyEqual (fun x => (↑C + 1) * f^[x] r) fun x => -↑C ^ 2

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