case none
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
s_succ_succ_nth_eq : Stream'.Seq.get? s (n + 2) = none
⊢ Stream'.Seq.tail (squashSeq s (n + 1)) = squashSeq (Stream'.Seq.tail s) n

case some
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : Stream'.Seq.get? s (n + 2) = some gp_succ_succ_n
⊢ Stream'.Seq.tail (squashSeq s (n + 1)) = squashSeq (Stream'.Seq.tail s) n
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
⊢ Stream'.Seq.tail (squashSeq s (n + 1)) = squashSeq (Stream'.Seq.tail s) n
cases' s_succ_succ_nth_eq : s.get? (n + 2) with gp_succ_succ_n
case some
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : Stream'.Seq.get? s (n + 2) = some gp_succ_succ_n
⊢ Stream'.Seq.tail (squashSeq s (n + 1)) = squashSeq (Stream'.Seq.tail s) n
case none
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
s_succ_succ_nth_eq : Stream'.Seq.get? s (n + 2) = none
⊢ Stream'.Seq.tail (squashSeq s (n + 1)) = squashSeq (Stream'.Seq.tail s) n

case some
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : Stream'.Seq.get? s (n + 2) = some gp_succ_succ_n
⊢ Stream'.Seq.tail (squashSeq s (n + 1)) = squashSeq (Stream'.Seq.tail s) n
case none =>
  cases s_succ_nth_eq : s.get? (n + 1) <;>
    simp only [squashSeq, Stream'.Seq.get?_tail, s_succ_nth_eq, s_succ_succ_nth_eq]
no goals
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
s_succ_succ_nth_eq : Stream'.Seq.get? s (n + 2) = none
⊢ Stream'.Seq.tail (squashSeq s (n + 1)) = squashSeq (Stream'.Seq.tail s) n
cases s_succ_nth_eq : s.get? (n + 1) <;>
  simp only [squashSeq, Stream'.Seq.get?_tail, s_succ_nth_eq, s_succ_succ_nth_eq]
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : Stream'.Seq.get? s (n + 2) = some gp_succ_succ_n
⊢ ∃ gp_succ_n, Stream'.Seq.get? s (n + 1) = some gp_succ_n

case intro
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : Stream'.Seq.get? s (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some gp_succ_n
⊢ Stream'.Seq.tail (squashSeq s (n + 1)) = squashSeq (Stream'.Seq.tail s) n
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : Stream'.Seq.get? s (n + 2) = some gp_succ_succ_n
⊢ Stream'.Seq.tail (squashSeq s (n + 1)) = squashSeq (Stream'.Seq.tail s) n
obtain ⟨gp_succ_n, s_succ_nth_eq⟩ : ∃ gp_succ_n, s.get? (n + 1) = some gp_succ_n
case intro
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : Stream'.Seq.get? s (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some gp_succ_n
⊢ Stream'.Seq.tail (squashSeq s (n + 1)) = squashSeq (Stream'.Seq.tail s) n
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : Stream'.Seq.get? s (n + 2) = some gp_succ_succ_n
⊢ ∃ gp_succ_n, Stream'.Seq.get? s (n + 1) = some gp_succ_n

case intro
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : Stream'.Seq.get? s (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some gp_succ_n
⊢ Stream'.Seq.tail (squashSeq s (n + 1)) = squashSeq (Stream'.Seq.tail s) n
exact s.ge_stable (n + 1).le_succ s_succ_succ_nth_eq
case intro.h
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : Stream'.Seq.get? s (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some gp_succ_n
m : ℕ
⊢ Stream'.Seq.get? (Stream'.Seq.tail (squashSeq s (n + 1))) m = Stream'.Seq.get? (squashSeq (Stream'.Seq.tail s) n) m
case intro
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : Stream'.Seq.get? s (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some gp_succ_n
⊢ Stream'.Seq.tail (squashSeq s (n + 1)) = squashSeq (Stream'.Seq.tail s) n
ext1 m
case intro.h.inl
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : Stream'.Seq.get? s (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some gp_succ_n
m : ℕ
m_eq_n : m = n
⊢ Stream'.Seq.get? (Stream'.Seq.tail (squashSeq s (n + 1))) m = Stream'.Seq.get? (squashSeq (Stream'.Seq.tail s) n) m

case intro.h.inr
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : Stream'.Seq.get? s (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some gp_succ_n
m : ℕ
m_ne_n : ¬m = n
⊢ Stream'.Seq.get? (Stream'.Seq.tail (squashSeq s (n + 1))) m = Stream'.Seq.get? (squashSeq (Stream'.Seq.tail s) n) m
case intro.h
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : Stream'.Seq.get? s (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some gp_succ_n
m : ℕ
⊢ Stream'.Seq.get? (Stream'.Seq.tail (squashSeq s (n + 1))) m = Stream'.Seq.get? (squashSeq (Stream'.Seq.tail s) n) m
cases' Decidable.em (m = n) with m_eq_n m_ne_n
no goals
case intro.h.inl
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : Stream'.Seq.get? s (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some gp_succ_n
m : ℕ
m_eq_n : m = n
⊢ Stream'.Seq.get? (Stream'.Seq.tail (squashSeq s (n + 1))) m = Stream'.Seq.get? (squashSeq (Stream'.Seq.tail s) n) m
simp [*, squashSeq]
case intro.h.inr
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : Stream'.Seq.get? s (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some gp_succ_n
m : ℕ
m_ne_n : ¬m = n
this : Stream'.Seq.get? (Stream'.Seq.tail s) m = Stream'.Seq.get? s (m + 1)
⊢ Stream'.Seq.get? (Stream'.Seq.tail (squashSeq s (n + 1))) m = Stream'.Seq.get? (squashSeq (Stream'.Seq.tail s) n) m
case intro.h.inr
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : Stream'.Seq.get? s (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some gp_succ_n
m : ℕ
m_ne_n : ¬m = n
⊢ Stream'.Seq.get? (Stream'.Seq.tail (squashSeq s (n + 1))) m = Stream'.Seq.get? (squashSeq (Stream'.Seq.tail s) n) m
have : s.tail.get? m = s.get? (m + 1) := s.get?_tail m
case intro.h.inr.none
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : Stream'.Seq.get? s (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some gp_succ_n
m : ℕ
m_ne_n : ¬m = n
this : Stream'.Seq.get? (Stream'.Seq.tail s) m = Stream'.Seq.get? s (m + 1)
s_succ_mth_eq : Stream'.Seq.get? s (m + 1) = none
⊢ Stream'.Seq.get? (Stream'.Seq.tail (squashSeq s (n + 1))) m = Stream'.Seq.get? (squashSeq (Stream'.Seq.tail s) n) m

case intro.h.inr.some
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : Stream'.Seq.get? s (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some gp_succ_n
m : ℕ
m_ne_n : ¬m = n
this : Stream'.Seq.get? (Stream'.Seq.tail s) m = Stream'.Seq.get? s (m + 1)
val✝ : Pair K
s_succ_mth_eq : Stream'.Seq.get? s (m + 1) = some val✝
⊢ Stream'.Seq.get? (Stream'.Seq.tail (squashSeq s (n + 1))) m = Stream'.Seq.get? (squashSeq (Stream'.Seq.tail s) n) m
case intro.h.inr
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : Stream'.Seq.get? s (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some gp_succ_n
m : ℕ
m_ne_n : ¬m = n
this : Stream'.Seq.get? (Stream'.Seq.tail s) m = Stream'.Seq.get? s (m + 1)
⊢ Stream'.Seq.get? (Stream'.Seq.tail (squashSeq s (n + 1))) m = Stream'.Seq.get? (squashSeq (Stream'.Seq.tail s) n) m
cases s_succ_mth_eq : s.get? (m + 1)
case intro.h.inr.none
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : Stream'.Seq.get? s (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some gp_succ_n
m : ℕ
m_ne_n : ¬m = n
this : Stream'.Seq.get? (Stream'.Seq.tail s) m = Stream'.Seq.get? s (m + 1)
s_succ_mth_eq : Stream'.Seq.get? s (m + 1) = none
x✝ : Stream'.Seq.get? (Stream'.Seq.tail s) m = none
⊢ Stream'.Seq.get? (Stream'.Seq.tail (squashSeq s (n + 1))) m = Stream'.Seq.get? (squashSeq (Stream'.Seq.tail s) n) m

case intro.h.inr.some
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : Stream'.Seq.get? s (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some gp_succ_n
m : ℕ
m_ne_n : ¬m = n
this : Stream'.Seq.get? (Stream'.Seq.tail s) m = Stream'.Seq.get? s (m + 1)
val✝ : Pair K
s_succ_mth_eq : Stream'.Seq.get? s (m + 1) = some val✝
x✝ : Stream'.Seq.get? (Stream'.Seq.tail s) m = some val✝
⊢ Stream'.Seq.get? (Stream'.Seq.tail (squashSeq s (n + 1))) m = Stream'.Seq.get? (squashSeq (Stream'.Seq.tail s) n) m
case intro.h.inr.none
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : Stream'.Seq.get? s (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some gp_succ_n
m : ℕ
m_ne_n : ¬m = n
this : Stream'.Seq.get? (Stream'.Seq.tail s) m = Stream'.Seq.get? s (m + 1)
s_succ_mth_eq : Stream'.Seq.get? s (m + 1) = none
⊢ Stream'.Seq.get? (Stream'.Seq.tail (squashSeq s (n + 1))) m = Stream'.Seq.get? (squashSeq (Stream'.Seq.tail s) n) m

case intro.h.inr.some
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : Stream'.Seq.get? s (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some gp_succ_n
m : ℕ
m_ne_n : ¬m = n
this : Stream'.Seq.get? (Stream'.Seq.tail s) m = Stream'.Seq.get? s (m + 1)
val✝ : Pair K
s_succ_mth_eq : Stream'.Seq.get? s (m + 1) = some val✝
⊢ Stream'.Seq.get? (Stream'.Seq.tail (squashSeq s (n + 1))) m = Stream'.Seq.get? (squashSeq (Stream'.Seq.tail s) n) m
all_goals have _ := this.trans s_succ_mth_eq
case intro.h.inr.some
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : Stream'.Seq.get? s (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some gp_succ_n
m : ℕ
m_ne_n : ¬m = n
this : Stream'.Seq.get? (Stream'.Seq.tail s) m = Stream'.Seq.get? s (m + 1)
val✝ : Pair K
s_succ_mth_eq : Stream'.Seq.get? s (m + 1) = some val✝
x✝ : Stream'.Seq.get? (Stream'.Seq.tail s) m = some val✝
⊢ Stream'.Seq.get? (Stream'.Seq.tail (squashSeq s (n + 1))) m = Stream'.Seq.get? (squashSeq (Stream'.Seq.tail s) n) m
case intro.h.inr.some
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : Stream'.Seq.get? s (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some gp_succ_n
m : ℕ
m_ne_n : ¬m = n
this : Stream'.Seq.get? (Stream'.Seq.tail s) m = Stream'.Seq.get? s (m + 1)
val✝ : Pair K
s_succ_mth_eq : Stream'.Seq.get? s (m + 1) = some val✝
⊢ Stream'.Seq.get? (Stream'.Seq.tail (squashSeq s (n + 1))) m = Stream'.Seq.get? (squashSeq (Stream'.Seq.tail s) n) m
have _ := this.trans s_succ_mth_eq
no goals
case intro.h.inr.none
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : Stream'.Seq.get? s (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some gp_succ_n
m : ℕ
m_ne_n : ¬m = n
this : Stream'.Seq.get? (Stream'.Seq.tail s) m = Stream'.Seq.get? s (m + 1)
s_succ_mth_eq : Stream'.Seq.get? s (m + 1) = none
x✝ : Stream'.Seq.get? (Stream'.Seq.tail s) m = none
⊢ Stream'.Seq.get? (Stream'.Seq.tail (squashSeq s (n + 1))) m = Stream'.Seq.get? (squashSeq (Stream'.Seq.tail s) n) m
simp only [*, squashSeq, Stream'.Seq.get?_tail, Stream'.Seq.get?_zipWith,
  Option.map₂_none_right]
no goals
case intro.h.inr.some
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : Stream'.Seq.get? s (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some gp_succ_n
m : ℕ
m_ne_n : ¬m = n
this : Stream'.Seq.get? (Stream'.Seq.tail s) m = Stream'.Seq.get? s (m + 1)
val✝ : Pair K
s_succ_mth_eq : Stream'.Seq.get? s (m + 1) = some val✝
x✝ : Stream'.Seq.get? (Stream'.Seq.tail s) m = some val✝
⊢ Stream'.Seq.get? (Stream'.Seq.tail (squashSeq s (n + 1))) m = Stream'.Seq.get? (squashSeq (Stream'.Seq.tail s) n) m
simp [*, squashSeq]