Map make filter Map find?

theorem map_make_filterMap_find?  [BEq α] [LawfulBEq α]  [DecidableEq γ] [LT γ] [DecidableLT γ] [StrictLT γ]  {m : Map α β}  {k : α} {v : β} {k' : γ} {v' : κ}  {f : α × β → Option (γ × κ)}  (hfind : m.find? k = .some v)  (hkv : f (k, v) = .some (k', v'))  (hf : ∀ kv, (∃ v'', f kv = .some (k', v'')) → kv.1 = k) :  (Map.make (m.toList.filterMap f)).find? k' = .some v':= by  rw [← Map.list_find?_iff_make_find?]  simp only [List.find?_filterMap]  have :    List.find? (fun a => Option.any (fun x => x.fst == k') (f a)) m.toList    = .some (k, v)  := by    apply Map.map_find?_implies_find?_weaker_pred hfind    · intros kv h      simp only [Option.any] at h      split at h      · rename_i f_out heq        simp at h        apply hf kv        exists f_out.snd        simp only [heq, ←h]      · contradiction    · simp [        Option.any,        hkv,      ]  simp [this, hkv]