Theorem: List.map_fst_lookup (Lean4Lean/Std/Basic.lean)

State before:
α : Type u_1
β : Type u_2
f : α → β
inst✝ : BEq β
l : List α
b : β
⊢ lookup b (map (fun a => (f a, a)) l) = find? (fun a => b == f a) l
Tactic:
induction l <;> simp_all [lookup, find?]
State after:
no goals