Map MOn Values some implies all from some alt proof

theorem mapMOnValues_some_implies_all_from_some_alt_proof [LT α] [DecidableLT α] {f : β → Option γ} {m₁ : Map α β} {m₂ : Map α γ} :  m₁.mapMOnValues f = some m₂ →  ∀ kv ∈ m₂.toList, ∃ v, (kv.fst, v) ∈ m₁.toList ∧ f v = kv.snd:= by  unfold mapMOnValues  intro h₁ kv h₂  cases h₃ : m₁.toList.mapM (λ x => match x with | (k, v) => do let v' ← f v ; pure (k, v'))  <;> rw [h₃] at h₁  <;> simp only [Option.pure_def, Option.bind_some_fun, Option.bind_none_fun, Option.some.injEq, reduceCtorEq] at h₁  case some ags =>    subst h₁    have (a, g) := kv ; clear kv    simp only    replace h₃ := List.mapM_some_implies_all_from_some h₃    replace ⟨(a', b), h₃, h₄⟩ := h₃ (a, g) h₂    simp only [Option.pure_def, Option.bind_eq_bind, Option.bind_eq_some_iff, Option.some.injEq,      Prod.mk.injEq, exists_eq_right_right] at h₄    replace ⟨h₄, h₄'⟩ := h₄    subst a'    exists b