Tactic to split if-then-else expressions.

source
def Mathlib.Tactic.splitIfs :
Lean.ParserDescr

Splits all if-then-else-expressions into multiple goals. Given a goal of the form `g (if p then x else y)`, `split_ifs` will produce two goals: `p ⊢ g x` and `¬p ⊢ g y`. If there are multiple ite-expressions, then `split_ifs` will split them all, starting with a top-most one whose condition does not contain another ite-expression. `split_ifs at *` splits all ite-expressions in all hypotheses as well as the goal. `split_ifs with h₁ h₂ h₃` overrides the default names for the hypotheses.

Equations

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

Instances For