English
If f and g agree on every element of l (i.e., f a = g a for all a ∈ l), then l.lookmap f = l.lookmap g.
Русский
Если f и g совпадают на каждом элементе списка l (для каждого a ∈ l: f a = g a), тогда l.lookmap f = l.lookmap g.
LaTeX
$$$\\forall l:\\mathrm{List}\\ \\alpha,\\ (\\forall a\\in l,\\ f\\ a = g\\ a) \\Rightarrow \\mathrm{lookmap}\\ f\\ l = \\mathrm{lookmap}\\ g\\ l.$$$
Lean4
theorem lookmap_congr {f g : α → Option α} : ∀ {l : List α}, (∀ a ∈ l, f a = g a) → l.lookmap f = l.lookmap g
| [], _ => rfl
| a :: l, H => by
obtain ⟨H₁, H₂⟩ := forall_mem_cons.1 H
rcases h : g a with - | b
· simp [h, H₁.trans h, lookmap_congr H₂]
· simp [lookmap_cons_some _ _ h, lookmap_cons_some _ _ (H₁.trans h)]
