grewriteTarget — Mathlib

Lean4
/-- Apply the `grewrite` tactic to the current goal. -/
def grewriteTarget (stx : Syntax) (symm : Bool) (config : GRewrite.Config) : TacticM Unit := do
  let goal ← getMainGoal
  Term.withSynthesize <|
      goal.withContext do
        let e ← elabTerm stx none true
        if e.hasSyntheticSorry then
          throwAbortTactic
        let goal ← getMainGoal
        let target ← goal.getType
        let r ← goal.grewrite target e (forwardImp := false) (symm := symm) (config := config)
        let mvarNew ← mkFreshExprSyntheticOpaqueMVar r.eNew (← goal.getTag)
        goal.assign (mkApp r.impProof mvarNew)
        replaceMainGoal (mvarNew.mvarId! :: r.mvarIds)
Похожие утверждения