Documentation

Mathlib.Tactic.ByCases

The by_cases! tactic #

The by_cases! tactic is a variant of the by_cases tactic that also calls push Not on the generated hypothesis that is a negation.

source
🔸 coverage
def Mathlib.Tactic.ByCases.byCases! :
Lean.ParserDescr

by_cases! h : p runs the by_cases h : p tactic, followed by push Not at h in the second subgoal. For example,

  • by_cases! h : a < b creates one goal with hypothesis h : a < b and another with h : b ≤ a.
  • by_cases! h : a ≠ b creates one goal with hypothesis h : a ≠ b and another with h : a = b.
Instances For