[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
terminated_at_n : TerminatedAt g n
⊢ continuantsAux g (n + 2) = continuantsAux g (n + 1)
[PROOFSTEP]
rw [terminatedAt_iff_s_none] at terminated_at_n 
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
terminated_at_n : Stream'.Seq.get? g.s n = none
⊢ continuantsAux g (n + 2) = continuantsAux g (n + 1)
[PROOFSTEP]
simp only [continuantsAux, Nat.add_eq, add_zero, terminated_at_n]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
n_lt_m : n < m
terminated_at_n : TerminatedAt g n
⊢ continuantsAux g m = continuantsAux g (n + 1)
[PROOFSTEP]
refine' Nat.le_induction rfl (fun k hnk hk => _) _ n_lt_m
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
n_lt_m : n < m
terminated_at_n : TerminatedAt g n
k : ℕ
hnk : Nat.succ n ≤ k
hk : continuantsAux g k = continuantsAux g (n + 1)
⊢ continuantsAux g (k + 1) = continuantsAux g (n + 1)
[PROOFSTEP]
rcases Nat.exists_eq_add_of_lt hnk with ⟨k, rfl⟩
[GOAL]
case intro
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
n_lt_m : n < m
terminated_at_n : TerminatedAt g n
k : ℕ
hnk : Nat.succ n ≤ n + k + 1
hk : continuantsAux g (n + k + 1) = continuantsAux g (n + 1)
⊢ continuantsAux g (n + k + 1 + 1) = continuantsAux g (n + 1)
[PROOFSTEP]
refine' (continuantsAux_stable_step_of_terminated _).trans hk
[GOAL]
case intro
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
n_lt_m : n < m
terminated_at_n : TerminatedAt g n
k : ℕ
hnk : Nat.succ n ≤ n + k + 1
hk : continuantsAux g (n + k + 1) = continuantsAux g (n + 1)
⊢ TerminatedAt g (n + k)
[PROOFSTEP]
exact terminated_stable (Nat.le_add_right _ _) terminated_at_n
[GOAL]
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
[PROOFSTEP]
change s.get? n = none at terminated_at_n 
[GOAL]
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
[PROOFSTEP]
induction' n with n IH generalizing s
[GOAL]
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)
[PROOFSTEP]
case zero => simp only [convergents'Aux, terminated_at_n, Stream'.Seq.head]
[GOAL]
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
[PROOFSTEP]
case zero => simp only [convergents'Aux, terminated_at_n, Stream'.Seq.head]
[GOAL]
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
[PROOFSTEP]
simp only [convergents'Aux, terminated_at_n, Stream'.Seq.head]
[GOAL]
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)
[PROOFSTEP]
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]
[GOAL]
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)
[PROOFSTEP]
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]
[GOAL]
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)
[PROOFSTEP]
cases' s_head_eq : s.head with gp_head
[GOAL]
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)
[PROOFSTEP]
case none => simp only [convergents'Aux, s_head_eq]
[GOAL]
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)
[PROOFSTEP]
case none => simp only [convergents'Aux, s_head_eq]
[GOAL]
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)
[PROOFSTEP]
simp only [convergents'Aux, s_head_eq]
[GOAL]
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)
[PROOFSTEP]
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]
[GOAL]
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)
[PROOFSTEP]
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]
[GOAL]
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)
[PROOFSTEP]
have : s.tail.TerminatedAt n := by simp only [Stream'.Seq.TerminatedAt, s.get?_tail, terminated_at_n]
[GOAL]
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
[PROOFSTEP]
simp only [Stream'.Seq.TerminatedAt, s.get?_tail, terminated_at_n]
[GOAL]
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)
[PROOFSTEP]
have := IH this
[GOAL]
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)
[PROOFSTEP]
rw [convergents'Aux] at this 
[GOAL]
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)
[PROOFSTEP]
simp [this, Nat.add_eq, add_zero, convergents'Aux, s_head_eq]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
n_le_m : n ≤ m
terminated_at_n : Stream'.Seq.TerminatedAt s n
⊢ convergents'Aux s m = convergents'Aux s n
[PROOFSTEP]
induction' n_le_m with m n_le_m IH
[GOAL]
case refl
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 = convergents'Aux s n
[PROOFSTEP]
rfl
[GOAL]
case step
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
m : ℕ
n_le_m : Nat.le n m
IH : convergents'Aux s m = convergents'Aux s n
⊢ convergents'Aux s (Nat.succ m) = convergents'Aux s n
[PROOFSTEP]
refine' (convergents'Aux_stable_step_of_terminated _).trans IH
[GOAL]
case step
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
m : ℕ
n_le_m : Nat.le n m
IH : convergents'Aux s m = convergents'Aux s n
⊢ Stream'.Seq.TerminatedAt s m
[PROOFSTEP]
exact s.terminated_stable n_le_m terminated_at_n
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
n_le_m : n ≤ m
terminated_at_n : TerminatedAt g n
⊢ continuants g m = continuants g n
[PROOFSTEP]
simp only [nth_cont_eq_succ_nth_cont_aux,
  continuantsAux_stable_of_terminated (Nat.pred_le_iff.mp n_le_m) terminated_at_n]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
n_le_m : n ≤ m
terminated_at_n : TerminatedAt g n
⊢ numerators g m = numerators g n
[PROOFSTEP]
simp only [num_eq_conts_a, continuants_stable_of_terminated n_le_m terminated_at_n]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
n_le_m : n ≤ m
terminated_at_n : TerminatedAt g n
⊢ denominators g m = denominators g n
[PROOFSTEP]
simp only [denom_eq_conts_b, continuants_stable_of_terminated n_le_m terminated_at_n]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
n_le_m : n ≤ m
terminated_at_n : TerminatedAt g n
⊢ convergents g m = convergents g n
[PROOFSTEP]
simp only [convergents, denominators_stable_of_terminated n_le_m terminated_at_n,
  numerators_stable_of_terminated n_le_m terminated_at_n]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
n_le_m : n ≤ m
terminated_at_n : TerminatedAt g n
⊢ convergents' g m = convergents' g n
[PROOFSTEP]
simp only [convergents', convergents'Aux_stable_of_terminated n_le_m terminated_at_n]
