Unfold definitions commonly used in well founded relation definitions.
This is primarily intended for internal use in `decreasing_tactic`

.

## Equations

- tacticSimp_wf = Lean.ParserDescr.node `tacticSimp_wf 1024 (Lean.ParserDescr.nonReservedSymbol "simp_wf" false)

## Instances For

Extensible helper tactic for `decreasing_tactic`

. This handles the "base case"
reasoning after applying lexicographic order lemmas.
It can be extended by adding more macro definitions, e.g.

```
macro_rules | `(tactic| decreasing_trivial) => `(tactic| linarith)
```

## Equations

- tacticDecreasing_trivial = Lean.ParserDescr.node `tacticDecreasing_trivial 1024 (Lean.ParserDescr.nonReservedSymbol "decreasing_trivial" false)

## Instances For

Constructs a proof of decreasing along a well founded relation, by applying
lexicographic order lemmas and using `ts`

to solve the base case. If it fails,
it prints a message to help the user diagnose an ill-founded recursive definition.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

`decreasing_tactic`

is called by default on well-founded recursions in order
to synthesize a proof that recursive calls decrease along the selected
well founded relation. It can be locally overridden by using `decreasing_by tac`

on the recursive definition, and it can also be globally extended by adding
more definitions for `decreasing_tactic`

(or `decreasing_trivial`

,
which this tactic calls).

## Equations

- tacticDecreasing_tactic = Lean.ParserDescr.node `tacticDecreasing_tactic 1024 (Lean.ParserDescr.nonReservedSymbol "decreasing_tactic" false)