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✝)
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
cases n
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✝)
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✝)
case zero =>
  cases g_s_head_eq : g.s.get? 0 <;>
    simp [g_s_head_eq, squashGCF, convergents', convergents'Aux, Stream'.Seq.head]
no goals
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✝)
case succ =>
  simp only [succ_succ_nth_convergent'_aux_eq_succ_nth_convergent'_aux_squashSeq, convergents',
    squashGCF]
no goals
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
cases g_s_head_eq : g.s.get? 0 <;>
  simp [g_s_head_eq, squashGCF, convergents', convergents'Aux, Stream'.Seq.head]
no goals
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✝)
simp only [succ_succ_nth_convergent'_aux_eq_succ_nth_convergent'_aux_squashSeq, convergents',
  squashGCF]