[GOAL]
α : Type u_1
g : GeneralizedContinuedFraction α
n : ℕ
⊢ TerminatedAt g n ↔ Stream'.Seq.TerminatedAt g.s n
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
g : GeneralizedContinuedFraction α
n : ℕ
⊢ TerminatedAt g n ↔ Stream'.Seq.get? g.s n = none
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
g : GeneralizedContinuedFraction α
n : ℕ
⊢ Stream'.Seq.get? (partialNumerators g) n = none ↔ Stream'.Seq.get? g.s n = none
[PROOFSTEP]
cases s_nth_eq : g.s.get? n
[GOAL]
case none
α : Type u_1
g : GeneralizedContinuedFraction α
n : ℕ
s_nth_eq : Stream'.Seq.get? g.s n = none
⊢ Stream'.Seq.get? (partialNumerators g) n = none ↔ none = none
[PROOFSTEP]
simp [partialNumerators, s_nth_eq]
[GOAL]
case some
α : Type u_1
g : GeneralizedContinuedFraction α
n : ℕ
val✝ : Pair α
s_nth_eq : Stream'.Seq.get? g.s n = some val✝
⊢ Stream'.Seq.get? (partialNumerators g) n = none ↔ some val✝ = none
[PROOFSTEP]
simp [partialNumerators, s_nth_eq]
[GOAL]
α : Type u_1
g : GeneralizedContinuedFraction α
n : ℕ
⊢ TerminatedAt g n ↔ Stream'.Seq.get? (partialNumerators g) n = none
[PROOFSTEP]
rw [terminatedAt_iff_s_none, part_num_none_iff_s_none]
[GOAL]
α : Type u_1
g : GeneralizedContinuedFraction α
n : ℕ
⊢ Stream'.Seq.get? (partialDenominators g) n = none ↔ Stream'.Seq.get? g.s n = none
[PROOFSTEP]
cases s_nth_eq : g.s.get? n
[GOAL]
case none
α : Type u_1
g : GeneralizedContinuedFraction α
n : ℕ
s_nth_eq : Stream'.Seq.get? g.s n = none
⊢ Stream'.Seq.get? (partialDenominators g) n = none ↔ none = none
[PROOFSTEP]
simp [partialDenominators, s_nth_eq]
[GOAL]
case some
α : Type u_1
g : GeneralizedContinuedFraction α
n : ℕ
val✝ : Pair α
s_nth_eq : Stream'.Seq.get? g.s n = some val✝
⊢ Stream'.Seq.get? (partialDenominators g) n = none ↔ some val✝ = none
[PROOFSTEP]
simp [partialDenominators, s_nth_eq]
[GOAL]
α : Type u_1
g : GeneralizedContinuedFraction α
n : ℕ
⊢ TerminatedAt g n ↔ Stream'.Seq.get? (partialDenominators g) n = none
[PROOFSTEP]
rw [terminatedAt_iff_s_none, part_denom_none_iff_s_none]
[GOAL]
α : Type u_1
g : GeneralizedContinuedFraction α
n : ℕ
gp : Pair α
s_nth_eq : Stream'.Seq.get? g.s n = some gp
⊢ Stream'.Seq.get? (partialNumerators g) n = some gp.a
[PROOFSTEP]
simp [partialNumerators, s_nth_eq]
[GOAL]
α : Type u_1
g : GeneralizedContinuedFraction α
n : ℕ
gp : Pair α
s_nth_eq : Stream'.Seq.get? g.s n = some gp
⊢ Stream'.Seq.get? (partialDenominators g) n = some gp.b
[PROOFSTEP]
simp [partialDenominators, s_nth_eq]
[GOAL]
α : Type u_1
g : GeneralizedContinuedFraction α
n : ℕ
a : α
nth_part_num_eq : Stream'.Seq.get? (partialNumerators g) n = some a
⊢ ∃ gp, Stream'.Seq.get? g.s n = some gp ∧ gp.a = a
[PROOFSTEP]
simpa [partialNumerators, Stream'.Seq.map_get?] using nth_part_num_eq
[GOAL]
α : Type u_1
g : GeneralizedContinuedFraction α
n : ℕ
b : α
nth_part_denom_eq : Stream'.Seq.get? (partialDenominators g) n = some b
⊢ ∃ gp, Stream'.Seq.get? g.s n = some gp ∧ gp.b = b
[PROOFSTEP]
simpa [partialDenominators, Stream'.Seq.map_get?] using nth_part_denom_eq
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
A : K
nth_num_eq : numerators g n = A
⊢ ∃ conts, continuants g n = conts ∧ conts.a = A
[PROOFSTEP]
simpa
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
B : K
nth_denom_eq : denominators g n = B
⊢ ∃ conts, continuants g n = conts ∧ conts.b = B
[PROOFSTEP]
simpa
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
⊢ convergents g 0 = g.h
[PROOFSTEP]
simp [convergent_eq_num_div_denom, num_eq_conts_a, denom_eq_conts_b, div_one]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
zeroth_s_eq : Stream'.Seq.get? g.s 0 = some gp
⊢ continuantsAux g 2 = { a := gp.b * g.h + gp.a, b := gp.b }
[PROOFSTEP]
simp [zeroth_s_eq, continuantsAux, nextContinuants, nextDenominator, nextNumerator]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
zeroth_s_eq : Stream'.Seq.get? g.s 0 = some gp
⊢ continuants g 1 = { a := gp.b * g.h + gp.a, b := gp.b }
[PROOFSTEP]
simp [nth_cont_eq_succ_nth_cont_aux]
  -- porting note: simp used to work here, but now it can't figure out that 1 + 1 = 2
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
zeroth_s_eq : Stream'.Seq.get? g.s 0 = some gp
⊢ continuantsAux g (1 + 1) = { a := gp.b * g.h + gp.a, b := gp.b }
[PROOFSTEP]
convert second_continuant_aux_eq zeroth_s_eq
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
zeroth_s_eq : Stream'.Seq.get? g.s 0 = some gp
⊢ numerators g 1 = gp.b * g.h + gp.a
[PROOFSTEP]
simp [num_eq_conts_a, first_continuant_eq zeroth_s_eq]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
zeroth_s_eq : Stream'.Seq.get? g.s 0 = some gp
⊢ denominators g 1 = gp.b
[PROOFSTEP]
simp [denom_eq_conts_b, first_continuant_eq zeroth_s_eq]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
⊢ convergents' g 0 = g.h
[PROOFSTEP]
simp [convergents']
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n✝ : ℕ
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
h : Stream'.Seq.head s = none
n : ℕ
⊢ convergents'Aux s (n + 1) = 0
[PROOFSTEP]
simp [convergents'Aux, h, convergents'Aux.match_1]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n✝ : ℕ
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
p : Pair K
h : Stream'.Seq.head s = some p
n : ℕ
⊢ convergents'Aux s (n + 1) = p.a / (p.b + convergents'Aux (Stream'.Seq.tail s) n)
[PROOFSTEP]
simp [convergents'Aux, h, convergents'Aux.match_1]
