English
Squashing at position n+1 and taking the tail is the same as squashing the tail at n: (squashSeq s (n+1)).tail = squashSeq s.tail n.
Русский
Сжатие на позиции n+1 и взятие хвоста такое же, как сжатие хвоста на позиции n: (squashSeq s (n+1)).tail = squashSeq s.tail n.
LaTeX
$$$$ (\text{squashSeq}(s,(n+1))).\text{tail} = \text{squashSeq}(s.tail,n). $$$$
Lean4
/-- Squashing at position `n + 1` and taking the tail is the same as squashing the tail of the
sequence at position `n`. -/
theorem squashSeq_succ_n_tail_eq_squashSeq_tail_n : (squashSeq s (n + 1)).tail = squashSeq s.tail n := by
cases s_succ_succ_nth_eq : s.get? (n + 2) with
| none =>
cases s_succ_nth_eq : s.get? (n + 1) <;>
simp only [squashSeq, Stream'.Seq.get?_tail, s_succ_nth_eq, s_succ_succ_nth_eq]
| some
gp_succ_succ_n =>
obtain ⟨gp_succ_n, s_succ_nth_eq⟩ : ∃ gp_succ_n, s.get? (n + 1) = some gp_succ_n :=
s.ge_stable (n + 1).le_succ s_succ_succ_nth_eq
ext1 m
rcases Decidable.em (m = n) with m_eq_n | m_ne_n
· simp [*, squashSeq]
· cases s_succ_mth_eq : s.get? (m + 1)
· simp only [*, squashSeq, Stream'.Seq.get?_tail, Stream'.Seq.get?_zipWith, Option.map₂_none_right]
· simp [*, squashSeq]
