# Documentation

Mathlib.Tactic.Cases

# 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
∨ 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
∨ 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
∨ 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
∨ 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
∨ q) : q ∨ p := by
rcases h with hp | hq
· exact Or.inr hp
· exact Or.inl hq
∨ 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 Lean.Parser.Tactic.ElimApp.evalNames (elimInfo : Lean.Meta.ElimInfo) (alts : ) (withArg : Lean.Syntax) (numEqs : ) (numGeneralized : ) (toClear : optParam () #[]) :
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.