[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
nth_fr_eq_zero : ifp_n.fr = 0
⊢ IntFractPair.stream v (n + 1) = none
[PROOFSTEP]
cases' ifp_n with _ fr
[GOAL]
case mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
b✝ : ℤ
fr : K
stream_nth_eq : IntFractPair.stream v n = some { b := b✝, fr := fr }
nth_fr_eq_zero : { b := b✝, fr := fr }.fr = 0
⊢ IntFractPair.stream v (n + 1) = none
[PROOFSTEP]
change fr = 0 at nth_fr_eq_zero 
[GOAL]
case mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
b✝ : ℤ
fr : K
stream_nth_eq : IntFractPair.stream v n = some { b := b✝, fr := fr }
nth_fr_eq_zero : fr = 0
⊢ IntFractPair.stream v (n + 1) = none
[PROOFSTEP]
simp [IntFractPair.stream, stream_nth_eq, nth_fr_eq_zero]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ IntFractPair.stream v (n + 1) = none ↔
    IntFractPair.stream v n = none ∨ ∃ ifp, IntFractPair.stream v n = some ifp ∧ ifp.fr = 0
[PROOFSTEP]
rw [IntFractPair.stream]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ (Option.bind (IntFractPair.stream v n) fun ap_n => if ap_n.fr = 0 then none else some (IntFractPair.of ap_n.fr⁻¹)) =
      none ↔
    IntFractPair.stream v n = none ∨ ∃ ifp, IntFractPair.stream v n = some ifp ∧ ifp.fr = 0
[PROOFSTEP]
cases IntFractPair.stream v n
[GOAL]
case none
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ (Option.bind none fun ap_n => if ap_n.fr = 0 then none else some (IntFractPair.of ap_n.fr⁻¹)) = none ↔
    none = none ∨ ∃ ifp, none = some ifp ∧ ifp.fr = 0
[PROOFSTEP]
simp [imp_false]
[GOAL]
case some
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
val✝ : IntFractPair K
⊢ (Option.bind (some val✝) fun ap_n => if ap_n.fr = 0 then none else some (IntFractPair.of ap_n.fr⁻¹)) = none ↔
    some val✝ = none ∨ ∃ ifp, some val✝ = some ifp ∧ ifp.fr = 0
[PROOFSTEP]
simp [imp_false]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
ifp_succ_n : IntFractPair K
⊢ IntFractPair.stream v (n + 1) = some ifp_succ_n ↔
    ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr ≠ 0 ∧ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
[PROOFSTEP]
simp [IntFractPair.stream, ite_eq_iff]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
a : ℤ
n : ℕ
⊢ IntFractPair.stream (↑a) (n + 1) = none
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
a : ℤ
⊢ IntFractPair.stream (↑a) (Nat.zero + 1) = none
[PROOFSTEP]
refine' IntFractPair.stream_eq_none_of_fr_eq_zero (IntFractPair.stream_zero (a : K)) _
[GOAL]
case zero
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
a : ℤ
⊢ (IntFractPair.of ↑a).fr = 0
[PROOFSTEP]
simp only [IntFractPair.of, Int.fract_intCast]
[GOAL]
case succ
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
a : ℤ
n : ℕ
ih : IntFractPair.stream (↑a) (n + 1) = none
⊢ IntFractPair.stream (↑a) (Nat.succ n + 1) = none
[PROOFSTEP]
exact IntFractPair.succ_nth_stream_eq_none_iff.mpr (Or.inl ih)
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
ifp_succ_n : IntFractPair K
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
succ_nth_fr_eq_zero : ifp_succ_n.fr = 0
⊢ ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr⁻¹ = ↑⌊ifp_n.fr⁻¹⌋
[PROOFSTEP]
rcases succ_nth_stream_eq_some_iff.mp stream_succ_nth_eq with ⟨ifp_n, seq_nth_eq, _, rfl⟩
[GOAL]
case intro.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
ifp_n : IntFractPair K
seq_nth_eq : IntFractPair.stream v n = some ifp_n
left✝ : ifp_n.fr ≠ 0
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
succ_nth_fr_eq_zero : (IntFractPair.of ifp_n.fr⁻¹).fr = 0
⊢ ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr⁻¹ = ↑⌊ifp_n.fr⁻¹⌋
[PROOFSTEP]
refine' ⟨ifp_n, seq_nth_eq, _⟩
[GOAL]
case intro.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
ifp_n : IntFractPair K
seq_nth_eq : IntFractPair.stream v n = some ifp_n
left✝ : ifp_n.fr ≠ 0
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
succ_nth_fr_eq_zero : (IntFractPair.of ifp_n.fr⁻¹).fr = 0
⊢ ifp_n.fr⁻¹ = ↑⌊ifp_n.fr⁻¹⌋
[PROOFSTEP]
simpa only [IntFractPair.of, Int.fract, sub_eq_zero] using succ_nth_fr_eq_zero
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
h : Int.fract v ≠ 0
n : ℕ
⊢ IntFractPair.stream v (n + 1) = IntFractPair.stream (Int.fract v)⁻¹ n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
h : Int.fract v ≠ 0
⊢ IntFractPair.stream v (Nat.zero + 1) = IntFractPair.stream (Int.fract v)⁻¹ Nat.zero
[PROOFSTEP]
have H : (IntFractPair.of v).fr = Int.fract v := rfl
[GOAL]
case zero
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
h : Int.fract v ≠ 0
H : (IntFractPair.of v).fr = Int.fract v
⊢ IntFractPair.stream v (Nat.zero + 1) = IntFractPair.stream (Int.fract v)⁻¹ Nat.zero
[PROOFSTEP]
rw [stream_zero, stream_succ_of_some (stream_zero v) (ne_of_eq_of_ne H h), H]
[GOAL]
case succ
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
h : Int.fract v ≠ 0
n : ℕ
ih : IntFractPair.stream v (n + 1) = IntFractPair.stream (Int.fract v)⁻¹ n
⊢ IntFractPair.stream v (Nat.succ n + 1) = IntFractPair.stream (Int.fract v)⁻¹ (Nat.succ n)
[PROOFSTEP]
cases' eq_or_ne (IntFractPair.stream (Int.fract v)⁻¹ n) none with hnone hsome
[GOAL]
case succ.inl
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
h : Int.fract v ≠ 0
n : ℕ
ih : IntFractPair.stream v (n + 1) = IntFractPair.stream (Int.fract v)⁻¹ n
hnone : IntFractPair.stream (Int.fract v)⁻¹ n = none
⊢ IntFractPair.stream v (Nat.succ n + 1) = IntFractPair.stream (Int.fract v)⁻¹ (Nat.succ n)
[PROOFSTEP]
rw [hnone] at ih 
[GOAL]
case succ.inl
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
h : Int.fract v ≠ 0
n : ℕ
ih : IntFractPair.stream v (n + 1) = none
hnone : IntFractPair.stream (Int.fract v)⁻¹ n = none
⊢ IntFractPair.stream v (Nat.succ n + 1) = IntFractPair.stream (Int.fract v)⁻¹ (Nat.succ n)
[PROOFSTEP]
rw [succ_nth_stream_eq_none_iff.mpr (Or.inl hnone), succ_nth_stream_eq_none_iff.mpr (Or.inl ih)]
[GOAL]
case succ.inr
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
h : Int.fract v ≠ 0
n : ℕ
ih : IntFractPair.stream v (n + 1) = IntFractPair.stream (Int.fract v)⁻¹ n
hsome : IntFractPair.stream (Int.fract v)⁻¹ n ≠ none
⊢ IntFractPair.stream v (Nat.succ n + 1) = IntFractPair.stream (Int.fract v)⁻¹ (Nat.succ n)
[PROOFSTEP]
obtain ⟨p, hp⟩ := Option.ne_none_iff_exists'.mp hsome
[GOAL]
case succ.inr.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
h : Int.fract v ≠ 0
n : ℕ
ih : IntFractPair.stream v (n + 1) = IntFractPair.stream (Int.fract v)⁻¹ n
hsome : IntFractPair.stream (Int.fract v)⁻¹ n ≠ none
p : IntFractPair K
hp : IntFractPair.stream (Int.fract v)⁻¹ n = some p
⊢ IntFractPair.stream v (Nat.succ n + 1) = IntFractPair.stream (Int.fract v)⁻¹ (Nat.succ n)
[PROOFSTEP]
rw [hp] at ih 
[GOAL]
case succ.inr.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
h : Int.fract v ≠ 0
n : ℕ
hsome : IntFractPair.stream (Int.fract v)⁻¹ n ≠ none
p : IntFractPair K
ih : IntFractPair.stream v (n + 1) = some p
hp : IntFractPair.stream (Int.fract v)⁻¹ n = some p
⊢ IntFractPair.stream v (Nat.succ n + 1) = IntFractPair.stream (Int.fract v)⁻¹ (Nat.succ n)
[PROOFSTEP]
cases' eq_or_ne p.fr 0 with hz hnz
[GOAL]
case succ.inr.intro.inl
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
h : Int.fract v ≠ 0
n : ℕ
hsome : IntFractPair.stream (Int.fract v)⁻¹ n ≠ none
p : IntFractPair K
ih : IntFractPair.stream v (n + 1) = some p
hp : IntFractPair.stream (Int.fract v)⁻¹ n = some p
hz : p.fr = 0
⊢ IntFractPair.stream v (Nat.succ n + 1) = IntFractPair.stream (Int.fract v)⁻¹ (Nat.succ n)
[PROOFSTEP]
rw [stream_eq_none_of_fr_eq_zero hp hz, stream_eq_none_of_fr_eq_zero ih hz]
[GOAL]
case succ.inr.intro.inr
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
h : Int.fract v ≠ 0
n : ℕ
hsome : IntFractPair.stream (Int.fract v)⁻¹ n ≠ none
p : IntFractPair K
ih : IntFractPair.stream v (n + 1) = some p
hp : IntFractPair.stream (Int.fract v)⁻¹ n = some p
hnz : p.fr ≠ 0
⊢ IntFractPair.stream v (Nat.succ n + 1) = IntFractPair.stream (Int.fract v)⁻¹ (Nat.succ n)
[PROOFSTEP]
rw [stream_succ_of_some hp hnz, stream_succ_of_some ih hnz]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
⊢ (of v).h = ↑(IntFractPair.seq1 v).fst.b
[PROOFSTEP]
cases aux_seq_eq : IntFractPair.seq1 v
[GOAL]
case mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
fst✝ : IntFractPair K
snd✝ : Stream'.Seq (IntFractPair K)
aux_seq_eq : IntFractPair.seq1 v = (fst✝, snd✝)
⊢ (of v).h = ↑(fst✝, snd✝).fst.b
[PROOFSTEP]
simp [of, aux_seq_eq]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
⊢ (of v).h = ↑⌊v⌋
[PROOFSTEP]
simp [of_h_eq_intFractPair_seq1_fst_b, IntFractPair.of]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ TerminatedAt (of v) n ↔ IntFractPair.stream v (n + 1) = none
[PROOFSTEP]
rw [of_terminatedAt_iff_intFractPair_seq1_terminatedAt, Stream'.Seq.TerminatedAt,
  IntFractPair.get?_seq1_eq_succ_get?_stream]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
gp_n : Pair K
s_nth_eq : Stream'.Seq.get? (of v).s n = some gp_n
⊢ ∃ ifp, IntFractPair.stream v (n + 1) = some ifp ∧ ↑ifp.b = gp_n.b
[PROOFSTEP]
obtain ⟨ifp, stream_succ_nth_eq, gp_n_eq⟩ :
  ∃ ifp, IntFractPair.stream v (n + 1) = some ifp ∧ Pair.mk 1 (ifp.b : K) = gp_n :=
  by
  unfold of IntFractPair.seq1 at s_nth_eq 
  simpa [Stream'.Seq.get?_tail, Stream'.Seq.map_get?] using s_nth_eq
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
gp_n : Pair K
s_nth_eq : Stream'.Seq.get? (of v).s n = some gp_n
⊢ ∃ ifp, IntFractPair.stream v (n + 1) = some ifp ∧ { a := 1, b := ↑ifp.b } = gp_n
[PROOFSTEP]
unfold of IntFractPair.seq1 at s_nth_eq 
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
gp_n : Pair K
s_nth_eq :
  Stream'.Seq.get?
      (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 }).s
      n =
    some gp_n
⊢ ∃ ifp, IntFractPair.stream v (n + 1) = some ifp ∧ { a := 1, b := ↑ifp.b } = gp_n
[PROOFSTEP]
simpa [Stream'.Seq.get?_tail, Stream'.Seq.map_get?] using s_nth_eq
[GOAL]
case intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
gp_n : Pair K
s_nth_eq : Stream'.Seq.get? (of v).s n = some gp_n
ifp : IntFractPair K
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp
gp_n_eq : { a := 1, b := ↑ifp.b } = gp_n
⊢ ∃ ifp, IntFractPair.stream v (n + 1) = some ifp ∧ ↑ifp.b = gp_n.b
[PROOFSTEP]
cases gp_n_eq
[GOAL]
case intro.intro.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
ifp : IntFractPair K
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp
s_nth_eq : Stream'.Seq.get? (of v).s n = some { a := 1, b := ↑ifp.b }
⊢ ∃ ifp_1, IntFractPair.stream v (n + 1) = some ifp_1 ∧ ↑ifp_1.b = { a := 1, b := ↑ifp.b }.b
[PROOFSTEP]
simp_all only [Option.some.injEq, exists_eq_left']
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
ifp_succ_n : IntFractPair K
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
⊢ Stream'.Seq.get? (of v).s n = some { a := 1, b := ↑ifp_succ_n.b }
[PROOFSTEP]
unfold of IntFractPair.seq1
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
ifp_succ_n : IntFractPair K
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
⊢ Stream'.Seq.get?
      (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 }).s
      n =
    some { a := 1, b := ↑ifp_succ_n.b }
[PROOFSTEP]
simp [Stream'.Seq.map_tail, Stream'.Seq.get?_tail, Stream'.Seq.map_get?, stream_succ_nth_eq]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
nth_fr_ne_zero : ifp_n.fr ≠ 0
⊢ IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
[PROOFSTEP]
cases ifp_n
[GOAL]
case mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
b✝ : ℤ
fr✝ : K
stream_nth_eq : IntFractPair.stream v n = some { b := b✝, fr := fr✝ }
nth_fr_ne_zero : { b := b✝, fr := fr✝ }.fr ≠ 0
⊢ IntFractPair.stream v (n + 1) = some (IntFractPair.of { b := b✝, fr := fr✝ }.fr⁻¹)
[PROOFSTEP]
simp [IntFractPair.stream, stream_nth_eq, nth_fr_ne_zero]
[GOAL]
case mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
b✝ : ℤ
fr✝ : K
stream_nth_eq : IntFractPair.stream v n = some { b := b✝, fr := fr✝ }
nth_fr_ne_zero : { b := b✝, fr := fr✝ }.fr ≠ 0
⊢ fr✝ = 0 → False
[PROOFSTEP]
intro
[GOAL]
case mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
b✝ : ℤ
fr✝ : K
stream_nth_eq : IntFractPair.stream v n = some { b := b✝, fr := fr✝ }
nth_fr_ne_zero : { b := b✝, fr := fr✝ }.fr ≠ 0
a✝ : fr✝ = 0
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
n : ℕ
v : K
⊢ Stream'.Seq.get? (of v).s 0 = Option.bind (IntFractPair.stream v 1) (some ∘ fun p => { a := 1, b := ↑p.b })
[PROOFSTEP]
rw [of, IntFractPair.seq1]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
n : ℕ
v : K
⊢ Stream'.Seq.get?
      (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 }).s
      0 =
    Option.bind (IntFractPair.stream v 1) (some ∘ fun p => { a := 1, b := ↑p.b })
[PROOFSTEP]
simp only [of, Stream'.Seq.map_tail, Stream'.Seq.map, Stream'.Seq.tail, Stream'.Seq.head, Stream'.Seq.get?, Stream'.map]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
n : ℕ
v : K
⊢ Option.map (fun p => { a := 1, b := ↑p.b }) (Stream'.nth (Stream'.tail (IntFractPair.stream v)) 0) =
    Option.bind (IntFractPair.stream v 1) (some ∘ fun p => { a := 1, b := ↑p.b })
[PROOFSTEP]
rw [← Stream'.nth_succ, Stream'.nth, Option.map]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
n : ℕ
v : K
⊢ (match IntFractPair.stream v (Nat.succ 0) with
    | some x => some { a := 1, b := ↑x.b }
    | none => none) =
    Option.bind (IntFractPair.stream v 1) (some ∘ fun p => { a := 1, b := ↑p.b })
[PROOFSTEP]
split
[GOAL]
case h_1
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
n : ℕ
v : K
x✝¹ : Option (IntFractPair K)
x✝ : IntFractPair K
heq✝ : IntFractPair.stream v (Nat.succ 0) = some x✝
⊢ some { a := 1, b := ↑x✝.b } = Option.bind (IntFractPair.stream v 1) (some ∘ fun p => { a := 1, b := ↑p.b })
[PROOFSTEP]
simp_all only [Option.some_bind, Option.none_bind, Function.comp_apply]
[GOAL]
case h_2
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
n : ℕ
v : K
x✝ : Option (IntFractPair K)
heq✝ : IntFractPair.stream v (Nat.succ 0) = none
⊢ none = Option.bind (IntFractPair.stream v 1) (some ∘ fun p => { a := 1, b := ↑p.b })
[PROOFSTEP]
simp_all only [Option.some_bind, Option.none_bind, Function.comp_apply]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
h : fract v ≠ 0
⊢ Stream'.Seq.head (of v).s = some { a := 1, b := ↑⌊(fract v)⁻¹⌋ }
[PROOFSTEP]
change (of v).s.get? 0 = _
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
h : fract v ≠ 0
⊢ Stream'.Seq.get? (of v).s 0 = some { a := 1, b := ↑⌊(fract v)⁻¹⌋ }
[PROOFSTEP]
rw [of_s_head_aux, stream_succ_of_some (stream_zero v) h, Option.bind]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
h : fract v ≠ 0
⊢ (match some (IntFractPair.of (IntFractPair.of v).fr⁻¹), some ∘ fun p => { a := 1, b := ↑p.b } with
    | none, x => none
    | some a, b => b a) =
    some { a := 1, b := ↑⌊(fract v)⁻¹⌋ }
[PROOFSTEP]
rfl
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
a : ℤ
⊢ ∀ (n : ℕ), Stream'.Seq.get? (of ↑a).s n = none
[PROOFSTEP]
intro n
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
a : ℤ
n : ℕ
⊢ Stream'.Seq.get? (of ↑a).s n = none
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
a : ℤ
⊢ Stream'.Seq.get? (of ↑a).s Nat.zero = none
[PROOFSTEP]
rw [of_s_head_aux, stream_succ_of_int, Option.bind]
[GOAL]
case succ
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
a : ℤ
n : ℕ
ih : Stream'.Seq.get? (of ↑a).s n = none
⊢ Stream'.Seq.get? (of ↑a).s (Nat.succ n) = none
[PROOFSTEP]
exact (of (a : K)).s.prop ih
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ n : ℕ
⊢ Stream'.Seq.get? (of v).s (n + 1) = Stream'.Seq.get? (of (fract v)⁻¹).s n
[PROOFSTEP]
cases' eq_or_ne (fract v) 0 with h h
[GOAL]
case inl
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ n : ℕ
h : fract v = 0
⊢ Stream'.Seq.get? (of v).s (n + 1) = Stream'.Seq.get? (of (fract v)⁻¹).s n
[PROOFSTEP]
obtain ⟨a, rfl⟩ : ∃ a : ℤ, v = a := ⟨⌊v⌋, eq_of_sub_eq_zero h⟩
[GOAL]
case inl.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
n✝ n : ℕ
a : ℤ
h : fract ↑a = 0
⊢ Stream'.Seq.get? (of ↑a).s (n + 1) = Stream'.Seq.get? (of (fract ↑a)⁻¹).s n
[PROOFSTEP]
rw [fract_intCast, inv_zero, of_s_of_int, ← cast_zero, of_s_of_int, Stream'.Seq.get?_nil, Stream'.Seq.get?_nil]
[GOAL]
case inr
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ n : ℕ
h : fract v ≠ 0
⊢ Stream'.Seq.get? (of v).s (n + 1) = Stream'.Seq.get? (of (fract v)⁻¹).s n
[PROOFSTEP]
cases' eq_or_ne ((of (fract v)⁻¹).s.get? n) none with h₁ h₁
[GOAL]
case inr.inl
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ n : ℕ
h : fract v ≠ 0
h₁ : Stream'.Seq.get? (of (fract v)⁻¹).s n = none
⊢ Stream'.Seq.get? (of v).s (n + 1) = Stream'.Seq.get? (of (fract v)⁻¹).s n
[PROOFSTEP]
rwa [h₁, ← terminatedAt_iff_s_none, of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none, stream_succ h, ←
  of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none, terminatedAt_iff_s_none]
[GOAL]
case inr.inr
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ n : ℕ
h : fract v ≠ 0
h₁ : Stream'.Seq.get? (of (fract v)⁻¹).s n ≠ none
⊢ Stream'.Seq.get? (of v).s (n + 1) = Stream'.Seq.get? (of (fract v)⁻¹).s n
[PROOFSTEP]
obtain ⟨p, hp⟩ := Option.ne_none_iff_exists'.mp h₁
[GOAL]
case inr.inr.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ n : ℕ
h : fract v ≠ 0
h₁ : Stream'.Seq.get? (of (fract v)⁻¹).s n ≠ none
p : Pair K
hp : Stream'.Seq.get? (of (fract v)⁻¹).s n = some p
⊢ Stream'.Seq.get? (of v).s (n + 1) = Stream'.Seq.get? (of (fract v)⁻¹).s n
[PROOFSTEP]
obtain ⟨p', hp'₁, _⟩ := exists_succ_get?_stream_of_gcf_of_get?_eq_some hp
[GOAL]
case inr.inr.intro.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ n : ℕ
h : fract v ≠ 0
h₁ : Stream'.Seq.get? (of (fract v)⁻¹).s n ≠ none
p : Pair K
hp : Stream'.Seq.get? (of (fract v)⁻¹).s n = some p
p' : IntFractPair K
hp'₁ : IntFractPair.stream (fract v)⁻¹ (n + 1) = some p'
right✝ : ↑p'.b = p.b
⊢ Stream'.Seq.get? (of v).s (n + 1) = Stream'.Seq.get? (of (fract v)⁻¹).s n
[PROOFSTEP]
have Hp := get?_of_eq_some_of_succ_get?_intFractPair_stream hp'₁
[GOAL]
case inr.inr.intro.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ n : ℕ
h : fract v ≠ 0
h₁ : Stream'.Seq.get? (of (fract v)⁻¹).s n ≠ none
p : Pair K
hp : Stream'.Seq.get? (of (fract v)⁻¹).s n = some p
p' : IntFractPair K
hp'₁ : IntFractPair.stream (fract v)⁻¹ (n + 1) = some p'
right✝ : ↑p'.b = p.b
Hp : Stream'.Seq.get? (of (fract v)⁻¹).s n = some { a := 1, b := ↑p'.b }
⊢ Stream'.Seq.get? (of v).s (n + 1) = Stream'.Seq.get? (of (fract v)⁻¹).s n
[PROOFSTEP]
rw [← stream_succ h] at hp'₁ 
[GOAL]
case inr.inr.intro.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ n : ℕ
h : fract v ≠ 0
h₁ : Stream'.Seq.get? (of (fract v)⁻¹).s n ≠ none
p : Pair K
hp : Stream'.Seq.get? (of (fract v)⁻¹).s n = some p
p' : IntFractPair K
hp'₁ : IntFractPair.stream v (n + 1 + 1) = some p'
right✝ : ↑p'.b = p.b
Hp : Stream'.Seq.get? (of (fract v)⁻¹).s n = some { a := 1, b := ↑p'.b }
⊢ Stream'.Seq.get? (of v).s (n + 1) = Stream'.Seq.get? (of (fract v)⁻¹).s n
[PROOFSTEP]
rw [Hp, get?_of_eq_some_of_succ_get?_intFractPair_stream hp'₁]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
a : ℤ
⊢ convergents' (of ↑a) n = ↑a
[PROOFSTEP]
induction' n with n
[GOAL]
case zero
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
a : ℤ
⊢ convergents' (of ↑a) Nat.zero = ↑a
[PROOFSTEP]
simp only [zeroth_convergent'_eq_h, of_h_eq_floor, floor_intCast, Nat.zero_eq]
[GOAL]
case succ
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
a : ℤ
n : ℕ
n_ih✝ : convergents' (of ↑a) n = ↑a
⊢ convergents' (of ↑a) (Nat.succ n) = ↑a
[PROOFSTEP]
rw [convergents', of_h_eq_floor, floor_intCast, add_right_eq_self]
[GOAL]
case succ
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
a : ℤ
n : ℕ
n_ih✝ : convergents' (of ↑a) n = ↑a
⊢ convergents'Aux (of ↑a).s (Nat.succ n) = 0
[PROOFSTEP]
exact convergents'Aux_succ_none ((of_s_of_int K a).symm ▸ Stream'.Seq.get?_nil 0) _
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ convergents' (of v) (n + 1) = ↑⌊v⌋ + 1 / convergents' (of (fract v)⁻¹) n
[PROOFSTEP]
cases' eq_or_ne (fract v) 0 with h h
[GOAL]
case inl
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
h : fract v = 0
⊢ convergents' (of v) (n + 1) = ↑⌊v⌋ + 1 / convergents' (of (fract v)⁻¹) n
[PROOFSTEP]
obtain ⟨a, rfl⟩ : ∃ a : ℤ, v = a := ⟨⌊v⌋, eq_of_sub_eq_zero h⟩
[GOAL]
case inl.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
n : ℕ
a : ℤ
h : fract ↑a = 0
⊢ convergents' (of ↑a) (n + 1) = ↑⌊↑a⌋ + 1 / convergents' (of (fract ↑a)⁻¹) n
[PROOFSTEP]
rw [convergents'_of_int, fract_intCast, inv_zero, ← cast_zero, convergents'_of_int, cast_zero, div_zero, add_zero,
  floor_intCast]
[GOAL]
case inr
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
h : fract v ≠ 0
⊢ convergents' (of v) (n + 1) = ↑⌊v⌋ + 1 / convergents' (of (fract v)⁻¹) n
[PROOFSTEP]
rw [convergents', of_h_eq_floor, add_right_inj, convergents'Aux_succ_some (of_s_head h)]
[GOAL]
case inr
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
h : fract v ≠ 0
⊢ { a := 1, b := ↑⌊(fract v)⁻¹⌋ }.a /
      ({ a := 1, b := ↑⌊(fract v)⁻¹⌋ }.b + convergents'Aux (Stream'.Seq.tail (of v).s) n) =
    1 / convergents' (of (fract v)⁻¹) n
[PROOFSTEP]
exact congr_arg ((· / ·) 1) (by rw [convergents', of_h_eq_floor, add_right_inj, of_s_tail])
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
h : fract v ≠ 0
⊢ { a := 1, b := ↑⌊(fract v)⁻¹⌋ }.b + convergents'Aux (Stream'.Seq.tail (of v).s) n = convergents' (of (fract v)⁻¹) n
[PROOFSTEP]
rw [convergents', of_h_eq_floor, add_right_inj, of_s_tail]
