chore: remove redundant spacing

avigad · Jan 6, 2025 · 5412d02 · 5412d02
1 parent dd0e13e
commit 5412d02
Show file tree

Hide file tree

Showing 9 changed files with 9 additions and 9 deletions.
diff --git a/MIL/C03_Logic/S01_Implication_and_the_Universal_Quantifier.lean b/MIL/C03_Logic/S01_Implication_and_the_Universal_Quantifier.lean
@@ -87,7 +87,7 @@ end
 At this stage, you also know that if you use
 the ``apply`` tactic to apply ``my_lemma``
 to a goal of the form ``|a * b| < δ``,
-you are left with new goals that require you to  prove
+you are left with new goals that require you to prove
 each of the hypotheses.
 
 .. index:: intro, tactics; intro

diff --git a/MIL/C03_Logic/S03_Negation.lean b/MIL/C03_Logic/S03_Negation.lean
@@ -381,7 +381,7 @@ example (h : ¬Monotone f) : ∃ x y, x ≤ y ∧ f y < f x := by
 -- SOLUTIONS:
 example (h : ¬Monotone f) : ∃ x y, x ≤ y ∧ f y < f x := by
   rw [Monotone] at h
-  push_neg  at h
+  push_neg at h
   exact h
 
 /- TEXT:

diff --git a/MIL/C04_Sets_and_Functions/S03_The_Schroeder_Bernstein_Theorem.lean b/MIL/C04_Sets_and_Functions/S03_The_Schroeder_Bernstein_Theorem.lean
@@ -266,7 +266,7 @@ SOLUTIONS: -/
     rw [if_pos x₁A, if_pos x₂A] at hxeq
     exact hf hxeq
 -- BOTH:
-  push_neg  at xA
+  push_neg at xA
 /- EXAMPLES:
   sorry
 SOLUTIONS: -/

diff --git a/MIL/C05_Elementary_Number_Theory/S01_Irrational_Roots.lean b/MIL/C05_Elementary_Number_Theory/S01_Irrational_Roots.lean
@@ -465,5 +465,5 @@ end
 --   have := Ne.symm (ne_of_lt this)
 --   intro h
 --   field_simp [this]  at h
---   norm_cast  at h
+--   norm_cast at h
 --   sorry
diff --git a/MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean b/MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean
@@ -142,7 +142,7 @@ SOLUTIONS: -/
   refine ⟨p, ?_, pp⟩
   show p > n
   by_contra ple
-  push_neg  at ple
+  push_neg at ple
   have : p ∣ Nat.factorial (n + 1) := by
 /- EXAMPLES:
     sorry

diff --git a/MIL/C10_Topology/S01_Filters.lean b/MIL/C10_Topology/S01_Filters.lean
@@ -49,7 +49,7 @@ condition then says that ``univ`` is sufficiently large, the second one says tha
 large set is sufficiently large and the third one says that the intersection of two sufficiently large sets
 is sufficiently large.
 
-It may be even  more useful to think of a filter on a type ``X``
+It may be even more useful to think of a filter on a type ``X``
 as a generalized element of ``Set X``. For instance, ``atTop`` is the
 "set of very large numbers" and ``𝓝 x₀`` is the "set of points very close to ``x₀``."
 One manifestation of this view is that we can associate to any ``s : Set X`` the so-called *principal filter*

diff --git a/MIL/C10_Topology/S03_Topological_Spaces.lean b/MIL/C10_Topology/S03_Topological_Spaces.lean
@@ -45,7 +45,7 @@ example {ι : Type*} [Fintype ι] {s : ι → Set X} (hs : ∀ i, IsOpen (s i))
 
 /- TEXT:
 
-Closed sets are then defined as sets whose complement  is open. A function between topological spaces
+Closed sets are then defined as sets whose complement is open. A function between topological spaces
 is (globally) continuous if all preimages of open sets are open.
 BOTH: -/
 -- QUOTE:

diff --git a/user_repo_source/.github/pull_request_template.md b/user_repo_source/.github/pull_request_template.md
@@ -1,3 +1,3 @@
 WARNING: Please do not open a pull request in this repository.
 
-This is not the relevant repository to contribute to Mathematics in Lean. This repository is cloned by people who want to study the book. It is automatically created from the source repository which can be found at  https://github.com/avigad/mathematics_in_lean_source and where you can open a pull-request.
+This is not the relevant repository to contribute to Mathematics in Lean. This repository is cloned by people who want to study the book. It is automatically created from the source repository which can be found at https://github.com/avigad/mathematics_in_lean_source and where you can open a pull-request.
diff --git a/user_repo_source/README.md b/user_repo_source/README.md
@@ -36,7 +36,7 @@ Do the following:
    You can call the copy `my_files` or whatever you want and use it to create
    your own Lean files as well.
 
-At that point, you can open the textbook in a web browser 
+At that point, you can open the textbook in a web browser
 at [https://leanprover-community.github.io/mathematics_in_lean/](https://leanprover-community.github.io/mathematics_in_lean/)
 and start reading and doing the exercises in VS Code.