[GOAL]
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
terminated_at_succ_n : Stream'.Seq.TerminatedAt s (n + 1)
⊢ squashSeq s n = s
[PROOFSTEP]
change s.get? (n + 1) = none at terminated_at_succ_n 
[GOAL]
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
terminated_at_succ_n : Stream'.Seq.get? s (n + 1) = none
⊢ squashSeq s n = s
[PROOFSTEP]
cases s_nth_eq : s.get? n
[GOAL]
case none
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
terminated_at_succ_n : Stream'.Seq.get? s (n + 1) = none
s_nth_eq : Stream'.Seq.get? s n = none
⊢ squashSeq s n = s
[PROOFSTEP]
simp only [*, squashSeq]
[GOAL]
case some
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
terminated_at_succ_n : Stream'.Seq.get? s (n + 1) = none
val✝ : Pair K
s_nth_eq : Stream'.Seq.get? s n = some val✝
⊢ squashSeq s n = s
[PROOFSTEP]
simp only [*, squashSeq]
[GOAL]
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_n gp_succ_n : Pair K
s_nth_eq : Stream'.Seq.get? s n = some gp_n
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some gp_succ_n
⊢ Stream'.Seq.get? (squashSeq s n) n = some { a := gp_n.a, b := gp_n.b + gp_succ_n.a / gp_succ_n.b }
[PROOFSTEP]
simp [*, squashSeq]
[GOAL]
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
[PROOFSTEP]
cases s_succ_nth_eq : s.get? (n + 1)
[GOAL]
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
[PROOFSTEP]
case none => rw [squashSeq_eq_self_of_terminated s_succ_nth_eq]
[GOAL]
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
[PROOFSTEP]
case none => rw [squashSeq_eq_self_of_terminated s_succ_nth_eq]
[GOAL]
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
[PROOFSTEP]
rw [squashSeq_eq_self_of_terminated s_succ_nth_eq]
[GOAL]
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
[PROOFSTEP]
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]
[GOAL]
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
[PROOFSTEP]
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]
[GOAL]
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
[PROOFSTEP]
obtain ⟨gp_n, s_nth_eq⟩ : ∃ gp_n, s.get? n = some gp_n
[GOAL]
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
[PROOFSTEP]
exact s.ge_stable n.le_succ s_succ_nth_eq
[GOAL]
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
[PROOFSTEP]
obtain ⟨gp_m, s_mth_eq⟩ : ∃ gp_m, s.get? m = some gp_m
[GOAL]
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
[PROOFSTEP]
exact s.ge_stable (le_of_lt m_lt_n) s_nth_eq
[GOAL]
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
[PROOFSTEP]
simp [*, squashSeq, m_lt_n.ne]
[GOAL]
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
[PROOFSTEP]
cases' s_succ_succ_nth_eq : s.get? (n + 2) with gp_succ_succ_n
[GOAL]
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
[PROOFSTEP]
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]
[GOAL]
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
[PROOFSTEP]
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]
[GOAL]
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
[PROOFSTEP]
cases s_succ_nth_eq : s.get? (n + 1)
[GOAL]
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
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = none
⊢ Stream'.Seq.tail (squashSeq s (n + 1)) = squashSeq (Stream'.Seq.tail s) n
[PROOFSTEP]
simp only [squashSeq, Stream'.Seq.get?_tail, s_succ_nth_eq, s_succ_succ_nth_eq]
[GOAL]
case some
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
val✝ : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some val✝
⊢ Stream'.Seq.tail (squashSeq s (n + 1)) = squashSeq (Stream'.Seq.tail s) n
[PROOFSTEP]
simp only [squashSeq, Stream'.Seq.get?_tail, s_succ_nth_eq, s_succ_succ_nth_eq]
[GOAL]
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
[PROOFSTEP]
case some =>
  obtain ⟨gp_succ_n, s_succ_nth_eq⟩ : ∃ gp_succ_n, s.get? (n + 1) = some gp_succ_n;
  exact s.ge_stable (n + 1).le_succ s_succ_succ_nth_eq
  ext1 m
  cases' Decidable.em (m = n) with m_eq_n m_ne_n
  · simp [*, squashSeq]
  · have : s.tail.get? m = s.get? (m + 1) := s.get?_tail m
    cases s_succ_mth_eq : s.get? (m + 1)
    all_goals have _ := this.trans s_succ_mth_eq
    · simp only [*, squashSeq, Stream'.Seq.get?_tail, Stream'.Seq.get?_zipWith, Option.map₂_none_right]
    · simp [*, squashSeq]
[GOAL]
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
[PROOFSTEP]
case some =>
  obtain ⟨gp_succ_n, s_succ_nth_eq⟩ : ∃ gp_succ_n, s.get? (n + 1) = some gp_succ_n;
  exact s.ge_stable (n + 1).le_succ s_succ_succ_nth_eq
  ext1 m
  cases' Decidable.em (m = n) with m_eq_n m_ne_n
  · simp [*, squashSeq]
  · have : s.tail.get? m = s.get? (m + 1) := s.get?_tail m
    cases s_succ_mth_eq : s.get? (m + 1)
    all_goals have _ := this.trans s_succ_mth_eq
    · simp only [*, squashSeq, Stream'.Seq.get?_tail, Stream'.Seq.get?_zipWith, Option.map₂_none_right]
    · simp [*, squashSeq]
[GOAL]
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
[PROOFSTEP]
obtain ⟨gp_succ_n, s_succ_nth_eq⟩ : ∃ gp_succ_n, s.get? (n + 1) = some gp_succ_n
[GOAL]
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
[PROOFSTEP]
exact s.ge_stable (n + 1).le_succ s_succ_succ_nth_eq
[GOAL]
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
[PROOFSTEP]
ext1 m
[GOAL]
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
[PROOFSTEP]
cases' Decidable.em (m = n) with m_eq_n m_ne_n
[GOAL]
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
[PROOFSTEP]
simp [*, squashSeq]
[GOAL]
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
[PROOFSTEP]
have : s.tail.get? m = s.get? (m + 1) := s.get?_tail m
[GOAL]
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
[PROOFSTEP]
cases s_succ_mth_eq : s.get? (m + 1)
[GOAL]
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
[PROOFSTEP]
all_goals have _ := this.trans s_succ_mth_eq
[GOAL]
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
[PROOFSTEP]
have _ := this.trans s_succ_mth_eq
[GOAL]
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
[PROOFSTEP]
have _ := this.trans s_succ_mth_eq
[GOAL]
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
[PROOFSTEP]
simp only [*, squashSeq, Stream'.Seq.get?_tail, Stream'.Seq.get?_zipWith, Option.map₂_none_right]
[GOAL]
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
[PROOFSTEP]
simp [*, squashSeq]
[GOAL]
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
⊢ convergents'Aux s (n + 2) = convergents'Aux (squashSeq s n) (n + 1)
[PROOFSTEP]
cases' s_succ_nth_eq : s.get? <| n + 1 with gp_succ_n
[GOAL]
case none
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = none
⊢ convergents'Aux s (n + 2) = convergents'Aux (squashSeq s n) (n + 1)
case some
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some gp_succ_n
⊢ convergents'Aux s (n + 2) = convergents'Aux (squashSeq s n) (n + 1)
[PROOFSTEP]
case none => rw [squashSeq_eq_self_of_terminated s_succ_nth_eq, convergents'Aux_stable_step_of_terminated s_succ_nth_eq]
[GOAL]
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = none
⊢ convergents'Aux s (n + 2) = convergents'Aux (squashSeq s n) (n + 1)
[PROOFSTEP]
case none => rw [squashSeq_eq_self_of_terminated s_succ_nth_eq, convergents'Aux_stable_step_of_terminated s_succ_nth_eq]
[GOAL]
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = none
⊢ convergents'Aux s (n + 2) = convergents'Aux (squashSeq s n) (n + 1)
[PROOFSTEP]
rw [squashSeq_eq_self_of_terminated s_succ_nth_eq, convergents'Aux_stable_step_of_terminated s_succ_nth_eq]
[GOAL]
case some
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some gp_succ_n
⊢ convergents'Aux s (n + 2) = convergents'Aux (squashSeq s n) (n + 1)
[PROOFSTEP]
case some =>
  induction' n with m IH generalizing s gp_succ_n
  case zero =>
    obtain ⟨gp_head, s_head_eq⟩ : ∃ gp_head, s.head = some gp_head
    exact s.ge_stable zero_le_one s_succ_nth_eq
    have : (squashSeq s 0).head = some ⟨gp_head.a, gp_head.b + gp_succ_n.a / gp_succ_n.b⟩ :=
      squashSeq_nth_of_not_terminated s_head_eq s_succ_nth_eq
    simp_all [convergents'Aux, Stream'.Seq.head, Stream'.Seq.get?_tail]
  case succ =>
    obtain ⟨gp_head, s_head_eq⟩ : ∃ gp_head, s.head = some gp_head
    exact s.ge_stable (m + 2).zero_le s_succ_nth_eq
    suffices gp_head.a / (gp_head.b + convergents'Aux s.tail (m + 2)) = convergents'Aux (squashSeq s (m + 1)) (m + 2) by
      simpa only [convergents'Aux, s_head_eq]
    have : convergents'Aux s.tail (m + 2) = convergents'Aux (squashSeq s.tail m) (m + 1) :=
      by
      refine' IH gp_succ_n _
      simpa [Stream'.Seq.get?_tail] using s_succ_nth_eq
    have : (squashSeq s (m + 1)).head = some gp_head := (squashSeq_nth_of_lt m.succ_pos).trans s_head_eq
    simp_all [convergents'Aux, squashSeq_succ_n_tail_eq_squashSeq_tail_n]
[GOAL]
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some gp_succ_n
⊢ convergents'Aux s (n + 2) = convergents'Aux (squashSeq s n) (n + 1)
[PROOFSTEP]
case some =>
  induction' n with m IH generalizing s gp_succ_n
  case zero =>
    obtain ⟨gp_head, s_head_eq⟩ : ∃ gp_head, s.head = some gp_head
    exact s.ge_stable zero_le_one s_succ_nth_eq
    have : (squashSeq s 0).head = some ⟨gp_head.a, gp_head.b + gp_succ_n.a / gp_succ_n.b⟩ :=
      squashSeq_nth_of_not_terminated s_head_eq s_succ_nth_eq
    simp_all [convergents'Aux, Stream'.Seq.head, Stream'.Seq.get?_tail]
  case succ =>
    obtain ⟨gp_head, s_head_eq⟩ : ∃ gp_head, s.head = some gp_head
    exact s.ge_stable (m + 2).zero_le s_succ_nth_eq
    suffices gp_head.a / (gp_head.b + convergents'Aux s.tail (m + 2)) = convergents'Aux (squashSeq s (m + 1)) (m + 2) by
      simpa only [convergents'Aux, s_head_eq]
    have : convergents'Aux s.tail (m + 2) = convergents'Aux (squashSeq s.tail m) (m + 1) :=
      by
      refine' IH gp_succ_n _
      simpa [Stream'.Seq.get?_tail] using s_succ_nth_eq
    have : (squashSeq s (m + 1)).head = some gp_head := (squashSeq_nth_of_lt m.succ_pos).trans s_head_eq
    simp_all [convergents'Aux, squashSeq_succ_n_tail_eq_squashSeq_tail_n]
[GOAL]
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (n + 1) = some gp_succ_n
⊢ convergents'Aux s (n + 2) = convergents'Aux (squashSeq s n) (n + 1)
[PROOFSTEP]
induction' n with m IH generalizing s gp_succ_n
[GOAL]
case zero
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s✝ : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_n✝ : Pair K
s_succ_nth_eq✝ : Stream'.Seq.get? s✝ (n + 1) = some gp_succ_n✝
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (Nat.zero + 1) = some gp_succ_n
⊢ convergents'Aux s (Nat.zero + 2) = convergents'Aux (squashSeq s Nat.zero) (Nat.zero + 1)
case succ
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s✝ : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_n✝ : Pair K
s_succ_nth_eq✝ : Stream'.Seq.get? s✝ (n + 1) = some gp_succ_n✝
m : ℕ
IH :
  ∀ {s : Stream'.Seq (Pair K)} (gp_succ_n : Pair K),
    Stream'.Seq.get? s (m + 1) = some gp_succ_n → convergents'Aux s (m + 2) = convergents'Aux (squashSeq s m) (m + 1)
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (Nat.succ m + 1) = some gp_succ_n
⊢ convergents'Aux s (Nat.succ m + 2) = convergents'Aux (squashSeq s (Nat.succ m)) (Nat.succ m + 1)
[PROOFSTEP]
case zero =>
  obtain ⟨gp_head, s_head_eq⟩ : ∃ gp_head, s.head = some gp_head
  exact s.ge_stable zero_le_one s_succ_nth_eq
  have : (squashSeq s 0).head = some ⟨gp_head.a, gp_head.b + gp_succ_n.a / gp_succ_n.b⟩ :=
    squashSeq_nth_of_not_terminated s_head_eq s_succ_nth_eq
  simp_all [convergents'Aux, Stream'.Seq.head, Stream'.Seq.get?_tail]
[GOAL]
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s✝ : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_n✝ : Pair K
s_succ_nth_eq✝ : Stream'.Seq.get? s✝ (n + 1) = some gp_succ_n✝
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (Nat.zero + 1) = some gp_succ_n
⊢ convergents'Aux s (Nat.zero + 2) = convergents'Aux (squashSeq s Nat.zero) (Nat.zero + 1)
[PROOFSTEP]
case zero =>
  obtain ⟨gp_head, s_head_eq⟩ : ∃ gp_head, s.head = some gp_head
  exact s.ge_stable zero_le_one s_succ_nth_eq
  have : (squashSeq s 0).head = some ⟨gp_head.a, gp_head.b + gp_succ_n.a / gp_succ_n.b⟩ :=
    squashSeq_nth_of_not_terminated s_head_eq s_succ_nth_eq
  simp_all [convergents'Aux, Stream'.Seq.head, Stream'.Seq.get?_tail]
[GOAL]
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s✝ : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_n✝ : Pair K
s_succ_nth_eq✝ : Stream'.Seq.get? s✝ (n + 1) = some gp_succ_n✝
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (Nat.zero + 1) = some gp_succ_n
⊢ convergents'Aux s (Nat.zero + 2) = convergents'Aux (squashSeq s Nat.zero) (Nat.zero + 1)
[PROOFSTEP]
obtain ⟨gp_head, s_head_eq⟩ : ∃ gp_head, s.head = some gp_head
[GOAL]
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s✝ : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_n✝ : Pair K
s_succ_nth_eq✝ : Stream'.Seq.get? s✝ (n + 1) = some gp_succ_n✝
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (Nat.zero + 1) = some gp_succ_n
⊢ ∃ gp_head, Stream'.Seq.head s = some gp_head
case intro
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s✝ : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_n✝ : Pair K
s_succ_nth_eq✝ : Stream'.Seq.get? s✝ (n + 1) = some gp_succ_n✝
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (Nat.zero + 1) = some gp_succ_n
gp_head : Pair K
s_head_eq : Stream'.Seq.head s = some gp_head
⊢ convergents'Aux s (Nat.zero + 2) = convergents'Aux (squashSeq s Nat.zero) (Nat.zero + 1)
[PROOFSTEP]
exact s.ge_stable zero_le_one s_succ_nth_eq
[GOAL]
case intro
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s✝ : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_n✝ : Pair K
s_succ_nth_eq✝ : Stream'.Seq.get? s✝ (n + 1) = some gp_succ_n✝
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (Nat.zero + 1) = some gp_succ_n
gp_head : Pair K
s_head_eq : Stream'.Seq.head s = some gp_head
⊢ convergents'Aux s (Nat.zero + 2) = convergents'Aux (squashSeq s Nat.zero) (Nat.zero + 1)
[PROOFSTEP]
have : (squashSeq s 0).head = some ⟨gp_head.a, gp_head.b + gp_succ_n.a / gp_succ_n.b⟩ :=
  squashSeq_nth_of_not_terminated s_head_eq s_succ_nth_eq
[GOAL]
case intro
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s✝ : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_n✝ : Pair K
s_succ_nth_eq✝ : Stream'.Seq.get? s✝ (n + 1) = some gp_succ_n✝
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (Nat.zero + 1) = some gp_succ_n
gp_head : Pair K
s_head_eq : Stream'.Seq.head s = some gp_head
this : Stream'.Seq.head (squashSeq s 0) = some { a := gp_head.a, b := gp_head.b + gp_succ_n.a / gp_succ_n.b }
⊢ convergents'Aux s (Nat.zero + 2) = convergents'Aux (squashSeq s Nat.zero) (Nat.zero + 1)
[PROOFSTEP]
simp_all [convergents'Aux, Stream'.Seq.head, Stream'.Seq.get?_tail]
[GOAL]
case succ
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s✝ : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_n✝ : Pair K
s_succ_nth_eq✝ : Stream'.Seq.get? s✝ (n + 1) = some gp_succ_n✝
m : ℕ
IH :
  ∀ {s : Stream'.Seq (Pair K)} (gp_succ_n : Pair K),
    Stream'.Seq.get? s (m + 1) = some gp_succ_n → convergents'Aux s (m + 2) = convergents'Aux (squashSeq s m) (m + 1)
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (Nat.succ m + 1) = some gp_succ_n
⊢ convergents'Aux s (Nat.succ m + 2) = convergents'Aux (squashSeq s (Nat.succ m)) (Nat.succ m + 1)
[PROOFSTEP]
case succ =>
  obtain ⟨gp_head, s_head_eq⟩ : ∃ gp_head, s.head = some gp_head
  exact s.ge_stable (m + 2).zero_le s_succ_nth_eq
  suffices gp_head.a / (gp_head.b + convergents'Aux s.tail (m + 2)) = convergents'Aux (squashSeq s (m + 1)) (m + 2) by
    simpa only [convergents'Aux, s_head_eq]
  have : convergents'Aux s.tail (m + 2) = convergents'Aux (squashSeq s.tail m) (m + 1) :=
    by
    refine' IH gp_succ_n _
    simpa [Stream'.Seq.get?_tail] using s_succ_nth_eq
  have : (squashSeq s (m + 1)).head = some gp_head := (squashSeq_nth_of_lt m.succ_pos).trans s_head_eq
  simp_all [convergents'Aux, squashSeq_succ_n_tail_eq_squashSeq_tail_n]
[GOAL]
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s✝ : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_n✝ : Pair K
s_succ_nth_eq✝ : Stream'.Seq.get? s✝ (n + 1) = some gp_succ_n✝
m : ℕ
IH :
  ∀ {s : Stream'.Seq (Pair K)} (gp_succ_n : Pair K),
    Stream'.Seq.get? s (m + 1) = some gp_succ_n → convergents'Aux s (m + 2) = convergents'Aux (squashSeq s m) (m + 1)
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (Nat.succ m + 1) = some gp_succ_n
⊢ convergents'Aux s (Nat.succ m + 2) = convergents'Aux (squashSeq s (Nat.succ m)) (Nat.succ m + 1)
[PROOFSTEP]
case succ =>
  obtain ⟨gp_head, s_head_eq⟩ : ∃ gp_head, s.head = some gp_head
  exact s.ge_stable (m + 2).zero_le s_succ_nth_eq
  suffices gp_head.a / (gp_head.b + convergents'Aux s.tail (m + 2)) = convergents'Aux (squashSeq s (m + 1)) (m + 2) by
    simpa only [convergents'Aux, s_head_eq]
  have : convergents'Aux s.tail (m + 2) = convergents'Aux (squashSeq s.tail m) (m + 1) :=
    by
    refine' IH gp_succ_n _
    simpa [Stream'.Seq.get?_tail] using s_succ_nth_eq
  have : (squashSeq s (m + 1)).head = some gp_head := (squashSeq_nth_of_lt m.succ_pos).trans s_head_eq
  simp_all [convergents'Aux, squashSeq_succ_n_tail_eq_squashSeq_tail_n]
[GOAL]
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s✝ : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_n✝ : Pair K
s_succ_nth_eq✝ : Stream'.Seq.get? s✝ (n + 1) = some gp_succ_n✝
m : ℕ
IH :
  ∀ {s : Stream'.Seq (Pair K)} (gp_succ_n : Pair K),
    Stream'.Seq.get? s (m + 1) = some gp_succ_n → convergents'Aux s (m + 2) = convergents'Aux (squashSeq s m) (m + 1)
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (Nat.succ m + 1) = some gp_succ_n
⊢ convergents'Aux s (Nat.succ m + 2) = convergents'Aux (squashSeq s (Nat.succ m)) (Nat.succ m + 1)
[PROOFSTEP]
obtain ⟨gp_head, s_head_eq⟩ : ∃ gp_head, s.head = some gp_head
[GOAL]
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s✝ : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_n✝ : Pair K
s_succ_nth_eq✝ : Stream'.Seq.get? s✝ (n + 1) = some gp_succ_n✝
m : ℕ
IH :
  ∀ {s : Stream'.Seq (Pair K)} (gp_succ_n : Pair K),
    Stream'.Seq.get? s (m + 1) = some gp_succ_n → convergents'Aux s (m + 2) = convergents'Aux (squashSeq s m) (m + 1)
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (Nat.succ m + 1) = some gp_succ_n
⊢ ∃ gp_head, Stream'.Seq.head s = some gp_head
case intro
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s✝ : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_n✝ : Pair K
s_succ_nth_eq✝ : Stream'.Seq.get? s✝ (n + 1) = some gp_succ_n✝
m : ℕ
IH :
  ∀ {s : Stream'.Seq (Pair K)} (gp_succ_n : Pair K),
    Stream'.Seq.get? s (m + 1) = some gp_succ_n → convergents'Aux s (m + 2) = convergents'Aux (squashSeq s m) (m + 1)
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (Nat.succ m + 1) = some gp_succ_n
gp_head : Pair K
s_head_eq : Stream'.Seq.head s = some gp_head
⊢ convergents'Aux s (Nat.succ m + 2) = convergents'Aux (squashSeq s (Nat.succ m)) (Nat.succ m + 1)
[PROOFSTEP]
exact s.ge_stable (m + 2).zero_le s_succ_nth_eq
[GOAL]
case intro
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s✝ : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_n✝ : Pair K
s_succ_nth_eq✝ : Stream'.Seq.get? s✝ (n + 1) = some gp_succ_n✝
m : ℕ
IH :
  ∀ {s : Stream'.Seq (Pair K)} (gp_succ_n : Pair K),
    Stream'.Seq.get? s (m + 1) = some gp_succ_n → convergents'Aux s (m + 2) = convergents'Aux (squashSeq s m) (m + 1)
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (Nat.succ m + 1) = some gp_succ_n
gp_head : Pair K
s_head_eq : Stream'.Seq.head s = some gp_head
⊢ convergents'Aux s (Nat.succ m + 2) = convergents'Aux (squashSeq s (Nat.succ m)) (Nat.succ m + 1)
[PROOFSTEP]
suffices gp_head.a / (gp_head.b + convergents'Aux s.tail (m + 2)) = convergents'Aux (squashSeq s (m + 1)) (m + 2) by
  simpa only [convergents'Aux, s_head_eq]
[GOAL]
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s✝ : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_n✝ : Pair K
s_succ_nth_eq✝ : Stream'.Seq.get? s✝ (n + 1) = some gp_succ_n✝
m : ℕ
IH :
  ∀ {s : Stream'.Seq (Pair K)} (gp_succ_n : Pair K),
    Stream'.Seq.get? s (m + 1) = some gp_succ_n → convergents'Aux s (m + 2) = convergents'Aux (squashSeq s m) (m + 1)
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (Nat.succ m + 1) = some gp_succ_n
gp_head : Pair K
s_head_eq : Stream'.Seq.head s = some gp_head
this :
  gp_head.a / (gp_head.b + convergents'Aux (Stream'.Seq.tail s) (m + 2)) = convergents'Aux (squashSeq s (m + 1)) (m + 2)
⊢ convergents'Aux s (Nat.succ m + 2) = convergents'Aux (squashSeq s (Nat.succ m)) (Nat.succ m + 1)
[PROOFSTEP]
simpa only [convergents'Aux, s_head_eq]
[GOAL]
case intro
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s✝ : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_n✝ : Pair K
s_succ_nth_eq✝ : Stream'.Seq.get? s✝ (n + 1) = some gp_succ_n✝
m : ℕ
IH :
  ∀ {s : Stream'.Seq (Pair K)} (gp_succ_n : Pair K),
    Stream'.Seq.get? s (m + 1) = some gp_succ_n → convergents'Aux s (m + 2) = convergents'Aux (squashSeq s m) (m + 1)
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (Nat.succ m + 1) = some gp_succ_n
gp_head : Pair K
s_head_eq : Stream'.Seq.head s = some gp_head
⊢ gp_head.a / (gp_head.b + convergents'Aux (Stream'.Seq.tail s) (m + 2)) = convergents'Aux (squashSeq s (m + 1)) (m + 2)
[PROOFSTEP]
have : convergents'Aux s.tail (m + 2) = convergents'Aux (squashSeq s.tail m) (m + 1) :=
  by
  refine' IH gp_succ_n _
  simpa [Stream'.Seq.get?_tail] using s_succ_nth_eq
[GOAL]
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s✝ : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_n✝ : Pair K
s_succ_nth_eq✝ : Stream'.Seq.get? s✝ (n + 1) = some gp_succ_n✝
m : ℕ
IH :
  ∀ {s : Stream'.Seq (Pair K)} (gp_succ_n : Pair K),
    Stream'.Seq.get? s (m + 1) = some gp_succ_n → convergents'Aux s (m + 2) = convergents'Aux (squashSeq s m) (m + 1)
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (Nat.succ m + 1) = some gp_succ_n
gp_head : Pair K
s_head_eq : Stream'.Seq.head s = some gp_head
⊢ convergents'Aux (Stream'.Seq.tail s) (m + 2) = convergents'Aux (squashSeq (Stream'.Seq.tail s) m) (m + 1)
[PROOFSTEP]
refine' IH gp_succ_n _
[GOAL]
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s✝ : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_n✝ : Pair K
s_succ_nth_eq✝ : Stream'.Seq.get? s✝ (n + 1) = some gp_succ_n✝
m : ℕ
IH :
  ∀ {s : Stream'.Seq (Pair K)} (gp_succ_n : Pair K),
    Stream'.Seq.get? s (m + 1) = some gp_succ_n → convergents'Aux s (m + 2) = convergents'Aux (squashSeq s m) (m + 1)
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (Nat.succ m + 1) = some gp_succ_n
gp_head : Pair K
s_head_eq : Stream'.Seq.head s = some gp_head
⊢ Stream'.Seq.get? (Stream'.Seq.tail s) (m + 1) = some gp_succ_n
[PROOFSTEP]
simpa [Stream'.Seq.get?_tail] using s_succ_nth_eq
[GOAL]
case intro
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s✝ : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_n✝ : Pair K
s_succ_nth_eq✝ : Stream'.Seq.get? s✝ (n + 1) = some gp_succ_n✝
m : ℕ
IH :
  ∀ {s : Stream'.Seq (Pair K)} (gp_succ_n : Pair K),
    Stream'.Seq.get? s (m + 1) = some gp_succ_n → convergents'Aux s (m + 2) = convergents'Aux (squashSeq s m) (m + 1)
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (Nat.succ m + 1) = some gp_succ_n
gp_head : Pair K
s_head_eq : Stream'.Seq.head s = some gp_head
this : convergents'Aux (Stream'.Seq.tail s) (m + 2) = convergents'Aux (squashSeq (Stream'.Seq.tail s) m) (m + 1)
⊢ gp_head.a / (gp_head.b + convergents'Aux (Stream'.Seq.tail s) (m + 2)) = convergents'Aux (squashSeq s (m + 1)) (m + 2)
[PROOFSTEP]
have : (squashSeq s (m + 1)).head = some gp_head := (squashSeq_nth_of_lt m.succ_pos).trans s_head_eq
[GOAL]
case intro
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s✝ : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_n✝ : Pair K
s_succ_nth_eq✝ : Stream'.Seq.get? s✝ (n + 1) = some gp_succ_n✝
m : ℕ
IH :
  ∀ {s : Stream'.Seq (Pair K)} (gp_succ_n : Pair K),
    Stream'.Seq.get? s (m + 1) = some gp_succ_n → convergents'Aux s (m + 2) = convergents'Aux (squashSeq s m) (m + 1)
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : Stream'.Seq.get? s (Nat.succ m + 1) = some gp_succ_n
gp_head : Pair K
s_head_eq : Stream'.Seq.head s = some gp_head
this✝ : convergents'Aux (Stream'.Seq.tail s) (m + 2) = convergents'Aux (squashSeq (Stream'.Seq.tail s) m) (m + 1)
this : Stream'.Seq.head (squashSeq s (m + 1)) = some gp_head
⊢ gp_head.a / (gp_head.b + convergents'Aux (Stream'.Seq.tail s) (m + 2)) = convergents'Aux (squashSeq s (m + 1)) (m + 2)
[PROOFSTEP]
simp_all [convergents'Aux, squashSeq_succ_n_tail_eq_squashSeq_tail_n]
[GOAL]
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
terminated_at_n : TerminatedAt g n
⊢ squashGCF g n = g
[PROOFSTEP]
cases n
[GOAL]
case zero
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
terminated_at_n : TerminatedAt g Nat.zero
⊢ squashGCF g Nat.zero = g
case succ
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
n✝ : ℕ
terminated_at_n : TerminatedAt g (Nat.succ n✝)
⊢ squashGCF g (Nat.succ n✝) = g
[PROOFSTEP]
case zero =>
  change g.s.get? 0 = none at terminated_at_n 
  simp only [convergents', squashGCF, convergents'Aux, terminated_at_n]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
terminated_at_n : TerminatedAt g Nat.zero
⊢ squashGCF g Nat.zero = g
[PROOFSTEP]
case zero =>
  change g.s.get? 0 = none at terminated_at_n 
  simp only [convergents', squashGCF, convergents'Aux, terminated_at_n]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
terminated_at_n : TerminatedAt g Nat.zero
⊢ squashGCF g Nat.zero = g
[PROOFSTEP]
change g.s.get? 0 = none at terminated_at_n 
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
terminated_at_n : Stream'.Seq.get? g.s 0 = none
⊢ squashGCF g Nat.zero = g
[PROOFSTEP]
simp only [convergents', squashGCF, convergents'Aux, terminated_at_n]
[GOAL]
case succ
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
n✝ : ℕ
terminated_at_n : TerminatedAt g (Nat.succ n✝)
⊢ squashGCF g (Nat.succ n✝) = g
[PROOFSTEP]
case succ =>
  cases g
  simp only [squashGCF, mk.injEq, true_and]
  exact squashSeq_eq_self_of_terminated terminated_at_n
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
n✝ : ℕ
terminated_at_n : TerminatedAt g (Nat.succ n✝)
⊢ squashGCF g (Nat.succ n✝) = g
[PROOFSTEP]
case succ =>
  cases g
  simp only [squashGCF, mk.injEq, true_and]
  exact squashSeq_eq_self_of_terminated terminated_at_n
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
n✝ : ℕ
terminated_at_n : TerminatedAt g (Nat.succ n✝)
⊢ squashGCF g (Nat.succ n✝) = g
[PROOFSTEP]
cases g
[GOAL]
case mk
K : Type u_1
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
n✝ : ℕ
h✝ : K
s✝ : Stream'.Seq (Pair K)
terminated_at_n : TerminatedAt { h := h✝, s := s✝ } (Nat.succ n✝)
⊢ squashGCF { h := h✝, s := s✝ } (Nat.succ n✝) = { h := h✝, s := s✝ }
[PROOFSTEP]
simp only [squashGCF, mk.injEq, true_and]
[GOAL]
case mk
K : Type u_1
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
n✝ : ℕ
h✝ : K
s✝ : Stream'.Seq (Pair K)
terminated_at_n : TerminatedAt { h := h✝, s := s✝ } (Nat.succ n✝)
⊢ squashSeq s✝ n✝ = s✝
[PROOFSTEP]
exact squashSeq_eq_self_of_terminated terminated_at_n
[GOAL]
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? (squashGCF g (n + 1)).s m = Stream'.Seq.get? g.s m
[PROOFSTEP]
simp only [squashGCF, squashSeq_nth_of_lt m_lt_n, Nat.add_eq, add_zero]
[GOAL]
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
⊢ convergents' g (n + 1) = convergents' (squashGCF g n) n
[PROOFSTEP]
cases n
[GOAL]
case zero
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
⊢ convergents' g (Nat.zero + 1) = convergents' (squashGCF g Nat.zero) Nat.zero
case succ
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
n✝ : ℕ
⊢ convergents' g (Nat.succ n✝ + 1) = convergents' (squashGCF g (Nat.succ n✝)) (Nat.succ n✝)
[PROOFSTEP]
case zero =>
  cases g_s_head_eq : g.s.get? 0 <;> simp [g_s_head_eq, squashGCF, convergents', convergents'Aux, Stream'.Seq.head]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
⊢ convergents' g (Nat.zero + 1) = convergents' (squashGCF g Nat.zero) Nat.zero
[PROOFSTEP]
case zero =>
  cases g_s_head_eq : g.s.get? 0 <;> simp [g_s_head_eq, squashGCF, convergents', convergents'Aux, Stream'.Seq.head]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
⊢ convergents' g (Nat.zero + 1) = convergents' (squashGCF g Nat.zero) Nat.zero
[PROOFSTEP]
cases g_s_head_eq : g.s.get? 0
[GOAL]
case none
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
g_s_head_eq : Stream'.Seq.get? g.s 0 = none
⊢ convergents' g (Nat.zero + 1) = convergents' (squashGCF g Nat.zero) Nat.zero
[PROOFSTEP]
simp [g_s_head_eq, squashGCF, convergents', convergents'Aux, Stream'.Seq.head]
[GOAL]
case some
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
val✝ : Pair K
g_s_head_eq : Stream'.Seq.get? g.s 0 = some val✝
⊢ convergents' g (Nat.zero + 1) = convergents' (squashGCF g Nat.zero) Nat.zero
[PROOFSTEP]
simp [g_s_head_eq, squashGCF, convergents', convergents'Aux, Stream'.Seq.head]
[GOAL]
case succ
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
n✝ : ℕ
⊢ convergents' g (Nat.succ n✝ + 1) = convergents' (squashGCF g (Nat.succ n✝)) (Nat.succ n✝)
[PROOFSTEP]
case succ => simp only [succ_succ_nth_convergent'_aux_eq_succ_nth_convergent'_aux_squashSeq, convergents', squashGCF]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
n✝ : ℕ
⊢ convergents' g (Nat.succ n✝ + 1) = convergents' (squashGCF g (Nat.succ n✝)) (Nat.succ n✝)
[PROOFSTEP]
case succ => simp only [succ_succ_nth_convergent'_aux_eq_succ_nth_convergent'_aux_squashSeq, convergents', squashGCF]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
n✝ : ℕ
⊢ convergents' g (Nat.succ n✝ + 1) = convergents' (squashGCF g (Nat.succ n✝)) (Nat.succ n✝)
[PROOFSTEP]
simp only [succ_succ_nth_convergent'_aux_eq_succ_nth_convergent'_aux_squashSeq, convergents', squashGCF]
[GOAL]
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
⊢ ∀ (n_1 : ℕ),
    (∀ (m : ℕ), m < n_1 → m ≤ n → continuantsAux g m = continuantsAux (squashGCF g n) m) →
      n_1 ≤ n → continuantsAux g n_1 = continuantsAux (squashGCF g n) n_1
[PROOFSTEP]
clear m
[GOAL]
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
⊢ ∀ (n_1 : ℕ),
    (∀ (m : ℕ), m < n_1 → m ≤ n → continuantsAux g m = continuantsAux (squashGCF g n) m) →
      n_1 ≤ n → continuantsAux g n_1 = continuantsAux (squashGCF g n) n_1
[PROOFSTEP]
intro m IH m_le_n
[GOAL]
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
IH : ∀ (m_1 : ℕ), m_1 < m → m_1 ≤ n → continuantsAux g m_1 = continuantsAux (squashGCF g n) m_1
m_le_n : m ≤ n
⊢ continuantsAux g m = continuantsAux (squashGCF g n) m
[PROOFSTEP]
cases' m with m'
[GOAL]
case zero
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
IH : ∀ (m : ℕ), m < Nat.zero → m ≤ n → continuantsAux g m = continuantsAux (squashGCF g n) m
m_le_n : Nat.zero ≤ n
⊢ continuantsAux g Nat.zero = continuantsAux (squashGCF g n) Nat.zero
[PROOFSTEP]
rfl
[GOAL]
case succ
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m' : ℕ
IH : ∀ (m : ℕ), m < Nat.succ m' → m ≤ n → continuantsAux g m = continuantsAux (squashGCF g n) m
m_le_n : Nat.succ m' ≤ n
⊢ continuantsAux g (Nat.succ m') = continuantsAux (squashGCF g n) (Nat.succ m')
[PROOFSTEP]
cases' n with n'
[GOAL]
case succ.zero
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m' : ℕ
IH : ∀ (m : ℕ), m < Nat.succ m' → m ≤ Nat.zero → continuantsAux g m = continuantsAux (squashGCF g Nat.zero) m
m_le_n : Nat.succ m' ≤ Nat.zero
⊢ continuantsAux g (Nat.succ m') = continuantsAux (squashGCF g Nat.zero) (Nat.succ m')
[PROOFSTEP]
exact (m'.not_succ_le_zero m_le_n).elim
[GOAL]
case succ.succ
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m' n' : ℕ
IH : ∀ (m : ℕ), m < Nat.succ m' → m ≤ Nat.succ n' → continuantsAux g m = continuantsAux (squashGCF g (Nat.succ n')) m
m_le_n : Nat.succ m' ≤ Nat.succ n'
⊢ continuantsAux g (Nat.succ m') = continuantsAux (squashGCF g (Nat.succ n')) (Nat.succ m')
[PROOFSTEP]
cases' m' with m''
[GOAL]
case succ.succ.zero
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
n' : ℕ
IH :
  ∀ (m : ℕ), m < Nat.succ Nat.zero → m ≤ Nat.succ n' → continuantsAux g m = continuantsAux (squashGCF g (Nat.succ n')) m
m_le_n : Nat.succ Nat.zero ≤ Nat.succ n'
⊢ continuantsAux g (Nat.succ Nat.zero) = continuantsAux (squashGCF g (Nat.succ n')) (Nat.succ Nat.zero)
[PROOFSTEP]
rfl
[GOAL]
case succ.succ.succ
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
n' m'' : ℕ
IH :
  ∀ (m : ℕ),
    m < Nat.succ (Nat.succ m'') → m ≤ Nat.succ n' → continuantsAux g m = continuantsAux (squashGCF g (Nat.succ n')) m
m_le_n : Nat.succ (Nat.succ m'') ≤ Nat.succ n'
⊢ continuantsAux g (Nat.succ (Nat.succ m'')) = continuantsAux (squashGCF g (Nat.succ n')) (Nat.succ (Nat.succ m''))
[PROOFSTEP]
have m'_lt_n : m'' + 1 < n' + 1 := m_le_n
[GOAL]
case succ.succ.succ
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
n' m'' : ℕ
IH :
  ∀ (m : ℕ),
    m < Nat.succ (Nat.succ m'') → m ≤ Nat.succ n' → continuantsAux g m = continuantsAux (squashGCF g (Nat.succ n')) m
m_le_n : Nat.succ (Nat.succ m'') ≤ Nat.succ n'
m'_lt_n : m'' + 1 < n' + 1
⊢ continuantsAux g (Nat.succ (Nat.succ m'')) = continuantsAux (squashGCF g (Nat.succ n')) (Nat.succ (Nat.succ m''))
[PROOFSTEP]
have succ_m''th_conts_aux_eq := IH (m'' + 1) (lt_add_one (m'' + 1)) m'_lt_n.le
[GOAL]
case succ.succ.succ
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
n' m'' : ℕ
IH :
  ∀ (m : ℕ),
    m < Nat.succ (Nat.succ m'') → m ≤ Nat.succ n' → continuantsAux g m = continuantsAux (squashGCF g (Nat.succ n')) m
m_le_n : Nat.succ (Nat.succ m'') ≤ Nat.succ n'
m'_lt_n : m'' + 1 < n' + 1
succ_m''th_conts_aux_eq : continuantsAux g (m'' + 1) = continuantsAux (squashGCF g (Nat.succ n')) (m'' + 1)
⊢ continuantsAux g (Nat.succ (Nat.succ m'')) = continuantsAux (squashGCF g (Nat.succ n')) (Nat.succ (Nat.succ m''))
[PROOFSTEP]
have : m'' < m'' + 2 := lt_add_of_pos_right m'' zero_lt_two
[GOAL]
case succ.succ.succ
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
n' m'' : ℕ
IH :
  ∀ (m : ℕ),
    m < Nat.succ (Nat.succ m'') → m ≤ Nat.succ n' → continuantsAux g m = continuantsAux (squashGCF g (Nat.succ n')) m
m_le_n : Nat.succ (Nat.succ m'') ≤ Nat.succ n'
m'_lt_n : m'' + 1 < n' + 1
succ_m''th_conts_aux_eq : continuantsAux g (m'' + 1) = continuantsAux (squashGCF g (Nat.succ n')) (m'' + 1)
this : m'' < m'' + 2
⊢ continuantsAux g (Nat.succ (Nat.succ m'')) = continuantsAux (squashGCF g (Nat.succ n')) (Nat.succ (Nat.succ m''))
[PROOFSTEP]
have m''th_conts_aux_eq := IH m'' this (le_trans this.le m_le_n)
[GOAL]
case succ.succ.succ
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
n' m'' : ℕ
IH :
  ∀ (m : ℕ),
    m < Nat.succ (Nat.succ m'') → m ≤ Nat.succ n' → continuantsAux g m = continuantsAux (squashGCF g (Nat.succ n')) m
m_le_n : Nat.succ (Nat.succ m'') ≤ Nat.succ n'
m'_lt_n : m'' + 1 < n' + 1
succ_m''th_conts_aux_eq : continuantsAux g (m'' + 1) = continuantsAux (squashGCF g (Nat.succ n')) (m'' + 1)
this : m'' < m'' + 2
m''th_conts_aux_eq : continuantsAux g m'' = continuantsAux (squashGCF g (Nat.succ n')) m''
⊢ continuantsAux g (Nat.succ (Nat.succ m'')) = continuantsAux (squashGCF g (Nat.succ n')) (Nat.succ (Nat.succ m''))
[PROOFSTEP]
have : (squashGCF g (n' + 1)).s.get? m'' = g.s.get? m'' := squashGCF_nth_of_lt (Nat.succ_lt_succ_iff.mp m'_lt_n)
[GOAL]
case succ.succ.succ
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
n' m'' : ℕ
IH :
  ∀ (m : ℕ),
    m < Nat.succ (Nat.succ m'') → m ≤ Nat.succ n' → continuantsAux g m = continuantsAux (squashGCF g (Nat.succ n')) m
m_le_n : Nat.succ (Nat.succ m'') ≤ Nat.succ n'
m'_lt_n : m'' + 1 < n' + 1
succ_m''th_conts_aux_eq : continuantsAux g (m'' + 1) = continuantsAux (squashGCF g (Nat.succ n')) (m'' + 1)
this✝ : m'' < m'' + 2
m''th_conts_aux_eq : continuantsAux g m'' = continuantsAux (squashGCF g (Nat.succ n')) m''
this : Stream'.Seq.get? (squashGCF g (n' + 1)).s m'' = Stream'.Seq.get? g.s m''
⊢ continuantsAux g (Nat.succ (Nat.succ m'')) = continuantsAux (squashGCF g (Nat.succ n')) (Nat.succ (Nat.succ m''))
[PROOFSTEP]
simp [continuantsAux, succ_m''th_conts_aux_eq, m''th_conts_aux_eq, this]
[GOAL]
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) n = some b → b ≠ 0
⊢ convergents g (n + 1) = convergents (squashGCF g n) n
[PROOFSTEP]
cases' Decidable.em (g.TerminatedAt n) with terminated_at_n not_terminated_at_n
[GOAL]
case inl
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) n = some b → b ≠ 0
terminated_at_n : TerminatedAt g n
⊢ convergents g (n + 1) = convergents (squashGCF g n) n
[PROOFSTEP]
have : squashGCF g n = g := squashGCF_eq_self_of_terminated terminated_at_n
[GOAL]
case inl
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) n = some b → b ≠ 0
terminated_at_n : TerminatedAt g n
this : squashGCF g n = g
⊢ convergents g (n + 1) = convergents (squashGCF g n) n
[PROOFSTEP]
simp only [this, convergents_stable_of_terminated n.le_succ terminated_at_n]
[GOAL]
case inr
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) n = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g n
⊢ convergents g (n + 1) = convergents (squashGCF g n) n
[PROOFSTEP]
obtain ⟨⟨a, b⟩, s_nth_eq⟩ : ∃ gp_n, g.s.get? n = some gp_n
[GOAL]
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) n = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g n
⊢ ∃ gp_n, Stream'.Seq.get? g.s n = some gp_n
case inr.intro.mk
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) n = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g n
a b : K
s_nth_eq : Stream'.Seq.get? g.s n = some { a := a, b := b }
⊢ convergents g (n + 1) = convergents (squashGCF g n) n
[PROOFSTEP]
exact Option.ne_none_iff_exists'.mp not_terminated_at_n
[GOAL]
case inr.intro.mk
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) n = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g n
a b : K
s_nth_eq : Stream'.Seq.get? g.s n = some { a := a, b := b }
⊢ convergents g (n + 1) = convergents (squashGCF g n) n
[PROOFSTEP]
have b_ne_zero : b ≠ 0 := nth_part_denom_ne_zero (part_denom_eq_s_b s_nth_eq)
[GOAL]
case inr.intro.mk
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) n = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g n
a b : K
s_nth_eq : Stream'.Seq.get? g.s n = some { a := a, b := b }
b_ne_zero : b ≠ 0
⊢ convergents g (n + 1) = convergents (squashGCF g n) n
[PROOFSTEP]
cases' n with n'
[GOAL]
case inr.intro.mk.zero
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) Nat.zero = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g Nat.zero
s_nth_eq : Stream'.Seq.get? g.s Nat.zero = some { a := a, b := b }
⊢ convergents g (Nat.zero + 1) = convergents (squashGCF g Nat.zero) Nat.zero
case inr.intro.mk.succ
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) (Nat.succ n') = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g (Nat.succ n')
s_nth_eq : Stream'.Seq.get? g.s (Nat.succ n') = some { a := a, b := b }
⊢ convergents g (Nat.succ n' + 1) = convergents (squashGCF g (Nat.succ n')) (Nat.succ n')
[PROOFSTEP]
case
  zero =>
  suffices (b * g.h + a) / b = g.h + a / b by
    simpa [squashGCF, s_nth_eq, convergent_eq_conts_a_div_conts_b,
      continuants_recurrenceAux s_nth_eq zeroth_continuant_aux_eq_one_zero first_continuant_aux_eq_h_one]
  calc
    (b * g.h + a) / b = b * g.h / b + a / b := by
      ring
        -- requires `Field`, not `DivisionRing`
    _ = g.h + a / b := by rw [mul_div_cancel_left _ b_ne_zero]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) Nat.zero = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g Nat.zero
s_nth_eq : Stream'.Seq.get? g.s Nat.zero = some { a := a, b := b }
⊢ convergents g (Nat.zero + 1) = convergents (squashGCF g Nat.zero) Nat.zero
[PROOFSTEP]
case
  zero =>
  suffices (b * g.h + a) / b = g.h + a / b by
    simpa [squashGCF, s_nth_eq, convergent_eq_conts_a_div_conts_b,
      continuants_recurrenceAux s_nth_eq zeroth_continuant_aux_eq_one_zero first_continuant_aux_eq_h_one]
  calc
    (b * g.h + a) / b = b * g.h / b + a / b := by
      ring
        -- requires `Field`, not `DivisionRing`
    _ = g.h + a / b := by rw [mul_div_cancel_left _ b_ne_zero]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) Nat.zero = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g Nat.zero
s_nth_eq : Stream'.Seq.get? g.s Nat.zero = some { a := a, b := b }
⊢ convergents g (Nat.zero + 1) = convergents (squashGCF g Nat.zero) Nat.zero
[PROOFSTEP]
suffices (b * g.h + a) / b = g.h + a / b by
  simpa [squashGCF, s_nth_eq, convergent_eq_conts_a_div_conts_b,
    continuants_recurrenceAux s_nth_eq zeroth_continuant_aux_eq_one_zero first_continuant_aux_eq_h_one]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) Nat.zero = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g Nat.zero
s_nth_eq : Stream'.Seq.get? g.s Nat.zero = some { a := a, b := b }
this : (b * g.h + a) / b = g.h + a / b
⊢ convergents g (Nat.zero + 1) = convergents (squashGCF g Nat.zero) Nat.zero
[PROOFSTEP]
simpa [squashGCF, s_nth_eq, convergent_eq_conts_a_div_conts_b,
  continuants_recurrenceAux s_nth_eq zeroth_continuant_aux_eq_one_zero first_continuant_aux_eq_h_one]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) Nat.zero = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g Nat.zero
s_nth_eq : Stream'.Seq.get? g.s Nat.zero = some { a := a, b := b }
⊢ (b * g.h + a) / b = g.h + a / b
[PROOFSTEP]
calc
  (b * g.h + a) / b = b * g.h / b + a / b := by
    ring
      -- requires `Field`, not `DivisionRing`
  _ = g.h + a / b := by rw [mul_div_cancel_left _ b_ne_zero]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) Nat.zero = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g Nat.zero
s_nth_eq : Stream'.Seq.get? g.s Nat.zero = some { a := a, b := b }
⊢ (b * g.h + a) / b = b * g.h / b + a / b
[PROOFSTEP]
ring
  -- requires `Field`, not `DivisionRing`
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) Nat.zero = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g Nat.zero
s_nth_eq : Stream'.Seq.get? g.s Nat.zero = some { a := a, b := b }
⊢ b * g.h / b + a / b = g.h + a / b
[PROOFSTEP]
rw [mul_div_cancel_left _ b_ne_zero]
[GOAL]
case inr.intro.mk.succ
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) (Nat.succ n') = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g (Nat.succ n')
s_nth_eq : Stream'.Seq.get? g.s (Nat.succ n') = some { a := a, b := b }
⊢ convergents g (Nat.succ n' + 1) = convergents (squashGCF g (Nat.succ n')) (Nat.succ n')
[PROOFSTEP]
case
  succ =>
  obtain ⟨⟨pa, pb⟩, s_n'th_eq⟩ : ∃ gp_n', g.s.get? n' = some gp_n' := g.s.ge_stable n'.le_succ s_nth_eq
  let g' := squashGCF g (n' + 1)
  set pred_conts := g.continuantsAux (n' + 1) with succ_n'th_conts_aux_eq
  set ppred_conts := g.continuantsAux n' with n'th_conts_aux_eq
  let pA := pred_conts.a
  let pB := pred_conts.b
  let ppA := ppred_conts.a
  let ppB := ppred_conts.b
  set pred_conts' := g'.continuantsAux (n' + 1) with succ_n'th_conts_aux_eq'
  set ppred_conts' := g'.continuantsAux n' with n'th_conts_aux_eq'
  let pA' := pred_conts'.a
  let pB' := pred_conts'.b
  let ppA' := ppred_conts'.a
  let ppB' := ppred_conts'.b
  have : g'.convergents (n' + 1) = ((pb + a / b) * pA' + pa * ppA') / ((pb + a / b) * pB' + pa * ppB') :=
    by
    have : g'.s.get? n' = some ⟨pa, pb + a / b⟩ := squashSeq_nth_of_not_terminated s_n'th_eq s_nth_eq
    rw [convergent_eq_conts_a_div_conts_b,
      continuants_recurrenceAux this n'th_conts_aux_eq'.symm succ_n'th_conts_aux_eq'.symm]
  rw [this]
    -- then compute the convergent of the original gcf by recursively unfolding the continuants
          -- computation twice
  have : g.convergents (n' + 2) = (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB) := by
    -- use the recurrence once
    have : g.continuantsAux (n' + 2) = ⟨pb * pA + pa * ppA, pb * pB + pa * ppB⟩ :=
      continuantsAux_recurrence s_n'th_eq n'th_conts_aux_eq.symm succ_n'th_conts_aux_eq.symm
    rw [convergent_eq_conts_a_div_conts_b, continuants_recurrenceAux s_nth_eq succ_n'th_conts_aux_eq.symm this]
  rw [this]
  suffices
    ((pb + a / b) * pA + pa * ppA) / ((pb + a / b) * pB + pa * ppB) =
      (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB)
    by
    obtain ⟨eq1, eq2, eq3, eq4⟩ : pA' = pA ∧ pB' = pB ∧ ppA' = ppA ∧ ppB' = ppB := by
      simp [*, (continuantsAux_eq_continuantsAux_squashGCF_of_le <| le_refl <| n' + 1).symm,
        (continuantsAux_eq_continuantsAux_squashGCF_of_le n'.le_succ).symm]
    symm
    simpa only [eq1, eq2, eq3, eq4, mul_div_cancel _ b_ne_zero]
  field_simp
  congr 1 <;> ring
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) (Nat.succ n') = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g (Nat.succ n')
s_nth_eq : Stream'.Seq.get? g.s (Nat.succ n') = some { a := a, b := b }
⊢ convergents g (Nat.succ n' + 1) = convergents (squashGCF g (Nat.succ n')) (Nat.succ n')
[PROOFSTEP]
case
  succ =>
  obtain ⟨⟨pa, pb⟩, s_n'th_eq⟩ : ∃ gp_n', g.s.get? n' = some gp_n' := g.s.ge_stable n'.le_succ s_nth_eq
  let g' := squashGCF g (n' + 1)
  set pred_conts := g.continuantsAux (n' + 1) with succ_n'th_conts_aux_eq
  set ppred_conts := g.continuantsAux n' with n'th_conts_aux_eq
  let pA := pred_conts.a
  let pB := pred_conts.b
  let ppA := ppred_conts.a
  let ppB := ppred_conts.b
  set pred_conts' := g'.continuantsAux (n' + 1) with succ_n'th_conts_aux_eq'
  set ppred_conts' := g'.continuantsAux n' with n'th_conts_aux_eq'
  let pA' := pred_conts'.a
  let pB' := pred_conts'.b
  let ppA' := ppred_conts'.a
  let ppB' := ppred_conts'.b
  have : g'.convergents (n' + 1) = ((pb + a / b) * pA' + pa * ppA') / ((pb + a / b) * pB' + pa * ppB') :=
    by
    have : g'.s.get? n' = some ⟨pa, pb + a / b⟩ := squashSeq_nth_of_not_terminated s_n'th_eq s_nth_eq
    rw [convergent_eq_conts_a_div_conts_b,
      continuants_recurrenceAux this n'th_conts_aux_eq'.symm succ_n'th_conts_aux_eq'.symm]
  rw [this]
    -- then compute the convergent of the original gcf by recursively unfolding the continuants
          -- computation twice
  have : g.convergents (n' + 2) = (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB) := by
    -- use the recurrence once
    have : g.continuantsAux (n' + 2) = ⟨pb * pA + pa * ppA, pb * pB + pa * ppB⟩ :=
      continuantsAux_recurrence s_n'th_eq n'th_conts_aux_eq.symm succ_n'th_conts_aux_eq.symm
    rw [convergent_eq_conts_a_div_conts_b, continuants_recurrenceAux s_nth_eq succ_n'th_conts_aux_eq.symm this]
  rw [this]
  suffices
    ((pb + a / b) * pA + pa * ppA) / ((pb + a / b) * pB + pa * ppB) =
      (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB)
    by
    obtain ⟨eq1, eq2, eq3, eq4⟩ : pA' = pA ∧ pB' = pB ∧ ppA' = ppA ∧ ppB' = ppB := by
      simp [*, (continuantsAux_eq_continuantsAux_squashGCF_of_le <| le_refl <| n' + 1).symm,
        (continuantsAux_eq_continuantsAux_squashGCF_of_le n'.le_succ).symm]
    symm
    simpa only [eq1, eq2, eq3, eq4, mul_div_cancel _ b_ne_zero]
  field_simp
  congr 1 <;> ring
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) (Nat.succ n') = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g (Nat.succ n')
s_nth_eq : Stream'.Seq.get? g.s (Nat.succ n') = some { a := a, b := b }
⊢ convergents g (Nat.succ n' + 1) = convergents (squashGCF g (Nat.succ n')) (Nat.succ n')
[PROOFSTEP]
obtain ⟨⟨pa, pb⟩, s_n'th_eq⟩ : ∃ gp_n', g.s.get? n' = some gp_n' := g.s.ge_stable n'.le_succ s_nth_eq
[GOAL]
case intro.mk
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) (Nat.succ n') = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g (Nat.succ n')
s_nth_eq : Stream'.Seq.get? g.s (Nat.succ n') = some { a := a, b := b }
pa pb : K
s_n'th_eq : Stream'.Seq.get? g.s n' = some { a := pa, b := pb }
⊢ convergents g (Nat.succ n' + 1) = convergents (squashGCF g (Nat.succ n')) (Nat.succ n')
[PROOFSTEP]
let g' := squashGCF g (n' + 1)
[GOAL]
case intro.mk
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) (Nat.succ n') = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g (Nat.succ n')
s_nth_eq : Stream'.Seq.get? g.s (Nat.succ n') = some { a := a, b := b }
pa pb : K
s_n'th_eq : Stream'.Seq.get? g.s n' = some { a := pa, b := pb }
g' : GeneralizedContinuedFraction K := squashGCF g (n' + 1)
⊢ convergents g (Nat.succ n' + 1) = convergents (squashGCF g (Nat.succ n')) (Nat.succ n')
[PROOFSTEP]
set pred_conts := g.continuantsAux (n' + 1) with succ_n'th_conts_aux_eq
[GOAL]
case intro.mk
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) (Nat.succ n') = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g (Nat.succ n')
s_nth_eq : Stream'.Seq.get? g.s (Nat.succ n') = some { a := a, b := b }
pa pb : K
s_n'th_eq : Stream'.Seq.get? g.s n' = some { a := pa, b := pb }
g' : GeneralizedContinuedFraction K := squashGCF g (n' + 1)
pred_conts : Pair K := continuantsAux g (n' + 1)
succ_n'th_conts_aux_eq : pred_conts = continuantsAux g (n' + 1)
⊢ convergents g (Nat.succ n' + 1) = convergents (squashGCF g (Nat.succ n')) (Nat.succ n')
[PROOFSTEP]
set ppred_conts := g.continuantsAux n' with n'th_conts_aux_eq
[GOAL]
case intro.mk
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) (Nat.succ n') = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g (Nat.succ n')
s_nth_eq : Stream'.Seq.get? g.s (Nat.succ n') = some { a := a, b := b }
pa pb : K
s_n'th_eq : Stream'.Seq.get? g.s n' = some { a := pa, b := pb }
g' : GeneralizedContinuedFraction K := squashGCF g (n' + 1)
pred_conts : Pair K := continuantsAux g (n' + 1)
succ_n'th_conts_aux_eq : pred_conts = continuantsAux g (n' + 1)
ppred_conts : Pair K := continuantsAux g n'
n'th_conts_aux_eq : ppred_conts = continuantsAux g n'
⊢ convergents g (Nat.succ n' + 1) = convergents (squashGCF g (Nat.succ n')) (Nat.succ n')
[PROOFSTEP]
let pA := pred_conts.a
[GOAL]
case intro.mk
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) (Nat.succ n') = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g (Nat.succ n')
s_nth_eq : Stream'.Seq.get? g.s (Nat.succ n') = some { a := a, b := b }
pa pb : K
s_n'th_eq : Stream'.Seq.get? g.s n' = some { a := pa, b := pb }
g' : GeneralizedContinuedFraction K := squashGCF g (n' + 1)
pred_conts : Pair K := continuantsAux g (n' + 1)
succ_n'th_conts_aux_eq : pred_conts = continuantsAux g (n' + 1)
ppred_conts : Pair K := continuantsAux g n'
n'th_conts_aux_eq : ppred_conts = continuantsAux g n'
pA : K := pred_conts.a
⊢ convergents g (Nat.succ n' + 1) = convergents (squashGCF g (Nat.succ n')) (Nat.succ n')
[PROOFSTEP]
let pB := pred_conts.b
[GOAL]
case intro.mk
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) (Nat.succ n') = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g (Nat.succ n')
s_nth_eq : Stream'.Seq.get? g.s (Nat.succ n') = some { a := a, b := b }
pa pb : K
s_n'th_eq : Stream'.Seq.get? g.s n' = some { a := pa, b := pb }
g' : GeneralizedContinuedFraction K := squashGCF g (n' + 1)
pred_conts : Pair K := continuantsAux g (n' + 1)
succ_n'th_conts_aux_eq : pred_conts = continuantsAux g (n' + 1)
ppred_conts : Pair K := continuantsAux g n'
n'th_conts_aux_eq : ppred_conts = continuantsAux g n'
pA : K := pred_conts.a
pB : K := pred_conts.b
⊢ convergents g (Nat.succ n' + 1) = convergents (squashGCF g (Nat.succ n')) (Nat.succ n')
[PROOFSTEP]
let ppA := ppred_conts.a
[GOAL]
case intro.mk
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) (Nat.succ n') = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g (Nat.succ n')
s_nth_eq : Stream'.Seq.get? g.s (Nat.succ n') = some { a := a, b := b }
pa pb : K
s_n'th_eq : Stream'.Seq.get? g.s n' = some { a := pa, b := pb }
g' : GeneralizedContinuedFraction K := squashGCF g (n' + 1)
pred_conts : Pair K := continuantsAux g (n' + 1)
succ_n'th_conts_aux_eq : pred_conts = continuantsAux g (n' + 1)
ppred_conts : Pair K := continuantsAux g n'
n'th_conts_aux_eq : ppred_conts = continuantsAux g n'
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
⊢ convergents g (Nat.succ n' + 1) = convergents (squashGCF g (Nat.succ n')) (Nat.succ n')
[PROOFSTEP]
let ppB := ppred_conts.b
[GOAL]
case intro.mk
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) (Nat.succ n') = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g (Nat.succ n')
s_nth_eq : Stream'.Seq.get? g.s (Nat.succ n') = some { a := a, b := b }
pa pb : K
s_n'th_eq : Stream'.Seq.get? g.s n' = some { a := pa, b := pb }
g' : GeneralizedContinuedFraction K := squashGCF g (n' + 1)
pred_conts : Pair K := continuantsAux g (n' + 1)
succ_n'th_conts_aux_eq : pred_conts = continuantsAux g (n' + 1)
ppred_conts : Pair K := continuantsAux g n'
n'th_conts_aux_eq : ppred_conts = continuantsAux g n'
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
⊢ convergents g (Nat.succ n' + 1) = convergents (squashGCF g (Nat.succ n')) (Nat.succ n')
[PROOFSTEP]
set pred_conts' := g'.continuantsAux (n' + 1) with succ_n'th_conts_aux_eq'
[GOAL]
case intro.mk
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) (Nat.succ n') = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g (Nat.succ n')
s_nth_eq : Stream'.Seq.get? g.s (Nat.succ n') = some { a := a, b := b }
pa pb : K
s_n'th_eq : Stream'.Seq.get? g.s n' = some { a := pa, b := pb }
g' : GeneralizedContinuedFraction K := squashGCF g (n' + 1)
pred_conts : Pair K := continuantsAux g (n' + 1)
succ_n'th_conts_aux_eq : pred_conts = continuantsAux g (n' + 1)
ppred_conts : Pair K := continuantsAux g n'
n'th_conts_aux_eq : ppred_conts = continuantsAux g n'
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
pred_conts' : Pair K := continuantsAux g' (n' + 1)
succ_n'th_conts_aux_eq' : pred_conts' = continuantsAux g' (n' + 1)
⊢ convergents g (Nat.succ n' + 1) = convergents (squashGCF g (Nat.succ n')) (Nat.succ n')
[PROOFSTEP]
set ppred_conts' := g'.continuantsAux n' with n'th_conts_aux_eq'
[GOAL]
case intro.mk
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) (Nat.succ n') = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g (Nat.succ n')
s_nth_eq : Stream'.Seq.get? g.s (Nat.succ n') = some { a := a, b := b }
pa pb : K
s_n'th_eq : Stream'.Seq.get? g.s n' = some { a := pa, b := pb }
g' : GeneralizedContinuedFraction K := squashGCF g (n' + 1)
pred_conts : Pair K := continuantsAux g (n' + 1)
succ_n'th_conts_aux_eq : pred_conts = continuantsAux g (n' + 1)
ppred_conts : Pair K := continuantsAux g n'
n'th_conts_aux_eq : ppred_conts = continuantsAux g n'
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
pred_conts' : Pair K := continuantsAux g' (n' + 1)
succ_n'th_conts_aux_eq' : pred_conts' = continuantsAux g' (n' + 1)
ppred_conts' : Pair K := continuantsAux g' n'
n'th_conts_aux_eq' : ppred_conts' = continuantsAux g' n'
⊢ convergents g (Nat.succ n' + 1) = convergents (squashGCF g (Nat.succ n')) (Nat.succ n')
[PROOFSTEP]
let pA' := pred_conts'.a
[GOAL]
case intro.mk
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) (Nat.succ n') = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g (Nat.succ n')
s_nth_eq : Stream'.Seq.get? g.s (Nat.succ n') = some { a := a, b := b }
pa pb : K
s_n'th_eq : Stream'.Seq.get? g.s n' = some { a := pa, b := pb }
g' : GeneralizedContinuedFraction K := squashGCF g (n' + 1)
pred_conts : Pair K := continuantsAux g (n' + 1)
succ_n'th_conts_aux_eq : pred_conts = continuantsAux g (n' + 1)
ppred_conts : Pair K := continuantsAux g n'
n'th_conts_aux_eq : ppred_conts = continuantsAux g n'
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
pred_conts' : Pair K := continuantsAux g' (n' + 1)
succ_n'th_conts_aux_eq' : pred_conts' = continuantsAux g' (n' + 1)
ppred_conts' : Pair K := continuantsAux g' n'
n'th_conts_aux_eq' : ppred_conts' = continuantsAux g' n'
pA' : K := pred_conts'.a
⊢ convergents g (Nat.succ n' + 1) = convergents (squashGCF g (Nat.succ n')) (Nat.succ n')
[PROOFSTEP]
let pB' := pred_conts'.b
[GOAL]
case intro.mk
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) (Nat.succ n') = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g (Nat.succ n')
s_nth_eq : Stream'.Seq.get? g.s (Nat.succ n') = some { a := a, b := b }
pa pb : K
s_n'th_eq : Stream'.Seq.get? g.s n' = some { a := pa, b := pb }
g' : GeneralizedContinuedFraction K := squashGCF g (n' + 1)
pred_conts : Pair K := continuantsAux g (n' + 1)
succ_n'th_conts_aux_eq : pred_conts = continuantsAux g (n' + 1)
ppred_conts : Pair K := continuantsAux g n'
n'th_conts_aux_eq : ppred_conts = continuantsAux g n'
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
pred_conts' : Pair K := continuantsAux g' (n' + 1)
succ_n'th_conts_aux_eq' : pred_conts' = continuantsAux g' (n' + 1)
ppred_conts' : Pair K := continuantsAux g' n'
n'th_conts_aux_eq' : ppred_conts' = continuantsAux g' n'
pA' : K := pred_conts'.a
pB' : K := pred_conts'.b
⊢ convergents g (Nat.succ n' + 1) = convergents (squashGCF g (Nat.succ n')) (Nat.succ n')
[PROOFSTEP]
let ppA' := ppred_conts'.a
[GOAL]
case intro.mk
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) (Nat.succ n') = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g (Nat.succ n')
s_nth_eq : Stream'.Seq.get? g.s (Nat.succ n') = some { a := a, b := b }
pa pb : K
s_n'th_eq : Stream'.Seq.get? g.s n' = some { a := pa, b := pb }
g' : GeneralizedContinuedFraction K := squashGCF g (n' + 1)
pred_conts : Pair K := continuantsAux g (n' + 1)
succ_n'th_conts_aux_eq : pred_conts = continuantsAux g (n' + 1)
ppred_conts : Pair K := continuantsAux g n'
n'th_conts_aux_eq : ppred_conts = continuantsAux g n'
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
pred_conts' : Pair K := continuantsAux g' (n' + 1)
succ_n'th_conts_aux_eq' : pred_conts' = continuantsAux g' (n' + 1)
ppred_conts' : Pair K := continuantsAux g' n'
n'th_conts_aux_eq' : ppred_conts' = continuantsAux g' n'
pA' : K := pred_conts'.a
pB' : K := pred_conts'.b
ppA' : K := ppred_conts'.a
⊢ convergents g (Nat.succ n' + 1) = convergents (squashGCF g (Nat.succ n')) (Nat.succ n')
[PROOFSTEP]
let ppB' := ppred_conts'.b
[GOAL]
case intro.mk
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) (Nat.succ n') = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g (Nat.succ n')
s_nth_eq : Stream'.Seq.get? g.s (Nat.succ n') = some { a := a, b := b }
pa pb : K
s_n'th_eq : Stream'.Seq.get? g.s n' = some { a := pa, b := pb }
g' : GeneralizedContinuedFraction K := squashGCF g (n' + 1)
pred_conts : Pair K := continuantsAux g (n' + 1)
succ_n'th_conts_aux_eq : pred_conts = continuantsAux g (n' + 1)
ppred_conts : Pair K := continuantsAux g n'
n'th_conts_aux_eq : ppred_conts = continuantsAux g n'
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
pred_conts' : Pair K := continuantsAux g' (n' + 1)
succ_n'th_conts_aux_eq' : pred_conts' = continuantsAux g' (n' + 1)
ppred_conts' : Pair K := continuantsAux g' n'
n'th_conts_aux_eq' : ppred_conts' = continuantsAux g' n'
pA' : K := pred_conts'.a
pB' : K := pred_conts'.b
ppA' : K := ppred_conts'.a
ppB' : K := ppred_conts'.b
⊢ convergents g (Nat.succ n' + 1) = convergents (squashGCF g (Nat.succ n')) (Nat.succ n')
[PROOFSTEP]
have : g'.convergents (n' + 1) = ((pb + a / b) * pA' + pa * ppA') / ((pb + a / b) * pB' + pa * ppB') :=
  by
  have : g'.s.get? n' = some ⟨pa, pb + a / b⟩ := squashSeq_nth_of_not_terminated s_n'th_eq s_nth_eq
  rw [convergent_eq_conts_a_div_conts_b,
    continuants_recurrenceAux this n'th_conts_aux_eq'.symm succ_n'th_conts_aux_eq'.symm]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) (Nat.succ n') = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g (Nat.succ n')
s_nth_eq : Stream'.Seq.get? g.s (Nat.succ n') = some { a := a, b := b }
pa pb : K
s_n'th_eq : Stream'.Seq.get? g.s n' = some { a := pa, b := pb }
g' : GeneralizedContinuedFraction K := squashGCF g (n' + 1)
pred_conts : Pair K := continuantsAux g (n' + 1)
succ_n'th_conts_aux_eq : pred_conts = continuantsAux g (n' + 1)
ppred_conts : Pair K := continuantsAux g n'
n'th_conts_aux_eq : ppred_conts = continuantsAux g n'
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
pred_conts' : Pair K := continuantsAux g' (n' + 1)
succ_n'th_conts_aux_eq' : pred_conts' = continuantsAux g' (n' + 1)
ppred_conts' : Pair K := continuantsAux g' n'
n'th_conts_aux_eq' : ppred_conts' = continuantsAux g' n'
pA' : K := pred_conts'.a
pB' : K := pred_conts'.b
ppA' : K := ppred_conts'.a
ppB' : K := ppred_conts'.b
⊢ convergents g' (n' + 1) = ((pb + a / b) * pA' + pa * ppA') / ((pb + a / b) * pB' + pa * ppB')
[PROOFSTEP]
have : g'.s.get? n' = some ⟨pa, pb + a / b⟩ := squashSeq_nth_of_not_terminated s_n'th_eq s_nth_eq
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) (Nat.succ n') = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g (Nat.succ n')
s_nth_eq : Stream'.Seq.get? g.s (Nat.succ n') = some { a := a, b := b }
pa pb : K
s_n'th_eq : Stream'.Seq.get? g.s n' = some { a := pa, b := pb }
g' : GeneralizedContinuedFraction K := squashGCF g (n' + 1)
pred_conts : Pair K := continuantsAux g (n' + 1)
succ_n'th_conts_aux_eq : pred_conts = continuantsAux g (n' + 1)
ppred_conts : Pair K := continuantsAux g n'
n'th_conts_aux_eq : ppred_conts = continuantsAux g n'
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
pred_conts' : Pair K := continuantsAux g' (n' + 1)
succ_n'th_conts_aux_eq' : pred_conts' = continuantsAux g' (n' + 1)
ppred_conts' : Pair K := continuantsAux g' n'
n'th_conts_aux_eq' : ppred_conts' = continuantsAux g' n'
pA' : K := pred_conts'.a
pB' : K := pred_conts'.b
ppA' : K := ppred_conts'.a
ppB' : K := ppred_conts'.b
this : Stream'.Seq.get? g'.s n' = some { a := pa, b := pb + a / b }
⊢ convergents g' (n' + 1) = ((pb + a / b) * pA' + pa * ppA') / ((pb + a / b) * pB' + pa * ppB')
[PROOFSTEP]
rw [convergent_eq_conts_a_div_conts_b,
  continuants_recurrenceAux this n'th_conts_aux_eq'.symm succ_n'th_conts_aux_eq'.symm]
[GOAL]
case intro.mk
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) (Nat.succ n') = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g (Nat.succ n')
s_nth_eq : Stream'.Seq.get? g.s (Nat.succ n') = some { a := a, b := b }
pa pb : K
s_n'th_eq : Stream'.Seq.get? g.s n' = some { a := pa, b := pb }
g' : GeneralizedContinuedFraction K := squashGCF g (n' + 1)
pred_conts : Pair K := continuantsAux g (n' + 1)
succ_n'th_conts_aux_eq : pred_conts = continuantsAux g (n' + 1)
ppred_conts : Pair K := continuantsAux g n'
n'th_conts_aux_eq : ppred_conts = continuantsAux g n'
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
pred_conts' : Pair K := continuantsAux g' (n' + 1)
succ_n'th_conts_aux_eq' : pred_conts' = continuantsAux g' (n' + 1)
ppred_conts' : Pair K := continuantsAux g' n'
n'th_conts_aux_eq' : ppred_conts' = continuantsAux g' n'
pA' : K := pred_conts'.a
pB' : K := pred_conts'.b
ppA' : K := ppred_conts'.a
ppB' : K := ppred_conts'.b
this : convergents g' (n' + 1) = ((pb + a / b) * pA' + pa * ppA') / ((pb + a / b) * pB' + pa * ppB')
⊢ convergents g (Nat.succ n' + 1) = convergents (squashGCF g (Nat.succ n')) (Nat.succ n')
[PROOFSTEP]
rw [this]
  -- then compute the convergent of the original gcf by recursively unfolding the continuants
        -- computation twice
[GOAL]
case intro.mk
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) (Nat.succ n') = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g (Nat.succ n')
s_nth_eq : Stream'.Seq.get? g.s (Nat.succ n') = some { a := a, b := b }
pa pb : K
s_n'th_eq : Stream'.Seq.get? g.s n' = some { a := pa, b := pb }
g' : GeneralizedContinuedFraction K := squashGCF g (n' + 1)
pred_conts : Pair K := continuantsAux g (n' + 1)
succ_n'th_conts_aux_eq : pred_conts = continuantsAux g (n' + 1)
ppred_conts : Pair K := continuantsAux g n'
n'th_conts_aux_eq : ppred_conts = continuantsAux g n'
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
pred_conts' : Pair K := continuantsAux g' (n' + 1)
succ_n'th_conts_aux_eq' : pred_conts' = continuantsAux g' (n' + 1)
ppred_conts' : Pair K := continuantsAux g' n'
n'th_conts_aux_eq' : ppred_conts' = continuantsAux g' n'
pA' : K := pred_conts'.a
pB' : K := pred_conts'.b
ppA' : K := ppred_conts'.a
ppB' : K := ppred_conts'.b
this : convergents g' (n' + 1) = ((pb + a / b) * pA' + pa * ppA') / ((pb + a / b) * pB' + pa * ppB')
⊢ convergents g (Nat.succ n' + 1) = ((pb + a / b) * pA' + pa * ppA') / ((pb + a / b) * pB' + pa * ppB')
[PROOFSTEP]
have : g.convergents (n' + 2) = (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB) := by
  -- use the recurrence once
  have : g.continuantsAux (n' + 2) = ⟨pb * pA + pa * ppA, pb * pB + pa * ppB⟩ :=
    continuantsAux_recurrence s_n'th_eq n'th_conts_aux_eq.symm succ_n'th_conts_aux_eq.symm
  rw [convergent_eq_conts_a_div_conts_b, continuants_recurrenceAux s_nth_eq succ_n'th_conts_aux_eq.symm this]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) (Nat.succ n') = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g (Nat.succ n')
s_nth_eq : Stream'.Seq.get? g.s (Nat.succ n') = some { a := a, b := b }
pa pb : K
s_n'th_eq : Stream'.Seq.get? g.s n' = some { a := pa, b := pb }
g' : GeneralizedContinuedFraction K := squashGCF g (n' + 1)
pred_conts : Pair K := continuantsAux g (n' + 1)
succ_n'th_conts_aux_eq : pred_conts = continuantsAux g (n' + 1)
ppred_conts : Pair K := continuantsAux g n'
n'th_conts_aux_eq : ppred_conts = continuantsAux g n'
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
pred_conts' : Pair K := continuantsAux g' (n' + 1)
succ_n'th_conts_aux_eq' : pred_conts' = continuantsAux g' (n' + 1)
ppred_conts' : Pair K := continuantsAux g' n'
n'th_conts_aux_eq' : ppred_conts' = continuantsAux g' n'
pA' : K := pred_conts'.a
pB' : K := pred_conts'.b
ppA' : K := ppred_conts'.a
ppB' : K := ppred_conts'.b
this : convergents g' (n' + 1) = ((pb + a / b) * pA' + pa * ppA') / ((pb + a / b) * pB' + pa * ppB')
⊢ convergents g (n' + 2) = (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB)
[PROOFSTEP]
have : g.continuantsAux (n' + 2) = ⟨pb * pA + pa * ppA, pb * pB + pa * ppB⟩ :=
  continuantsAux_recurrence s_n'th_eq n'th_conts_aux_eq.symm succ_n'th_conts_aux_eq.symm
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) (Nat.succ n') = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g (Nat.succ n')
s_nth_eq : Stream'.Seq.get? g.s (Nat.succ n') = some { a := a, b := b }
pa pb : K
s_n'th_eq : Stream'.Seq.get? g.s n' = some { a := pa, b := pb }
g' : GeneralizedContinuedFraction K := squashGCF g (n' + 1)
pred_conts : Pair K := continuantsAux g (n' + 1)
succ_n'th_conts_aux_eq : pred_conts = continuantsAux g (n' + 1)
ppred_conts : Pair K := continuantsAux g n'
n'th_conts_aux_eq : ppred_conts = continuantsAux g n'
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
pred_conts' : Pair K := continuantsAux g' (n' + 1)
succ_n'th_conts_aux_eq' : pred_conts' = continuantsAux g' (n' + 1)
ppred_conts' : Pair K := continuantsAux g' n'
n'th_conts_aux_eq' : ppred_conts' = continuantsAux g' n'
pA' : K := pred_conts'.a
pB' : K := pred_conts'.b
ppA' : K := ppred_conts'.a
ppB' : K := ppred_conts'.b
this✝ : convergents g' (n' + 1) = ((pb + a / b) * pA' + pa * ppA') / ((pb + a / b) * pB' + pa * ppB')
this : continuantsAux g (n' + 2) = { a := pb * pA + pa * ppA, b := pb * pB + pa * ppB }
⊢ convergents g (n' + 2) = (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB)
[PROOFSTEP]
rw [convergent_eq_conts_a_div_conts_b, continuants_recurrenceAux s_nth_eq succ_n'th_conts_aux_eq.symm this]
[GOAL]
case intro.mk
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) (Nat.succ n') = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g (Nat.succ n')
s_nth_eq : Stream'.Seq.get? g.s (Nat.succ n') = some { a := a, b := b }
pa pb : K
s_n'th_eq : Stream'.Seq.get? g.s n' = some { a := pa, b := pb }
g' : GeneralizedContinuedFraction K := squashGCF g (n' + 1)
pred_conts : Pair K := continuantsAux g (n' + 1)
succ_n'th_conts_aux_eq : pred_conts = continuantsAux g (n' + 1)
ppred_conts : Pair K := continuantsAux g n'
n'th_conts_aux_eq : ppred_conts = continuantsAux g n'
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
pred_conts' : Pair K := continuantsAux g' (n' + 1)
succ_n'th_conts_aux_eq' : pred_conts' = continuantsAux g' (n' + 1)
ppred_conts' : Pair K := continuantsAux g' n'
n'th_conts_aux_eq' : ppred_conts' = continuantsAux g' n'
pA' : K := pred_conts'.a
pB' : K := pred_conts'.b
ppA' : K := ppred_conts'.a
ppB' : K := ppred_conts'.b
this✝ : convergents g' (n' + 1) = ((pb + a / b) * pA' + pa * ppA') / ((pb + a / b) * pB' + pa * ppB')
this : convergents g (n' + 2) = (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB)
⊢ convergents g (Nat.succ n' + 1) = ((pb + a / b) * pA' + pa * ppA') / ((pb + a / b) * pB' + pa * ppB')
[PROOFSTEP]
rw [this]
[GOAL]
case intro.mk
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) (Nat.succ n') = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g (Nat.succ n')
s_nth_eq : Stream'.Seq.get? g.s (Nat.succ n') = some { a := a, b := b }
pa pb : K
s_n'th_eq : Stream'.Seq.get? g.s n' = some { a := pa, b := pb }
g' : GeneralizedContinuedFraction K := squashGCF g (n' + 1)
pred_conts : Pair K := continuantsAux g (n' + 1)
succ_n'th_conts_aux_eq : pred_conts = continuantsAux g (n' + 1)
ppred_conts : Pair K := continuantsAux g n'
n'th_conts_aux_eq : ppred_conts = continuantsAux g n'
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
pred_conts' : Pair K := continuantsAux g' (n' + 1)
succ_n'th_conts_aux_eq' : pred_conts' = continuantsAux g' (n' + 1)
ppred_conts' : Pair K := continuantsAux g' n'
n'th_conts_aux_eq' : ppred_conts' = continuantsAux g' n'
pA' : K := pred_conts'.a
pB' : K := pred_conts'.b
ppA' : K := ppred_conts'.a
ppB' : K := ppred_conts'.b
this✝ : convergents g' (n' + 1) = ((pb + a / b) * pA' + pa * ppA') / ((pb + a / b) * pB' + pa * ppB')
this : convergents g (n' + 2) = (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB)
⊢ (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB) =
    ((pb + a / b) * pA' + pa * ppA') / ((pb + a / b) * pB' + pa * ppB')
[PROOFSTEP]
suffices
  ((pb + a / b) * pA + pa * ppA) / ((pb + a / b) * pB + pa * ppB) =
    (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB)
  by
  obtain ⟨eq1, eq2, eq3, eq4⟩ : pA' = pA ∧ pB' = pB ∧ ppA' = ppA ∧ ppB' = ppB := by
    simp [*, (continuantsAux_eq_continuantsAux_squashGCF_of_le <| le_refl <| n' + 1).symm,
      (continuantsAux_eq_continuantsAux_squashGCF_of_le n'.le_succ).symm]
  symm
  simpa only [eq1, eq2, eq3, eq4, mul_div_cancel _ b_ne_zero]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) (Nat.succ n') = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g (Nat.succ n')
s_nth_eq : Stream'.Seq.get? g.s (Nat.succ n') = some { a := a, b := b }
pa pb : K
s_n'th_eq : Stream'.Seq.get? g.s n' = some { a := pa, b := pb }
g' : GeneralizedContinuedFraction K := squashGCF g (n' + 1)
pred_conts : Pair K := continuantsAux g (n' + 1)
succ_n'th_conts_aux_eq : pred_conts = continuantsAux g (n' + 1)
ppred_conts : Pair K := continuantsAux g n'
n'th_conts_aux_eq : ppred_conts = continuantsAux g n'
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
pred_conts' : Pair K := continuantsAux g' (n' + 1)
succ_n'th_conts_aux_eq' : pred_conts' = continuantsAux g' (n' + 1)
ppred_conts' : Pair K := continuantsAux g' n'
n'th_conts_aux_eq' : ppred_conts' = continuantsAux g' n'
pA' : K := pred_conts'.a
pB' : K := pred_conts'.b
ppA' : K := ppred_conts'.a
ppB' : K := ppred_conts'.b
this✝¹ : convergents g' (n' + 1) = ((pb + a / b) * pA' + pa * ppA') / ((pb + a / b) * pB' + pa * ppB')
this✝ : convergents g (n' + 2) = (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB)
this :
  ((pb + a / b) * pA + pa * ppA) / ((pb + a / b) * pB + pa * ppB) =
    (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB)
⊢ (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB) =
    ((pb + a / b) * pA' + pa * ppA') / ((pb + a / b) * pB' + pa * ppB')
[PROOFSTEP]
obtain ⟨eq1, eq2, eq3, eq4⟩ : pA' = pA ∧ pB' = pB ∧ ppA' = ppA ∧ ppB' = ppB := by
  simp [*, (continuantsAux_eq_continuantsAux_squashGCF_of_le <| le_refl <| n' + 1).symm,
    (continuantsAux_eq_continuantsAux_squashGCF_of_le n'.le_succ).symm]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) (Nat.succ n') = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g (Nat.succ n')
s_nth_eq : Stream'.Seq.get? g.s (Nat.succ n') = some { a := a, b := b }
pa pb : K
s_n'th_eq : Stream'.Seq.get? g.s n' = some { a := pa, b := pb }
g' : GeneralizedContinuedFraction K := squashGCF g (n' + 1)
pred_conts : Pair K := continuantsAux g (n' + 1)
succ_n'th_conts_aux_eq : pred_conts = continuantsAux g (n' + 1)
ppred_conts : Pair K := continuantsAux g n'
n'th_conts_aux_eq : ppred_conts = continuantsAux g n'
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
pred_conts' : Pair K := continuantsAux g' (n' + 1)
succ_n'th_conts_aux_eq' : pred_conts' = continuantsAux g' (n' + 1)
ppred_conts' : Pair K := continuantsAux g' n'
n'th_conts_aux_eq' : ppred_conts' = continuantsAux g' n'
pA' : K := pred_conts'.a
pB' : K := pred_conts'.b
ppA' : K := ppred_conts'.a
ppB' : K := ppred_conts'.b
this✝¹ : convergents g' (n' + 1) = ((pb + a / b) * pA' + pa * ppA') / ((pb + a / b) * pB' + pa * ppB')
this✝ : convergents g (n' + 2) = (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB)
this :
  ((pb + a / b) * pA + pa * ppA) / ((pb + a / b) * pB + pa * ppB) =
    (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB)
⊢ pA' = pA ∧ pB' = pB ∧ ppA' = ppA ∧ ppB' = ppB
[PROOFSTEP]
simp [*, (continuantsAux_eq_continuantsAux_squashGCF_of_le <| le_refl <| n' + 1).symm,
  (continuantsAux_eq_continuantsAux_squashGCF_of_le n'.le_succ).symm]
[GOAL]
case intro.intro.intro
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) (Nat.succ n') = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g (Nat.succ n')
s_nth_eq : Stream'.Seq.get? g.s (Nat.succ n') = some { a := a, b := b }
pa pb : K
s_n'th_eq : Stream'.Seq.get? g.s n' = some { a := pa, b := pb }
g' : GeneralizedContinuedFraction K := squashGCF g (n' + 1)
pred_conts : Pair K := continuantsAux g (n' + 1)
succ_n'th_conts_aux_eq : pred_conts = continuantsAux g (n' + 1)
ppred_conts : Pair K := continuantsAux g n'
n'th_conts_aux_eq : ppred_conts = continuantsAux g n'
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
pred_conts' : Pair K := continuantsAux g' (n' + 1)
succ_n'th_conts_aux_eq' : pred_conts' = continuantsAux g' (n' + 1)
ppred_conts' : Pair K := continuantsAux g' n'
n'th_conts_aux_eq' : ppred_conts' = continuantsAux g' n'
pA' : K := pred_conts'.a
pB' : K := pred_conts'.b
ppA' : K := ppred_conts'.a
ppB' : K := ppred_conts'.b
this✝¹ : convergents g' (n' + 1) = ((pb + a / b) * pA' + pa * ppA') / ((pb + a / b) * pB' + pa * ppB')
this✝ : convergents g (n' + 2) = (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB)
this :
  ((pb + a / b) * pA + pa * ppA) / ((pb + a / b) * pB + pa * ppB) =
    (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB)
eq1 : pA' = pA
eq2 : pB' = pB
eq3 : ppA' = ppA
eq4 : ppB' = ppB
⊢ (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB) =
    ((pb + a / b) * pA' + pa * ppA') / ((pb + a / b) * pB' + pa * ppB')
[PROOFSTEP]
symm
[GOAL]
case intro.intro.intro
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) (Nat.succ n') = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g (Nat.succ n')
s_nth_eq : Stream'.Seq.get? g.s (Nat.succ n') = some { a := a, b := b }
pa pb : K
s_n'th_eq : Stream'.Seq.get? g.s n' = some { a := pa, b := pb }
g' : GeneralizedContinuedFraction K := squashGCF g (n' + 1)
pred_conts : Pair K := continuantsAux g (n' + 1)
succ_n'th_conts_aux_eq : pred_conts = continuantsAux g (n' + 1)
ppred_conts : Pair K := continuantsAux g n'
n'th_conts_aux_eq : ppred_conts = continuantsAux g n'
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
pred_conts' : Pair K := continuantsAux g' (n' + 1)
succ_n'th_conts_aux_eq' : pred_conts' = continuantsAux g' (n' + 1)
ppred_conts' : Pair K := continuantsAux g' n'
n'th_conts_aux_eq' : ppred_conts' = continuantsAux g' n'
pA' : K := pred_conts'.a
pB' : K := pred_conts'.b
ppA' : K := ppred_conts'.a
ppB' : K := ppred_conts'.b
this✝¹ : convergents g' (n' + 1) = ((pb + a / b) * pA' + pa * ppA') / ((pb + a / b) * pB' + pa * ppB')
this✝ : convergents g (n' + 2) = (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB)
this :
  ((pb + a / b) * pA + pa * ppA) / ((pb + a / b) * pB + pa * ppB) =
    (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB)
eq1 : pA' = pA
eq2 : pB' = pB
eq3 : ppA' = ppA
eq4 : ppB' = ppB
⊢ ((pb + a / b) * pA' + pa * ppA') / ((pb + a / b) * pB' + pa * ppB') =
    (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB)
[PROOFSTEP]
simpa only [eq1, eq2, eq3, eq4, mul_div_cancel _ b_ne_zero]
[GOAL]
case intro.mk
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) (Nat.succ n') = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g (Nat.succ n')
s_nth_eq : Stream'.Seq.get? g.s (Nat.succ n') = some { a := a, b := b }
pa pb : K
s_n'th_eq : Stream'.Seq.get? g.s n' = some { a := pa, b := pb }
g' : GeneralizedContinuedFraction K := squashGCF g (n' + 1)
pred_conts : Pair K := continuantsAux g (n' + 1)
succ_n'th_conts_aux_eq : pred_conts = continuantsAux g (n' + 1)
ppred_conts : Pair K := continuantsAux g n'
n'th_conts_aux_eq : ppred_conts = continuantsAux g n'
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
pred_conts' : Pair K := continuantsAux g' (n' + 1)
succ_n'th_conts_aux_eq' : pred_conts' = continuantsAux g' (n' + 1)
ppred_conts' : Pair K := continuantsAux g' n'
n'th_conts_aux_eq' : ppred_conts' = continuantsAux g' n'
pA' : K := pred_conts'.a
pB' : K := pred_conts'.b
ppA' : K := ppred_conts'.a
ppB' : K := ppred_conts'.b
this✝ : convergents g' (n' + 1) = ((pb + a / b) * pA' + pa * ppA') / ((pb + a / b) * pB' + pa * ppB')
this : convergents g (n' + 2) = (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB)
⊢ ((pb + a / b) * pA + pa * ppA) / ((pb + a / b) * pB + pa * ppB) =
    (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB)
[PROOFSTEP]
field_simp
[GOAL]
case intro.mk
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) (Nat.succ n') = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g (Nat.succ n')
s_nth_eq : Stream'.Seq.get? g.s (Nat.succ n') = some { a := a, b := b }
pa pb : K
s_n'th_eq : Stream'.Seq.get? g.s n' = some { a := pa, b := pb }
g' : GeneralizedContinuedFraction K := squashGCF g (n' + 1)
pred_conts : Pair K := continuantsAux g (n' + 1)
succ_n'th_conts_aux_eq : pred_conts = continuantsAux g (n' + 1)
ppred_conts : Pair K := continuantsAux g n'
n'th_conts_aux_eq : ppred_conts = continuantsAux g n'
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
pred_conts' : Pair K := continuantsAux g' (n' + 1)
succ_n'th_conts_aux_eq' : pred_conts' = continuantsAux g' (n' + 1)
ppred_conts' : Pair K := continuantsAux g' n'
n'th_conts_aux_eq' : ppred_conts' = continuantsAux g' n'
pA' : K := pred_conts'.a
pB' : K := pred_conts'.b
ppA' : K := ppred_conts'.a
ppB' : K := ppred_conts'.b
this✝ : convergents g' (n' + 1) = ((pb + a / b) * pA' + pa * ppA') / ((pb + a / b) * pB' + pa * ppB')
this : convergents g (n' + 2) = (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB)
⊢ ((pb * b + a) * (continuantsAux g (n' + 1)).a + pa * (continuantsAux g n').a * b) /
      ((pb * b + a) * (continuantsAux g (n' + 1)).b + pa * (continuantsAux g n').b * b) =
    (b * (pb * (continuantsAux g (n' + 1)).a + pa * (continuantsAux g n').a) + a * (continuantsAux g (n' + 1)).a) /
      (b * (pb * (continuantsAux g (n' + 1)).b + pa * (continuantsAux g n').b) + a * (continuantsAux g (n' + 1)).b)
[PROOFSTEP]
congr 1
[GOAL]
case intro.mk.e_a
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) (Nat.succ n') = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g (Nat.succ n')
s_nth_eq : Stream'.Seq.get? g.s (Nat.succ n') = some { a := a, b := b }
pa pb : K
s_n'th_eq : Stream'.Seq.get? g.s n' = some { a := pa, b := pb }
g' : GeneralizedContinuedFraction K := squashGCF g (n' + 1)
pred_conts : Pair K := continuantsAux g (n' + 1)
succ_n'th_conts_aux_eq : pred_conts = continuantsAux g (n' + 1)
ppred_conts : Pair K := continuantsAux g n'
n'th_conts_aux_eq : ppred_conts = continuantsAux g n'
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
pred_conts' : Pair K := continuantsAux g' (n' + 1)
succ_n'th_conts_aux_eq' : pred_conts' = continuantsAux g' (n' + 1)
ppred_conts' : Pair K := continuantsAux g' n'
n'th_conts_aux_eq' : ppred_conts' = continuantsAux g' n'
pA' : K := pred_conts'.a
pB' : K := pred_conts'.b
ppA' : K := ppred_conts'.a
ppB' : K := ppred_conts'.b
this✝ : convergents g' (n' + 1) = ((pb + a / b) * pA' + pa * ppA') / ((pb + a / b) * pB' + pa * ppB')
this : convergents g (n' + 2) = (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB)
⊢ (pb * b + a) * (continuantsAux g (n' + 1)).a + pa * (continuantsAux g n').a * b =
    b * (pb * (continuantsAux g (n' + 1)).a + pa * (continuantsAux g n').a) + a * (continuantsAux g (n' + 1)).a
[PROOFSTEP]
ring
[GOAL]
case intro.mk.e_a
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_part_denom_ne_zero : ∀ {b : K}, Stream'.Seq.get? (partialDenominators g) (Nat.succ n') = some b → b ≠ 0
not_terminated_at_n : ¬TerminatedAt g (Nat.succ n')
s_nth_eq : Stream'.Seq.get? g.s (Nat.succ n') = some { a := a, b := b }
pa pb : K
s_n'th_eq : Stream'.Seq.get? g.s n' = some { a := pa, b := pb }
g' : GeneralizedContinuedFraction K := squashGCF g (n' + 1)
pred_conts : Pair K := continuantsAux g (n' + 1)
succ_n'th_conts_aux_eq : pred_conts = continuantsAux g (n' + 1)
ppred_conts : Pair K := continuantsAux g n'
n'th_conts_aux_eq : ppred_conts = continuantsAux g n'
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
pred_conts' : Pair K := continuantsAux g' (n' + 1)
succ_n'th_conts_aux_eq' : pred_conts' = continuantsAux g' (n' + 1)
ppred_conts' : Pair K := continuantsAux g' n'
n'th_conts_aux_eq' : ppred_conts' = continuantsAux g' n'
pA' : K := pred_conts'.a
pB' : K := pred_conts'.b
ppA' : K := ppred_conts'.a
ppB' : K := ppred_conts'.b
this✝ : convergents g' (n' + 1) = ((pb + a / b) * pA' + pa * ppA') / ((pb + a / b) * pB' + pa * ppB')
this : convergents g (n' + 2) = (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB)
⊢ (pb * b + a) * (continuantsAux g (n' + 1)).b + pa * (continuantsAux g n').b * b =
    b * (pb * (continuantsAux g (n' + 1)).b + pa * (continuantsAux g n').b) + a * (continuantsAux g (n' + 1)).b
[PROOFSTEP]
ring
[GOAL]
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b
⊢ convergents g n = convergents' g n
[PROOFSTEP]
induction' n with n IH generalizing g
[GOAL]
case zero
K : Type u_1
n : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
g : GeneralizedContinuedFraction K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < Nat.zero → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b
⊢ convergents g Nat.zero = convergents' g Nat.zero
case succ
K : Type u_1
n✝ : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n✝ → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
n : ℕ
IH :
  ∀ {g : GeneralizedContinuedFraction K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b) →
      convergents g n = convergents' g n
g : GeneralizedContinuedFraction K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < Nat.succ n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b
⊢ convergents g (Nat.succ n) = convergents' g (Nat.succ n)
[PROOFSTEP]
case zero => simp
[GOAL]
K : Type u_1
n : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
g : GeneralizedContinuedFraction K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < Nat.zero → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b
⊢ convergents g Nat.zero = convergents' g Nat.zero
[PROOFSTEP]
case zero => simp
[GOAL]
K : Type u_1
n : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
g : GeneralizedContinuedFraction K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < Nat.zero → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b
⊢ convergents g Nat.zero = convergents' g Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ
K : Type u_1
n✝ : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n✝ → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
n : ℕ
IH :
  ∀ {g : GeneralizedContinuedFraction K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b) →
      convergents g n = convergents' g n
g : GeneralizedContinuedFraction K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < Nat.succ n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b
⊢ convergents g (Nat.succ n) = convergents' g (Nat.succ n)
[PROOFSTEP]
case succ =>
  let g' := squashGCF g n
  suffices g.convergents (n + 1) = g'.convergents' n by rwa [succ_nth_convergent'_eq_squashGCF_nth_convergent']
  cases' Decidable.em (TerminatedAt g n) with terminated_at_n not_terminated_at_n
  · have g'_eq_g : g' = g := squashGCF_eq_self_of_terminated terminated_at_n
    rw [convergents_stable_of_terminated n.le_succ terminated_at_n, g'_eq_g, IH _]
    intro _ _ m_lt_n s_mth_eq
    exact s_pos (Nat.lt.step m_lt_n) s_mth_eq
  · suffices g.convergents (n + 1) = g'.convergents n by
      -- invoke the IH for the squashed gcf
      rwa [← IH]
      intro gp' m m_lt_n s_mth_eq'
      cases' m_lt_n with n succ_m_lt_n
      ·
        -- the difficult case at the squashed position: we first obtain the values from
                  -- the sequence
        obtain ⟨gp_succ_m, s_succ_mth_eq⟩ : ∃ gp_succ_m, g.s.get? (m + 1) = some gp_succ_m
        exact Option.ne_none_iff_exists'.mp not_terminated_at_n
        obtain ⟨gp_m, mth_s_eq⟩ : ∃ gp_m, g.s.get? m = some gp_m
        exact g.s.ge_stable m.le_succ s_succ_mth_eq
        suffices 0 < gp_m.a ∧ 0 < gp_m.b + gp_succ_m.a / gp_succ_m.b
          by
          have ot : g'.s.get? m = some ⟨gp_m.a, gp_m.b + gp_succ_m.a / gp_succ_m.b⟩ :=
            squashSeq_nth_of_not_terminated mth_s_eq s_succ_mth_eq
          have : gp' = ⟨gp_m.a, gp_m.b + gp_succ_m.a / gp_succ_m.b⟩ := by simp_all only [Option.some.injEq]
          rwa [this]
        have m_lt_n : m < m.succ := Nat.lt_succ_self m
        refine' ⟨(s_pos (Nat.lt.step m_lt_n) mth_s_eq).left, _⟩
        refine' add_pos (s_pos (Nat.lt.step m_lt_n) mth_s_eq).right _
        have : 0 < gp_succ_m.a ∧ 0 < gp_succ_m.b := s_pos (lt_add_one <| m + 1) s_succ_mth_eq
        exact div_pos this.left this.right
      ·
        -- the easy case: before the squashed position, nothing changes
        refine' s_pos (Nat.lt.step <| Nat.lt.step succ_m_lt_n) _
        exact Eq.trans (squashGCF_nth_of_lt succ_m_lt_n).symm s_mth_eq'
    have : ∀ ⦃b⦄, g.partialDenominators.get? n = some b → b ≠ 0 :=
      by
      intro b nth_part_denom_eq
      obtain ⟨gp, s_nth_eq, ⟨refl⟩⟩ : ∃ gp, g.s.get? n = some gp ∧ gp.b = b
      exact exists_s_b_of_part_denom nth_part_denom_eq
      exact (ne_of_lt (s_pos (lt_add_one n) s_nth_eq).right).symm
    exact succ_nth_convergent_eq_squashGCF_nth_convergent @this
[GOAL]
K : Type u_1
n✝ : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n✝ → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
n : ℕ
IH :
  ∀ {g : GeneralizedContinuedFraction K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b) →
      convergents g n = convergents' g n
g : GeneralizedContinuedFraction K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < Nat.succ n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b
⊢ convergents g (Nat.succ n) = convergents' g (Nat.succ n)
[PROOFSTEP]
case succ =>
  let g' := squashGCF g n
  suffices g.convergents (n + 1) = g'.convergents' n by rwa [succ_nth_convergent'_eq_squashGCF_nth_convergent']
  cases' Decidable.em (TerminatedAt g n) with terminated_at_n not_terminated_at_n
  · have g'_eq_g : g' = g := squashGCF_eq_self_of_terminated terminated_at_n
    rw [convergents_stable_of_terminated n.le_succ terminated_at_n, g'_eq_g, IH _]
    intro _ _ m_lt_n s_mth_eq
    exact s_pos (Nat.lt.step m_lt_n) s_mth_eq
  · suffices g.convergents (n + 1) = g'.convergents n by
      -- invoke the IH for the squashed gcf
      rwa [← IH]
      intro gp' m m_lt_n s_mth_eq'
      cases' m_lt_n with n succ_m_lt_n
      ·
        -- the difficult case at the squashed position: we first obtain the values from
                  -- the sequence
        obtain ⟨gp_succ_m, s_succ_mth_eq⟩ : ∃ gp_succ_m, g.s.get? (m + 1) = some gp_succ_m
        exact Option.ne_none_iff_exists'.mp not_terminated_at_n
        obtain ⟨gp_m, mth_s_eq⟩ : ∃ gp_m, g.s.get? m = some gp_m
        exact g.s.ge_stable m.le_succ s_succ_mth_eq
        suffices 0 < gp_m.a ∧ 0 < gp_m.b + gp_succ_m.a / gp_succ_m.b
          by
          have ot : g'.s.get? m = some ⟨gp_m.a, gp_m.b + gp_succ_m.a / gp_succ_m.b⟩ :=
            squashSeq_nth_of_not_terminated mth_s_eq s_succ_mth_eq
          have : gp' = ⟨gp_m.a, gp_m.b + gp_succ_m.a / gp_succ_m.b⟩ := by simp_all only [Option.some.injEq]
          rwa [this]
        have m_lt_n : m < m.succ := Nat.lt_succ_self m
        refine' ⟨(s_pos (Nat.lt.step m_lt_n) mth_s_eq).left, _⟩
        refine' add_pos (s_pos (Nat.lt.step m_lt_n) mth_s_eq).right _
        have : 0 < gp_succ_m.a ∧ 0 < gp_succ_m.b := s_pos (lt_add_one <| m + 1) s_succ_mth_eq
        exact div_pos this.left this.right
      ·
        -- the easy case: before the squashed position, nothing changes
        refine' s_pos (Nat.lt.step <| Nat.lt.step succ_m_lt_n) _
        exact Eq.trans (squashGCF_nth_of_lt succ_m_lt_n).symm s_mth_eq'
    have : ∀ ⦃b⦄, g.partialDenominators.get? n = some b → b ≠ 0 :=
      by
      intro b nth_part_denom_eq
      obtain ⟨gp, s_nth_eq, ⟨refl⟩⟩ : ∃ gp, g.s.get? n = some gp ∧ gp.b = b
      exact exists_s_b_of_part_denom nth_part_denom_eq
      exact (ne_of_lt (s_pos (lt_add_one n) s_nth_eq).right).symm
    exact succ_nth_convergent_eq_squashGCF_nth_convergent @this
[GOAL]
K : Type u_1
n✝ : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n✝ → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
n : ℕ
IH :
  ∀ {g : GeneralizedContinuedFraction K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b) →
      convergents g n = convergents' g n
g : GeneralizedContinuedFraction K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < Nat.succ n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b
⊢ convergents g (Nat.succ n) = convergents' g (Nat.succ n)
[PROOFSTEP]
let g' := squashGCF g n
[GOAL]
K : Type u_1
n✝ : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n✝ → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
n : ℕ
IH :
  ∀ {g : GeneralizedContinuedFraction K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b) →
      convergents g n = convergents' g n
g : GeneralizedContinuedFraction K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < Nat.succ n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GeneralizedContinuedFraction K := squashGCF g n
⊢ convergents g (Nat.succ n) = convergents' g (Nat.succ n)
[PROOFSTEP]
suffices g.convergents (n + 1) = g'.convergents' n by rwa [succ_nth_convergent'_eq_squashGCF_nth_convergent']
[GOAL]
K : Type u_1
n✝ : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n✝ → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
n : ℕ
IH :
  ∀ {g : GeneralizedContinuedFraction K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b) →
      convergents g n = convergents' g n
g : GeneralizedContinuedFraction K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < Nat.succ n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GeneralizedContinuedFraction K := squashGCF g n
this : convergents g (n + 1) = convergents' g' n
⊢ convergents g (Nat.succ n) = convergents' g (Nat.succ n)
[PROOFSTEP]
rwa [succ_nth_convergent'_eq_squashGCF_nth_convergent']
[GOAL]
K : Type u_1
n✝ : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n✝ → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
n : ℕ
IH :
  ∀ {g : GeneralizedContinuedFraction K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b) →
      convergents g n = convergents' g n
g : GeneralizedContinuedFraction K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < Nat.succ n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GeneralizedContinuedFraction K := squashGCF g n
⊢ convergents g (n + 1) = convergents' g' n
[PROOFSTEP]
cases' Decidable.em (TerminatedAt g n) with terminated_at_n not_terminated_at_n
[GOAL]
case inl
K : Type u_1
n✝ : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n✝ → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
n : ℕ
IH :
  ∀ {g : GeneralizedContinuedFraction K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b) →
      convergents g n = convergents' g n
g : GeneralizedContinuedFraction K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < Nat.succ n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GeneralizedContinuedFraction K := squashGCF g n
terminated_at_n : TerminatedAt g n
⊢ convergents g (n + 1) = convergents' g' n
[PROOFSTEP]
have g'_eq_g : g' = g := squashGCF_eq_self_of_terminated terminated_at_n
[GOAL]
case inl
K : Type u_1
n✝ : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n✝ → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
n : ℕ
IH :
  ∀ {g : GeneralizedContinuedFraction K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b) →
      convergents g n = convergents' g n
g : GeneralizedContinuedFraction K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < Nat.succ n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GeneralizedContinuedFraction K := squashGCF g n
terminated_at_n : TerminatedAt g n
g'_eq_g : g' = g
⊢ convergents g (n + 1) = convergents' g' n
[PROOFSTEP]
rw [convergents_stable_of_terminated n.le_succ terminated_at_n, g'_eq_g, IH _]
[GOAL]
K : Type u_1
n✝ : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n✝ → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
n : ℕ
IH :
  ∀ {g : GeneralizedContinuedFraction K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b) →
      convergents g n = convergents' g n
g : GeneralizedContinuedFraction K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < Nat.succ n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GeneralizedContinuedFraction K := squashGCF g n
terminated_at_n : TerminatedAt g n
g'_eq_g : g' = g
⊢ ∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b
[PROOFSTEP]
intro _ _ m_lt_n s_mth_eq
[GOAL]
K : Type u_1
n✝ : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n✝ → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
n : ℕ
IH :
  ∀ {g : GeneralizedContinuedFraction K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b) →
      convergents g n = convergents' g n
g : GeneralizedContinuedFraction K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < Nat.succ n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GeneralizedContinuedFraction K := squashGCF g n
terminated_at_n : TerminatedAt g n
g'_eq_g : g' = g
gp✝ : Pair K
m✝ : ℕ
m_lt_n : m✝ < n
s_mth_eq : Stream'.Seq.get? g.s m✝ = some gp✝
⊢ 0 < gp✝.a ∧ 0 < gp✝.b
[PROOFSTEP]
exact s_pos (Nat.lt.step m_lt_n) s_mth_eq
[GOAL]
case inr
K : Type u_1
n✝ : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n✝ → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
n : ℕ
IH :
  ∀ {g : GeneralizedContinuedFraction K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b) →
      convergents g n = convergents' g n
g : GeneralizedContinuedFraction K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < Nat.succ n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GeneralizedContinuedFraction K := squashGCF g n
not_terminated_at_n : ¬TerminatedAt g n
⊢ convergents g (n + 1) = convergents' g' n
[PROOFSTEP]
suffices g.convergents (n + 1) = g'.convergents n by
  -- invoke the IH for the squashed gcf
  rwa [← IH]
  intro gp' m m_lt_n s_mth_eq'
  cases' m_lt_n with n succ_m_lt_n
  ·
    -- the difficult case at the squashed position: we first obtain the values from
              -- the sequence
    obtain ⟨gp_succ_m, s_succ_mth_eq⟩ : ∃ gp_succ_m, g.s.get? (m + 1) = some gp_succ_m
    exact Option.ne_none_iff_exists'.mp not_terminated_at_n
    obtain ⟨gp_m, mth_s_eq⟩ : ∃ gp_m, g.s.get? m = some gp_m
    exact g.s.ge_stable m.le_succ s_succ_mth_eq
    suffices 0 < gp_m.a ∧ 0 < gp_m.b + gp_succ_m.a / gp_succ_m.b
      by
      have ot : g'.s.get? m = some ⟨gp_m.a, gp_m.b + gp_succ_m.a / gp_succ_m.b⟩ :=
        squashSeq_nth_of_not_terminated mth_s_eq s_succ_mth_eq
      have : gp' = ⟨gp_m.a, gp_m.b + gp_succ_m.a / gp_succ_m.b⟩ := by simp_all only [Option.some.injEq]
      rwa [this]
    have m_lt_n : m < m.succ := Nat.lt_succ_self m
    refine' ⟨(s_pos (Nat.lt.step m_lt_n) mth_s_eq).left, _⟩
    refine' add_pos (s_pos (Nat.lt.step m_lt_n) mth_s_eq).right _
    have : 0 < gp_succ_m.a ∧ 0 < gp_succ_m.b := s_pos (lt_add_one <| m + 1) s_succ_mth_eq
    exact div_pos this.left this.right
  ·
    -- the easy case: before the squashed position, nothing changes
    refine' s_pos (Nat.lt.step <| Nat.lt.step succ_m_lt_n) _
    exact Eq.trans (squashGCF_nth_of_lt succ_m_lt_n).symm s_mth_eq'
[GOAL]
K : Type u_1
n✝ : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n✝ → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
n : ℕ
IH :
  ∀ {g : GeneralizedContinuedFraction K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b) →
      convergents g n = convergents' g n
g : GeneralizedContinuedFraction K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < Nat.succ n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GeneralizedContinuedFraction K := squashGCF g n
not_terminated_at_n : ¬TerminatedAt g n
this : convergents g (n + 1) = convergents g' n
⊢ convergents g (n + 1) = convergents' g' n
[PROOFSTEP]
rwa [← IH]
[GOAL]
K : Type u_1
n✝ : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n✝ → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
n : ℕ
IH :
  ∀ {g : GeneralizedContinuedFraction K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b) →
      convergents g n = convergents' g n
g : GeneralizedContinuedFraction K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < Nat.succ n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GeneralizedContinuedFraction K := squashGCF g n
not_terminated_at_n : ¬TerminatedAt g n
this : convergents g (n + 1) = convergents g' n
⊢ ∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g'.s m = some gp → 0 < gp.a ∧ 0 < gp.b
[PROOFSTEP]
intro gp' m m_lt_n s_mth_eq'
[GOAL]
K : Type u_1
n✝ : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n✝ → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
n : ℕ
IH :
  ∀ {g : GeneralizedContinuedFraction K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b) →
      convergents g n = convergents' g n
g : GeneralizedContinuedFraction K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < Nat.succ n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GeneralizedContinuedFraction K := squashGCF g n
not_terminated_at_n : ¬TerminatedAt g n
this : convergents g (n + 1) = convergents g' n
gp' : Pair K
m : ℕ
m_lt_n : m < n
s_mth_eq' : Stream'.Seq.get? g'.s m = some gp'
⊢ 0 < gp'.a ∧ 0 < gp'.b
[PROOFSTEP]
cases' m_lt_n with n succ_m_lt_n
[GOAL]
case refl
K : Type u_1
n : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
g : GeneralizedContinuedFraction K
gp' : Pair K
m : ℕ
IH :
  ∀ {g : GeneralizedContinuedFraction K},
    (∀ {gp : Pair K} {m_1 : ℕ}, m_1 < Nat.succ m → Stream'.Seq.get? g.s m_1 = some gp → 0 < gp.a ∧ 0 < gp.b) →
      convergents g (Nat.succ m) = convergents' g (Nat.succ m)
s_pos :
  ∀ {gp : Pair K} {m_1 : ℕ}, m_1 < Nat.succ (Nat.succ m) → Stream'.Seq.get? g.s m_1 = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GeneralizedContinuedFraction K := squashGCF g (Nat.succ m)
not_terminated_at_n : ¬TerminatedAt g (Nat.succ m)
this : convergents g (Nat.succ m + 1) = convergents g' (Nat.succ m)
s_mth_eq' : Stream'.Seq.get? g'.s m = some gp'
⊢ 0 < gp'.a ∧ 0 < gp'.b
[PROOFSTEP]
obtain ⟨gp_succ_m, s_succ_mth_eq⟩ : ∃ gp_succ_m, g.s.get? (m + 1) = some gp_succ_m
[GOAL]
K : Type u_1
n : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
g : GeneralizedContinuedFraction K
gp' : Pair K
m : ℕ
IH :
  ∀ {g : GeneralizedContinuedFraction K},
    (∀ {gp : Pair K} {m_1 : ℕ}, m_1 < Nat.succ m → Stream'.Seq.get? g.s m_1 = some gp → 0 < gp.a ∧ 0 < gp.b) →
      convergents g (Nat.succ m) = convergents' g (Nat.succ m)
s_pos :
  ∀ {gp : Pair K} {m_1 : ℕ}, m_1 < Nat.succ (Nat.succ m) → Stream'.Seq.get? g.s m_1 = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GeneralizedContinuedFraction K := squashGCF g (Nat.succ m)
not_terminated_at_n : ¬TerminatedAt g (Nat.succ m)
this : convergents g (Nat.succ m + 1) = convergents g' (Nat.succ m)
s_mth_eq' : Stream'.Seq.get? g'.s m = some gp'
⊢ ∃ gp_succ_m, Stream'.Seq.get? g.s (m + 1) = some gp_succ_m
case refl.intro
K : Type u_1
n : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
g : GeneralizedContinuedFraction K
gp' : Pair K
m : ℕ
IH :
  ∀ {g : GeneralizedContinuedFraction K},
    (∀ {gp : Pair K} {m_1 : ℕ}, m_1 < Nat.succ m → Stream'.Seq.get? g.s m_1 = some gp → 0 < gp.a ∧ 0 < gp.b) →
      convergents g (Nat.succ m) = convergents' g (Nat.succ m)
s_pos :
  ∀ {gp : Pair K} {m_1 : ℕ}, m_1 < Nat.succ (Nat.succ m) → Stream'.Seq.get? g.s m_1 = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GeneralizedContinuedFraction K := squashGCF g (Nat.succ m)
not_terminated_at_n : ¬TerminatedAt g (Nat.succ m)
this : convergents g (Nat.succ m + 1) = convergents g' (Nat.succ m)
s_mth_eq' : Stream'.Seq.get? g'.s m = some gp'
gp_succ_m : Pair K
s_succ_mth_eq : Stream'.Seq.get? g.s (m + 1) = some gp_succ_m
⊢ 0 < gp'.a ∧ 0 < gp'.b
[PROOFSTEP]
exact Option.ne_none_iff_exists'.mp not_terminated_at_n
[GOAL]
case refl.intro
K : Type u_1
n : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
g : GeneralizedContinuedFraction K
gp' : Pair K
m : ℕ
IH :
  ∀ {g : GeneralizedContinuedFraction K},
    (∀ {gp : Pair K} {m_1 : ℕ}, m_1 < Nat.succ m → Stream'.Seq.get? g.s m_1 = some gp → 0 < gp.a ∧ 0 < gp.b) →
      convergents g (Nat.succ m) = convergents' g (Nat.succ m)
s_pos :
  ∀ {gp : Pair K} {m_1 : ℕ}, m_1 < Nat.succ (Nat.succ m) → Stream'.Seq.get? g.s m_1 = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GeneralizedContinuedFraction K := squashGCF g (Nat.succ m)
not_terminated_at_n : ¬TerminatedAt g (Nat.succ m)
this : convergents g (Nat.succ m + 1) = convergents g' (Nat.succ m)
s_mth_eq' : Stream'.Seq.get? g'.s m = some gp'
gp_succ_m : Pair K
s_succ_mth_eq : Stream'.Seq.get? g.s (m + 1) = some gp_succ_m
⊢ 0 < gp'.a ∧ 0 < gp'.b
[PROOFSTEP]
obtain ⟨gp_m, mth_s_eq⟩ : ∃ gp_m, g.s.get? m = some gp_m
[GOAL]
K : Type u_1
n : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
g : GeneralizedContinuedFraction K
gp' : Pair K
m : ℕ
IH :
  ∀ {g : GeneralizedContinuedFraction K},
    (∀ {gp : Pair K} {m_1 : ℕ}, m_1 < Nat.succ m → Stream'.Seq.get? g.s m_1 = some gp → 0 < gp.a ∧ 0 < gp.b) →
      convergents g (Nat.succ m) = convergents' g (Nat.succ m)
s_pos :
  ∀ {gp : Pair K} {m_1 : ℕ}, m_1 < Nat.succ (Nat.succ m) → Stream'.Seq.get? g.s m_1 = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GeneralizedContinuedFraction K := squashGCF g (Nat.succ m)
not_terminated_at_n : ¬TerminatedAt g (Nat.succ m)
this : convergents g (Nat.succ m + 1) = convergents g' (Nat.succ m)
s_mth_eq' : Stream'.Seq.get? g'.s m = some gp'
gp_succ_m : Pair K
s_succ_mth_eq : Stream'.Seq.get? g.s (m + 1) = some gp_succ_m
⊢ ∃ gp_m, Stream'.Seq.get? g.s m = some gp_m
case refl.intro.intro
K : Type u_1
n : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
g : GeneralizedContinuedFraction K
gp' : Pair K
m : ℕ
IH :
  ∀ {g : GeneralizedContinuedFraction K},
    (∀ {gp : Pair K} {m_1 : ℕ}, m_1 < Nat.succ m → Stream'.Seq.get? g.s m_1 = some gp → 0 < gp.a ∧ 0 < gp.b) →
      convergents g (Nat.succ m) = convergents' g (Nat.succ m)
s_pos :
  ∀ {gp : Pair K} {m_1 : ℕ}, m_1 < Nat.succ (Nat.succ m) → Stream'.Seq.get? g.s m_1 = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GeneralizedContinuedFraction K := squashGCF g (Nat.succ m)
not_terminated_at_n : ¬TerminatedAt g (Nat.succ m)
this : convergents g (Nat.succ m + 1) = convergents g' (Nat.succ m)
s_mth_eq' : Stream'.Seq.get? g'.s m = some gp'
gp_succ_m : Pair K
s_succ_mth_eq : Stream'.Seq.get? g.s (m + 1) = some gp_succ_m
gp_m : Pair K
mth_s_eq : Stream'.Seq.get? g.s m = some gp_m
⊢ 0 < gp'.a ∧ 0 < gp'.b
[PROOFSTEP]
exact g.s.ge_stable m.le_succ s_succ_mth_eq
[GOAL]
case refl.intro.intro
K : Type u_1
n : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
g : GeneralizedContinuedFraction K
gp' : Pair K
m : ℕ
IH :
  ∀ {g : GeneralizedContinuedFraction K},
    (∀ {gp : Pair K} {m_1 : ℕ}, m_1 < Nat.succ m → Stream'.Seq.get? g.s m_1 = some gp → 0 < gp.a ∧ 0 < gp.b) →
      convergents g (Nat.succ m) = convergents' g (Nat.succ m)
s_pos :
  ∀ {gp : Pair K} {m_1 : ℕ}, m_1 < Nat.succ (Nat.succ m) → Stream'.Seq.get? g.s m_1 = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GeneralizedContinuedFraction K := squashGCF g (Nat.succ m)
not_terminated_at_n : ¬TerminatedAt g (Nat.succ m)
this : convergents g (Nat.succ m + 1) = convergents g' (Nat.succ m)
s_mth_eq' : Stream'.Seq.get? g'.s m = some gp'
gp_succ_m : Pair K
s_succ_mth_eq : Stream'.Seq.get? g.s (m + 1) = some gp_succ_m
gp_m : Pair K
mth_s_eq : Stream'.Seq.get? g.s m = some gp_m
⊢ 0 < gp'.a ∧ 0 < gp'.b
[PROOFSTEP]
suffices 0 < gp_m.a ∧ 0 < gp_m.b + gp_succ_m.a / gp_succ_m.b
  by
  have ot : g'.s.get? m = some ⟨gp_m.a, gp_m.b + gp_succ_m.a / gp_succ_m.b⟩ :=
    squashSeq_nth_of_not_terminated mth_s_eq s_succ_mth_eq
  have : gp' = ⟨gp_m.a, gp_m.b + gp_succ_m.a / gp_succ_m.b⟩ := by simp_all only [Option.some.injEq]
  rwa [this]
[GOAL]
K : Type u_1
n : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
g : GeneralizedContinuedFraction K
gp' : Pair K
m : ℕ
IH :
  ∀ {g : GeneralizedContinuedFraction K},
    (∀ {gp : Pair K} {m_1 : ℕ}, m_1 < Nat.succ m → Stream'.Seq.get? g.s m_1 = some gp → 0 < gp.a ∧ 0 < gp.b) →
      convergents g (Nat.succ m) = convergents' g (Nat.succ m)
s_pos :
  ∀ {gp : Pair K} {m_1 : ℕ}, m_1 < Nat.succ (Nat.succ m) → Stream'.Seq.get? g.s m_1 = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GeneralizedContinuedFraction K := squashGCF g (Nat.succ m)
not_terminated_at_n : ¬TerminatedAt g (Nat.succ m)
this✝ : convergents g (Nat.succ m + 1) = convergents g' (Nat.succ m)
s_mth_eq' : Stream'.Seq.get? g'.s m = some gp'
gp_succ_m : Pair K
s_succ_mth_eq : Stream'.Seq.get? g.s (m + 1) = some gp_succ_m
gp_m : Pair K
mth_s_eq : Stream'.Seq.get? g.s m = some gp_m
this : 0 < gp_m.a ∧ 0 < gp_m.b + gp_succ_m.a / gp_succ_m.b
⊢ 0 < gp'.a ∧ 0 < gp'.b
[PROOFSTEP]
have ot : g'.s.get? m = some ⟨gp_m.a, gp_m.b + gp_succ_m.a / gp_succ_m.b⟩ :=
  squashSeq_nth_of_not_terminated mth_s_eq s_succ_mth_eq
[GOAL]
K : Type u_1
n : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
g : GeneralizedContinuedFraction K
gp' : Pair K
m : ℕ
IH :
  ∀ {g : GeneralizedContinuedFraction K},
    (∀ {gp : Pair K} {m_1 : ℕ}, m_1 < Nat.succ m → Stream'.Seq.get? g.s m_1 = some gp → 0 < gp.a ∧ 0 < gp.b) →
      convergents g (Nat.succ m) = convergents' g (Nat.succ m)
s_pos :
  ∀ {gp : Pair K} {m_1 : ℕ}, m_1 < Nat.succ (Nat.succ m) → Stream'.Seq.get? g.s m_1 = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GeneralizedContinuedFraction K := squashGCF g (Nat.succ m)
not_terminated_at_n : ¬TerminatedAt g (Nat.succ m)
this✝ : convergents g (Nat.succ m + 1) = convergents g' (Nat.succ m)
s_mth_eq' : Stream'.Seq.get? g'.s m = some gp'
gp_succ_m : Pair K
s_succ_mth_eq : Stream'.Seq.get? g.s (m + 1) = some gp_succ_m
gp_m : Pair K
mth_s_eq : Stream'.Seq.get? g.s m = some gp_m
this : 0 < gp_m.a ∧ 0 < gp_m.b + gp_succ_m.a / gp_succ_m.b
ot : Stream'.Seq.get? g'.s m = some { a := gp_m.a, b := gp_m.b + gp_succ_m.a / gp_succ_m.b }
⊢ 0 < gp'.a ∧ 0 < gp'.b
[PROOFSTEP]
have : gp' = ⟨gp_m.a, gp_m.b + gp_succ_m.a / gp_succ_m.b⟩ := by simp_all only [Option.some.injEq]
[GOAL]
K : Type u_1
n : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
g : GeneralizedContinuedFraction K
gp' : Pair K
m : ℕ
IH :
  ∀ {g : GeneralizedContinuedFraction K},
    (∀ {gp : Pair K} {m_1 : ℕ}, m_1 < Nat.succ m → Stream'.Seq.get? g.s m_1 = some gp → 0 < gp.a ∧ 0 < gp.b) →
      convergents g (Nat.succ m) = convergents' g (Nat.succ m)
s_pos :
  ∀ {gp : Pair K} {m_1 : ℕ}, m_1 < Nat.succ (Nat.succ m) → Stream'.Seq.get? g.s m_1 = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GeneralizedContinuedFraction K := squashGCF g (Nat.succ m)
not_terminated_at_n : ¬TerminatedAt g (Nat.succ m)
this✝ : convergents g (Nat.succ m + 1) = convergents g' (Nat.succ m)
s_mth_eq' : Stream'.Seq.get? g'.s m = some gp'
gp_succ_m : Pair K
s_succ_mth_eq : Stream'.Seq.get? g.s (m + 1) = some gp_succ_m
gp_m : Pair K
mth_s_eq : Stream'.Seq.get? g.s m = some gp_m
this : 0 < gp_m.a ∧ 0 < gp_m.b + gp_succ_m.a / gp_succ_m.b
ot : Stream'.Seq.get? g'.s m = some { a := gp_m.a, b := gp_m.b + gp_succ_m.a / gp_succ_m.b }
⊢ gp' = { a := gp_m.a, b := gp_m.b + gp_succ_m.a / gp_succ_m.b }
[PROOFSTEP]
simp_all only [Option.some.injEq]
[GOAL]
K : Type u_1
n : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
g : GeneralizedContinuedFraction K
gp' : Pair K
m : ℕ
IH :
  ∀ {g : GeneralizedContinuedFraction K},
    (∀ {gp : Pair K} {m_1 : ℕ}, m_1 < Nat.succ m → Stream'.Seq.get? g.s m_1 = some gp → 0 < gp.a ∧ 0 < gp.b) →
      convergents g (Nat.succ m) = convergents' g (Nat.succ m)
s_pos :
  ∀ {gp : Pair K} {m_1 : ℕ}, m_1 < Nat.succ (Nat.succ m) → Stream'.Seq.get? g.s m_1 = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GeneralizedContinuedFraction K := squashGCF g (Nat.succ m)
not_terminated_at_n : ¬TerminatedAt g (Nat.succ m)
this✝¹ : convergents g (Nat.succ m + 1) = convergents g' (Nat.succ m)
s_mth_eq' : Stream'.Seq.get? g'.s m = some gp'
gp_succ_m : Pair K
s_succ_mth_eq : Stream'.Seq.get? g.s (m + 1) = some gp_succ_m
gp_m : Pair K
mth_s_eq : Stream'.Seq.get? g.s m = some gp_m
this✝ : 0 < gp_m.a ∧ 0 < gp_m.b + gp_succ_m.a / gp_succ_m.b
ot : Stream'.Seq.get? g'.s m = some { a := gp_m.a, b := gp_m.b + gp_succ_m.a / gp_succ_m.b }
this : gp' = { a := gp_m.a, b := gp_m.b + gp_succ_m.a / gp_succ_m.b }
⊢ 0 < gp'.a ∧ 0 < gp'.b
[PROOFSTEP]
rwa [this]
[GOAL]
case refl.intro.intro
K : Type u_1
n : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
g : GeneralizedContinuedFraction K
gp' : Pair K
m : ℕ
IH :
  ∀ {g : GeneralizedContinuedFraction K},
    (∀ {gp : Pair K} {m_1 : ℕ}, m_1 < Nat.succ m → Stream'.Seq.get? g.s m_1 = some gp → 0 < gp.a ∧ 0 < gp.b) →
      convergents g (Nat.succ m) = convergents' g (Nat.succ m)
s_pos :
  ∀ {gp : Pair K} {m_1 : ℕ}, m_1 < Nat.succ (Nat.succ m) → Stream'.Seq.get? g.s m_1 = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GeneralizedContinuedFraction K := squashGCF g (Nat.succ m)
not_terminated_at_n : ¬TerminatedAt g (Nat.succ m)
this : convergents g (Nat.succ m + 1) = convergents g' (Nat.succ m)
s_mth_eq' : Stream'.Seq.get? g'.s m = some gp'
gp_succ_m : Pair K
s_succ_mth_eq : Stream'.Seq.get? g.s (m + 1) = some gp_succ_m
gp_m : Pair K
mth_s_eq : Stream'.Seq.get? g.s m = some gp_m
⊢ 0 < gp_m.a ∧ 0 < gp_m.b + gp_succ_m.a / gp_succ_m.b
[PROOFSTEP]
have m_lt_n : m < m.succ := Nat.lt_succ_self m
[GOAL]
case refl.intro.intro
K : Type u_1
n : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
g : GeneralizedContinuedFraction K
gp' : Pair K
m : ℕ
IH :
  ∀ {g : GeneralizedContinuedFraction K},
    (∀ {gp : Pair K} {m_1 : ℕ}, m_1 < Nat.succ m → Stream'.Seq.get? g.s m_1 = some gp → 0 < gp.a ∧ 0 < gp.b) →
      convergents g (Nat.succ m) = convergents' g (Nat.succ m)
s_pos :
  ∀ {gp : Pair K} {m_1 : ℕ}, m_1 < Nat.succ (Nat.succ m) → Stream'.Seq.get? g.s m_1 = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GeneralizedContinuedFraction K := squashGCF g (Nat.succ m)
not_terminated_at_n : ¬TerminatedAt g (Nat.succ m)
this : convergents g (Nat.succ m + 1) = convergents g' (Nat.succ m)
s_mth_eq' : Stream'.Seq.get? g'.s m = some gp'
gp_succ_m : Pair K
s_succ_mth_eq : Stream'.Seq.get? g.s (m + 1) = some gp_succ_m
gp_m : Pair K
mth_s_eq : Stream'.Seq.get? g.s m = some gp_m
m_lt_n : m < Nat.succ m
⊢ 0 < gp_m.a ∧ 0 < gp_m.b + gp_succ_m.a / gp_succ_m.b
[PROOFSTEP]
refine' ⟨(s_pos (Nat.lt.step m_lt_n) mth_s_eq).left, _⟩
[GOAL]
case refl.intro.intro
K : Type u_1
n : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
g : GeneralizedContinuedFraction K
gp' : Pair K
m : ℕ
IH :
  ∀ {g : GeneralizedContinuedFraction K},
    (∀ {gp : Pair K} {m_1 : ℕ}, m_1 < Nat.succ m → Stream'.Seq.get? g.s m_1 = some gp → 0 < gp.a ∧ 0 < gp.b) →
      convergents g (Nat.succ m) = convergents' g (Nat.succ m)
s_pos :
  ∀ {gp : Pair K} {m_1 : ℕ}, m_1 < Nat.succ (Nat.succ m) → Stream'.Seq.get? g.s m_1 = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GeneralizedContinuedFraction K := squashGCF g (Nat.succ m)
not_terminated_at_n : ¬TerminatedAt g (Nat.succ m)
this : convergents g (Nat.succ m + 1) = convergents g' (Nat.succ m)
s_mth_eq' : Stream'.Seq.get? g'.s m = some gp'
gp_succ_m : Pair K
s_succ_mth_eq : Stream'.Seq.get? g.s (m + 1) = some gp_succ_m
gp_m : Pair K
mth_s_eq : Stream'.Seq.get? g.s m = some gp_m
m_lt_n : m < Nat.succ m
⊢ 0 < gp_m.b + gp_succ_m.a / gp_succ_m.b
[PROOFSTEP]
refine' add_pos (s_pos (Nat.lt.step m_lt_n) mth_s_eq).right _
[GOAL]
case refl.intro.intro
K : Type u_1
n : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
g : GeneralizedContinuedFraction K
gp' : Pair K
m : ℕ
IH :
  ∀ {g : GeneralizedContinuedFraction K},
    (∀ {gp : Pair K} {m_1 : ℕ}, m_1 < Nat.succ m → Stream'.Seq.get? g.s m_1 = some gp → 0 < gp.a ∧ 0 < gp.b) →
      convergents g (Nat.succ m) = convergents' g (Nat.succ m)
s_pos :
  ∀ {gp : Pair K} {m_1 : ℕ}, m_1 < Nat.succ (Nat.succ m) → Stream'.Seq.get? g.s m_1 = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GeneralizedContinuedFraction K := squashGCF g (Nat.succ m)
not_terminated_at_n : ¬TerminatedAt g (Nat.succ m)
this : convergents g (Nat.succ m + 1) = convergents g' (Nat.succ m)
s_mth_eq' : Stream'.Seq.get? g'.s m = some gp'
gp_succ_m : Pair K
s_succ_mth_eq : Stream'.Seq.get? g.s (m + 1) = some gp_succ_m
gp_m : Pair K
mth_s_eq : Stream'.Seq.get? g.s m = some gp_m
m_lt_n : m < Nat.succ m
⊢ 0 < gp_succ_m.a / gp_succ_m.b
[PROOFSTEP]
have : 0 < gp_succ_m.a ∧ 0 < gp_succ_m.b := s_pos (lt_add_one <| m + 1) s_succ_mth_eq
[GOAL]
case refl.intro.intro
K : Type u_1
n : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
g : GeneralizedContinuedFraction K
gp' : Pair K
m : ℕ
IH :
  ∀ {g : GeneralizedContinuedFraction K},
    (∀ {gp : Pair K} {m_1 : ℕ}, m_1 < Nat.succ m → Stream'.Seq.get? g.s m_1 = some gp → 0 < gp.a ∧ 0 < gp.b) →
      convergents g (Nat.succ m) = convergents' g (Nat.succ m)
s_pos :
  ∀ {gp : Pair K} {m_1 : ℕ}, m_1 < Nat.succ (Nat.succ m) → Stream'.Seq.get? g.s m_1 = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GeneralizedContinuedFraction K := squashGCF g (Nat.succ m)
not_terminated_at_n : ¬TerminatedAt g (Nat.succ m)
this✝ : convergents g (Nat.succ m + 1) = convergents g' (Nat.succ m)
s_mth_eq' : Stream'.Seq.get? g'.s m = some gp'
gp_succ_m : Pair K
s_succ_mth_eq : Stream'.Seq.get? g.s (m + 1) = some gp_succ_m
gp_m : Pair K
mth_s_eq : Stream'.Seq.get? g.s m = some gp_m
m_lt_n : m < Nat.succ m
this : 0 < gp_succ_m.a ∧ 0 < gp_succ_m.b
⊢ 0 < gp_succ_m.a / gp_succ_m.b
[PROOFSTEP]
exact div_pos this.left this.right
[GOAL]
case step
K : Type u_1
n✝ : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n✝ → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
g : GeneralizedContinuedFraction K
gp' : Pair K
m n : ℕ
succ_m_lt_n : Nat.le (Nat.succ m) n
IH :
  ∀ {g : GeneralizedContinuedFraction K},
    (∀ {gp : Pair K} {m : ℕ}, m < Nat.succ n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b) →
      convergents g (Nat.succ n) = convergents' g (Nat.succ n)
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < Nat.succ (Nat.succ n) → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GeneralizedContinuedFraction K := squashGCF g (Nat.succ n)
not_terminated_at_n : ¬TerminatedAt g (Nat.succ n)
this : convergents g (Nat.succ n + 1) = convergents g' (Nat.succ n)
s_mth_eq' : Stream'.Seq.get? g'.s m = some gp'
⊢ 0 < gp'.a ∧ 0 < gp'.b
[PROOFSTEP]
refine' s_pos (Nat.lt.step <| Nat.lt.step succ_m_lt_n) _
[GOAL]
case step
K : Type u_1
n✝ : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n✝ → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
g : GeneralizedContinuedFraction K
gp' : Pair K
m n : ℕ
succ_m_lt_n : Nat.le (Nat.succ m) n
IH :
  ∀ {g : GeneralizedContinuedFraction K},
    (∀ {gp : Pair K} {m : ℕ}, m < Nat.succ n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b) →
      convergents g (Nat.succ n) = convergents' g (Nat.succ n)
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < Nat.succ (Nat.succ n) → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GeneralizedContinuedFraction K := squashGCF g (Nat.succ n)
not_terminated_at_n : ¬TerminatedAt g (Nat.succ n)
this : convergents g (Nat.succ n + 1) = convergents g' (Nat.succ n)
s_mth_eq' : Stream'.Seq.get? g'.s m = some gp'
⊢ Stream'.Seq.get? g.s m = some gp'
[PROOFSTEP]
exact Eq.trans (squashGCF_nth_of_lt succ_m_lt_n).symm s_mth_eq'
[GOAL]
case inr
K : Type u_1
n✝ : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n✝ → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
n : ℕ
IH :
  ∀ {g : GeneralizedContinuedFraction K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b) →
      convergents g n = convergents' g n
g : GeneralizedContinuedFraction K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < Nat.succ n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GeneralizedContinuedFraction K := squashGCF g n
not_terminated_at_n : ¬TerminatedAt g n
⊢ convergents g (n + 1) = convergents g' n
[PROOFSTEP]
have : ∀ ⦃b⦄, g.partialDenominators.get? n = some b → b ≠ 0 :=
  by
  intro b nth_part_denom_eq
  obtain ⟨gp, s_nth_eq, ⟨refl⟩⟩ : ∃ gp, g.s.get? n = some gp ∧ gp.b = b
  exact exists_s_b_of_part_denom nth_part_denom_eq
  exact (ne_of_lt (s_pos (lt_add_one n) s_nth_eq).right).symm
[GOAL]
K : Type u_1
n✝ : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n✝ → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
n : ℕ
IH :
  ∀ {g : GeneralizedContinuedFraction K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b) →
      convergents g n = convergents' g n
g : GeneralizedContinuedFraction K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < Nat.succ n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GeneralizedContinuedFraction K := squashGCF g n
not_terminated_at_n : ¬TerminatedAt g n
⊢ ∀ ⦃b : K⦄, Stream'.Seq.get? (partialDenominators g) n = some b → b ≠ 0
[PROOFSTEP]
intro b nth_part_denom_eq
[GOAL]
K : Type u_1
n✝ : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n✝ → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
n : ℕ
IH :
  ∀ {g : GeneralizedContinuedFraction K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b) →
      convergents g n = convergents' g n
g : GeneralizedContinuedFraction K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < Nat.succ n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GeneralizedContinuedFraction K := squashGCF g n
not_terminated_at_n : ¬TerminatedAt g n
b : K
nth_part_denom_eq : Stream'.Seq.get? (partialDenominators g) n = some b
⊢ b ≠ 0
[PROOFSTEP]
obtain ⟨gp, s_nth_eq, ⟨refl⟩⟩ : ∃ gp, g.s.get? n = some gp ∧ gp.b = b
[GOAL]
K : Type u_1
n✝ : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n✝ → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
n : ℕ
IH :
  ∀ {g : GeneralizedContinuedFraction K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b) →
      convergents g n = convergents' g n
g : GeneralizedContinuedFraction K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < Nat.succ n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GeneralizedContinuedFraction K := squashGCF g n
not_terminated_at_n : ¬TerminatedAt g n
b : K
nth_part_denom_eq : Stream'.Seq.get? (partialDenominators g) n = some b
⊢ ∃ gp, Stream'.Seq.get? g.s n = some gp ∧ gp.b = b
case intro.intro.refl
K : Type u_1
n✝ : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n✝ → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
n : ℕ
IH :
  ∀ {g : GeneralizedContinuedFraction K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b) →
      convergents g n = convergents' g n
g : GeneralizedContinuedFraction K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < Nat.succ n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GeneralizedContinuedFraction K := squashGCF g n
not_terminated_at_n : ¬TerminatedAt g n
gp : Pair K
s_nth_eq : Stream'.Seq.get? g.s n = some gp
nth_part_denom_eq : Stream'.Seq.get? (partialDenominators g) n = some gp.b
⊢ gp.b ≠ 0
[PROOFSTEP]
exact exists_s_b_of_part_denom nth_part_denom_eq
[GOAL]
case intro.intro.refl
K : Type u_1
n✝ : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n✝ → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
n : ℕ
IH :
  ∀ {g : GeneralizedContinuedFraction K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b) →
      convergents g n = convergents' g n
g : GeneralizedContinuedFraction K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < Nat.succ n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GeneralizedContinuedFraction K := squashGCF g n
not_terminated_at_n : ¬TerminatedAt g n
gp : Pair K
s_nth_eq : Stream'.Seq.get? g.s n = some gp
nth_part_denom_eq : Stream'.Seq.get? (partialDenominators g) n = some gp.b
⊢ gp.b ≠ 0
[PROOFSTEP]
exact (ne_of_lt (s_pos (lt_add_one n) s_nth_eq).right).symm
[GOAL]
case inr
K : Type u_1
n✝ : ℕ
g✝ : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : LinearOrderedField K
s_pos✝ : ∀ {gp : Pair K} {m : ℕ}, m < n✝ → Stream'.Seq.get? g✝.s m = some gp → 0 < gp.a ∧ 0 < gp.b
n : ℕ
IH :
  ∀ {g : GeneralizedContinuedFraction K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b) →
      convergents g n = convergents' g n
g : GeneralizedContinuedFraction K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < Nat.succ n → Stream'.Seq.get? g.s m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GeneralizedContinuedFraction K := squashGCF g n
not_terminated_at_n : ¬TerminatedAt g n
this : ∀ ⦃b : K⦄, Stream'.Seq.get? (partialDenominators g) n = some b → b ≠ 0
⊢ convergents g (n + 1) = convergents g' n
[PROOFSTEP]
exact succ_nth_convergent_eq_squashGCF_nth_convergent @this
[GOAL]
K : Type u_1
n : ℕ
inst✝ : LinearOrderedField K
c : ContinuedFraction K
⊢ convergents ↑↑c = convergents' ↑↑c
[PROOFSTEP]
ext n
[GOAL]
case a
K : Type u_1
n✝ : ℕ
inst✝ : LinearOrderedField K
c : ContinuedFraction K
n : ℕ
⊢ Stream'.nth (convergents ↑↑c) n = Stream'.nth (convergents' ↑↑c) n
[PROOFSTEP]
apply convergents_eq_convergents'
[GOAL]
case a.s_pos
K : Type u_1
n✝ : ℕ
inst✝ : LinearOrderedField K
c : ContinuedFraction K
n : ℕ
⊢ ∀ {gp : Pair K} {m : ℕ}, m < n → Stream'.Seq.get? (↑↑c).s m = some gp → 0 < gp.a ∧ 0 < gp.b
[PROOFSTEP]
intro gp m _ s_nth_eq
[GOAL]
case a.s_pos
K : Type u_1
n✝ : ℕ
inst✝ : LinearOrderedField K
c : ContinuedFraction K
n : ℕ
gp : Pair K
m : ℕ
a✝ : m < n
s_nth_eq : Stream'.Seq.get? (↑↑c).s m = some gp
⊢ 0 < gp.a ∧ 0 < gp.b
[PROOFSTEP]
exact
  ⟨zero_lt_one.trans_le ((c : SimpleContinuedFraction K).property m gp.a (part_num_eq_s_a s_nth_eq)).symm.le,
    c.property m gp.b <| part_denom_eq_s_b s_nth_eq⟩
