Lean4
@[tactic Mathlib.Tactic.GCongr.«tacticRel[_]»]
public meta def «_aux_Mathlib_Tactic_GCongr_Core___elabRules_Mathlib_Tactic_GCongr_tacticRel[_]_1» :
Lean.Elab.Tactic.Tactic✝ := fun
| `(tactic| rel [$hyps,*]) => do
let g ← getMainGoal
g.withContext
(do
let hyps ← hyps.getElems.mapM (elabTerm · none)
let some (_rel, lhs, rhs) := getRel (← withReducible g.getType') |
throwError"rel failed, goal not a relation"
unless ← isDefEq (← inferType lhs) (← inferType rhs) do
throwError"rel failed, goal not a relation"
let assum g := g.gcongrForward hyps
let (_, _, unsolvedGoalStates) ← g.gcongr none [] (mainGoalDischarger := assum)
match unsolvedGoalStates.toList with
-- if all goals are solved, succeed!
| [] =>
pure
()
-- if not, fail and report the unsolved goals
| unsolvedGoalStates =>
do
let unsolvedGoals ← liftMetaM <| List.mapM MVarId.getType unsolvedGoalStates
let g := Lean.MessageData.joinSep (unsolvedGoals.map Lean.MessageData.ofExpr) Format.line
throwError "rel failed, cannot prove goal by 'substituting' the listed relationships. \
The steps which could not be automatically justified were:\n{g}")
| _ => no_error_if_unused% throwUnsupportedSyntax✝
