style: remove three double spaces (#11186)

leanprover-community · Mar 26, 2024 · 951decc · 951decc
1 parent 30452cd
commit 951decc
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 4 deletions.
diff --git a/Mathlib/Data/List/NodupEquivFin.lean b/Mathlib/Data/List/NodupEquivFin.lean
@@ -19,8 +19,8 @@ Given a list `l`,
   sending `⟨x, hx⟩` to `⟨indexOf x l, _⟩`;
 
 * if `l` has no duplicates and contains every element of a type `α`, then
-  `List.Nodup.getEquivOfForallMemList` defines an equivalence between
-  `Fin (length l)` and `α`;  if `α` does not have decidable equality, then
+  `List.Nodup.getEquivOfForallMemList` defines an equivalence between `Fin (length l)` and `α`;
+  if `α` does not have decidable equality, then
   there is a bijection `List.Nodup.getBijectionOfForallMemList`;
 
 * if `l` is sorted w.r.t. `(<)`, then `List.Sorted.getIso` is the same bijection reinterpreted

diff --git a/Mathlib/GroupTheory/Submonoid/Membership.lean b/Mathlib/GroupTheory/Submonoid/Membership.lean
@@ -371,7 +371,7 @@ theorem card_le_one_iff_eq_bot : card S ≤ 1 ↔ S = ⊥ :=
 
 @[to_additive]
 lemma eq_bot_iff_card : S = ⊥ ↔ card S = 1 :=
-  ⟨by rintro rfl;  exact card_bot, eq_bot_of_card_eq⟩
+  ⟨by rintro rfl; exact card_bot, eq_bot_of_card_eq⟩
 
 end Submonoid
 

diff --git a/Mathlib/Order/PartialSups.lean b/Mathlib/Order/PartialSups.lean
@@ -61,7 +61,7 @@ theorem partialSups_succ (f : ℕ → α) (n : ℕ) :
 #align partial_sups_succ partialSups_succ
 
 lemma partialSups_iff_forall {f : ℕ → α} (p : α → Prop)
-    (hp : ∀ {a b}, p (a ⊔ b) ↔ p a ∧ p b) : ∀  {n : ℕ}, p (partialSups f n) ↔ ∀ k ≤ n, p (f k)
+    (hp : ∀ {a b}, p (a ⊔ b) ↔ p a ∧ p b) : ∀ {n : ℕ}, p (partialSups f n) ↔ ∀ k ≤ n, p (f k)
   | 0 => by simp
   | (n + 1) => by simp [hp, partialSups_iff_forall, ← Nat.lt_succ_iff, ← Nat.forall_lt_succ]