`by_cases`

and `if then else`

tactics #

This implements the `if`

tactic, which is a structured proof version of `by_cases`

.
It allows writing `if h : t then tac1 else tac2`

for case analysis on `h : t`

,

In tactic mode, `if h : t then tac1 else tac2`

can be used as alternative syntax for:

```
by_cases h : t
· tac1
· tac2
```

It performs case distinction on `h : t`

or `h : ¬t¬t`

and `tac1`

and `tac2`

are the subproofs.

You can use `?_`

or `_`

for either subproof to delay the goal to after the tactic, but
if a tactic sequence is provided for `tac1`

or `tac2`

then it will require the goal to be closed
by the end of the block.

## Equations

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

In tactic mode, `if t then tac1 else tac2`

is alternative syntax for:

```
by_cases t
· tac1
· tac2
```

It performs case distinction on `h† : t`

or `h† : ¬t¬t`

, where `h†`

is an anonymous
hypothesis, and `tac1`

and `tac2`

are the subproofs. (It doesn't actually use
nondependent `if`

, since this wouldn't add anything to the context and hence would be
useless for proving theorems. To actually insert an `ite`

application use
`refine if t then ?_ else ?_`

.)

## Equations

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