English
For any as, bs, we have zipLeft as bs = (zipLeft' as bs).fst, i.e. the first component of zipLeft' equals the standard zipLeft.
Русский
Для любых as, bs верно, что zipLeft as bs = (zipLeft' as bs).fst, то есть первая часть пары zipLeft' совпадает с обычным zipLeft.
LaTeX
$$$\\forall as:\\text{List }\\alpha,\\ \\forall bs:\\text{List }\\beta,\\ \\mathrm{zipLeft}\\ as\\ bs = (\\mathrm{zipLeft}'\\ as\\ bs).fst$$$
Lean4
theorem zipLeft_eq_zipLeft' (as : List α) (bs : List β) : zipLeft as bs = (zipLeft' as bs).fst :=
by
rw [zipLeft, zipLeft']
cases as with
| nil => rfl
| cons _ atl =>
cases bs with
| nil => rfl
| cons _ btl =>
rw [zipWithLeft, zipWithLeft', cons_inj_right]
exact zipLeft_eq_zipLeft' atl btl
