From afcbd63dd0d5b8b88fe4b4f32feb5f767318bb8d Mon Sep 17 00:00:00 2001
From: qiancy98 <49993496+qiancy98@users.noreply.github.com>
Date: Wed, 4 Sep 2024 10:30:45 +0800
Subject: [PATCH 1/2] Update propositions_and_proofs.md
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

修改了一句我看不懂的翻译
---
 propositions_and_proofs.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/propositions_and_proofs.md b/propositions_and_proofs.md
index a538ca5..c2acdc6 100644
--- a/propositions_and_proofs.md
+++ b/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)

From 15448ae399661eed68088f5c8fbd202c97d7aa48 Mon Sep 17 00:00:00 2001
From: qiancy98 <49993496+qiancy98@users.noreply.github.com>
Date: Wed, 4 Sep 2024 15:34:33 +0800
Subject: [PATCH 2/2] Update quantifiers_and_equality.md
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

删掉多余字符`'`
---
 quantifiers_and_equality.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/quantifiers_and_equality.md b/quantifiers_and_equality.md
index 74b3223..b6da4b4 100644
--- a/quantifiers_and_equality.md
+++ b/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)