synthesizeInstance — Mathlib

Lean4
/-- Synthesize instance of type `type` and
  1. assign it to `x` if `x` is meta variable
  2. check it is equal to `x` -/
def synthesizeInstance (thmId : Origin) (x type : Expr) : MetaM Bool := do
  match (← trySynthInstance type) with
  | .some val =>
    if (← withReducibleAndInstances <| isDefEq x val) then
      return true
    else
      trace[Meta.Tactic.fun_prop]"{(← ppOrigin thmId)}, failed to assign instance{(indentExpr type)}
        synthesized value{(indentExpr val)}\nis not definitionally equal to{indentExpr x}"
      return false
  | _ =>
    trace[Meta.Tactic.fun_prop]"{(← ppOrigin thmId)}, failed to synthesize instance{indentExpr type}"
    return false
Похожие утверждения