The parser/printer uses an "inverted" meaning for the many constructor: rather than representing a sum of products, here it represents a product of sums. We fix this by applying invert, defined below, to the result.

Takes the number of fields of a single constructor and patterns to match its fields against (not necessarily the same number). The returned lists each contain one element per field of the constructor. The name is the name which will be used in the top-level cases tactic, and the rcases_patt is the pattern which the field will be matched against by subsequent cases tactics.

rcases h e pat performs case distinction on e using pat to name the arising new variables and assumptions. If h is some name, a new assumption h : e = pat will relate the expression e with the current pattern.

syntax for a rcases pattern: ('?' expr (: n)?) | ((h :)? expr (with patt_list)?)

The rcases tactic is the same as cases, but with more flexibility in the with pattern syntax to allow for recursive case splitting. The pattern syntax uses the following recursive grammar:

patt ::= (patt_list "|")* patt_list
patt_list ::= id | "_" | "⟨" (patt ",")* patt "⟩"

A pattern like ⟨a, b, c⟩ | ⟨d, e⟩ will do a split over the inductive datatype, naming the first three parameters of the first constructor as a,b,c and the first two of the second constructor d,e. If the list is not as long as the number of arguments to the constructor or the number of constructors, the remaining variables will be automatically named. If there are nested brackets such as ⟨⟨a⟩, b | c⟩ | d then these will cause more case splits as necessary. If there are too many arguments, such as ⟨a, b, c⟩ for splitting on ∃ x, ∃ y, p x, then it will be treated as ⟨a, ⟨b, c⟩⟩, splitting the last parameter as necessary.

rcases also has special support for quotient types: quotient induction into Prop works like matching on the constructor quot.mk.

rcases h : e with PAT will do the same as rcases e with PAT with the exception that an assumption h : e = PAT will be added to the context.

rcases? e will perform case splits on e in the same way as rcases e, but rather than accepting a pattern, it does a maximal cases and prints the pattern that would produce this case splitting. The default maximum depth is 5, but this can be modified with rcases? e : n.

The rintro tactic is a combination of the intros tactic with rcases to allow for destructuring patterns while introducing variables. See rcases for a description of supported patterns. For example, rintro (a | ⟨b, c⟩) ⟨d, e⟩ will introduce two variables, and then do case splits on both of them producing two subgoals, one with variables a d e and the other with b c d e.

rintro? will introduce and case split on variables in the same way as rintro, but will also print the rintro invocation that would have the same result. Like rcases?, rintro? : n allows for modifying the depth of splitting; the default is 5.

Alias for rintro.

The obtain tactic is a combination of have and rcases. obtain ⟨patt⟩ : type, { ... } is equivalent to have h : type, { ... }, rcases h with ⟨patt⟩. The syntax obtain ⟨patt⟩ : type := proof is also supported. If ⟨patt⟩ is omitted, rcases will try to infer the pattern. If type is omitted, := proof is required.