Lean4
/-- Applies a "peel theorem" with two main arguments, where the first is the new goal
and the second can be filled in using `e`. Then it intros two variables with the
provided names.
If, for example, `goal : ∃ y : α, q y` and `thm := Exists.imp`, the metavariable returned has
type `q x` where `x : α` has been introduced into the context. -/
def applyPeelThm (thm : Name) (goal : MVarId) (e : Expr) (ty target : Expr) (n : Name) (n' : Name) :
MetaM (FVarId × List MVarId) := do
let new_goal :: ge :: _ ← goal.applyConst thm <|> throwPeelError ty target |
throwError"peel: internal error"
ge.assignIfDefEq e <|> throwPeelError ty target
let (fvars, new_goal) ← new_goal.introN 2 [n, n']
return (fvars[1]!, [new_goal])
