The `tauto`

tactic.

Tries to apply de-Morgan-like rules on a hypothesis.

## Equations

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

The list of hypothesis left to work on, renamed to be up-to-date with the current goal.

The current goal.

currentGoal : Lean.MVarId

State of the `distribNotAt`

function. We need to carry around the list of
remaining hypothesis as fvars so that we can incrementally apply the
`AssertAfterResult.subst`

from each step to each of them. Otherwise,
they could end up referring to old hypotheses.

## Instances For

Calls `distribNotAt`

on the head of `state.fvars`

up to `nIters`

times, returning
early on failure.

For each fvar in `fvars`

, calls `distribNotAt`

and carries along the resulting
renamings.

Tries to apply de-Morgan-like rules on all hypotheses. Always succeeds, regardless of whether any progress was actually made.

## Equations

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

Function elaborating `Config`

.

## Equations

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

Matches propositions where we want to apply the `constructor`

tactic
in the core loop of `tauto`

.

## Equations

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

Matches propositions where we want to apply the `cases`

tactic
in the core loop of `tauto`

.

## Equations

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

The core loop of the `tauto`

tactic. Repeatedly tries to break down propositions
until no more progress can be made. Tries `assumption`

and `contradiction`

at every
step, to discharge goals as soon as possible. Does not do anything that requires
backtracking.

TODO: The Lean 3 version uses more-powerful versions of `contradiction`

and `assumption`

that additionally apply `symm`

and use a fancy union-find data structure to avoid
duplicated work.

## Equations

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

Matches propositions where we want to apply the `constructor`

tactic in the
finishing stage of `tauto`

.

## Equations

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

Implementation of the `tauto`

tactic.

## Equations

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

`tauto`

breaks down assumptions of the form `_ ∧ _∧ _`

, `_ ∨ _∨ _`

, `_ ↔ _↔ _`

and `∃ _, _∃ _, _`

and splits a goal of the form `_ ∧ _∧ _`

, `_ ↔ _↔ _`

or `∃ _, _∃ _, _`

until it can be discharged
using `reflexivity`

or `solve_by_elim`

.
This is a finishing tactic: it either closes the goal or raises an error.

The Lean 3 version of this tactic by default attempted to avoid classical reasoning
where possible. This Lean 4 version makes no such attempt. The `itauto`

tactic
is designed for that purpose.

## Equations

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