K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
terminates : Terminates (of v)
⊢ ∃ a, ∀ (b : ℕ), b ≥ a → v = convergents (of v) b
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
terminates : Terminates (of v)
⊢ ∀ᶠ (n : ℕ) in atTop, v = convergents (of v) n
rw [eventually_atTop]
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
terminates : Terminates (of v)
⊢ ∃ n, TerminatedAt (of v) n

case intro
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
terminates : Terminates (of v)
n : ℕ
terminated_at_n : TerminatedAt (of v) n
⊢ ∃ a, ∀ (b : ℕ), b ≥ a → v = convergents (of v) b
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
terminates : Terminates (of v)
⊢ ∃ a, ∀ (b : ℕ), b ≥ a → v = convergents (of v) b
obtain ⟨n, terminated_at_n⟩ : ∃ n, (of v).TerminatedAt n
case intro
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
terminates : Terminates (of v)
n : ℕ
terminated_at_n : TerminatedAt (of v) n
⊢ ∃ a, ∀ (b : ℕ), b ≥ a → v = convergents (of v) b
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
terminates : Terminates (of v)
⊢ ∃ n, TerminatedAt (of v) n

case intro
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
terminates : Terminates (of v)
n : ℕ
terminated_at_n : TerminatedAt (of v) n
⊢ ∃ a, ∀ (b : ℕ), b ≥ a → v = convergents (of v) b
exact terminates
case intro
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
terminates : Terminates (of v)
n : ℕ
terminated_at_n : TerminatedAt (of v) n
⊢ ∀ (b : ℕ), b ≥ n → v = convergents (of v) b
case intro
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
terminates : Terminates (of v)
n : ℕ
terminated_at_n : TerminatedAt (of v) n
⊢ ∃ a, ∀ (b : ℕ), b ≥ a → v = convergents (of v) b
use n
case intro
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
terminates : Terminates (of v)
n : ℕ
terminated_at_n : TerminatedAt (of v) n
m : ℕ
m_geq_n : m ≥ n
⊢ v = convergents (of v) m
case intro
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
terminates : Terminates (of v)
n : ℕ
terminated_at_n : TerminatedAt (of v) n
⊢ ∀ (b : ℕ), b ≥ n → v = convergents (of v) b
intro m m_geq_n
case intro
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
terminates : Terminates (of v)
n : ℕ
terminated_at_n : TerminatedAt (of v) n
m : ℕ
m_geq_n : m ≥ n
⊢ v = convergents (of v) n
case intro
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
terminates : Terminates (of v)
n : ℕ
terminated_at_n : TerminatedAt (of v) n
m : ℕ
m_geq_n : m ≥ n
⊢ v = convergents (of v) m
rw [convergents_stable_of_terminated m_geq_n terminated_at_n]
no goals
case intro
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
terminates : Terminates (of v)
n : ℕ
terminated_at_n : TerminatedAt (of v) n
m : ℕ
m_geq_n : m ≥ n
⊢ v = convergents (of v) n
exact of_correctness_of_terminatedAt terminated_at_n