English
Symmetric statement to distrib_right: map₂ f (a.map g) b = (map₂ f' a b).map g' under a left-commuting hypothesis.
Русский
Симметричное утверждение к распределению слева: map₂ f (a.map g) b = (map₂ f' a b).map g' при условии левого коммутирования.
LaTeX
$$$\\forall {a : \\mathrm{Option}\\, \\alpha} {b : \\mathrm{Option}\\, \\beta} {g : \\alpha \\to \\alpha'} {f : \\alpha' \\to \\beta \\to \\gamma} {f' : \\alpha \\to \\beta \\to \\delta} {g' : \\delta \\to \\gamma},\\; (\\forall a b, f (g a) b = g' (f' a b)) \\\\Rightarrow \\; \\operatorname{Option.map}_2 f (\\operatorname{Option.map} g a) b = \\operatorname{Option.map}_2 f' a b\\;\\map g'$$$$
Lean4
/-- Symmetric statement to `Option.map_map₂_distrib_left`. -/
theorem map₂_map_left_comm {f : α' → β → γ} {g : α → α'} {f' : α → β → δ} {g' : δ → γ}
(h_left_comm : ∀ a b, f (g a) b = g' (f' a b)) : map₂ f (a.map g) b = (map₂ f' a b).map g' := by grind
