Lean4
/-- `fin_cases h` performs case analysis on a hypothesis of the form
`h : A`, where `[Fintype A]` is available, or
`h : a ∈ A`, where `A : Finset X`, `A : Multiset X` or `A : List X`.
As an example, in
```
example (f : ℕ → Prop) (p : Fin 3) (h0 : f 0) (h1 : f 1) (h2 : f 2) : f p.val := by
fin_cases p; simp
all_goals assumption
```
after `fin_cases p; simp`, there are three goals, `f 0`, `f 1`, and `f 2`.
-/
@[tactic_parser 1000]
public meta def finCases : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Lean.Elab.Tactic.finCases 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "fin_cases " false✝)
(ParserDescr.binary✝ `orelse (ParserDescr.nodeWithAntiquot✝ "*" `token.«*» (ParserDescr.symbol✝ "*"))
((with_annotate_term"sepBy1(" @ParserDescr.sepBy1✝) (ParserDescr.cat✝ `term 0) "," (ParserDescr.symbol✝ ", ")
Bool.false✝)))
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " with ")
((with_annotate_term"sepBy1(" @ParserDescr.sepBy1✝) (ParserDescr.cat✝ `term 0) "," (ParserDescr.symbol✝ ", ")
Bool.false✝))))
