head?_lookupAll — Mathlib

English

For any a, if l is a list of Sigma β, then the equation head? (lookupAll a l) = dlookup a l holds (simp).

Русский

Для любого a для списка Sigma β верно head? (lookupAll a l) = dlookup a l (simp).

LaTeX

$$$ \text{head?}( \text{lookupAll} a\ l) = \text{dlookup} a\ l $$$

Lean4

theorem head?_lookupAll (a : α) : ∀ l : List (Sigma β), head? (lookupAll a l) = dlookup a l
  | [] => by simp
  | ⟨a', b⟩ :: l => by
    by_cases h : a = a'
    · subst h; simp
    · rw [lookupAll_cons_ne, dlookup_cons_ne, head?_lookupAll a l] <;> assumption

Похожие утверждения