Deploying to gh-pages from @ 5ee70f8 🚀

print.html

@@ -2213,7 +2213,7 @@ <h3 id="析取"><a class="header" href="#析取">析取</a></h3>
 ``hqr : q → r``, and produces a proof of ``r``. In the following example, we use
 ``Or.elim`` to prove ``p ∨ q → q ∨ p``.
 -->
-<p>析取消去规则稍微复杂一点。这个想法是，我们可以从 <code>p ∨ q</code> 证明 <code>r</code>，通过从 <code>p</code> 证明 <code>r</code>，且从 <code>q</code> 证明 <code>r</code>。换句话说，它是一种逐情况证明。在表达式 <code>Or.elim hpq hpr hqr</code> 中，<code>Or.elim</code> 接受三个论证，<code>hpq : p ∨ q</code>，<code>hpr : p → r</code> 和 <code>hqr : q → r</code>，生成 <code>r</code> 的证明。在下面的例子中，我们使用 <code>Or.elim</code> 证明 <code>p ∨ q → q ∨ p</code>。</p>
+<p>析取消去规则稍微复杂一点。这个想法是，如果我们想要从 <code>p ∨ q</code> 证明 <code>r</code>，只需要展示 <code>p</code> 可以证明 <code>r</code>，且 <code>q</code> 也可以证明 <code>r</code>。换句话说，它是一种逐情况证明。在表达式 <code>Or.elim hpq hpr hqr</code> 中，<code>Or.elim</code> 接受三个论证，<code>hpq : p ∨ q</code>，<code>hpr : p → r</code> 和 <code>hqr : q → r</code>，生成 <code>r</code> 的证明。在下面的例子中，我们使用 <code>Or.elim</code> 证明 <code>p ∨ q → q ∨ p</code>。</p>
 <pre><code class="language-lean">variable (p q r : Prop)
 
 example (h : p ∨ q) : q ∨ p :=
@@ -3674,7 +3674,7 @@ <h2 id="多来点儿证明语法"><a class="header" href="#多来点儿证明语
 expression introduced in this way using the keyword ``this``:
 -->
 <p>我们已经看到像 <code>fun</code>、<code>have</code> 和 <code>show</code> 这样的关键字使得写出反映非正式数学证明结构的正式证明项成为可能。在本节中，我们将讨论证明语言的一些通常很方便的附加特性。</p>
-<p>首先，我们可以使用匿名的 <code>have</code> 表达式来引入一个辅助目标，而不需要标注它。我们可以使用关键字 <code>this</code>'来引用最后一个以这种方式引入的表达式:</p>
+<p>首先，我们可以使用匿名的 <code>have</code> 表达式来引入一个辅助目标，而不需要标注它。我们可以使用关键字 <code>this</code> 来引用最后一个以这种方式引入的表达式:</p>
 <pre><code class="language-lean">variable (f : Nat → Nat)
 variable (h : ∀ x : Nat, f x ≤ f (x + 1))
 

propositions_and_proofs.html

@@ -757,7 +757,7 @@ <h3 id="析取"><a class="header" href="#析取">析取</a></h3>
 ``hqr : q → r``, and produces a proof of ``r``. In the following example, we use
 ``Or.elim`` to prove ``p ∨ q → q ∨ p``.
 -->
-<p>析取消去规则稍微复杂一点。这个想法是，我们可以从 <code>p ∨ q</code> 证明 <code>r</code>，通过从 <code>p</code> 证明 <code>r</code>，且从 <code>q</code> 证明 <code>r</code>。换句话说，它是一种逐情况证明。在表达式 <code>Or.elim hpq hpr hqr</code> 中，<code>Or.elim</code> 接受三个论证，<code>hpq : p ∨ q</code>，<code>hpr : p → r</code> 和 <code>hqr : q → r</code>，生成 <code>r</code> 的证明。在下面的例子中，我们使用 <code>Or.elim</code> 证明 <code>p ∨ q → q ∨ p</code>。</p>
+<p>析取消去规则稍微复杂一点。这个想法是，如果我们想要从 <code>p ∨ q</code> 证明 <code>r</code>，只需要展示 <code>p</code> 可以证明 <code>r</code>，且 <code>q</code> 也可以证明 <code>r</code>。换句话说，它是一种逐情况证明。在表达式 <code>Or.elim hpq hpr hqr</code> 中，<code>Or.elim</code> 接受三个论证，<code>hpq : p ∨ q</code>，<code>hpr : p → r</code> 和 <code>hqr : q → r</code>，生成 <code>r</code> 的证明。在下面的例子中，我们使用 <code>Or.elim</code> 证明 <code>p ∨ q → q ∨ p</code>。</p>
 <pre><code class="language-lean">variable (p q r : Prop)
 
 example (h : p ∨ q) : q ∨ p :=

quantifiers_and_equality.html

@@ -1062,7 +1062,7 @@ <h2 id="多来点儿证明语法"><a class="header" href="#多来点儿证明语
 expression introduced in this way using the keyword ``this``:
 -->
 <p>我们已经看到像 <code>fun</code>、<code>have</code> 和 <code>show</code> 这样的关键字使得写出反映非正式数学证明结构的正式证明项成为可能。在本节中，我们将讨论证明语言的一些通常很方便的附加特性。</p>
-<p>首先，我们可以使用匿名的 <code>have</code> 表达式来引入一个辅助目标，而不需要标注它。我们可以使用关键字 <code>this</code>'来引用最后一个以这种方式引入的表达式:</p>
+<p>首先，我们可以使用匿名的 <code>have</code> 表达式来引入一个辅助目标，而不需要标注它。我们可以使用关键字 <code>this</code> 来引用最后一个以这种方式引入的表达式:</p>
 <pre><code class="language-lean">variable (f : Nat → Nat)
 variable (h : ∀ x : Nat, f x ≤ f (x + 1))