Map MOn Values ok implies all ok

public theorem mapMOnValues_ok_implies_all_ok [LT α] [DecidableLT α] {f : β → Except ε γ} {m₁ : Map α β} {m₂ : Map α γ} :  m₁.mapMOnValues f = .ok m₂ →  ∀ kv ∈ m₁.toList, ∃ v, (kv.fst, v) ∈ m₂.toList ∧ f kv.snd = .ok v:= by  unfold mapMOnValues  intro h₁ kv h₂  cases h₃ : m₁.toList.mapM λ kv => match kv with | (k, v) => do let v' ← f v ; pure (k, v')  <;> rw [h₃] at h₁  <;> simp only [pure, Except.pure, Except.bind_ok, Except.bind_err, Except.ok.injEq, reduceCtorEq] at h₁  case ok ags =>    subst h₁    have (a, b) := kv ; clear kv    simp only    replace ⟨(a', g), h₃, h₄⟩ := List.mapM_ok_implies_all_ok h₃ (a, b) h₂    simp [pure, Except.pure] at h₄    cases h₅ : f b <;> simp [h₅] at h₄    replace ⟨h₄, h₄'⟩ := h₄ ; subst a' g ; rename_i g    exists g