[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ ∀ (n : ℕ),
    (∀ (m : ℕ), m < n → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts) →
      ∃ conts, continuantsAux (of v) n = Pair.map Rat.cast conts
[PROOFSTEP]
clear n
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
⊢ ∀ (n : ℕ),
    (∀ (m : ℕ), m < n → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts) →
      ∃ conts, continuantsAux (of v) n = Pair.map Rat.cast conts
[PROOFSTEP]
let g := of v
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
⊢ ∀ (n : ℕ),
    (∀ (m : ℕ), m < n → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts) →
      ∃ conts, continuantsAux (of v) n = Pair.map Rat.cast conts
[PROOFSTEP]
intro n IH
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH : ∀ (m : ℕ), m < n → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
⊢ ∃ conts, continuantsAux (of v) n = Pair.map Rat.cast conts
[PROOFSTEP]
rcases n with
  (_ | _ | n)
    -- n = 0
[GOAL]
case zero
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
IH : ∀ (m : ℕ), m < Nat.zero → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
⊢ ∃ conts, continuantsAux (of v) Nat.zero = Pair.map Rat.cast conts
[PROOFSTEP]
suffices ∃ gp : Pair ℚ, Pair.mk (1 : K) 0 = gp.map (↑) by simpa [continuantsAux]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
IH : ∀ (m : ℕ), m < Nat.zero → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
this : ∃ gp, { a := 1, b := 0 } = Pair.map Rat.cast gp
⊢ ∃ conts, continuantsAux (of v) Nat.zero = Pair.map Rat.cast conts
[PROOFSTEP]
simpa [continuantsAux]
[GOAL]
case zero
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
IH : ∀ (m : ℕ), m < Nat.zero → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
⊢ ∃ gp, { a := 1, b := 0 } = Pair.map Rat.cast gp
[PROOFSTEP]
use Pair.mk 1 0
[GOAL]
case h
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
IH : ∀ (m : ℕ), m < Nat.zero → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
⊢ { a := 1, b := 0 } = Pair.map Rat.cast { a := 1, b := 0 }
[PROOFSTEP]
simp
  -- n = 1
[GOAL]
case succ.zero
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
IH : ∀ (m : ℕ), m < Nat.succ Nat.zero → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
⊢ ∃ conts, continuantsAux (of v) (Nat.succ Nat.zero) = Pair.map Rat.cast conts
[PROOFSTEP]
suffices ∃ conts : Pair ℚ, Pair.mk g.h 1 = conts.map (↑) by simpa [continuantsAux]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
IH : ∀ (m : ℕ), m < Nat.succ Nat.zero → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
this : ∃ conts, { a := g.h, b := 1 } = Pair.map Rat.cast conts
⊢ ∃ conts, continuantsAux (of v) (Nat.succ Nat.zero) = Pair.map Rat.cast conts
[PROOFSTEP]
simpa [continuantsAux]
[GOAL]
case succ.zero
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
IH : ∀ (m : ℕ), m < Nat.succ Nat.zero → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
⊢ ∃ conts, { a := g.h, b := 1 } = Pair.map Rat.cast conts
[PROOFSTEP]
use Pair.mk ⌊v⌋ 1
[GOAL]
case h
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
IH : ∀ (m : ℕ), m < Nat.succ Nat.zero → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
⊢ { a := g.h, b := 1 } = Pair.map Rat.cast { a := ↑⌊v⌋, b := 1 }
[PROOFSTEP]
simp
  -- 2 ≤ n
[GOAL]
case succ.succ
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH : ∀ (m : ℕ), m < Nat.succ (Nat.succ n) → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
⊢ ∃ conts, continuantsAux (of v) (Nat.succ (Nat.succ n)) = Pair.map Rat.cast conts
[PROOFSTEP]
cases' IH (n + 1) <| lt_add_one (n + 1) with pred_conts pred_conts_eq
[GOAL]
case succ.succ.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH : ∀ (m : ℕ), m < Nat.succ (Nat.succ n) → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : continuantsAux (of v) (n + 1) = Pair.map Rat.cast pred_conts
⊢ ∃ conts, continuantsAux (of v) (Nat.succ (Nat.succ n)) = Pair.map Rat.cast conts
[PROOFSTEP]
cases' s_ppred_nth_eq : g.s.get? n with gp_n
[GOAL]
case succ.succ.intro.none
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH : ∀ (m : ℕ), m < Nat.succ (Nat.succ n) → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : continuantsAux (of v) (n + 1) = Pair.map Rat.cast pred_conts
s_ppred_nth_eq : Stream'.Seq.get? g.s n = none
⊢ ∃ conts, continuantsAux (of v) (Nat.succ (Nat.succ n)) = Pair.map Rat.cast conts
[PROOFSTEP]
use pred_conts
[GOAL]
case h
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH : ∀ (m : ℕ), m < Nat.succ (Nat.succ n) → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : continuantsAux (of v) (n + 1) = Pair.map Rat.cast pred_conts
s_ppred_nth_eq : Stream'.Seq.get? g.s n = none
⊢ continuantsAux (of v) (Nat.succ (Nat.succ n)) = Pair.map Rat.cast pred_conts
[PROOFSTEP]
have : g.continuantsAux (n + 2) = g.continuantsAux (n + 1) :=
  continuantsAux_stable_of_terminated (n + 1).le_succ s_ppred_nth_eq
[GOAL]
case h
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH : ∀ (m : ℕ), m < Nat.succ (Nat.succ n) → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : continuantsAux (of v) (n + 1) = Pair.map Rat.cast pred_conts
s_ppred_nth_eq : Stream'.Seq.get? g.s n = none
this : continuantsAux g (n + 2) = continuantsAux g (n + 1)
⊢ continuantsAux (of v) (Nat.succ (Nat.succ n)) = Pair.map Rat.cast pred_conts
[PROOFSTEP]
simp only [this, pred_conts_eq]
  -- option.some
[GOAL]
case succ.succ.intro.some
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH : ∀ (m : ℕ), m < Nat.succ (Nat.succ n) → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : continuantsAux (of v) (n + 1) = Pair.map Rat.cast pred_conts
gp_n : Pair K
s_ppred_nth_eq : Stream'.Seq.get? g.s n = some gp_n
⊢ ∃ conts, continuantsAux (of v) (Nat.succ (Nat.succ n)) = Pair.map Rat.cast conts
[PROOFSTEP]
cases' IH n <| lt_of_le_of_lt n.le_succ <| lt_add_one <| n + 1 with ppred_conts ppred_conts_eq
[GOAL]
case succ.succ.intro.some.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH : ∀ (m : ℕ), m < Nat.succ (Nat.succ n) → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : continuantsAux (of v) (n + 1) = Pair.map Rat.cast pred_conts
gp_n : Pair K
s_ppred_nth_eq : Stream'.Seq.get? g.s n = some gp_n
ppred_conts : Pair ℚ
ppred_conts_eq : continuantsAux (of v) n = Pair.map Rat.cast ppred_conts
⊢ ∃ conts, continuantsAux (of v) (Nat.succ (Nat.succ n)) = Pair.map Rat.cast conts
[PROOFSTEP]
obtain ⟨a_eq_one, z, b_eq_z⟩ : gp_n.a = 1 ∧ ∃ z : ℤ, gp_n.b = (z : K)
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH : ∀ (m : ℕ), m < Nat.succ (Nat.succ n) → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : continuantsAux (of v) (n + 1) = Pair.map Rat.cast pred_conts
gp_n : Pair K
s_ppred_nth_eq : Stream'.Seq.get? g.s n = some gp_n
ppred_conts : Pair ℚ
ppred_conts_eq : continuantsAux (of v) n = Pair.map Rat.cast ppred_conts
⊢ gp_n.a = 1 ∧ ∃ z, gp_n.b = ↑z
case succ.succ.intro.some.intro.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH : ∀ (m : ℕ), m < Nat.succ (Nat.succ n) → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : continuantsAux (of v) (n + 1) = Pair.map Rat.cast pred_conts
gp_n : Pair K
s_ppred_nth_eq : Stream'.Seq.get? g.s n = some gp_n
ppred_conts : Pair ℚ
ppred_conts_eq : continuantsAux (of v) n = Pair.map Rat.cast ppred_conts
a_eq_one : gp_n.a = 1
z : ℤ
b_eq_z : gp_n.b = ↑z
⊢ ∃ conts, continuantsAux (of v) (Nat.succ (Nat.succ n)) = Pair.map Rat.cast conts
[PROOFSTEP]
exact of_part_num_eq_one_and_exists_int_part_denom_eq s_ppred_nth_eq
[GOAL]
case succ.succ.intro.some.intro.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH : ∀ (m : ℕ), m < Nat.succ (Nat.succ n) → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : continuantsAux (of v) (n + 1) = Pair.map Rat.cast pred_conts
gp_n : Pair K
s_ppred_nth_eq : Stream'.Seq.get? g.s n = some gp_n
ppred_conts : Pair ℚ
ppred_conts_eq : continuantsAux (of v) n = Pair.map Rat.cast ppred_conts
a_eq_one : gp_n.a = 1
z : ℤ
b_eq_z : gp_n.b = ↑z
⊢ ∃ conts, continuantsAux (of v) (Nat.succ (Nat.succ n)) = Pair.map Rat.cast conts
[PROOFSTEP]
simp only [a_eq_one, b_eq_z, continuantsAux_recurrence s_ppred_nth_eq ppred_conts_eq pred_conts_eq]
[GOAL]
case succ.succ.intro.some.intro.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH : ∀ (m : ℕ), m < Nat.succ (Nat.succ n) → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : continuantsAux (of v) (n + 1) = Pair.map Rat.cast pred_conts
gp_n : Pair K
s_ppred_nth_eq : Stream'.Seq.get? g.s n = some gp_n
ppred_conts : Pair ℚ
ppred_conts_eq : continuantsAux (of v) n = Pair.map Rat.cast ppred_conts
a_eq_one : gp_n.a = 1
z : ℤ
b_eq_z : gp_n.b = ↑z
⊢ ∃ conts,
    { a := ↑z * (Pair.map Rat.cast pred_conts).a + 1 * (Pair.map Rat.cast ppred_conts).a,
        b := ↑z * (Pair.map Rat.cast pred_conts).b + 1 * (Pair.map Rat.cast ppred_conts).b } =
      Pair.map Rat.cast conts
[PROOFSTEP]
use nextContinuants 1 (z : ℚ) ppred_conts pred_conts
[GOAL]
case h
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH : ∀ (m : ℕ), m < Nat.succ (Nat.succ n) → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : continuantsAux (of v) (n + 1) = Pair.map Rat.cast pred_conts
gp_n : Pair K
s_ppred_nth_eq : Stream'.Seq.get? g.s n = some gp_n
ppred_conts : Pair ℚ
ppred_conts_eq : continuantsAux (of v) n = Pair.map Rat.cast ppred_conts
a_eq_one : gp_n.a = 1
z : ℤ
b_eq_z : gp_n.b = ↑z
⊢ { a := ↑z * (Pair.map Rat.cast pred_conts).a + 1 * (Pair.map Rat.cast ppred_conts).a,
      b := ↑z * (Pair.map Rat.cast pred_conts).b + 1 * (Pair.map Rat.cast ppred_conts).b } =
    Pair.map Rat.cast (nextContinuants 1 (↑z) ppred_conts pred_conts)
[PROOFSTEP]
cases ppred_conts
[GOAL]
case h.mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH : ∀ (m : ℕ), m < Nat.succ (Nat.succ n) → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : continuantsAux (of v) (n + 1) = Pair.map Rat.cast pred_conts
gp_n : Pair K
s_ppred_nth_eq : Stream'.Seq.get? g.s n = some gp_n
a_eq_one : gp_n.a = 1
z : ℤ
b_eq_z : gp_n.b = ↑z
a✝ b✝ : ℚ
ppred_conts_eq : continuantsAux (of v) n = Pair.map Rat.cast { a := a✝, b := b✝ }
⊢ { a := ↑z * (Pair.map Rat.cast pred_conts).a + 1 * (Pair.map Rat.cast { a := a✝, b := b✝ }).a,
      b := ↑z * (Pair.map Rat.cast pred_conts).b + 1 * (Pair.map Rat.cast { a := a✝, b := b✝ }).b } =
    Pair.map Rat.cast (nextContinuants 1 ↑z { a := a✝, b := b✝ } pred_conts)
[PROOFSTEP]
cases pred_conts
[GOAL]
case h.mk.mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH : ∀ (m : ℕ), m < Nat.succ (Nat.succ n) → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
gp_n : Pair K
s_ppred_nth_eq : Stream'.Seq.get? g.s n = some gp_n
a_eq_one : gp_n.a = 1
z : ℤ
b_eq_z : gp_n.b = ↑z
a✝¹ b✝¹ : ℚ
ppred_conts_eq : continuantsAux (of v) n = Pair.map Rat.cast { a := a✝¹, b := b✝¹ }
a✝ b✝ : ℚ
pred_conts_eq : continuantsAux (of v) (n + 1) = Pair.map Rat.cast { a := a✝, b := b✝ }
⊢ { a := ↑z * (Pair.map Rat.cast { a := a✝, b := b✝ }).a + 1 * (Pair.map Rat.cast { a := a✝¹, b := b✝¹ }).a,
      b := ↑z * (Pair.map Rat.cast { a := a✝, b := b✝ }).b + 1 * (Pair.map Rat.cast { a := a✝¹, b := b✝¹ }).b } =
    Pair.map Rat.cast (nextContinuants 1 ↑z { a := a✝¹, b := b✝¹ } { a := a✝, b := b✝ })
[PROOFSTEP]
simp [nextContinuants, nextNumerator, nextDenominator]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ ∃ conts, continuants (of v) n = Pair.map Rat.cast conts
[PROOFSTEP]
rw [nth_cont_eq_succ_nth_cont_aux]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ ∃ conts, continuantsAux (of v) (n + 1) = Pair.map Rat.cast conts
[PROOFSTEP]
exact exists_gcf_pair_rat_eq_of_nth_conts_aux v <| n + 1
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ ∃ q, numerators (of v) n = ↑q
[PROOFSTEP]
rcases exists_gcf_pair_rat_eq_nth_conts v n with ⟨⟨a, _⟩, nth_cont_eq⟩
[GOAL]
case intro.mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
a b✝ : ℚ
nth_cont_eq : continuants (of v) n = Pair.map Rat.cast { a := a, b := b✝ }
⊢ ∃ q, numerators (of v) n = ↑q
[PROOFSTEP]
use a
[GOAL]
case h
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
a b✝ : ℚ
nth_cont_eq : continuants (of v) n = Pair.map Rat.cast { a := a, b := b✝ }
⊢ numerators (of v) n = ↑a
[PROOFSTEP]
simp [num_eq_conts_a, nth_cont_eq]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ ∃ q, denominators (of v) n = ↑q
[PROOFSTEP]
rcases exists_gcf_pair_rat_eq_nth_conts v n with ⟨⟨_, b⟩, nth_cont_eq⟩
[GOAL]
case intro.mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
a✝ b : ℚ
nth_cont_eq : continuants (of v) n = Pair.map Rat.cast { a := a✝, b := b }
⊢ ∃ q, denominators (of v) n = ↑q
[PROOFSTEP]
use b
[GOAL]
case h
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
a✝ b : ℚ
nth_cont_eq : continuants (of v) n = Pair.map Rat.cast { a := a✝, b := b }
⊢ denominators (of v) n = ↑b
[PROOFSTEP]
simp [denom_eq_conts_b, nth_cont_eq]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ ∃ q, convergents (of v) n = ↑q
[PROOFSTEP]
rcases exists_rat_eq_nth_numerator v n with ⟨Aₙ, nth_num_eq⟩
[GOAL]
case intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
Aₙ : ℚ
nth_num_eq : numerators (of v) n = ↑Aₙ
⊢ ∃ q, convergents (of v) n = ↑q
[PROOFSTEP]
rcases exists_rat_eq_nth_denominator v n with ⟨Bₙ, nth_denom_eq⟩
[GOAL]
case intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
Aₙ : ℚ
nth_num_eq : numerators (of v) n = ↑Aₙ
Bₙ : ℚ
nth_denom_eq : denominators (of v) n = ↑Bₙ
⊢ ∃ q, convergents (of v) n = ↑q
[PROOFSTEP]
use Aₙ / Bₙ
[GOAL]
case h
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
Aₙ : ℚ
nth_num_eq : numerators (of v) n = ↑Aₙ
Bₙ : ℚ
nth_denom_eq : denominators (of v) n = ↑Bₙ
⊢ convergents (of v) n = ↑(Aₙ / Bₙ)
[PROOFSTEP]
simp [nth_num_eq, nth_denom_eq, convergent_eq_num_div_denom]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
terminates : Terminates (of v)
⊢ ∃ q, v = ↑q
[PROOFSTEP]
obtain ⟨n, v_eq_conv⟩ : ∃ n, v = (of v).convergents n
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
terminates : Terminates (of v)
⊢ ∃ n, v = convergents (of v) n
case intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
terminates : Terminates (of v)
n : ℕ
v_eq_conv : v = convergents (of v) n
⊢ ∃ q, v = ↑q
[PROOFSTEP]
exact of_correctness_of_terminates terminates
[GOAL]
case intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
terminates : Terminates (of v)
n : ℕ
v_eq_conv : v = convergents (of v) n
⊢ ∃ q, v = ↑q
[PROOFSTEP]
obtain ⟨q, conv_eq_q⟩ : ∃ q : ℚ, (of v).convergents n = (↑q : K)
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
terminates : Terminates (of v)
n : ℕ
v_eq_conv : v = convergents (of v) n
⊢ ∃ q, convergents (of v) n = ↑q
case intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
terminates : Terminates (of v)
n : ℕ
v_eq_conv : v = convergents (of v) n
q : ℚ
conv_eq_q : convergents (of v) n = ↑q
⊢ ∃ q, v = ↑q
[PROOFSTEP]
exact exists_rat_eq_nth_convergent v n
[GOAL]
case intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
terminates : Terminates (of v)
n : ℕ
v_eq_conv : v = convergents (of v) n
q : ℚ
conv_eq_q : convergents (of v) n = ↑q
⊢ ∃ q, v = ↑q
[PROOFSTEP]
have : v = (↑q : K) := Eq.trans v_eq_conv conv_eq_q
[GOAL]
case intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
terminates : Terminates (of v)
n : ℕ
v_eq_conv : v = convergents (of v) n
q : ℚ
conv_eq_q : convergents (of v) n = ↑q
this : v = ↑q
⊢ ∃ q, v = ↑q
[PROOFSTEP]
use q, this
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ mapFr Rat.cast (IntFractPair.of q) = IntFractPair.of v
[PROOFSTEP]
simp [IntFractPair.of, v_eq_q]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream v n
[PROOFSTEP]
induction' n with n IH
[GOAL]
case zero
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q Nat.zero) = IntFractPair.stream v Nat.zero
case succ
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream v n
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (Nat.succ n)) = IntFractPair.stream v (Nat.succ n)
[PROOFSTEP]
case zero =>
  -- Porting note: was
      -- simp [IntFractPair.stream, coe_of_rat_eq v_eq_q]simp only [IntFractPair.stream, Option.map_some',
    coe_of_rat_eq v_eq_q]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q Nat.zero) = IntFractPair.stream v Nat.zero
[PROOFSTEP]
case zero =>
  -- Porting note: was
      -- simp [IntFractPair.stream, coe_of_rat_eq v_eq_q]simp only [IntFractPair.stream, Option.map_some',
    coe_of_rat_eq v_eq_q]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q Nat.zero) = IntFractPair.stream v Nat.zero
[PROOFSTEP]
simp only [IntFractPair.stream, Option.map_some', coe_of_rat_eq v_eq_q]
[GOAL]
case succ
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream v n
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (Nat.succ n)) = IntFractPair.stream v (Nat.succ n)
[PROOFSTEP]
case succ =>
  rw [v_eq_q] at IH 
  cases' stream_q_nth_eq : IntFractPair.stream q n with ifp_n
  case none => simp [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq]
  case some =>
    cases' ifp_n with b fr
    cases' Decidable.em (fr = 0) with fr_zero fr_ne_zero
    · simp [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq, fr_zero]
    · replace IH : some (IntFractPair.mk b (fr : K)) = IntFractPair.stream (↑q) n; · rwa [stream_q_nth_eq] at IH 
      have : (fr : K)⁻¹ = ((fr⁻¹ : ℚ) : K) := by norm_cast
      have coe_of_fr := coe_of_rat_eq this
      simpa [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq, fr_ne_zero]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream v n
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (Nat.succ n)) = IntFractPair.stream v (Nat.succ n)
[PROOFSTEP]
case succ =>
  rw [v_eq_q] at IH 
  cases' stream_q_nth_eq : IntFractPair.stream q n with ifp_n
  case none => simp [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq]
  case some =>
    cases' ifp_n with b fr
    cases' Decidable.em (fr = 0) with fr_zero fr_ne_zero
    · simp [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq, fr_zero]
    · replace IH : some (IntFractPair.mk b (fr : K)) = IntFractPair.stream (↑q) n; · rwa [stream_q_nth_eq] at IH 
      have : (fr : K)⁻¹ = ((fr⁻¹ : ℚ) : K) := by norm_cast
      have coe_of_fr := coe_of_rat_eq this
      simpa [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq, fr_ne_zero]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream v n
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (Nat.succ n)) = IntFractPair.stream v (Nat.succ n)
[PROOFSTEP]
rw [v_eq_q] at IH 
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream (↑q) n
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (Nat.succ n)) = IntFractPair.stream v (Nat.succ n)
[PROOFSTEP]
cases' stream_q_nth_eq : IntFractPair.stream q n with ifp_n
[GOAL]
case none
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream (↑q) n
stream_q_nth_eq : IntFractPair.stream q n = none
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (Nat.succ n)) = IntFractPair.stream v (Nat.succ n)
case some
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream (↑q) n
ifp_n : IntFractPair ℚ
stream_q_nth_eq : IntFractPair.stream q n = some ifp_n
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (Nat.succ n)) = IntFractPair.stream v (Nat.succ n)
[PROOFSTEP]
case none => simp [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream (↑q) n
stream_q_nth_eq : IntFractPair.stream q n = none
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (Nat.succ n)) = IntFractPair.stream v (Nat.succ n)
[PROOFSTEP]
case none => simp [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream (↑q) n
stream_q_nth_eq : IntFractPair.stream q n = none
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (Nat.succ n)) = IntFractPair.stream v (Nat.succ n)
[PROOFSTEP]
simp [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq]
[GOAL]
case some
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream (↑q) n
ifp_n : IntFractPair ℚ
stream_q_nth_eq : IntFractPair.stream q n = some ifp_n
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (Nat.succ n)) = IntFractPair.stream v (Nat.succ n)
[PROOFSTEP]
case some =>
  cases' ifp_n with b fr
  cases' Decidable.em (fr = 0) with fr_zero fr_ne_zero
  · simp [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq, fr_zero]
  · replace IH : some (IntFractPair.mk b (fr : K)) = IntFractPair.stream (↑q) n; · rwa [stream_q_nth_eq] at IH 
    have : (fr : K)⁻¹ = ((fr⁻¹ : ℚ) : K) := by norm_cast
    have coe_of_fr := coe_of_rat_eq this
    simpa [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq, fr_ne_zero]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream (↑q) n
ifp_n : IntFractPair ℚ
stream_q_nth_eq : IntFractPair.stream q n = some ifp_n
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (Nat.succ n)) = IntFractPair.stream v (Nat.succ n)
[PROOFSTEP]
case some =>
  cases' ifp_n with b fr
  cases' Decidable.em (fr = 0) with fr_zero fr_ne_zero
  · simp [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq, fr_zero]
  · replace IH : some (IntFractPair.mk b (fr : K)) = IntFractPair.stream (↑q) n; · rwa [stream_q_nth_eq] at IH 
    have : (fr : K)⁻¹ = ((fr⁻¹ : ℚ) : K) := by norm_cast
    have coe_of_fr := coe_of_rat_eq this
    simpa [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq, fr_ne_zero]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream (↑q) n
ifp_n : IntFractPair ℚ
stream_q_nth_eq : IntFractPair.stream q n = some ifp_n
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (Nat.succ n)) = IntFractPair.stream v (Nat.succ n)
[PROOFSTEP]
cases' ifp_n with b fr
[GOAL]
case mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream (↑q) n
b : ℤ
fr : ℚ
stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (Nat.succ n)) = IntFractPair.stream v (Nat.succ n)
[PROOFSTEP]
cases' Decidable.em (fr = 0) with fr_zero fr_ne_zero
[GOAL]
case mk.inl
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream (↑q) n
b : ℤ
fr : ℚ
stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }
fr_zero : fr = 0
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (Nat.succ n)) = IntFractPair.stream v (Nat.succ n)
[PROOFSTEP]
simp [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq, fr_zero]
[GOAL]
case mk.inr
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream (↑q) n
b : ℤ
fr : ℚ
stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }
fr_ne_zero : ¬fr = 0
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (Nat.succ n)) = IntFractPair.stream v (Nat.succ n)
[PROOFSTEP]
replace IH : some (IntFractPair.mk b (fr : K)) = IntFractPair.stream (↑q) n
[GOAL]
case IH
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream (↑q) n
b : ℤ
fr : ℚ
stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }
fr_ne_zero : ¬fr = 0
⊢ some { b := b, fr := ↑fr } = IntFractPair.stream (↑q) n
[PROOFSTEP]
rwa [stream_q_nth_eq] at IH 
[GOAL]
case mk.inr
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
b : ℤ
fr : ℚ
stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }
fr_ne_zero : ¬fr = 0
IH : some { b := b, fr := ↑fr } = IntFractPair.stream (↑q) n
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (Nat.succ n)) = IntFractPair.stream v (Nat.succ n)
[PROOFSTEP]
have : (fr : K)⁻¹ = ((fr⁻¹ : ℚ) : K) := by norm_cast
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
b : ℤ
fr : ℚ
stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }
fr_ne_zero : ¬fr = 0
IH : some { b := b, fr := ↑fr } = IntFractPair.stream (↑q) n
⊢ (↑fr)⁻¹ = ↑fr⁻¹
[PROOFSTEP]
norm_cast
[GOAL]
case mk.inr
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
b : ℤ
fr : ℚ
stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }
fr_ne_zero : ¬fr = 0
IH : some { b := b, fr := ↑fr } = IntFractPair.stream (↑q) n
this : (↑fr)⁻¹ = ↑fr⁻¹
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (Nat.succ n)) = IntFractPair.stream v (Nat.succ n)
[PROOFSTEP]
have coe_of_fr := coe_of_rat_eq this
[GOAL]
case mk.inr
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
b : ℤ
fr : ℚ
stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }
fr_ne_zero : ¬fr = 0
IH : some { b := b, fr := ↑fr } = IntFractPair.stream (↑q) n
this : (↑fr)⁻¹ = ↑fr⁻¹
coe_of_fr : mapFr Rat.cast (IntFractPair.of fr⁻¹) = IntFractPair.of (↑fr)⁻¹
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (Nat.succ n)) = IntFractPair.stream v (Nat.succ n)
[PROOFSTEP]
simpa [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq, fr_ne_zero]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ Stream'.map (Option.map (mapFr Rat.cast)) (IntFractPair.stream q) = IntFractPair.stream v
[PROOFSTEP]
funext n
[GOAL]
case h
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
⊢ Stream'.map (Option.map (mapFr Rat.cast)) (IntFractPair.stream q) n = IntFractPair.stream v n
[PROOFSTEP]
exact IntFractPair.coe_stream_nth_rat_eq v_eq_q n
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ ↑(of q).h = (of v).h
[PROOFSTEP]
unfold of IntFractPair.seq1
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ ↑(match
          (IntFractPair.of q,
            Stream'.Seq.tail
              { val := IntFractPair.stream q, property := (_ : Stream'.IsSeq (IntFractPair.stream q)) }) with
        | (h, s) => { h := ↑h.b, s := Stream'.Seq.map (fun p => { a := 1, b := ↑p.b }) s }).h =
    (match
        (IntFractPair.of v,
          Stream'.Seq.tail
            { val := IntFractPair.stream v, property := (_ : Stream'.IsSeq (IntFractPair.stream v)) }) with
      | (h, s) => { h := ↑h.b, s := Stream'.Seq.map (fun p => { a := 1, b := ↑p.b }) s }).h
[PROOFSTEP]
rw [← IntFractPair.coe_of_rat_eq v_eq_q]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ ↑(match
          (IntFractPair.of q,
            Stream'.Seq.tail
              { val := IntFractPair.stream q, property := (_ : Stream'.IsSeq (IntFractPair.stream q)) }) with
        | (h, s) => { h := ↑h.b, s := Stream'.Seq.map (fun p => { a := 1, b := ↑p.b }) s }).h =
    (match
        (IntFractPair.mapFr Rat.cast (IntFractPair.of q),
          Stream'.Seq.tail
            { val := IntFractPair.stream v, property := (_ : Stream'.IsSeq (IntFractPair.stream v)) }) with
      | (h, s) => { h := ↑h.b, s := Stream'.Seq.map (fun p => { a := 1, b := ↑p.b }) s }).h
[PROOFSTEP]
simp
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ Option.map (Pair.map Rat.cast) (Stream'.Seq.get? (of q).s n) = Stream'.Seq.get? (of v).s n
[PROOFSTEP]
simp only [of, IntFractPair.seq1, Stream'.Seq.map_get?, Stream'.Seq.get?_tail]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ Option.map (Pair.map Rat.cast)
      (Option.map (fun p => { a := 1, b := ↑p.b })
        (Stream'.Seq.get? { val := IntFractPair.stream q, property := (_ : Stream'.IsSeq (IntFractPair.stream q)) }
          (n + 1))) =
    Option.map (fun p => { a := 1, b := ↑p.b })
      (Stream'.Seq.get? { val := IntFractPair.stream v, property := (_ : Stream'.IsSeq (IntFractPair.stream v)) }
        (n + 1))
[PROOFSTEP]
simp only [Stream'.Seq.get?]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ Option.map (Pair.map Rat.cast) (Option.map (fun p => { a := 1, b := ↑p.b }) (IntFractPair.stream q (n + 1))) =
    Option.map (fun p => { a := 1, b := ↑p.b }) (IntFractPair.stream v (n + 1))
[PROOFSTEP]
rw [← IntFractPair.coe_stream'_rat_eq v_eq_q]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ Option.map (Pair.map Rat.cast) (Option.map (fun p => { a := 1, b := ↑p.b }) (IntFractPair.stream q (n + 1))) =
    Option.map (fun p => { a := 1, b := ↑p.b })
      (Stream'.map (Option.map (IntFractPair.mapFr Rat.cast)) (IntFractPair.stream q) (n + 1))
[PROOFSTEP]
rcases succ_nth_stream_eq : IntFractPair.stream q (n + 1) with (_ | ⟨_, _⟩)
[GOAL]
case none
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
succ_nth_stream_eq : IntFractPair.stream q (n + 1) = none
⊢ Option.map (Pair.map Rat.cast) (Option.map (fun p => { a := 1, b := ↑p.b }) none) =
    Option.map (fun p => { a := 1, b := ↑p.b })
      (Stream'.map (Option.map (IntFractPair.mapFr Rat.cast)) (IntFractPair.stream q) (n + 1))
[PROOFSTEP]
simp [Stream'.map, Stream'.nth, succ_nth_stream_eq]
[GOAL]
case some.mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
b✝ : ℤ
fr✝ : ℚ
succ_nth_stream_eq : IntFractPair.stream q (n + 1) = some { b := b✝, fr := fr✝ }
⊢ Option.map (Pair.map Rat.cast) (Option.map (fun p => { a := 1, b := ↑p.b }) (some { b := b✝, fr := fr✝ })) =
    Option.map (fun p => { a := 1, b := ↑p.b })
      (Stream'.map (Option.map (IntFractPair.mapFr Rat.cast)) (IntFractPair.stream q) (n + 1))
[PROOFSTEP]
simp [Stream'.map, Stream'.nth, succ_nth_stream_eq]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ Stream'.Seq.map (Pair.map Rat.cast) (of q).s = (of v).s
[PROOFSTEP]
ext n
[GOAL]
case h.a
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
a✝ : Pair K
⊢ a✝ ∈ Stream'.Seq.get? (Stream'.Seq.map (Pair.map Rat.cast) (of q).s) n ↔ a✝ ∈ Stream'.Seq.get? (of v).s n
[PROOFSTEP]
rw [← coe_of_s_get?_rat_eq v_eq_q]
[GOAL]
case h.a
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
a✝ : Pair K
⊢ a✝ ∈ Stream'.Seq.get? (Stream'.Seq.map (Pair.map Rat.cast) (of q).s) n ↔
    a✝ ∈ Option.map (Pair.map Rat.cast) (Stream'.Seq.get? (of q).s n)
[PROOFSTEP]
rfl
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ { h := ↑(of q).h, s := Stream'.Seq.map (Pair.map Rat.cast) (of q).s } = of v
[PROOFSTEP]
cases' gcf_v_eq : of v with h s
[GOAL]
case mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
h : K
s : Stream'.Seq (Pair K)
gcf_v_eq : of v = { h := h, s := s }
⊢ { h := ↑(of q).h, s := Stream'.Seq.map (Pair.map Rat.cast) (of q).s } = { h := h, s := s }
[PROOFSTEP]
subst v
[GOAL]
case mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n : ℕ
h : K
s : Stream'.Seq (Pair K)
gcf_v_eq : of ↑q = { h := h, s := s }
⊢ { h := ↑(of q).h, s := Stream'.Seq.map (Pair.map Rat.cast) (of q).s } = { h := h, s := s }
[PROOFSTEP]
obtain rfl : ↑⌊(q : K)⌋ = h := by injection gcf_v_eq
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n : ℕ
h : K
s : Stream'.Seq (Pair K)
gcf_v_eq : of ↑q = { h := h, s := s }
⊢ ↑⌊↑q⌋ = h
[PROOFSTEP]
injection gcf_v_eq
[GOAL]
case mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n : ℕ
s : Stream'.Seq (Pair K)
gcf_v_eq : of ↑q = { h := ↑⌊↑q⌋, s := s }
⊢ { h := ↑(of q).h, s := Stream'.Seq.map (Pair.map Rat.cast) (of q).s } = { h := ↑⌊↑q⌋, s := s }
[PROOFSTEP]
simp only [gcf_v_eq, Int.cast_inj, Rat.floor_cast, of_h_eq_floor, eq_self_iff_true, Rat.cast_coe_int, and_self,
  coe_of_h_rat_eq rfl, coe_of_s_rat_eq rfl]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
q✝ : ℚ
v_eq_q✝ : v✝ = ↑q✝
n : ℕ
v : K
q : ℚ
v_eq_q : v = ↑q
⊢ Terminates (of v) ↔ Terminates (of q)
[PROOFSTEP]
constructor
[GOAL]
case mp
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
q✝ : ℚ
v_eq_q✝ : v✝ = ↑q✝
n : ℕ
v : K
q : ℚ
v_eq_q : v = ↑q
⊢ Terminates (of v) → Terminates (of q)
[PROOFSTEP]
intro h
[GOAL]
case mpr
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
q✝ : ℚ
v_eq_q✝ : v✝ = ↑q✝
n : ℕ
v : K
q : ℚ
v_eq_q : v = ↑q
⊢ Terminates (of q) → Terminates (of v)
[PROOFSTEP]
intro h
[GOAL]
case mp
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
q✝ : ℚ
v_eq_q✝ : v✝ = ↑q✝
n : ℕ
v : K
q : ℚ
v_eq_q : v = ↑q
h : Terminates (of v)
⊢ Terminates (of q)
[PROOFSTEP]
cases' h with n h
[GOAL]
case mpr
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
q✝ : ℚ
v_eq_q✝ : v✝ = ↑q✝
n : ℕ
v : K
q : ℚ
v_eq_q : v = ↑q
h : Terminates (of q)
⊢ Terminates (of v)
[PROOFSTEP]
cases' h with n h
[GOAL]
case mp.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
q✝ : ℚ
v_eq_q✝ : v✝ = ↑q✝
n✝ : ℕ
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
h : Stream'.Seq.TerminatedAt (of v).s n
⊢ Terminates (of q)
[PROOFSTEP]
use n
[GOAL]
case mpr.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
q✝ : ℚ
v_eq_q✝ : v✝ = ↑q✝
n✝ : ℕ
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
h : Stream'.Seq.TerminatedAt (of q).s n
⊢ Terminates (of v)
[PROOFSTEP]
use n
[GOAL]
case h
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
q✝ : ℚ
v_eq_q✝ : v✝ = ↑q✝
n✝ : ℕ
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
h : Stream'.Seq.TerminatedAt (of v).s n
⊢ Stream'.Seq.TerminatedAt (of q).s n
[PROOFSTEP]
simp only [Stream'.Seq.TerminatedAt, (coe_of_s_get?_rat_eq v_eq_q n).symm] at h ⊢
[GOAL]
case h
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
q✝ : ℚ
v_eq_q✝ : v✝ = ↑q✝
n✝ : ℕ
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
h : Stream'.Seq.TerminatedAt (of q).s n
⊢ Stream'.Seq.TerminatedAt (of v).s n
[PROOFSTEP]
simp only [Stream'.Seq.TerminatedAt, (coe_of_s_get?_rat_eq v_eq_q n).symm] at h ⊢
[GOAL]
case h
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
q✝ : ℚ
v_eq_q✝ : v✝ = ↑q✝
n✝ : ℕ
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
h : Option.map (Pair.map Rat.cast) (Stream'.Seq.get? (of q).s n) = none
⊢ Stream'.Seq.get? (of q).s n = none
[PROOFSTEP]
cases h' : (of q).s.get? n
[GOAL]
case h
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
q✝ : ℚ
v_eq_q✝ : v✝ = ↑q✝
n✝ : ℕ
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
h : Stream'.Seq.get? (of q).s n = none
⊢ Option.map (Pair.map Rat.cast) (Stream'.Seq.get? (of q).s n) = none
[PROOFSTEP]
cases h' : (of q).s.get? n
[GOAL]
case h.none
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
q✝ : ℚ
v_eq_q✝ : v✝ = ↑q✝
n✝ : ℕ
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
h : Option.map (Pair.map Rat.cast) (Stream'.Seq.get? (of q).s n) = none
h' : Stream'.Seq.get? (of q).s n = none
⊢ none = none
[PROOFSTEP]
simp only [h'] at h 
[GOAL]
case h.some
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
q✝ : ℚ
v_eq_q✝ : v✝ = ↑q✝
n✝ : ℕ
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
h : Option.map (Pair.map Rat.cast) (Stream'.Seq.get? (of q).s n) = none
val✝ : Pair ℚ
h' : Stream'.Seq.get? (of q).s n = some val✝
⊢ some val✝ = none
[PROOFSTEP]
simp only [h'] at h 
[GOAL]
case h.none
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
q✝ : ℚ
v_eq_q✝ : v✝ = ↑q✝
n✝ : ℕ
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
h h' : Stream'.Seq.get? (of q).s n = none
⊢ Option.map (Pair.map Rat.cast) none = none
[PROOFSTEP]
simp only [h'] at h 
[GOAL]
case h.some
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
q✝ : ℚ
v_eq_q✝ : v✝ = ↑q✝
n✝ : ℕ
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
h : Stream'.Seq.get? (of q).s n = none
val✝ : Pair ℚ
h' : Stream'.Seq.get? (of q).s n = some val✝
⊢ Option.map (Pair.map Rat.cast) (some val✝) = none
[PROOFSTEP]
simp only [h'] at h 
[GOAL]
case h.none
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
q✝ : ℚ
v_eq_q✝ : v✝ = ↑q✝
n✝ : ℕ
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
h' : Stream'.Seq.get? (of q).s n = none
h : Option.map (Pair.map Rat.cast) none = none
⊢ none = none
[PROOFSTEP]
trivial
[GOAL]
case h.some
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
q✝ : ℚ
v_eq_q✝ : v✝ = ↑q✝
n✝ : ℕ
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
val✝ : Pair ℚ
h' : Stream'.Seq.get? (of q).s n = some val✝
h : Option.map (Pair.map Rat.cast) (some val✝) = none
⊢ some val✝ = none
[PROOFSTEP]
trivial
[GOAL]
case h.none
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
q✝ : ℚ
v_eq_q✝ : v✝ = ↑q✝
n✝ : ℕ
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
h' : Stream'.Seq.get? (of q).s n = none
h : True
⊢ Option.map (Pair.map Rat.cast) none = none
[PROOFSTEP]
trivial
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n : ℕ
ifp_n ifp_succ_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n
⊢ ifp_succ_n.fr.num < ifp_n.fr.num
[PROOFSTEP]
obtain ⟨ifp_n', stream_nth_eq', ifp_n_fract_ne_zero, IntFractPair.of_eq_ifp_succ_n⟩ :
  ∃ ifp_n', IntFractPair.stream q n = some ifp_n' ∧ ifp_n'.fr ≠ 0 ∧ IntFractPair.of ifp_n'.fr⁻¹ = ifp_succ_n
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n : ℕ
ifp_n ifp_succ_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n
⊢ ∃ ifp_n', IntFractPair.stream q n = some ifp_n' ∧ ifp_n'.fr ≠ 0 ∧ IntFractPair.of ifp_n'.fr⁻¹ = ifp_succ_n
case intro.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n : ℕ
ifp_n ifp_succ_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n
ifp_n' : IntFractPair ℚ
stream_nth_eq' : IntFractPair.stream q n = some ifp_n'
ifp_n_fract_ne_zero : ifp_n'.fr ≠ 0
IntFractPair.of_eq_ifp_succ_n : IntFractPair.of ifp_n'.fr⁻¹ = ifp_succ_n
⊢ ifp_succ_n.fr.num < ifp_n.fr.num
[PROOFSTEP]
exact succ_nth_stream_eq_some_iff.mp stream_succ_nth_eq
[GOAL]
case intro.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n : ℕ
ifp_n ifp_succ_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n
ifp_n' : IntFractPair ℚ
stream_nth_eq' : IntFractPair.stream q n = some ifp_n'
ifp_n_fract_ne_zero : ifp_n'.fr ≠ 0
IntFractPair.of_eq_ifp_succ_n : IntFractPair.of ifp_n'.fr⁻¹ = ifp_succ_n
⊢ ifp_succ_n.fr.num < ifp_n.fr.num
[PROOFSTEP]
have : ifp_n = ifp_n' := by injection Eq.trans stream_nth_eq.symm stream_nth_eq'
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n : ℕ
ifp_n ifp_succ_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n
ifp_n' : IntFractPair ℚ
stream_nth_eq' : IntFractPair.stream q n = some ifp_n'
ifp_n_fract_ne_zero : ifp_n'.fr ≠ 0
IntFractPair.of_eq_ifp_succ_n : IntFractPair.of ifp_n'.fr⁻¹ = ifp_succ_n
⊢ ifp_n = ifp_n'
[PROOFSTEP]
injection Eq.trans stream_nth_eq.symm stream_nth_eq'
[GOAL]
case intro.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n : ℕ
ifp_n ifp_succ_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n
ifp_n' : IntFractPair ℚ
stream_nth_eq' : IntFractPair.stream q n = some ifp_n'
ifp_n_fract_ne_zero : ifp_n'.fr ≠ 0
IntFractPair.of_eq_ifp_succ_n : IntFractPair.of ifp_n'.fr⁻¹ = ifp_succ_n
this : ifp_n = ifp_n'
⊢ ifp_succ_n.fr.num < ifp_n.fr.num
[PROOFSTEP]
cases this
[GOAL]
case intro.intro.intro.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n : ℕ
ifp_n ifp_succ_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n
stream_nth_eq' : IntFractPair.stream q n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
IntFractPair.of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
⊢ ifp_succ_n.fr.num < ifp_n.fr.num
[PROOFSTEP]
rw [← IntFractPair.of_eq_ifp_succ_n]
[GOAL]
case intro.intro.intro.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n : ℕ
ifp_n ifp_succ_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n
stream_nth_eq' : IntFractPair.stream q n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
IntFractPair.of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
⊢ (IntFractPair.of ifp_n.fr⁻¹).fr.num < ifp_n.fr.num
[PROOFSTEP]
cases' nth_stream_fr_nonneg_lt_one stream_nth_eq with zero_le_ifp_n_fract ifp_n_fract_lt_one
[GOAL]
case intro.intro.intro.refl.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n : ℕ
ifp_n ifp_succ_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n
stream_nth_eq' : IntFractPair.stream q n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
IntFractPair.of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
zero_le_ifp_n_fract : 0 ≤ ifp_n.fr
ifp_n_fract_lt_one : ifp_n.fr < 1
⊢ (IntFractPair.of ifp_n.fr⁻¹).fr.num < ifp_n.fr.num
[PROOFSTEP]
have : 0 < ifp_n.fr := lt_of_le_of_ne zero_le_ifp_n_fract <| ifp_n_fract_ne_zero.symm
[GOAL]
case intro.intro.intro.refl.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n : ℕ
ifp_n ifp_succ_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n
stream_nth_eq' : IntFractPair.stream q n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
IntFractPair.of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
zero_le_ifp_n_fract : 0 ≤ ifp_n.fr
ifp_n_fract_lt_one : ifp_n.fr < 1
this : 0 < ifp_n.fr
⊢ (IntFractPair.of ifp_n.fr⁻¹).fr.num < ifp_n.fr.num
[PROOFSTEP]
exact of_inv_fr_num_lt_num_of_pos this
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n : ℕ
⊢ ∀ {ifp_n : IntFractPair ℚ}, IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑n
[PROOFSTEP]
induction' n with n IH
[GOAL]
case zero
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n : ℕ
⊢ ∀ {ifp_n : IntFractPair ℚ},
    IntFractPair.stream q Nat.zero = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑Nat.zero
case succ
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n✝ n : ℕ
IH : ∀ {ifp_n : IntFractPair ℚ}, IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑n
⊢ ∀ {ifp_n : IntFractPair ℚ},
    IntFractPair.stream q (Nat.succ n) = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑(Nat.succ n)
[PROOFSTEP]
case zero =>
  intro ifp_zero stream_zero_eq
  have : IntFractPair.of q = ifp_zero := by injection stream_zero_eq
  simp [le_refl, this.symm]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n : ℕ
⊢ ∀ {ifp_n : IntFractPair ℚ},
    IntFractPair.stream q Nat.zero = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑Nat.zero
[PROOFSTEP]
case zero =>
  intro ifp_zero stream_zero_eq
  have : IntFractPair.of q = ifp_zero := by injection stream_zero_eq
  simp [le_refl, this.symm]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n : ℕ
⊢ ∀ {ifp_n : IntFractPair ℚ},
    IntFractPair.stream q Nat.zero = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑Nat.zero
[PROOFSTEP]
intro ifp_zero stream_zero_eq
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n : ℕ
ifp_zero : IntFractPair ℚ
stream_zero_eq : IntFractPair.stream q Nat.zero = some ifp_zero
⊢ ifp_zero.fr.num ≤ (IntFractPair.of q).fr.num - ↑Nat.zero
[PROOFSTEP]
have : IntFractPair.of q = ifp_zero := by injection stream_zero_eq
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n : ℕ
ifp_zero : IntFractPair ℚ
stream_zero_eq : IntFractPair.stream q Nat.zero = some ifp_zero
⊢ IntFractPair.of q = ifp_zero
[PROOFSTEP]
injection stream_zero_eq
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n : ℕ
ifp_zero : IntFractPair ℚ
stream_zero_eq : IntFractPair.stream q Nat.zero = some ifp_zero
this : IntFractPair.of q = ifp_zero
⊢ ifp_zero.fr.num ≤ (IntFractPair.of q).fr.num - ↑Nat.zero
[PROOFSTEP]
simp [le_refl, this.symm]
[GOAL]
case succ
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n✝ n : ℕ
IH : ∀ {ifp_n : IntFractPair ℚ}, IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑n
⊢ ∀ {ifp_n : IntFractPair ℚ},
    IntFractPair.stream q (Nat.succ n) = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑(Nat.succ n)
[PROOFSTEP]
case succ =>
  intro ifp_succ_n stream_succ_nth_eq
  suffices ifp_succ_n.fr.num + 1 ≤ (IntFractPair.of q).fr.num - n
    by
    rw [Int.ofNat_succ, sub_add_eq_sub_sub]
    solve_by_elim [le_sub_right_of_add_le]
  rcases succ_nth_stream_eq_some_iff.mp stream_succ_nth_eq with ⟨ifp_n, stream_nth_eq, -⟩
  have : ifp_succ_n.fr.num < ifp_n.fr.num := stream_succ_nth_fr_num_lt_nth_fr_num_rat stream_nth_eq stream_succ_nth_eq
  have : ifp_succ_n.fr.num + 1 ≤ ifp_n.fr.num := Int.add_one_le_of_lt this
  exact le_trans this (IH stream_nth_eq)
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n✝ n : ℕ
IH : ∀ {ifp_n : IntFractPair ℚ}, IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑n
⊢ ∀ {ifp_n : IntFractPair ℚ},
    IntFractPair.stream q (Nat.succ n) = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑(Nat.succ n)
[PROOFSTEP]
case succ =>
  intro ifp_succ_n stream_succ_nth_eq
  suffices ifp_succ_n.fr.num + 1 ≤ (IntFractPair.of q).fr.num - n
    by
    rw [Int.ofNat_succ, sub_add_eq_sub_sub]
    solve_by_elim [le_sub_right_of_add_le]
  rcases succ_nth_stream_eq_some_iff.mp stream_succ_nth_eq with ⟨ifp_n, stream_nth_eq, -⟩
  have : ifp_succ_n.fr.num < ifp_n.fr.num := stream_succ_nth_fr_num_lt_nth_fr_num_rat stream_nth_eq stream_succ_nth_eq
  have : ifp_succ_n.fr.num + 1 ≤ ifp_n.fr.num := Int.add_one_le_of_lt this
  exact le_trans this (IH stream_nth_eq)
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n✝ n : ℕ
IH : ∀ {ifp_n : IntFractPair ℚ}, IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑n
⊢ ∀ {ifp_n : IntFractPair ℚ},
    IntFractPair.stream q (Nat.succ n) = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑(Nat.succ n)
[PROOFSTEP]
intro ifp_succ_n stream_succ_nth_eq
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n✝ n : ℕ
IH : ∀ {ifp_n : IntFractPair ℚ}, IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑n
ifp_succ_n : IntFractPair ℚ
stream_succ_nth_eq : IntFractPair.stream q (Nat.succ n) = some ifp_succ_n
⊢ ifp_succ_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑(Nat.succ n)
[PROOFSTEP]
suffices ifp_succ_n.fr.num + 1 ≤ (IntFractPair.of q).fr.num - n
  by
  rw [Int.ofNat_succ, sub_add_eq_sub_sub]
  solve_by_elim [le_sub_right_of_add_le]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n✝ n : ℕ
IH : ∀ {ifp_n : IntFractPair ℚ}, IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑n
ifp_succ_n : IntFractPair ℚ
stream_succ_nth_eq : IntFractPair.stream q (Nat.succ n) = some ifp_succ_n
this : ifp_succ_n.fr.num + 1 ≤ (IntFractPair.of q).fr.num - ↑n
⊢ ifp_succ_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑(Nat.succ n)
[PROOFSTEP]
rw [Int.ofNat_succ, sub_add_eq_sub_sub]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n✝ n : ℕ
IH : ∀ {ifp_n : IntFractPair ℚ}, IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑n
ifp_succ_n : IntFractPair ℚ
stream_succ_nth_eq : IntFractPair.stream q (Nat.succ n) = some ifp_succ_n
this : ifp_succ_n.fr.num + 1 ≤ (IntFractPair.of q).fr.num - ↑n
⊢ ifp_succ_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑n - 1
[PROOFSTEP]
solve_by_elim [le_sub_right_of_add_le]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n✝ n : ℕ
IH : ∀ {ifp_n : IntFractPair ℚ}, IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑n
ifp_succ_n : IntFractPair ℚ
stream_succ_nth_eq : IntFractPair.stream q (Nat.succ n) = some ifp_succ_n
⊢ ifp_succ_n.fr.num + 1 ≤ (IntFractPair.of q).fr.num - ↑n
[PROOFSTEP]
rcases succ_nth_stream_eq_some_iff.mp stream_succ_nth_eq with ⟨ifp_n, stream_nth_eq, -⟩
[GOAL]
case intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n✝ n : ℕ
IH : ∀ {ifp_n : IntFractPair ℚ}, IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑n
ifp_succ_n : IntFractPair ℚ
stream_succ_nth_eq : IntFractPair.stream q (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
⊢ ifp_succ_n.fr.num + 1 ≤ (IntFractPair.of q).fr.num - ↑n
[PROOFSTEP]
have : ifp_succ_n.fr.num < ifp_n.fr.num := stream_succ_nth_fr_num_lt_nth_fr_num_rat stream_nth_eq stream_succ_nth_eq
[GOAL]
case intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n✝ n : ℕ
IH : ∀ {ifp_n : IntFractPair ℚ}, IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑n
ifp_succ_n : IntFractPair ℚ
stream_succ_nth_eq : IntFractPair.stream q (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
this : ifp_succ_n.fr.num < ifp_n.fr.num
⊢ ifp_succ_n.fr.num + 1 ≤ (IntFractPair.of q).fr.num - ↑n
[PROOFSTEP]
have : ifp_succ_n.fr.num + 1 ≤ ifp_n.fr.num := Int.add_one_le_of_lt this
[GOAL]
case intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n✝ n : ℕ
IH : ∀ {ifp_n : IntFractPair ℚ}, IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑n
ifp_succ_n : IntFractPair ℚ
stream_succ_nth_eq : IntFractPair.stream q (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
this✝ : ifp_succ_n.fr.num < ifp_n.fr.num
this : ifp_succ_n.fr.num + 1 ≤ ifp_n.fr.num
⊢ ifp_succ_n.fr.num + 1 ≤ (IntFractPair.of q).fr.num - ↑n
[PROOFSTEP]
exact le_trans this (IH stream_nth_eq)
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q✝ : ℚ
n : ℕ
q : ℚ
⊢ ∃ n, IntFractPair.stream q n = none
[PROOFSTEP]
let fract_q_num := (Int.fract q).num
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q✝ : ℚ
n : ℕ
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
⊢ ∃ n, IntFractPair.stream q n = none
[PROOFSTEP]
let n := fract_q_num.natAbs + 1
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q✝ : ℚ
n✝ : ℕ
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
n : ℕ := Int.natAbs fract_q_num + 1
⊢ ∃ n, IntFractPair.stream q n = none
[PROOFSTEP]
cases' stream_nth_eq : IntFractPair.stream q n with ifp
[GOAL]
case none
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q✝ : ℚ
n✝ : ℕ
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
n : ℕ := Int.natAbs fract_q_num + 1
stream_nth_eq : IntFractPair.stream q n = none
⊢ ∃ n, IntFractPair.stream q n = none
[PROOFSTEP]
use n, stream_nth_eq
[GOAL]
case some
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q✝ : ℚ
n✝ : ℕ
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
n : ℕ := Int.natAbs fract_q_num + 1
ifp : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp
⊢ ∃ n, IntFractPair.stream q n = none
[PROOFSTEP]
have ifp_fr_num_le_q_fr_num_sub_n : ifp.fr.num ≤ fract_q_num - n := stream_nth_fr_num_le_fr_num_sub_n_rat stream_nth_eq
[GOAL]
case some
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q✝ : ℚ
n✝ : ℕ
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
n : ℕ := Int.natAbs fract_q_num + 1
ifp : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp
ifp_fr_num_le_q_fr_num_sub_n : ifp.fr.num ≤ fract_q_num - ↑n
⊢ ∃ n, IntFractPair.stream q n = none
[PROOFSTEP]
have : fract_q_num - n = -1 :=
  by
  have : 0 ≤ fract_q_num :=
    Rat.num_nonneg_iff_zero_le.mpr
      (Int.fract_nonneg q)
        -- Porting note: was
              -- simp [Int.natAbs_of_nonneg this, sub_add_eq_sub_sub_swap, sub_right_comm]
  simp only [Nat.cast_add, Int.natAbs_of_nonneg this, Nat.cast_one, sub_add_eq_sub_sub_swap, sub_right_comm, sub_self,
    zero_sub]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q✝ : ℚ
n✝ : ℕ
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
n : ℕ := Int.natAbs fract_q_num + 1
ifp : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp
ifp_fr_num_le_q_fr_num_sub_n : ifp.fr.num ≤ fract_q_num - ↑n
⊢ fract_q_num - ↑n = -1
[PROOFSTEP]
have : 0 ≤ fract_q_num :=
  Rat.num_nonneg_iff_zero_le.mpr
    (Int.fract_nonneg q)
      -- Porting note: was
            -- simp [Int.natAbs_of_nonneg this, sub_add_eq_sub_sub_swap, sub_right_comm]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q✝ : ℚ
n✝ : ℕ
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
n : ℕ := Int.natAbs fract_q_num + 1
ifp : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp
ifp_fr_num_le_q_fr_num_sub_n : ifp.fr.num ≤ fract_q_num - ↑n
this : 0 ≤ fract_q_num
⊢ fract_q_num - ↑n = -1
[PROOFSTEP]
simp only [Nat.cast_add, Int.natAbs_of_nonneg this, Nat.cast_one, sub_add_eq_sub_sub_swap, sub_right_comm, sub_self,
  zero_sub]
[GOAL]
case some
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q✝ : ℚ
n✝ : ℕ
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
n : ℕ := Int.natAbs fract_q_num + 1
ifp : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp
ifp_fr_num_le_q_fr_num_sub_n : ifp.fr.num ≤ fract_q_num - ↑n
this : fract_q_num - ↑n = -1
⊢ ∃ n, IntFractPair.stream q n = none
[PROOFSTEP]
have : 0 ≤ ifp.fr := (nth_stream_fr_nonneg_lt_one stream_nth_eq).left
[GOAL]
case some
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q✝ : ℚ
n✝ : ℕ
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
n : ℕ := Int.natAbs fract_q_num + 1
ifp : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp
ifp_fr_num_le_q_fr_num_sub_n : ifp.fr.num ≤ fract_q_num - ↑n
this✝ : fract_q_num - ↑n = -1
this : 0 ≤ ifp.fr
⊢ ∃ n, IntFractPair.stream q n = none
[PROOFSTEP]
have : 0 ≤ ifp.fr.num := Rat.num_nonneg_iff_zero_le.mpr this
[GOAL]
case some
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q✝ : ℚ
n✝ : ℕ
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
n : ℕ := Int.natAbs fract_q_num + 1
ifp : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp
ifp_fr_num_le_q_fr_num_sub_n : ifp.fr.num ≤ fract_q_num - ↑n
this✝¹ : fract_q_num - ↑n = -1
this✝ : 0 ≤ ifp.fr
this : 0 ≤ ifp.fr.num
⊢ ∃ n, IntFractPair.stream q n = none
[PROOFSTEP]
linarith
