Map make filter Map find? none

theorem map_make_filterMap_find?_none  [LT α] [DecidableLT α] [StrictLT α] [DecidableEq α]  [DecidableEq γ] [LT γ] [DecidableLT γ] [StrictLT γ]  {m : Map α β}  {k : α} {k' : γ}  {f : α × β → Option (γ × κ)}  (hfind : m.find? k = .none)  (hf : ∀ kv, (∃ v'', f kv = .some (k', v'')) → kv.1 = k) :  (Map.make (m.toList.filterMap f)).find? k' = .none:= by  apply Map.all_absent_find?_none  intros v hmem_k'_v  have := Map.mem_make_mem_list hmem_k'_v  have ⟨(k'', v''), hmem_kv, hfkv⟩ := List.mem_filterMap.mp this  have heq_k'' := hf (k'', v'')  simp only [    hfkv, Option.some.injEq,    Prod.mk.injEq, true_and, exists_eq',    forall_const,  ] at heq_k''  have := Map.in_list_implies_contains hmem_kv  have := Map.contains_iff_some_find?.mp this  simp [heq_k'', hfind] at this