Find? notmem keys

public theorem find?_notmem_keys [LT α] [DecidableLT α] [StrictLT α] [DecidableEq α] {m : Map α β} {k : α}  (wf : m.WellFormed) :  m.find? k = none ↔ k ∉ m.keys:= by  unfold find? at *  constructor <;> intro h₁  case mp =>    split at h₁ <;> simp at h₁    rename_i h₂    intro h₃    replace ⟨v, h₃⟩ := in_keys_exists_value h₃    apply h₂ k v ; clear h₂    replace h₃ := (in_list_iff_find?_some wf).mp h₃    unfold find? at h₃    split at h₃ <;> simp only [Option.some.injEq, reduceCtorEq] at h₃    · subst v ; rename_i k' v h₂      simp only [h₂, Option.some.injEq, Prod.mk.injEq, and_true]      simpa using List.find?_some h₂  case mpr =>    split <;> simp ; rename_i k' v h₂    · apply h₁ ; clear h₁      have h₃ := List.find?_some h₂ ; simp at h₃ ; subst k'      replace h₂ := List.mem_of_find?_eq_some h₂      exact in_list_in_keys h₂