Merge pull request #10 from qiancy98/patch-1

typofix: 一些小修改

propositions_and_proofs.md

@@ -764,7 +764,7 @@ takes three arguments, ``hpq : p ∨ q``, ``hpr : p → r`` and
 ``Or.elim`` to prove ``p ∨ q → q ∨ p``.
 -->
 
-析取消去规则稍微复杂一点。这个想法是，我们可以从 ``p ∨ q`` 证明 ``r``，通过从 ``p`` 证明 ``r``，且从 ``q`` 证明 ``r``。换句话说，它是一种逐情况证明。在表达式 ``Or.elim hpq hpr hqr`` 中，``Or.elim`` 接受三个论证，``hpq : p ∨ q``，``hpr : p → r`` 和 ``hqr : q → r``，生成 ``r`` 的证明。在下面的例子中，我们使用 ``Or.elim`` 证明 ``p ∨ q → q ∨ p``。
+析取消去规则稍微复杂一点。这个想法是，如果我们想要从 ``p ∨ q`` 证明 ``r``，只需要展示 ``p`` 可以证明 ``r``，且 ``q`` 也可以证明 ``r``。换句话说，它是一种逐情况证明。在表达式 ``Or.elim hpq hpr hqr`` 中，``Or.elim`` 接受三个论证，``hpq : p ∨ q``，``hpr : p → r`` 和 ``hqr : q → r``，生成 ``r`` 的证明。在下面的例子中，我们使用 ``Or.elim`` 证明 ``p ∨ q → q ∨ p``。
 
 ```lean
 variable (p q r : Prop)

quantifiers_and_equality.md

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