English
If g1 ∘ f1 = g2 ∘ f2, then for any a, map g1 (map f1 (some a)) = map g2 (map f2 (some a)).
Русский
Если g1 ∘ f1 = g2 ∘ f2, то для любого a выполняется map g1 (map f1 (some a)) = map g2 (map f2 (some a)).
LaTeX
$$$$ \forall {f_1 : \alpha \to \beta} {f_2 : \alpha \to \gamma} {g_1 : \beta \to \delta} {g_2 : \gamma \to \delta} (h : g_1 \circ f_1 = g_2 \circ f_2) (a : \alpha), \\ (Option.map f_1 a).map g_1 = (Option.map f_2 a).map g_2 $$$$
Lean4
theorem map_comm {f₁ : α → β} {f₂ : α → γ} {g₁ : β → δ} {g₂ : γ → δ} (h : g₁ ∘ f₁ = g₂ ∘ f₂) (a : α) :
(Option.map f₁ a).map g₁ = (Option.map f₂ a).map g₂ := by rw [map_map, h, ← map_map]
