diff --git a/MIL/C01_Introduction/S02_Overview.lean b/MIL/C01_Introduction/S02_Overview.lean
index 44ac67f..358ef99 100644
--- a/MIL/C01_Introduction/S02_Overview.lean
+++ b/MIL/C01_Introduction/S02_Overview.lean
@@ -219,13 +219,13 @@ Marc Huisinga,
 Benjamin Jones,
 Julian Külshammer,
 Victor Liu, Jimmy Lu,
-Martin C. Martin, Giovanni Mascellani, John McDowell, Bhavik Mehta, Isaiah Mindich,
+Martin C. Martin, Giovanni Mascellani, John McDowell, Joseph McKinsey, Bhavik Mehta, Isaiah Mindich,
 Kabelo Moiloa, Hunter Monroe, Pietro Monticone,
 Oliver Nash, Emanuelle Natale, Filippo A. E. Nuccio,
 Pim Otte,
 Bartosz Piotrowski,
 Nicolas Rolland, Keith Rush,
-Yannick Seurin, Guilherme Silva,
+Yannick Seurin, Guilherme Silva, Bernardo Subercaseaux,
 Pedro Sánchez Terraf, Matthew Toohey, Alistair Tucker,
 Floris van Doorn,
 Eric Wieser,
diff --git a/MIL/C04_Sets_and_Functions/S01_Sets.lean b/MIL/C04_Sets_and_Functions/S01_Sets.lean
index 6cee327..2233a88 100644
--- a/MIL/C04_Sets_and_Functions/S01_Sets.lean
+++ b/MIL/C04_Sets_and_Functions/S01_Sets.lean
@@ -459,7 +459,7 @@ and anonymous constructors,
 these two expressions behave roughly the same.
 As a result, we usually don't need to use ``bex_def``
 to transform them explicitly.
-Here is are some examples of how they are used:
+Here are some examples of how they are used:
 TEXT. -/
 -- BOTH:
 section
diff --git a/MIL/C04_Sets_and_Functions/S02_Functions.lean b/MIL/C04_Sets_and_Functions/S02_Functions.lean
index 5b18022..7125899 100644
--- a/MIL/C04_Sets_and_Functions/S02_Functions.lean
+++ b/MIL/C04_Sets_and_Functions/S02_Functions.lean
@@ -407,7 +407,7 @@ to their full domain,
 there are often relativized versions that restrict
 the statements to a subset of the domain type.
 
-Here is are some examples of ``InjOn`` and ``range`` in use:
+Here are some examples of ``InjOn`` and ``range`` in use:
 BOTH: -/
 section
 
diff --git a/MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean b/MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean
index 6704547..89ec17b 100644
--- a/MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean
+++ b/MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean
@@ -175,7 +175,7 @@ The codomain of ``f`` can be any type that supports a commutative,
 associative addition operation with a zero element.
 If you import ``Algebra.BigOperators.Basic`` and issue the command
 ``open BigOperators``, you can use the more suggestive notation
-``∑ x in s, f x``. Of course, there is are an analogous operation and
+``∑ x in s, f x``. Of course, there is an analogous operation and
 notation for finite products.
 
 We will talk about the ``Finset`` type and the operations
diff --git a/MIL/C07_Hierarchies/S01_Basics.lean b/MIL/C07_Hierarchies/S01_Basics.lean
index 0d540ef..0259167 100644
--- a/MIL/C07_Hierarchies/S01_Basics.lean
+++ b/MIL/C07_Hierarchies/S01_Basics.lean
@@ -762,7 +762,6 @@ that every preorder comes with a ``<₁`` which has a default value built from `
 TEXT. -/
 
 -- SOLUTIONS:
-
 class LT₁ (α : Type) where
   /-- The Less-Than relation -/
   lt : α → α → Prop