Extra tactics and implementation for some tactics defined at `Init/Tactic.lean`

`iterate n tac`

runs `tac`

exactly `n`

times.
`iterate tac`

runs `tac`

repeatedly until failure.

`iterate`

's argument is a tactic sequence,
so multiple tactics can be run using `iterate n (tac₁; tac₂; ⋯)`

or

```
iterate n
tac₁
tac₂
⋯
```

## Equations

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

## Instances For

Rewrites with the given rules, normalizing casts prior to each step.

## Equations

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

## Instances For

Normalize casts in the goal and the given expression, then close the goal with `exact`

.

## Equations

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

## Instances For

Normalize casts in the goal and the given expression, then `apply`

the expression to the goal.

## Equations

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