Intro Patterns

SSReflect intro patterns come after => tactical. The general syntax here would be tac=> intro_pats. This first executes tac, and then intro_pats. All intro patterns listed below are equivalent to their SSReflect counterparts (if there are such).

1. name (introduce with a given name), ? (introduce with an autogenerated name), _ (clear), -> (rewrite left), <- (rewrite right). All listed patterns are applied to the to element of the goal stack.
2. * (introduce everything), > (introduce all named variables)
3. ! applies a correspondent existential lemma (marked with @[ext]) to the goal
4. /t: applies t to the top element on the goal stack
5. /(_ t): applies top element on the goal stack to t
6. /[swap],/[dup], /[apply]: swaps first two top hypothesis on the stack, duplicates top hypothesis on the stack, applies the first top hypothesis to the second top hypothesis
7. []: equivalent to scase
8. ![]: iterative version of []. Destructs the top element on the goal stack and all its nested structures. Equivalent to [x .. [.. [y]]], e.g. to destruct ∃ (x y : Nat)
9. [ branch_1 | branch_2 | .. | branch_n ]: equivalent to scase, but runs branch_i on the i-th subgoal, which appears after case analysis
10. ⟨ branch_1 | branch_2 | .. | branch_n ⟩ : equivalent to constructor, but runs branch_i on the i-th subgoal, which appears after applying a corresponding constructor analysis
11. ?[]: destructs the top element on the goal stack and suggests you to use [ | ... | ] with a correct number of alternations instead.
12. { name_1 name_2 .. name_n }: clears all name_is
13. {}name: equivalent to clear name; intro name
14. /=, /==: equivalent to dsimp and simp correspondingly
15. //: calls ssr_triv tactic (combination of simp_all and trivial). If you want to augment it with an extra tactic tac, you can write:

macro_rules : tactic
  | `(tactic| ssr_triv) => `(tactic| tac)

Note that // will never fail. If it cannot solve the goal, it will leave it unchanged.

16. //=, //==: equivalent to // /= and // /==
17. /[tac t]: calls tactic t

Moreover, intro patterns are extensible. If you want to add your own intro pattern pat, just write:

syntax <pat> : ssrIntro.
elab_rules : tactic
  | `(ssrIntro| pat) => <implementation>