English
If v = ↑q for rational q, then the nth element of the stream q maps to the nth element of the stream v under the appropriate map Fr.
Русский
Если v = ↑q для рационального q, то n-й элемент потока q отображается в n-й элемент потока v через соответствующее отображение Fr.
LaTeX
$$$\\forall n,\\ ((IntFractPair.stream q\\ n).map (mapFr (↑)) = IntFractPair.stream v\\ n)$$$
Lean4
theorem coe_stream_nth_rat_eq (v_eq_q : v = (↑q : K)) (n : ℕ) :
((IntFractPair.stream q n).map (mapFr (↑)) : Option <| IntFractPair K) = IntFractPair.stream v n := by
induction n with
| zero => simp only [IntFractPair.stream, Option.map_some, coe_of_rat_eq v_eq_q]
| succ n IH =>
rw [v_eq_q] at IH
cases stream_q_nth_eq : IntFractPair.stream q n with
| none => simp [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq]
| some ifp_n =>
obtain ⟨b, fr⟩ := ifp_n
rcases Decidable.em (fr = 0) with fr_zero | fr_ne_zero
· simp [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq, fr_zero]
· replace IH : some (IntFractPair.mk b (fr : K)) = IntFractPair.stream (↑q) n := by rwa [stream_q_nth_eq] at IH
have : (fr : K)⁻¹ = ((fr⁻¹ : ℚ) : K) := by norm_cast
have coe_of_fr := coe_of_rat_eq this
simpa [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq, fr_ne_zero]
