Map make append find disjoint

public theorem map_make_append_find_disjoint'  [LT α] [StrictLT α] [DecidableEq α] [DecidableLT α]  [SizeOf α] [SizeOf β]  {l₁ : List (α × β)} {l₂ : List (α × β)} {k : α} {v : β}  (hfind₁ : l₁.find? (λ ⟨k', _⟩ => k' == k) = none)  (hfind₂ : l₂.find? (λ ⟨k', _⟩ => k' == k) = .some (k, v))  (heq : ∀ x₁ x₂, x₁ ∈ l₂ → x₂ ∈ l₂ → x₁.fst = x₂.fst → x₁ = x₂) :  (Map.make (l₁ ++ l₂)).find? k = some v:= by  have : (l₂.find? (λ ⟨k', _⟩ => k' == k)).isSome  := by simp only [hfind₂, Option.isSome]  have ⟨v', hfind_k, hmem⟩ := map_make_append_find_disjoint hfind₁ this  have := List.mem_of_find?_eq_some hfind₂  have := heq _ _ this hmem  simp only [Prod.mk.injEq, true_and, forall_const] at this  simp only [this, hfind_k]