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 }
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 }
unfold of IntFractPair.seq1
no goals
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 }
simp [Stream'.Seq.map_tail, Stream'.Seq.get?_tail, Stream'.Seq.map_get?, stream_succ_nth_eq]