7.1. Running Tactics

Tactics are included in terms using Lean.Parser.Term.byTactic : term`by tac` constructs a term of the expected type by running the tactic(s) `tac`. by, which is followed by a sequence of tactics in which each has the same indentation:

term ::= ...
    | `by tac` constructs a term of the expected type by running the tactic(s) `tac`. by
      A sequence of tactics in brackets, or a delimiter-free indented sequence of tactics.
Delimiter-free indentation is determined by the *first* tactic of the sequence. tacticSeq

Alternatively, explicit braces and semicolons may be used:

term ::= ...
    | `by tac` constructs a term of the expected type by running the tactic(s) `tac`. by A sequence of tactics in brackets, or a delimiter-free indented sequence of tactics.
Delimiter-free indentation is determined by the *first* tactic of the sequence. The syntax `{ tacs }` is an alternative syntax for `· tacs`.
It runs the tactics in sequence, and fails if the goal is not solved. { tactic* }