extractRewriteHypEq — Mathlib

Lean4
/-- Checks that the input `Expr` represents a proof produced by `(e)rw at` and returns the type of the
LHS of the equality (from the lemma used).
This will be defeq to the hypothesis being written, but not necessarily reducibly so.
-/
def extractRewriteHypEq (e : Expr) : MetaM Expr := do
  let (.anonymous, .mk (e :: _)) := e.getAppFnArgs |
    throwError"Unexpected term produced by `erw at`, head is not an mvar applied to a proof."
  let (``Eq.mp, #[_, _, e, _]) := e.getAppFnArgs |
    throwError"Unexpected term produced by `erw at`, head is not an `Eq.mp`."
  let some (_, inferred, _) := (← inferType e).eq? |
    throwError"Unexpected term produced by `erw at`, inferred type is not an equality."
  return inferred
Похожие утверждения