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)) #[]) : Lean.Elab.TermElabM (Array Lean.MVarId)

Equations

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

def Mathlib.Tactic.induction' : Lean.ParserDescr

Equations

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

def Mathlib.Tactic.cases' : Lean.ParserDescr

Equations

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