maybeProveInjective — Mathlib

Lean4
/-- Given a metavariable `ginj` of type `Injective f`, try to prove it.
Returns whether it was successful. -/
def maybeProveInjective (ginj : Expr) (using? : Option Expr) : MetaM Bool := do
  -- Try the `using` clause

  if let some u := using? then
    if ← isDefEq ginj u then
      ginj.mvarId!.assign u
      return true
    else
      let err ← mkHasTypeButIsExpectedMsg (← inferType u) (← inferType ginj)
      throwError "Using clause {err}"
  if ← ginj.mvarId!.assumptionCore then
    return true
  let ok ←
    observing? do
        let [] ← ginj.mvarId!.apply (← mkConstWithFreshMVarLevels ``Equiv.injective) |
          failure
  if ok.isSome then
    return true
  return false
Похожие утверждения