5.13. Proofs
The syntax for invoking tactics (Lean.Parser.Term.byTactic : term`by tac` constructs a term of the expected type by running the tactic(s) `tac`. by) is described in the section on proofs.
The syntax for invoking tactics (Lean.Parser.Term.byTactic : term`by tac` constructs a term of the expected type by running the tactic(s) `tac`. by) is described in the section on proofs.