applySimpResultToProp variant

Stream: lean4

[Moritz Doll]

For a feature in mathlib4, I needed the following part of applySimpResultToProp:

def applySimpResultToProp' (proof : Expr) (prop : Expr) (r : Simp.Result) : MetaM (Expr × Expr) :=
  do
  match r.proof? with
  | some eqProof => return ((← mkEqMP eqProof proof), r.expr)
  | none =>
    if r.expr != prop then
      return ((← mkExpectedTypeHint proof r.expr), r.expr)
    else
      return (proof, r.expr)

Would it be a welcome PR to move this into Core?