lookupAll_eq_dlookup — Mathlib

English

If l has NodupKeys, then the list lookupAll a l equals the toList of dlookup a l: lookupAll a l = (dlookup a l).toList.

Русский

Если l имеет NodupKeys, то lookupAll a l равен toList от dlookup a l: lookupAll a l = (dlookup a l).toList.

LaTeX

$$$ \mathrm{lookupAll} a l = (\mathrm{dlookup} a l).\mathrm{toList} $$$

Lean4

theorem lookupAll_eq_dlookup (a : α) {l : List (Sigma β)} (h : l.NodupKeys) : lookupAll a l = (dlookup a l).toList :=
  by
  rw [← head?_lookupAll]
  have h1 := lookupAll_length_le_one a h; revert h1
  rcases lookupAll a l with (_ | ⟨b, _ | ⟨c, l⟩⟩) <;> intro h1 <;> try rfl
  exact absurd h1 (by simp)

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