-- Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean
theorem nth_stream_fr_nonneg_lt_one {ifp_n : IntFractPair K}
    (nth_stream_eq : IntFractPair.stream v n = some ifp_n) : 0 ≤ ifp_n.fr ∧ ifp_n.fr < 1

Proof state:
case succ
K : Type u_1
v : K
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
ifp_n : IntFractPair K
n✝ : ℕ
nth_stream_eq : IntFractPair.stream v (n✝ + 1) = some ifp_n
⊢ 0 ≤ ifp_n.fr ∧ ifp_n.fr < 1

Tactic:
rcases succ_nth_stream_eq_some_iff.1 nth_stream_eq with ⟨_, _, _, ifp_of_eq_ifp_n⟩

Result:
case succ.intro.intro.intro
K : Type u_1
v : K
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
ifp_n : IntFractPair K
n✝ : ℕ
nth_stream_eq : IntFractPair.stream v (n✝ + 1) = some ifp_n
w✝ : IntFractPair K
left✝¹ : IntFractPair.stream v n✝ = some w✝
left✝ : w✝.fr ≠ 0
ifp_of_eq_ifp_n : IntFractPair.of w✝.fr⁻¹ = ifp_n
⊢ 0 ≤ ifp_n.fr ∧ ifp_n.fr < 1

Proof state:
K : Type u_1
v : K
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v 0 = some ifp_n
⊢ IntFractPair.of v = ifp_n

Tactic:
injection nth_stream_eq

Result:
no goals

Proof state:
case zero
K : Type u_1
v : K
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v 0 = some ifp_n
⊢ 0 ≤ ifp_n.fr ∧ ifp_n.fr < 1

Tactic:
have : IntFractPair.of v = ifp_n := by injection nth_stream_eq

Result:
case zero
K : Type u_1
v : K
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v 0 = some ifp_n
this : IntFractPair.of v = ifp_n
⊢ 0 ≤ ifp_n.fr ∧ ifp_n.fr < 1

Proof state:
case succ.intro.intro.intro
K : Type u_1
v : K
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
ifp_n : IntFractPair K
n✝ : ℕ
nth_stream_eq : IntFractPair.stream v (n✝ + 1) = some ifp_n
w✝ : IntFractPair K
left✝¹ : IntFractPair.stream v n✝ = some w✝
left✝ : w✝.fr ≠ 0
ifp_of_eq_ifp_n : IntFractPair.of w✝.fr⁻¹ = ifp_n
⊢ 0 ≤ ifp_n.fr ∧ ifp_n.fr < 1

Tactic:
rw [← ifp_of_eq_ifp_n, IntFractPair.of]

Result:
case succ.intro.intro.intro
K : Type u_1
v : K
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
ifp_n : IntFractPair K
n✝ : ℕ
nth_stream_eq : IntFractPair.stream v (n✝ + 1) = some ifp_n
w✝ : IntFractPair K
left✝¹ : IntFractPair.stream v n✝ = some w✝
left✝ : w✝.fr ≠ 0
ifp_of_eq_ifp_n : IntFractPair.of w✝.fr⁻¹ = ifp_n
⊢ 0 ≤ { b := ⌊w✝.fr⁻¹⌋, fr := fract w✝.fr⁻¹ }.fr ∧ { b := ⌊w✝.fr⁻¹⌋, fr := fract w✝.fr⁻¹ }.fr < 1

Proof state:
case zero
K : Type u_1
v : K
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v 0 = some ifp_n
this : IntFractPair.of v = ifp_n
⊢ 0 ≤ ifp_n.fr ∧ ifp_n.fr < 1

Tactic:
rw [← this, IntFractPair.of]

Result:
case zero
K : Type u_1
v : K
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v 0 = some ifp_n
this : IntFractPair.of v = ifp_n
⊢ 0 ≤ { b := ⌊v⌋, fr := fract v }.fr ∧ { b := ⌊v⌋, fr := fract v }.fr < 1

Proof state:
case zero
K : Type u_1
v : K
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v 0 = some ifp_n
this : IntFractPair.of v = ifp_n
⊢ 0 ≤ { b := ⌊v⌋, fr := fract v }.fr ∧ { b := ⌊v⌋, fr := fract v }.fr < 1

Tactic:
exact ⟨fract_nonneg _, fract_lt_one _⟩

Result:
no goals

Proof state:
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
⊢ 0 ≤ ifp_n.fr ∧ ifp_n.fr < 1

Tactic:
cases n with
| zero =>
  have : IntFractPair.of v = ifp_n := by injection nth_stream_eq
  rw [← this, IntFractPair.of]
  exact ⟨fract_nonneg _, fract_lt_one _⟩
| succ =>
  rcases succ_nth_stream_eq_some_iff.1 nth_stream_eq with ⟨_, _, _, ifp_of_eq_ifp_n⟩
  rw [← ifp_of_eq_ifp_n, IntFractPair.of]
  exact ⟨fract_nonneg _, fract_lt_one _⟩

Result:
no goals

Proof state:
case succ.intro.intro.intro
K : Type u_1
v : K
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
ifp_n : IntFractPair K
n✝ : ℕ
nth_stream_eq : IntFractPair.stream v (n✝ + 1) = some ifp_n
w✝ : IntFractPair K
left✝¹ : IntFractPair.stream v n✝ = some w✝
left✝ : w✝.fr ≠ 0
ifp_of_eq_ifp_n : IntFractPair.of w✝.fr⁻¹ = ifp_n
⊢ 0 ≤ { b := ⌊w✝.fr⁻¹⌋, fr := fract w✝.fr⁻¹ }.fr ∧ { b := ⌊w✝.fr⁻¹⌋, fr := fract w✝.fr⁻¹ }.fr < 1

Tactic:
exact ⟨fract_nonneg _, fract_lt_one _⟩

Result:
no goals