no goals
α : 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
simpa [partialNumerators, Stream'.Seq.map_get?] using nth_part_num_eq