K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s n = none
⊢ convergents'Aux s (n + 1) = convergents'Aux s n
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.TerminatedAt s n
⊢ convergents'Aux s (n + 1) = convergents'Aux s n
change s.get? n = none at terminated_at_n
case zero
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
s✝ : Stream'.Seq (Pair K)
terminated_at_n✝ : Stream'.Seq.get? s✝ n = none
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s Nat.zero = none
⊢ convergents'Aux s (Nat.zero + 1) = convergents'Aux s Nat.zero

case succ
K : Type u_1
g : GeneralizedContinuedFraction K
n✝ m : ℕ
inst✝ : DivisionRing K
s✝ : Stream'.Seq (Pair K)
terminated_at_n✝ : Stream'.Seq.get? s✝ n✝ = none
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, Stream'.Seq.get? s n = none → convergents'Aux s (n + 1) = convergents'Aux s n
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s (Nat.succ n) = none
⊢ convergents'Aux s (Nat.succ n + 1) = convergents'Aux s (Nat.succ n)
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s n = none
⊢ convergents'Aux s (n + 1) = convergents'Aux s n
induction' n with n IH generalizing s
case succ
K : Type u_1
g : GeneralizedContinuedFraction K
n✝ m : ℕ
inst✝ : DivisionRing K
s✝ : Stream'.Seq (Pair K)
terminated_at_n✝ : Stream'.Seq.get? s✝ n✝ = none
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, Stream'.Seq.get? s n = none → convergents'Aux s (n + 1) = convergents'Aux s n
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s (Nat.succ n) = none
⊢ convergents'Aux s (Nat.succ n + 1) = convergents'Aux s (Nat.succ n)
case zero
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
s✝ : Stream'.Seq (Pair K)
terminated_at_n✝ : Stream'.Seq.get? s✝ n = none
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s Nat.zero = none
⊢ convergents'Aux s (Nat.zero + 1) = convergents'Aux s Nat.zero

case succ
K : Type u_1
g : GeneralizedContinuedFraction K
n✝ m : ℕ
inst✝ : DivisionRing K
s✝ : Stream'.Seq (Pair K)
terminated_at_n✝ : Stream'.Seq.get? s✝ n✝ = none
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, Stream'.Seq.get? s n = none → convergents'Aux s (n + 1) = convergents'Aux s n
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s (Nat.succ n) = none
⊢ convergents'Aux s (Nat.succ n + 1) = convergents'Aux s (Nat.succ n)
case zero => simp only [convergents'Aux, terminated_at_n, Stream'.Seq.head]
no goals
case succ
K : Type u_1
g : GeneralizedContinuedFraction K
n✝ m : ℕ
inst✝ : DivisionRing K
s✝ : Stream'.Seq (Pair K)
terminated_at_n✝ : Stream'.Seq.get? s✝ n✝ = none
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, Stream'.Seq.get? s n = none → convergents'Aux s (n + 1) = convergents'Aux s n
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s (Nat.succ n) = none
⊢ convergents'Aux s (Nat.succ n + 1) = convergents'Aux s (Nat.succ n)
case succ =>
  cases' s_head_eq : s.head with gp_head
  case none => simp only [convergents'Aux, s_head_eq]
  case some =>
    have : s.tail.TerminatedAt n := by
      simp only [Stream'.Seq.TerminatedAt, s.get?_tail, terminated_at_n]
    have := IH this
    rw [convergents'Aux] at this
    simp [this, Nat.add_eq, add_zero, convergents'Aux, s_head_eq]
no goals
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
s✝ : Stream'.Seq (Pair K)
terminated_at_n✝ : Stream'.Seq.get? s✝ n = none
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s Nat.zero = none
⊢ convergents'Aux s (Nat.zero + 1) = convergents'Aux s Nat.zero
simp only [convergents'Aux, terminated_at_n, Stream'.Seq.head]
case none
K : Type u_1
g : GeneralizedContinuedFraction K
n✝ m : ℕ
inst✝ : DivisionRing K
s✝ : Stream'.Seq (Pair K)
terminated_at_n✝ : Stream'.Seq.get? s✝ n✝ = none
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, Stream'.Seq.get? s n = none → convergents'Aux s (n + 1) = convergents'Aux s n
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s (Nat.succ n) = none
s_head_eq : Stream'.Seq.head s = none
⊢ convergents'Aux s (Nat.succ n + 1) = convergents'Aux s (Nat.succ n)

case some
K : Type u_1
g : GeneralizedContinuedFraction K
n✝ m : ℕ
inst✝ : DivisionRing K
s✝ : Stream'.Seq (Pair K)
terminated_at_n✝ : Stream'.Seq.get? s✝ n✝ = none
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, Stream'.Seq.get? s n = none → convergents'Aux s (n + 1) = convergents'Aux s n
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s (Nat.succ n) = none
gp_head : Pair K
s_head_eq : Stream'.Seq.head s = some gp_head
⊢ convergents'Aux s (Nat.succ n + 1) = convergents'Aux s (Nat.succ n)
K : Type u_1
g : GeneralizedContinuedFraction K
n✝ m : ℕ
inst✝ : DivisionRing K
s✝ : Stream'.Seq (Pair K)
terminated_at_n✝ : Stream'.Seq.get? s✝ n✝ = none
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, Stream'.Seq.get? s n = none → convergents'Aux s (n + 1) = convergents'Aux s n
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s (Nat.succ n) = none
⊢ convergents'Aux s (Nat.succ n + 1) = convergents'Aux s (Nat.succ n)
cases' s_head_eq : s.head with gp_head
case some
K : Type u_1
g : GeneralizedContinuedFraction K
n✝ m : ℕ
inst✝ : DivisionRing K
s✝ : Stream'.Seq (Pair K)
terminated_at_n✝ : Stream'.Seq.get? s✝ n✝ = none
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, Stream'.Seq.get? s n = none → convergents'Aux s (n + 1) = convergents'Aux s n
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s (Nat.succ n) = none
gp_head : Pair K
s_head_eq : Stream'.Seq.head s = some gp_head
⊢ convergents'Aux s (Nat.succ n + 1) = convergents'Aux s (Nat.succ n)
case none
K : Type u_1
g : GeneralizedContinuedFraction K
n✝ m : ℕ
inst✝ : DivisionRing K
s✝ : Stream'.Seq (Pair K)
terminated_at_n✝ : Stream'.Seq.get? s✝ n✝ = none
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, Stream'.Seq.get? s n = none → convergents'Aux s (n + 1) = convergents'Aux s n
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s (Nat.succ n) = none
s_head_eq : Stream'.Seq.head s = none
⊢ convergents'Aux s (Nat.succ n + 1) = convergents'Aux s (Nat.succ n)

case some
K : Type u_1
g : GeneralizedContinuedFraction K
n✝ m : ℕ
inst✝ : DivisionRing K
s✝ : Stream'.Seq (Pair K)
terminated_at_n✝ : Stream'.Seq.get? s✝ n✝ = none
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, Stream'.Seq.get? s n = none → convergents'Aux s (n + 1) = convergents'Aux s n
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s (Nat.succ n) = none
gp_head : Pair K
s_head_eq : Stream'.Seq.head s = some gp_head
⊢ convergents'Aux s (Nat.succ n + 1) = convergents'Aux s (Nat.succ n)
case none => simp only [convergents'Aux, s_head_eq]
no goals
case some
K : Type u_1
g : GeneralizedContinuedFraction K
n✝ m : ℕ
inst✝ : DivisionRing K
s✝ : Stream'.Seq (Pair K)
terminated_at_n✝ : Stream'.Seq.get? s✝ n✝ = none
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, Stream'.Seq.get? s n = none → convergents'Aux s (n + 1) = convergents'Aux s n
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s (Nat.succ n) = none
gp_head : Pair K
s_head_eq : Stream'.Seq.head s = some gp_head
⊢ convergents'Aux s (Nat.succ n + 1) = convergents'Aux s (Nat.succ n)
case some =>
  have : s.tail.TerminatedAt n := by
    simp only [Stream'.Seq.TerminatedAt, s.get?_tail, terminated_at_n]
  have := IH this
  rw [convergents'Aux] at this
  simp [this, Nat.add_eq, add_zero, convergents'Aux, s_head_eq]
no goals
K : Type u_1
g : GeneralizedContinuedFraction K
n✝ m : ℕ
inst✝ : DivisionRing K
s✝ : Stream'.Seq (Pair K)
terminated_at_n✝ : Stream'.Seq.get? s✝ n✝ = none
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, Stream'.Seq.get? s n = none → convergents'Aux s (n + 1) = convergents'Aux s n
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s (Nat.succ n) = none
s_head_eq : Stream'.Seq.head s = none
⊢ convergents'Aux s (Nat.succ n + 1) = convergents'Aux s (Nat.succ n)
simp only [convergents'Aux, s_head_eq]
K : Type u_1
g : GeneralizedContinuedFraction K
n✝ m : ℕ
inst✝ : DivisionRing K
s✝ : Stream'.Seq (Pair K)
terminated_at_n✝ : Stream'.Seq.get? s✝ n✝ = none
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, Stream'.Seq.get? s n = none → convergents'Aux s (n + 1) = convergents'Aux s n
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s (Nat.succ n) = none
gp_head : Pair K
s_head_eq : Stream'.Seq.head s = some gp_head
this : Stream'.Seq.TerminatedAt (Stream'.Seq.tail s) n
⊢ convergents'Aux s (Nat.succ n + 1) = convergents'Aux s (Nat.succ n)
K : Type u_1
g : GeneralizedContinuedFraction K
n✝ m : ℕ
inst✝ : DivisionRing K
s✝ : Stream'.Seq (Pair K)
terminated_at_n✝ : Stream'.Seq.get? s✝ n✝ = none
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, Stream'.Seq.get? s n = none → convergents'Aux s (n + 1) = convergents'Aux s n
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s (Nat.succ n) = none
gp_head : Pair K
s_head_eq : Stream'.Seq.head s = some gp_head
⊢ convergents'Aux s (Nat.succ n + 1) = convergents'Aux s (Nat.succ n)
have : s.tail.TerminatedAt n := by
  simp only [Stream'.Seq.TerminatedAt, s.get?_tail, terminated_at_n]
K : Type u_1
g : GeneralizedContinuedFraction K
n✝ m : ℕ
inst✝ : DivisionRing K
s✝ : Stream'.Seq (Pair K)
terminated_at_n✝ : Stream'.Seq.get? s✝ n✝ = none
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, Stream'.Seq.get? s n = none → convergents'Aux s (n + 1) = convergents'Aux s n
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s (Nat.succ n) = none
gp_head : Pair K
s_head_eq : Stream'.Seq.head s = some gp_head
this✝ : Stream'.Seq.TerminatedAt (Stream'.Seq.tail s) n
this : convergents'Aux (Stream'.Seq.tail s) (n + 1) = convergents'Aux (Stream'.Seq.tail s) n
⊢ convergents'Aux s (Nat.succ n + 1) = convergents'Aux s (Nat.succ n)
K : Type u_1
g : GeneralizedContinuedFraction K
n✝ m : ℕ
inst✝ : DivisionRing K
s✝ : Stream'.Seq (Pair K)
terminated_at_n✝ : Stream'.Seq.get? s✝ n✝ = none
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, Stream'.Seq.get? s n = none → convergents'Aux s (n + 1) = convergents'Aux s n
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s (Nat.succ n) = none
gp_head : Pair K
s_head_eq : Stream'.Seq.head s = some gp_head
this : Stream'.Seq.TerminatedAt (Stream'.Seq.tail s) n
⊢ convergents'Aux s (Nat.succ n + 1) = convergents'Aux s (Nat.succ n)
have := IH this
K : Type u_1
g : GeneralizedContinuedFraction K
n✝ m : ℕ
inst✝ : DivisionRing K
s✝ : Stream'.Seq (Pair K)
terminated_at_n✝ : Stream'.Seq.get? s✝ n✝ = none
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, Stream'.Seq.get? s n = none → convergents'Aux s (n + 1) = convergents'Aux s n
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s (Nat.succ n) = none
gp_head : Pair K
s_head_eq : Stream'.Seq.head s = some gp_head
this✝ : Stream'.Seq.TerminatedAt (Stream'.Seq.tail s) n
this :
  (match Stream'.Seq.head (Stream'.Seq.tail s) with
    | none => 0
    | some gp => gp.a / (gp.b + convergents'Aux (Stream'.Seq.tail (Stream'.Seq.tail s)) n)) =
    convergents'Aux (Stream'.Seq.tail s) n
⊢ convergents'Aux s (Nat.succ n + 1) = convergents'Aux s (Nat.succ n)
K : Type u_1
g : GeneralizedContinuedFraction K
n✝ m : ℕ
inst✝ : DivisionRing K
s✝ : Stream'.Seq (Pair K)
terminated_at_n✝ : Stream'.Seq.get? s✝ n✝ = none
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, Stream'.Seq.get? s n = none → convergents'Aux s (n + 1) = convergents'Aux s n
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s (Nat.succ n) = none
gp_head : Pair K
s_head_eq : Stream'.Seq.head s = some gp_head
this✝ : Stream'.Seq.TerminatedAt (Stream'.Seq.tail s) n
this : convergents'Aux (Stream'.Seq.tail s) (n + 1) = convergents'Aux (Stream'.Seq.tail s) n
⊢ convergents'Aux s (Nat.succ n + 1) = convergents'Aux s (Nat.succ n)
rw [convergents'Aux] at this
no goals
K : Type u_1
g : GeneralizedContinuedFraction K
n✝ m : ℕ
inst✝ : DivisionRing K
s✝ : Stream'.Seq (Pair K)
terminated_at_n✝ : Stream'.Seq.get? s✝ n✝ = none
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, Stream'.Seq.get? s n = none → convergents'Aux s (n + 1) = convergents'Aux s n
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s (Nat.succ n) = none
gp_head : Pair K
s_head_eq : Stream'.Seq.head s = some gp_head
this✝ : Stream'.Seq.TerminatedAt (Stream'.Seq.tail s) n
this :
  (match Stream'.Seq.head (Stream'.Seq.tail s) with
    | none => 0
    | some gp => gp.a / (gp.b + convergents'Aux (Stream'.Seq.tail (Stream'.Seq.tail s)) n)) =
    convergents'Aux (Stream'.Seq.tail s) n
⊢ convergents'Aux s (Nat.succ n + 1) = convergents'Aux s (Nat.succ n)
simp [this, Nat.add_eq, add_zero, convergents'Aux, s_head_eq]
no goals
K : Type u_1
g : GeneralizedContinuedFraction K
n✝ m : ℕ
inst✝ : DivisionRing K
s✝ : Stream'.Seq (Pair K)
terminated_at_n✝ : Stream'.Seq.get? s✝ n✝ = none
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, Stream'.Seq.get? s n = none → convergents'Aux s (n + 1) = convergents'Aux s n
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s (Nat.succ n) = none
gp_head : Pair K
s_head_eq : Stream'.Seq.head s = some gp_head
⊢ Stream'.Seq.TerminatedAt (Stream'.Seq.tail s) n
simp only [Stream'.Seq.TerminatedAt, s.get?_tail, terminated_at_n]