diff --git a/MIL/C06_Discrete_Mathematics/S02_Counting_Arguments.lean b/MIL/C06_Discrete_Mathematics/S02_Counting_Arguments.lean
index f4aa772..a9f30ee 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
@@ -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.
 
@@ -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)
@@ -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.
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