## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

- Lean.expandExplicitBindersAux combinator idents type? body = Lean.expandExplicitBindersAux.loop combinator idents type? (Array.size idents) body

## Instances For

## Equations

- One or more equations did not get rendered due to their size.
- Lean.expandExplicitBindersAux.loop combinator idents type? 0 acc = pure acc

## Instances For

## Equations

- Lean.expandBrackedBindersAux combinator binders body = Lean.expandBrackedBindersAux.loop combinator binders (Array.size binders) body

## Instances For

## Equations

- One or more equations did not get rendered due to their size.
- Lean.expandBrackedBindersAux.loop combinator binders 0 acc = pure acc

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

Step-wise reasoning over transitive relations.

```
calc
a = b := pab
b = c := pbc
...
y = z := pyz
```

proves `a = z`

from the given step-wise proofs. `=`

can be replaced with any
relation implementing the typeclass `Trans`

. Instead of repeating the right-
hand sides, subsequent left-hand sides can be replaced with `_`

.

```
calc
a = b := pab
_ = c := pbc
...
_ = z := pyz
```

It is also possible to write the *first* relation as `<lhs>\n _ = <rhs> := <proof>`

. This is useful for aligning relation symbols, especially on longer:
identifiers:

```
calc abc
_ = bce := pabce
_ = cef := pbcef
...
_ = xyz := pwxyz
```

`calc`

has term mode and tactic mode variants. This is the term mode variant.

See Theorem Proving in Lean 4 for more information.

## Equations

- calc = Lean.ParserDescr.node `calc 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "calc") calcSteps)

## Instances For

Step-wise reasoning over transitive relations.

```
calc
a = b := pab
b = c := pbc
...
y = z := pyz
```

proves `a = z`

from the given step-wise proofs. `=`

can be replaced with any
relation implementing the typeclass `Trans`

. Instead of repeating the right-
hand sides, subsequent left-hand sides can be replaced with `_`

.

```
calc
a = b := pab
_ = c := pbc
...
_ = z := pyz
```

It is also possible to write the *first* relation as `<lhs>\n _ = <rhs> := <proof>`

. This is useful for aligning relation symbols:

```
calc abc
_ = bce := pabce
_ = cef := pbcef
...
_ = xyz := pwxyz
```

`calc`

has term mode and tactic mode variants. This is the tactic mode variant,
which supports an additional feature: it works even if the goal is `a = z'`

for some other `z'`

; in this case it will not close the goal but will instead
leave a subgoal proving `z = z'`

.

See Theorem Proving in Lean 4 for more information.

## Equations

- calcTactic = Lean.ParserDescr.node `calcTactic 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "calc" false) calcSteps)

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

Apply function extensionality and introduce new hypotheses.
The tactic `funext`

will keep applying the `funext`

lemma until the goal target is not reducible to

```
|- ((fun x => ...) = (fun x => ...))
```

The variant `funext h₁ ... hₙ`

applies `funext`

`n`

times, and uses the given identifiers to name the new hypotheses.
Patterns can be used like in the `intro`

tactic. Example, given a goal

```
|- ((fun x : Nat × Bool => ...) = (fun x => ...))
```

`funext (a, b)`

applies `funext`

once and performs pattern matching on the newly introduced pair.

## Equations

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

## Instances For

Expands

```
class abbrev C <params> := D_1, ..., D_n
```

into

```
class C <params> extends D_1, ..., D_n
attribute [instance] C.mk
```

## Equations

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

## Instances For

## Equations

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

## Instances For

`· tac`

focuses on the main goal and tries to solve it using `tac`

, or else fails.

## Equations

- cdot = Lean.ParserDescr.node `cdot 1022 (Lean.ParserDescr.binary `andthen cdotTk (Lean.ParserDescr.const `tacticSeqIndentGt))

## Instances For

Similar to `first`

, but succeeds only if one the given tactics solves the current goal.

## Equations

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

## Instances For

`repeat`

and `while`

notation #

## Equations

- Lean.Loop.forIn x init f = Lean.Loop.forIn.loop f init

## Instances For

## Equations

- Lean.doElemRepeat_ = Lean.ParserDescr.node `Lean.doElemRepeat_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "repeat ") (Lean.ParserDescr.const `doSeq))

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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