7.1. タクティクの実行（Running Tactics）

タクティクは Lean.Parser.Term.byTactic : term`by tac` constructs a term of the expected type by running the tactic(s) `tac`. by を使用して項に含まれ、その後に同じインデントを持つタクティクの列が続きます：

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

あるいは、波括弧とセミコロンを明示的に使用することもできます：

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* }