The by_cases! tactic

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

def byCases! : Lean.ParserDescr

by_cases! h : p runs the by_cases h : p tactic, followed by try push_neg 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.

Equations

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