English
For any f, as, bs, if length as ≤ length bs, then map₂Left f as bs equals zipWith (λ a b, f a (Some b)) as bs.
Русский
Для любого f, as, bs, если длина as ≤ длина bs, то map₂Left f as bs = zipWith (λ a b, f a (Some b)) as bs.
LaTeX
$$$\\forall f:\\alpha \\to \\mathrm{Option}\\,\\beta \\to \\gamma\\ ,\\ \\forall as bs,\\ \\mathrm{length}(as) \\le \\mathrm{length}(bs) \\Rightarrow\\ \\mathrm{map₂Left}\\ f\\ as\\ bs = \\mathrm{zipWith}(\\\\lambda a b. f\\ a(\\\\mathrm{Some}\\ b))\\ as\\ bs$$$
Lean4
theorem map₂Left_eq_zipWith :
∀ as bs, length as ≤ length bs → map₂Left f as bs = zipWith (fun a b => f a (some b)) as bs
| [], [], _ => by simp
| [], _ :: _, _ => by simp
| a :: as, [], h => by simp at h
| a :: as, b :: bs, h => by
simp only [length_cons, succ_le_succ_iff] at h
simp [h, map₂Left_eq_zipWith]
