# 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.

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

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

Instances For

source
def Mathlib.Tactic.induction' :
Lean.ParserDescr

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

source
def Mathlib.Tactic.cases' :
Lean.ParserDescr

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.

Instances For