Map make append find disjoint

public theorem map_make_append_find_disjoint  [LT α] [StrictLT α] [DecidableEq α] [DecidableLT α]  [SizeOf α] [SizeOf β]  {l₁ : List (α × β)} {l₂ : List (α × β)} {k : α}  (hfind₁ : l₁.find? (λ ⟨k', _⟩ => k' == k) = none)  (hfind₂ : (l₂.find? (λ ⟨k', _⟩ => k' == k)).isSome) :  ∃ v,    (Map.make (l₁ ++ l₂)).find? k = some v ∧    (k, v) ∈ l₂:= by  have hwf : (Map.make (l₁ ++ l₂)).WellFormed := by    exact Map.make_wf _  have hsub :    (Map.make (l₁ ++ l₂)).toList ⊆ l₁ ++ l₂  := by    apply List.canonicalize_subseteq  simp [Subset, List.Subset] at hsub  have ⟨v, hv⟩ :    ∃ v, (Map.make (l₁ ++ l₂)).find? k = some v  := by    simp only [Option.isSome] at hfind₂    split at hfind₂    rotate_left    contradiction    rename_i kv hkv    exists kv.snd    rw [make_find?_eq_list_find?]    rw [List.find?_append]    rw [hkv, hfind₁]    simp  simp only [hv, Option.some.injEq, exists_eq_left']  have := Map.find?_mem_toList hv  have := hsub k v this  cases this with  | inl hmem₁ =>    have := List.find?_eq_none.mp hfind₁    specialize this (k, v) hmem₁    simp at this  | inr h => exact h