From 024eeab9372546214a24d6b86723115f9fcfa7e7 Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Mon, 20 Jan 2025 16:42:59 -0500
Subject: [PATCH] typos from Bernardo Subercaseaux

---
 MIL/C01_Introduction/S02_Overview.lean                        | 4 ++--
 MIL/C04_Sets_and_Functions/S01_Sets.lean                      | 2 +-
 MIL/C04_Sets_and_Functions/S02_Functions.lean                 | 2 +-
 .../S02_Induction_and_Recursion.lean                          | 2 +-
 MIL/C07_Hierarchies/S01_Basics.lean                           | 1 -
 5 files changed, 5 insertions(+), 6 deletions(-)

diff --git a/MIL/C01_Introduction/S02_Overview.lean b/MIL/C01_Introduction/S02_Overview.lean
index 44ac67f2..358ef990 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 6cee3271..2233a883 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 5b180223..71258998 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 67045472..89ec17b3 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 0d540ef7..02591673 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