In list iff find? some

public theorem in_list_iff_find?_some [DecidableEq α] [LT α] [DecidableLT α] [StrictLT α] {k : α} {v : β} {m : Map α β}  (wf : m.WellFormed) :  (k, v) ∈ m.toList ↔ m.find? k = some v:= by  unfold find?  constructor  case mp =>    intro h₁    cases h₂ : m.toList.find? λ x => match x with | (k', _) => k' == k    case none =>      exfalso      rw [List.find?_eq_none] at h₂      apply h₂ (k, v) h₁ ; clear h₂      simp only [beq_self_eq_true]    case some kv =>      simp only [Option.some.injEq]      have h₃ := List.find?_some h₂      simp only [beq_iff_eq] at h₃      subst h₃      replace h₃ := List.mem_of_find?_eq_some h₂      apply (key_maps_to_one_value kv.fst v kv.snd m wf h₁ _).symm      trivial  case mpr => exact find?_mem_toList