Lean4
/-- `interval_cases n` searches for upper and lower bounds on a variable `n`,
and if bounds are found,
splits into separate cases for each possible value of `n`.
As an example, in
```
example (n : ℕ) (w₁ : n ≥ 3) (w₂ : n < 5) : n = 3 ∨ n = 4 := by
interval_cases n
all_goals simp
```
after `interval_cases n`, the goals are `3 = 3 ∨ 3 = 4` and `4 = 3 ∨ 4 = 4`.
You can also explicitly specify a lower and upper bound to use,
as `interval_cases using hl, hu`.
The hypotheses should be in the form `hl : a ≤ n` and `hu : n < b`,
in which case `interval_cases` calls `fin_cases` on the resulting fact `n ∈ Set.Ico a b`.
You can specify a name `h` for the new hypothesis,
as `interval_cases h : n` or `interval_cases h : n using hl, hu`.
-/
@[tactic_parser 1000]
public meta def intervalCases : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.intervalCases 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "interval_cases" false✝)
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) (ParserDescr.const✝ `colGt))
(ParserDescr.unary✝ `optional
(ParserDescr.unary✝ `atomic
(ParserDescr.binary✝ `andthen Lean.binderIdent (ParserDescr.symbol✝ " : ")))))
(ParserDescr.cat✝ `term 0))))
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " using ") (ParserDescr.cat✝ `term 0))
(ParserDescr.symbol✝ ", "))
(ParserDescr.cat✝ `term 0))))
