.. _proofs_with_structure:

有结构的证明
============

从某种角度看，:numref:`第 %s 章 <proofs_by_calculation>`中的计算式证明全都是一步证明。在本章中，我们逐渐引入多步证明的组成部分。这些组成部分包括：建立之后会再次引用的“中间”事实；调用由你自己或他人先前证明过的具名引理；以及拆解由较简单陈述通过逻辑符号 :math:`\lor`、:math:`\land` 和 :math:`\exists` 组合而成的复杂数学陈述。

本章还介绍 Lean 语言的关键交互功能：实时更新的 *infoview*，它会跟踪你当前的假设和目标。

本章的工作会在中间插入一章之后，于 :numref:`第 %s 章 <proofs_with_structure_ii>`继续。

.. include:: ch02_Proofs_with_Structure/01_Intermediate_Steps.inc
.. include:: ch02_Proofs_with_Structure/02_Invoking_Lemmas.inc
.. include:: ch02_Proofs_with_Structure/03_Or.inc
.. include:: ch02_Proofs_with_Structure/04_And.inc
.. include:: ch02_Proofs_with_Structure/05_Exists.inc