The arguments to the `simpa`

family tactics.

## Equations

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

This is a "finishing" tactic modification of `simp`

. It has two forms.

`simpa [rules, ⋯] using e⋯] using e`

will simplify the goal and the type of`e`

using`rules`

, then try to close the goal using`e`

.

Simplifying the type of `e`

makes it more likely to match the goal
(which has also been simplified). This construction also tends to be
more robust under changes to the simp lemma set.

`simpa [rules, ⋯]⋯]`

will simplify the goal and the type of a hypothesis`this`

if present in the context, then try to close the goal using the`assumption`

tactic.

#TODO: implement `?`

## Equations

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

This is a "finishing" tactic modification of `simp`

. It has two forms.

`simpa [rules, ⋯] using e⋯] using e`

will simplify the goal and the type of`e`

using`rules`

, then try to close the goal using`e`

.

Simplifying the type of `e`

makes it more likely to match the goal
(which has also been simplified). This construction also tends to be
more robust under changes to the simp lemma set.

`simpa [rules, ⋯]⋯]`

will simplify the goal and the type of a hypothesis`this`

if present in the context, then try to close the goal using the`assumption`

tactic.

#TODO: implement `?`

## Equations

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

This is a "finishing" tactic modification of `simp`

. It has two forms.

`simpa [rules, ⋯] using e⋯] using e`

will simplify the goal and the type of`e`

using`rules`

, then try to close the goal using`e`

.

Simplifying the type of `e`

makes it more likely to match the goal
(which has also been simplified). This construction also tends to be
more robust under changes to the simp lemma set.

`simpa [rules, ⋯]⋯]`

will simplify the goal and the type of a hypothesis`this`

if present in the context, then try to close the goal using the`assumption`

tactic.

#TODO: implement `?`

## Equations

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

This is a "finishing" tactic modification of `simp`

. It has two forms.

`simpa [rules, ⋯] using e⋯] using e`

will simplify the goal and the type of`e`

using`rules`

, then try to close the goal using`e`

.

`e`

makes it more likely to match the goal
(which has also been simplified). This construction also tends to be
more robust under changes to the simp lemma set.

`simpa [rules, ⋯]⋯]`

will simplify the goal and the type of a hypothesis`this`

if present in the context, then try to close the goal using the`assumption`

tactic.

#TODO: implement `?`

## Equations

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

Gets the value of the `linter.unnecessarySimpa`

option.