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

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.

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.