From 057dcb4d4de2cf3ba7cb60868c0686e6c4106aed Mon Sep 17 00:00:00 2001 From: Yannick Seurin Date: Fri, 13 Jun 2025 15:17:34 +0200 Subject: [PATCH 1/5] =?UTF-8?q?avoid=20deprecated=20notation=20=E2=88=91?= =?UTF-8?q?=20i=20in=20s?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- MIL/C06_Discrete_Mathematics/S02_Counting_Arguments.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/MIL/C06_Discrete_Mathematics/S02_Counting_Arguments.lean b/MIL/C06_Discrete_Mathematics/S02_Counting_Arguments.lean index f4aa772..7cb6772 100644 --- a/MIL/C06_Discrete_Mathematics/S02_Counting_Arguments.lean +++ b/MIL/C06_Discrete_Mathematics/S02_Counting_Arguments.lean @@ -117,7 +117,7 @@ example (n : ℕ) : #(triangle n) = (n + 1) * n / 2 := by intro x _ y _ xney simp [disjoint_iff_ne, xney] -- continue the calculation - transitivity (∑ i in range (n+1), i) + transitivity (∑ i ∈ range (n+1), i) · congr; ext i rw [card_image_of_injective, card_range] intros i1 i2; simp From 7c27a4d1f1f43b2244072d3f9e5c891cbc24cfcc Mon Sep 17 00:00:00 2001 From: Yannick Seurin Date: Fri, 13 Jun 2025 15:18:56 +0200 Subject: [PATCH 2/5] =?UTF-8?q?replace=20Nat=20with=20=E2=84=95?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- MIL/C06_Discrete_Mathematics/S02_Counting_Arguments.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/MIL/C06_Discrete_Mathematics/S02_Counting_Arguments.lean b/MIL/C06_Discrete_Mathematics/S02_Counting_Arguments.lean index 7cb6772..8c7faae 100644 --- a/MIL/C06_Discrete_Mathematics/S02_Counting_Arguments.lean +++ b/MIL/C06_Discrete_Mathematics/S02_Counting_Arguments.lean @@ -253,7 +253,7 @@ EXAMPLES: -/ section -- QUOTE: open Classical -variable (s t : Finset Nat) (a b : Nat) +variable (s t : Finset ℕ) (a b : ℕ) theorem doubleCounting {α β : Type*} (s : Finset α) (t : Finset β) (r : α → β → Prop) From 2b08ff43a2bb8bdb97c45a0fd7d63cd6f21af6cc Mon Sep 17 00:00:00 2001 From: Yannick Seurin Date: Fri, 13 Jun 2025 15:21:57 +0200 Subject: [PATCH 3/5] simplify exercise solution --- MIL/C06_Discrete_Mathematics/S02_Counting_Arguments.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/MIL/C06_Discrete_Mathematics/S02_Counting_Arguments.lean b/MIL/C06_Discrete_Mathematics/S02_Counting_Arguments.lean index 8c7faae..6518db7 100644 --- a/MIL/C06_Discrete_Mathematics/S02_Counting_Arguments.lean +++ b/MIL/C06_Discrete_Mathematics/S02_Counting_Arguments.lean @@ -236,7 +236,7 @@ example (n : ℕ) : #(triangle' n) = #(triangle n) := by omega . simp; omega rw [this, card_image_of_injOn] - rintro ⟨p1, p2⟩ hp ⟨q1, q2⟩ hq; simp [f] at * + rintro ⟨p1, p2⟩ hp ⟨q1, q2⟩ hq; simp [f] BOTH: -/ -- QUOTE. From effc27b0ba3a300cb5ab43116cbf757377237b58 Mon Sep 17 00:00:00 2001 From: Yannick Seurin Date: Fri, 13 Jun 2025 17:32:42 +0200 Subject: [PATCH 4/5] simplify exercise solution --- MIL/C06_Discrete_Mathematics/S02_Counting_Arguments.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/MIL/C06_Discrete_Mathematics/S02_Counting_Arguments.lean b/MIL/C06_Discrete_Mathematics/S02_Counting_Arguments.lean index 6518db7..a9f30ee 100644 --- a/MIL/C06_Discrete_Mathematics/S02_Counting_Arguments.lean +++ b/MIL/C06_Discrete_Mathematics/S02_Counting_Arguments.lean @@ -313,9 +313,8 @@ BOTH: -/ sorry /- SOLUTIONS: rcases ht' with ⟨m, ⟨hm, hm'⟩, k, ⟨hk, hk'⟩, hmk⟩ + use m, hm, k, hk have : m = k + 1 ∨ k = m + 1 := by omega - rcases this with rfl | rfl - . use k, hk, k+1, hm; simp - . use m, hm, m+1, hk; simp + rcases this with h | h <;> simp [h] BOTH: -/ -- QUOTE. From 197c7fd0dc39ed143addcd3956612c98aa85a146 Mon Sep 17 00:00:00 2001 From: Yannick Seurin Date: Mon, 16 Jun 2025 12:09:46 +0200 Subject: [PATCH 5/5] typo --- MIL/C06_Discrete_Mathematics/S03_Inductive_Structures.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/MIL/C06_Discrete_Mathematics/S03_Inductive_Structures.lean b/MIL/C06_Discrete_Mathematics/S03_Inductive_Structures.lean index b6631e9..e224982 100644 --- a/MIL/C06_Discrete_Mathematics/S03_Inductive_Structures.lean +++ b/MIL/C06_Discrete_Mathematics/S03_Inductive_Structures.lean @@ -131,7 +131,7 @@ linear-time implementation. Try proving ``reverse (as ++ bs) = reverse bs ++ reverse as`` and ``reverse (reverse as) = as``. You can use ``cons_append`` and ``append_assoc``, but you -You may need to come up with auxiliary lemmas and prove them. +may need to come up with auxiliary lemmas and prove them. EXAMPLES: -/ -- QUOTE: def reverseαα : List α → List α := sorry