Map MOn Values preserves keys

public theorem mapMOnValues_preserves_keys [LT α] [DecidableLT α] [StrictLT α] {f : β → Option γ} {m₁ : Map α β} {m₂ : Map α γ} :  m₁.mapMOnValues f = some m₂ →  m₁.toList.map Prod.fst = m₂.toList.map Prod.fst:= by  intro h₁  simp only [mapMOnValues, Option.pure_def, Option.bind_eq_bind, Option.bind_eq_some_iff,    Option.some.injEq] at h₁  replace ⟨xs, h₁, h₂⟩ := h₁  subst h₂  cases h₂ : m₁.toList <;> simp only [h₂, List.mapM_nil, List.mapM_cons, Option.pure_def,    Option.bind_eq_bind, Option.bind_eq_some_iff, Option.some.injEq] at h₁  case nil => simp [h₁]  case cons kv tl =>    have (k, v) := kv ; clear kv    replace ⟨(k', y), ⟨y', h₁, h₃⟩, ⟨tl', h₄, h₅⟩⟩ := h₁    subst h₅    simp only [Prod.mk.injEq, List.map_cons, toList_mk_id, List.cons.injEq] at *    replace ⟨h₃, h₃'⟩ := h₃    subst k' y'    have ih := mapMOnValues_preserves_keys (m₁ := mk tl) (m₂ := mk tl') (f := f)    simp only [mapMOnValues, Option.pure_def, Option.bind_eq_bind, toList_mk_id,      Option.bind_eq_some_iff, Option.some.injEq, mk.injEq, exists_eq_right] at ih    specialize ih h₄    simp [ih, and_self]