Disjoint insert left iff

theorem disjoint_insert_left_iff {m₁ m₂ : M V} {i : K} {x : V} (hi : get? m₁ i = none) :    insert m₁ i x ##ₘ m₂ ↔ get? m₂ i = none ∧ m₁ ##ₘ m₂ := by  refine ⟨fun hd => ⟨?_, fun k ⟨hs1, hs2⟩ => ?_⟩, fun ⟨h1, h2⟩ => disjoint_insert_left h1 h2⟩  · rcases h : get? m₂ i with _ | _    · rfl    · exact absurd (hd i ⟨by simp [get?_insert_eq rfl], by simp [h]⟩) id  · by_cases hik : i = k    · subst hik; simp [hi] at hs1    · exact hd k ⟨by simp [get?_insert_ne hik, hs1], hs2⟩