Map MOn Values some wf alt proof

theorem mapMOnValues_some_wf_alt_proof [LT α] [DecidableLT α] [StrictLT α] {f : β → Option γ} {m₁ : Map α β} {m₂ : Map α γ} :  m₁.WellFormed →  (m₁.mapMOnValues f = some m₂) →  m₂.WellFormed:= by  simp only [wf_iff_sorted, toList]  intro wf h₁  simp only [mapMOnValues, Option.pure_def, do_some] at h₁  replace ⟨xs, h₁, h₂⟩ := h₁  subst h₂  simp only  replace h₁ := List.mapM_some_eq_filterMap h₁  subst h₁  apply List.filterMap_sortedBy _ wf  intro (k, v) (k', v') h₁  simp only at *  cases h₂ : f v <;> simp [h₂] at h₁  exact h₁.left