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

case some
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
val✝ : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some val✝
⊢ Stream'.Seq.get? (squashSeq s n) m = Stream'.Seq.get? s m
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
⊢ Stream'.Seq.get? (squashSeq s n) m = Stream'.Seq.get? s m
cases s_succ_nth_eq : s.get? (n + 1)
case some
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
val✝ : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some val✝
⊢ Stream'.Seq.get? (squashSeq s n) m = Stream'.Seq.get? s m
case none
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = none
⊢ Stream'.Seq.get? (squashSeq s n) m = Stream'.Seq.get? s m

case some
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
val✝ : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some val✝
⊢ Stream'.Seq.get? (squashSeq s n) m = Stream'.Seq.get? s m
case none => rw [squashSeq_eq_self_of_terminated s_succ_nth_eq]
no goals
case some
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
val✝ : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some val✝
⊢ Stream'.Seq.get? (squashSeq s n) m = Stream'.Seq.get? s m
case some =>
  obtain ⟨gp_n, s_nth_eq⟩ : ∃ gp_n, s.get? n = some gp_n
  exact s.ge_stable n.le_succ s_succ_nth_eq
  obtain ⟨gp_m, s_mth_eq⟩ : ∃ gp_m, s.get? m = some gp_m
  exact s.ge_stable (le_of_lt m_lt_n) s_nth_eq
  simp [*, squashSeq, m_lt_n.ne]
no goals
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = none
⊢ Stream'.Seq.get? (squashSeq s n) m = Stream'.Seq.get? s m
rw [squashSeq_eq_self_of_terminated s_succ_nth_eq]
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
val✝ : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some val✝
⊢ ∃ gp_n, Stream'.Seq.get? s n = some gp_n

case intro
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
val✝ : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some val✝
gp_n : Pair K
s_nth_eq : Stream'.Seq.get? s n = some gp_n
⊢ Stream'.Seq.get? (squashSeq s n) m = Stream'.Seq.get? s m
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
val✝ : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some val✝
⊢ Stream'.Seq.get? (squashSeq s n) m = Stream'.Seq.get? s m
obtain ⟨gp_n, s_nth_eq⟩ : ∃ gp_n, s.get? n = some gp_n
case intro
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
val✝ : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some val✝
gp_n : Pair K
s_nth_eq : Stream'.Seq.get? s n = some gp_n
⊢ Stream'.Seq.get? (squashSeq s n) m = Stream'.Seq.get? s m
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
val✝ : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some val✝
⊢ ∃ gp_n, Stream'.Seq.get? s n = some gp_n

case intro
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
val✝ : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some val✝
gp_n : Pair K
s_nth_eq : Stream'.Seq.get? s n = some gp_n
⊢ Stream'.Seq.get? (squashSeq s n) m = Stream'.Seq.get? s m
exact s.ge_stable n.le_succ s_succ_nth_eq
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
val✝ : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some val✝
gp_n : Pair K
s_nth_eq : Stream'.Seq.get? s n = some gp_n
⊢ ∃ gp_m, Stream'.Seq.get? s m = some gp_m

case intro.intro
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
val✝ : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some val✝
gp_n : Pair K
s_nth_eq : Stream'.Seq.get? s n = some gp_n
gp_m : Pair K
s_mth_eq : Stream'.Seq.get? s m = some gp_m
⊢ Stream'.Seq.get? (squashSeq s n) m = Stream'.Seq.get? s m
case intro
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
val✝ : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some val✝
gp_n : Pair K
s_nth_eq : Stream'.Seq.get? s n = some gp_n
⊢ Stream'.Seq.get? (squashSeq s n) m = Stream'.Seq.get? s m
obtain ⟨gp_m, s_mth_eq⟩ : ∃ gp_m, s.get? m = some gp_m
case intro.intro
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
val✝ : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some val✝
gp_n : Pair K
s_nth_eq : Stream'.Seq.get? s n = some gp_n
gp_m : Pair K
s_mth_eq : Stream'.Seq.get? s m = some gp_m
⊢ Stream'.Seq.get? (squashSeq s n) m = Stream'.Seq.get? s m
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
val✝ : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some val✝
gp_n : Pair K
s_nth_eq : Stream'.Seq.get? s n = some gp_n
⊢ ∃ gp_m, Stream'.Seq.get? s m = some gp_m

case intro.intro
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
val✝ : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some val✝
gp_n : Pair K
s_nth_eq : Stream'.Seq.get? s n = some gp_n
gp_m : Pair K
s_mth_eq : Stream'.Seq.get? s m = some gp_m
⊢ Stream'.Seq.get? (squashSeq s n) m = Stream'.Seq.get? s m
exact s.ge_stable (le_of_lt m_lt_n) s_nth_eq
no goals
case intro.intro
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
val✝ : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some val✝
gp_n : Pair K
s_nth_eq : Stream'.Seq.get? s n = some gp_n
gp_m : Pair K
s_mth_eq : Stream'.Seq.get? s m = some gp_m
⊢ Stream'.Seq.get? (squashSeq s n) m = Stream'.Seq.get? s m
simp [*, squashSeq, m_lt_n.ne]