[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp ppred pred : Pair K
nth_s_eq : Stream'.Seq.get? g.s n = some gp
nth_conts_aux_eq : continuantsAux g n = ppred
succ_nth_conts_aux_eq : continuantsAux g (n + 1) = pred
⊢ continuantsAux g (n + 2) = { a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b }
[PROOFSTEP]
simp [*, continuantsAux, nextContinuants, nextDenominator, nextNumerator]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp ppred pred : Pair K
nth_s_eq : Stream'.Seq.get? g.s n = some gp
nth_conts_aux_eq : continuantsAux g n = ppred
succ_nth_conts_aux_eq : continuantsAux g (n + 1) = pred
⊢ continuants g (n + 1) = { a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b }
[PROOFSTEP]
simp [nth_cont_eq_succ_nth_cont_aux, continuantsAux_recurrence nth_s_eq nth_conts_aux_eq succ_nth_conts_aux_eq]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp ppred pred : Pair K
succ_nth_s_eq : Stream'.Seq.get? g.s (n + 1) = some gp
nth_conts_eq : continuants g n = ppred
succ_nth_conts_eq : continuants g (n + 1) = pred
⊢ continuants g (n + 2) = { a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b }
[PROOFSTEP]
rw [nth_cont_eq_succ_nth_cont_aux] at nth_conts_eq succ_nth_conts_eq 
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp ppred pred : Pair K
succ_nth_s_eq : Stream'.Seq.get? g.s (n + 1) = some gp
nth_conts_eq : continuantsAux g (n + 1) = ppred
succ_nth_conts_eq : continuantsAux g (n + 1 + 1) = pred
⊢ continuants g (n + 2) = { a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b }
[PROOFSTEP]
exact continuants_recurrenceAux succ_nth_s_eq nth_conts_eq succ_nth_conts_eq
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
ppredA predA : K
succ_nth_s_eq : Stream'.Seq.get? g.s (n + 1) = some gp
nth_num_eq : numerators g n = ppredA
succ_nth_num_eq : numerators g (n + 1) = predA
⊢ numerators g (n + 2) = gp.b * predA + gp.a * ppredA
[PROOFSTEP]
obtain ⟨ppredConts, nth_conts_eq, ⟨rfl⟩⟩ : ∃ conts, g.continuants n = conts ∧ conts.a = ppredA
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
ppredA predA : K
succ_nth_s_eq : Stream'.Seq.get? g.s (n + 1) = some gp
nth_num_eq : numerators g n = ppredA
succ_nth_num_eq : numerators g (n + 1) = predA
⊢ ∃ conts, continuants g n = conts ∧ conts.a = ppredA
case intro.intro.refl
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
predA : K
succ_nth_s_eq : Stream'.Seq.get? g.s (n + 1) = some gp
succ_nth_num_eq : numerators g (n + 1) = predA
ppredConts : Pair K
nth_conts_eq : continuants g n = ppredConts
nth_num_eq : numerators g n = ppredConts.a
⊢ numerators g (n + 2) = gp.b * predA + gp.a * ppredConts.a
[PROOFSTEP]
exact exists_conts_a_of_num nth_num_eq
[GOAL]
case intro.intro.refl
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
predA : K
succ_nth_s_eq : Stream'.Seq.get? g.s (n + 1) = some gp
succ_nth_num_eq : numerators g (n + 1) = predA
ppredConts : Pair K
nth_conts_eq : continuants g n = ppredConts
nth_num_eq : numerators g n = ppredConts.a
⊢ numerators g (n + 2) = gp.b * predA + gp.a * ppredConts.a
[PROOFSTEP]
obtain ⟨predConts, succ_nth_conts_eq, ⟨rfl⟩⟩ : ∃ conts, g.continuants (n + 1) = conts ∧ conts.a = predA
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
predA : K
succ_nth_s_eq : Stream'.Seq.get? g.s (n + 1) = some gp
succ_nth_num_eq : numerators g (n + 1) = predA
ppredConts : Pair K
nth_conts_eq : continuants g n = ppredConts
nth_num_eq : numerators g n = ppredConts.a
⊢ ∃ conts, continuants g (n + 1) = conts ∧ conts.a = predA
case intro.intro.refl.intro.intro.refl
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
succ_nth_s_eq : Stream'.Seq.get? g.s (n + 1) = some gp
ppredConts : Pair K
nth_conts_eq : continuants g n = ppredConts
nth_num_eq : numerators g n = ppredConts.a
predConts : Pair K
succ_nth_conts_eq : continuants g (n + 1) = predConts
succ_nth_num_eq : numerators g (n + 1) = predConts.a
⊢ numerators g (n + 2) = gp.b * predConts.a + gp.a * ppredConts.a
[PROOFSTEP]
exact exists_conts_a_of_num succ_nth_num_eq
[GOAL]
case intro.intro.refl.intro.intro.refl
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
succ_nth_s_eq : Stream'.Seq.get? g.s (n + 1) = some gp
ppredConts : Pair K
nth_conts_eq : continuants g n = ppredConts
nth_num_eq : numerators g n = ppredConts.a
predConts : Pair K
succ_nth_conts_eq : continuants g (n + 1) = predConts
succ_nth_num_eq : numerators g (n + 1) = predConts.a
⊢ numerators g (n + 2) = gp.b * predConts.a + gp.a * ppredConts.a
[PROOFSTEP]
rw [num_eq_conts_a, continuants_recurrence succ_nth_s_eq nth_conts_eq succ_nth_conts_eq]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
ppredB predB : K
succ_nth_s_eq : Stream'.Seq.get? g.s (n + 1) = some gp
nth_denom_eq : denominators g n = ppredB
succ_nth_denom_eq : denominators g (n + 1) = predB
⊢ denominators g (n + 2) = gp.b * predB + gp.a * ppredB
[PROOFSTEP]
obtain ⟨ppredConts, nth_conts_eq, ⟨rfl⟩⟩ : ∃ conts, g.continuants n = conts ∧ conts.b = ppredB
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
ppredB predB : K
succ_nth_s_eq : Stream'.Seq.get? g.s (n + 1) = some gp
nth_denom_eq : denominators g n = ppredB
succ_nth_denom_eq : denominators g (n + 1) = predB
⊢ ∃ conts, continuants g n = conts ∧ conts.b = ppredB
case intro.intro.refl
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
predB : K
succ_nth_s_eq : Stream'.Seq.get? g.s (n + 1) = some gp
succ_nth_denom_eq : denominators g (n + 1) = predB
ppredConts : Pair K
nth_conts_eq : continuants g n = ppredConts
nth_denom_eq : denominators g n = ppredConts.b
⊢ denominators g (n + 2) = gp.b * predB + gp.a * ppredConts.b
[PROOFSTEP]
exact exists_conts_b_of_denom nth_denom_eq
[GOAL]
case intro.intro.refl
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
predB : K
succ_nth_s_eq : Stream'.Seq.get? g.s (n + 1) = some gp
succ_nth_denom_eq : denominators g (n + 1) = predB
ppredConts : Pair K
nth_conts_eq : continuants g n = ppredConts
nth_denom_eq : denominators g n = ppredConts.b
⊢ denominators g (n + 2) = gp.b * predB + gp.a * ppredConts.b
[PROOFSTEP]
obtain ⟨predConts, succ_nth_conts_eq, ⟨rfl⟩⟩ : ∃ conts, g.continuants (n + 1) = conts ∧ conts.b = predB
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
predB : K
succ_nth_s_eq : Stream'.Seq.get? g.s (n + 1) = some gp
succ_nth_denom_eq : denominators g (n + 1) = predB
ppredConts : Pair K
nth_conts_eq : continuants g n = ppredConts
nth_denom_eq : denominators g n = ppredConts.b
⊢ ∃ conts, continuants g (n + 1) = conts ∧ conts.b = predB
case intro.intro.refl.intro.intro.refl
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
succ_nth_s_eq : Stream'.Seq.get? g.s (n + 1) = some gp
ppredConts : Pair K
nth_conts_eq : continuants g n = ppredConts
nth_denom_eq : denominators g n = ppredConts.b
predConts : Pair K
succ_nth_conts_eq : continuants g (n + 1) = predConts
succ_nth_denom_eq : denominators g (n + 1) = predConts.b
⊢ denominators g (n + 2) = gp.b * predConts.b + gp.a * ppredConts.b
[PROOFSTEP]
exact exists_conts_b_of_denom succ_nth_denom_eq
[GOAL]
case intro.intro.refl.intro.intro.refl
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
succ_nth_s_eq : Stream'.Seq.get? g.s (n + 1) = some gp
ppredConts : Pair K
nth_conts_eq : continuants g n = ppredConts
nth_denom_eq : denominators g n = ppredConts.b
predConts : Pair K
succ_nth_conts_eq : continuants g (n + 1) = predConts
succ_nth_denom_eq : denominators g (n + 1) = predConts.b
⊢ denominators g (n + 2) = gp.b * predConts.b + gp.a * ppredConts.b
[PROOFSTEP]
rw [denom_eq_conts_b, continuants_recurrence succ_nth_s_eq nth_conts_eq succ_nth_conts_eq]
