English
For any a, l, the map of dlookup by the Sigma-map equals the find? predicate on l.
Русский
Для любого a, l отображение dlookup через Sigma.map эквивалентно find? по l.
LaTeX
$$$ (dlookup a l).map (\\Sigma.mk a) = \\mathrm{find?}(\\lambda s. a = s.1)\\ l $$$
Lean4
theorem dlookup_map (l : List (Sigma β)) {f : α → α'} (hf : Function.Injective f) (g : ∀ a, β a → β' (f a)) (a : α) :
(l.map (.map f g)).dlookup (f a) = (l.dlookup a).map (g a) := by
induction l with
| nil => grind
| cons s _
_ =>
have (h : a ≠ s.fst) : ¬f a = (⟨f s.fst, g s.fst s.snd⟩ : Sigma β').fst := fun he => h <| hf he
by_cases a = s.fst <;> grind [Sigma.map]
