# Backward compatible implementation of lean 3 `cases`

tactic #

This tactic is similar to the `cases`

tactic in Lean 4 core, but the syntax for giving
names is different:

```
example (h : p ∨ q) : q ∨ p := by
cases h with
| inl hp => exact Or.inr hp
| inr hq => exact Or.inl hq
example (h : p ∨ q) : q ∨ p := by
cases' h with hp hq
· exact Or.inr hp
· exact Or.inl hq
example (h : p ∨ q) : q ∨ p := by
rcases h with hp | hq
· exact Or.inr hp
· exact Or.inl hq
```

Prefer `cases`

or `rcases`

when possible, because these tactics promote structured proofs.

def
Mathlib.Tactic.ElimApp.evalNames
(elimInfo : Lean.Meta.ElimInfo)
(alts : Array Lean.Elab.Tactic.ElimApp.Alt)
(withArg : Lean.Syntax)
(numEqs : optParam Nat 0)
(generalized : optParam (Array Lean.FVarId) #[])
(toClear : optParam (Array Lean.FVarId) #[])
(toTag : optParam (Array (Lean.Ident × Lean.FVarId)) #[])
:

## Equations

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

## Instances For

The `induction'`

tactic is similar to the `induction`

tactic in Lean 4 core,
but with slightly different syntax (such as, no requirement to name the constructors).

```
open Nat
example (n : ℕ) : 0 < factorial n := by
induction' n with n ih
· rw [factorial_zero]
simp
· rw [factorial_succ]
apply mul_pos (succ_pos n) ih
example (n : ℕ) : 0 < factorial n := by
induction n
case zero =>
rw [factorial_zero]
simp
case succ n ih =>
rw [factorial_succ]
apply mul_pos (succ_pos n) ih
```

## Equations

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

## Instances For

The `cases'`

tactic is similar to the `cases`

tactic in Lean 4 core, but the syntax for giving
names is different:

```
example (h : p ∨ q) : q ∨ p := by
cases h with
| inl hp => exact Or.inr hp
| inr hq => exact Or.inl hq
example (h : p ∨ q) : q ∨ p := by
cases' h with hp hq
· exact Or.inr hp
· exact Or.inl hq
example (h : p ∨ q) : q ∨ p := by
rcases h with hp | hq
· exact Or.inr hp
· exact Or.inl hq
```

Prefer `cases`

or `rcases`

when possible, because these tactics promote structured proofs.

## Equations

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