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)
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
induction' n with n IH generalizing g
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)
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)
case zero => simp
no goals
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
simp
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)
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)
let g' := squashGCF g n
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
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)
suffices g.convergents (n + 1) = g'.convergents' n by
  rwa [succ_nth_convergent'_eq_squashGCF_nth_convergent']
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

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
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
cases' Decidable.em (TerminatedAt g n) with terminated_at_n not_terminated_at_n
no goals
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)
rwa [succ_nth_convergent'_eq_squashGCF_nth_convergent']
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
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
have g'_eq_g : g' = g := squashGCF_eq_self_of_terminated terminated_at_n
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
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
rw [convergents_stable_of_terminated n.le_succ terminated_at_n, g'_eq_g, IH _]
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
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
intro _ _ m_lt_n s_mth_eq
no goals
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
exact s_pos (Nat.lt.step m_lt_n) s_mth_eq
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
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
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
no goals
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
exact succ_nth_convergent_eq_squashGCF_nth_convergent @this
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
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
rwa [← IH]
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
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
intro gp' m m_lt_n s_mth_eq'
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

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
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
cases' m_lt_n with n succ_m_lt_n
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
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
obtain ⟨gp_succ_m, s_succ_mth_eq⟩ : ∃ gp_succ_m, g.s.get? (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
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
exact Option.ne_none_iff_exists'.mp not_terminated_at_n
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
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
obtain ⟨gp_m, mth_s_eq⟩ : ∃ gp_m, g.s.get? 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
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
exact g.s.ge_stable m.le_succ s_succ_mth_eq
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
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
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]
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
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
have m_lt_n : m < m.succ := Nat.lt_succ_self 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
m_lt_n : m < Nat.succ m
⊢ 0 < gp_m.b + gp_succ_m.a / gp_succ_m.b
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
refine' ⟨(s_pos (Nat.lt.step m_lt_n) mth_s_eq).left, _⟩
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
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
refine' add_pos (s_pos (Nat.lt.step m_lt_n) mth_s_eq).right _
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
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
have : 0 < gp_succ_m.a ∧ 0 < gp_succ_m.b := s_pos (lt_add_one <| m + 1) s_succ_mth_eq
no goals
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
exact div_pos this.left this.right
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
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
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
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
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
have : gp' = ⟨gp_m.a, gp_m.b + gp_succ_m.a / gp_succ_m.b⟩ := by
  simp_all only [Option.some.injEq]
no goals
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
rwa [this]
no goals
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 }
simp_all only [Option.some.injEq]
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'
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
refine' s_pos (Nat.lt.step <| Nat.lt.step succ_m_lt_n) _
no goals
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'
exact Eq.trans (squashGCF_nth_of_lt succ_m_lt_n).symm s_mth_eq'
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
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
intro b nth_part_denom_eq
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
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
obtain ⟨gp, s_nth_eq, ⟨refl⟩⟩ : ∃ gp, g.s.get? 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
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
exact exists_s_b_of_part_denom nth_part_denom_eq
no goals
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
exact (ne_of_lt (s_pos (lt_add_one n) s_nth_eq).right).symm