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 })
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 })
rw [of, IntFractPair.seq1]
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 })
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 })
simp only [of, Stream'.Seq.map_tail, Stream'.Seq.map, Stream'.Seq.tail, Stream'.Seq.head,
  Stream'.Seq.get?, Stream'.map]
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 })
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 })
rw [← Stream'.nth_succ, Stream'.nth, Option.map]
no goals
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 })
split <;> simp_all only [Option.some_bind, Option.none_bind, Function.comp_apply]