Unfold definitions commonly used in well founded relation definitions.

Since Lean 4.12, Lean unfolds these definitions automatically before presenting the goal to the
user, and this tactic should no longer be necessary. Calls to `simp_wf`

can be removed or replaced
by plain calls to `simp`

.

## Equations

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

## Instances For

This tactic is used internally by lean before presenting the proof obligations from a well-founded
definition to the user via `decreasing_by`

. It is not necessary to use this tactic manually.

## Equations

- tacticClean_wf = Lean.ParserDescr.node `tacticClean_wf 1024 (Lean.ParserDescr.nonReservedSymbol "clean_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

Variant of `decreasing_trivial`

that does not use `omega`

, intended to be used in core modules
before `omega`

is available.

## Equations

- tacticDecreasing_trivial_pre_omega = Lean.ParserDescr.node `tacticDecreasing_trivial_pre_omega 1024 (Lean.ParserDescr.nonReservedSymbol "decreasing_trivial_pre_omega" false)

## Instances For

Constructs a proof of decreasing along a well founded relation, by simplifying, then applying
lexicographic order lemmas and finally 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)