chore(Order/SuccPred/CompleteLinearOrder): spacing fixes (#19799)

Author: vihdzp

Mathlib/Order/SuccPred/CompleteLinearOrder.lean

@@ -19,8 +19,7 @@ section ConditionallyCompleteLinearOrder
 variable [ConditionallyCompleteLinearOrder α] [Nonempty ι] {f : ι → α} {s : Set α} {x : α}
 
 lemma csSup_mem_of_not_isSuccPrelimit
-    (hne : s.Nonempty) (hbdd : BddAbove s) (hlim : ¬ IsSuccPrelimit (sSup s)) :
-    sSup s ∈ s := by
+    (hne : s.Nonempty) (hbdd : BddAbove s) (hlim : ¬ IsSuccPrelimit (sSup s)) : sSup s ∈ s := by
   obtain ⟨y, hy⟩ := not_forall_not.mp hlim
   obtain ⟨i, his, hi⟩ := exists_lt_of_lt_csSup hne hy.lt
   exact eq_of_le_of_not_lt (le_csSup hbdd his) (hy.2 hi) ▸ his
@@ -29,8 +28,7 @@ lemma csSup_mem_of_not_isSuccPrelimit
 alias csSup_mem_of_not_isSuccLimit := csSup_mem_of_not_isSuccPrelimit
 
 lemma csInf_mem_of_not_isPredPrelimit
-    (hne : s.Nonempty) (hbdd : BddBelow s) (hlim : ¬ IsPredPrelimit (sInf s)) :
-    sInf s ∈ s := by
+    (hne : s.Nonempty) (hbdd : BddBelow s) (hlim : ¬ IsPredPrelimit (sInf s)) : sInf s ∈ s := by
   obtain ⟨y, hy⟩ := not_forall_not.mp hlim
   obtain ⟨i, his, hi⟩ := exists_lt_of_csInf_lt hne hy.lt
   exact eq_of_le_of_not_lt (csInf_le hbdd his) (hy.2 · hi) ▸ his
@@ -39,17 +37,15 @@ lemma csInf_mem_of_not_isPredPrelimit
 alias csInf_mem_of_not_isPredLimit := csInf_mem_of_not_isPredPrelimit
 
 lemma exists_eq_ciSup_of_not_isSuccPrelimit
-    (hf : BddAbove (Set.range f)) (hf' : ¬ IsSuccPrelimit (⨆ i, f i)) :
-    ∃ i, f i = ⨆ i, f i :=
-  csSup_mem_of_not_isSuccPrelimit (Set.range_nonempty f) hf hf'
+    (hf : BddAbove (range f)) (hf' : ¬ IsSuccPrelimit (⨆ i, f i)) : ∃ i, f i = ⨆ i, f i :=
+  csSup_mem_of_not_isSuccPrelimit (range_nonempty f) hf hf'
 
 @[deprecated exists_eq_ciSup_of_not_isSuccPrelimit (since := "2024-09-05")]
 alias exists_eq_ciSup_of_not_isSuccLimit := exists_eq_ciSup_of_not_isSuccPrelimit
 
 lemma exists_eq_ciInf_of_not_isPredPrelimit
-    (hf : BddBelow (Set.range f)) (hf' : ¬ IsPredPrelimit (⨅ i, f i)) :
-    ∃ i, f i = ⨅ i, f i :=
-  csInf_mem_of_not_isPredPrelimit (Set.range_nonempty f) hf hf'
+    (hf : BddBelow (range f)) (hf' : ¬ IsPredPrelimit (⨅ i, f i)) : ∃ i, f i = ⨅ i, f i :=
+  csInf_mem_of_not_isPredPrelimit (range_nonempty f) hf hf'
 
 @[deprecated exists_eq_ciInf_of_not_isPredPrelimit (since := "2024-09-05")]
 alias exists_eq_ciInf_of_not_isPredLimit := exists_eq_ciInf_of_not_isPredPrelimit
@@ -69,15 +65,15 @@ lemma IsGLB.mem_of_nonempty_of_not_isPredPrelimit
 alias IsGLB.mem_of_nonempty_of_not_isPredLimit := IsGLB.mem_of_nonempty_of_not_isPredPrelimit
 
 lemma IsLUB.exists_of_nonempty_of_not_isSuccPrelimit
-    (hf : IsLUB (Set.range f) x) (hx : ¬ IsSuccPrelimit x) :
-    ∃ i, f i = x := hf.mem_of_nonempty_of_not_isSuccPrelimit (Set.range_nonempty f) hx
+    (hf : IsLUB (range f) x) (hx : ¬ IsSuccPrelimit x) : ∃ i, f i = x :=
+  hf.mem_of_nonempty_of_not_isSuccPrelimit (range_nonempty f) hx
 
 @[deprecated IsLUB.exists_of_nonempty_of_not_isSuccPrelimit (since := "2024-09-05")]
 alias IsLUB.exists_of_nonempty_of_not_isSuccLimit := IsLUB.exists_of_nonempty_of_not_isSuccPrelimit
 
 lemma IsGLB.exists_of_nonempty_of_not_isPredPrelimit
-    (hf : IsGLB (Set.range f) x) (hx : ¬ IsPredPrelimit x) :
-    ∃ i, f i = x := hf.mem_of_nonempty_of_not_isPredPrelimit (Set.range_nonempty f) hx
+    (hf : IsGLB (range f) x) (hx : ¬ IsPredPrelimit x) : ∃ i, f i = x :=
+  hf.mem_of_nonempty_of_not_isPredPrelimit (range_nonempty f) hx
 
 @[deprecated IsGLB.exists_of_nonempty_of_not_isPredPrelimit (since := "2024-09-05")]
 alias IsGLB.exists_of_nonempty_of_not_isPredLimit := IsGLB.exists_of_nonempty_of_not_isPredPrelimit
@@ -110,9 +106,8 @@ variable [ConditionallyCompleteLinearOrderBot α] {f : ι → α} {s : Set α} {
 
 /-- See `csSup_mem_of_not_isSuccPrelimit` for the `ConditionallyCompleteLinearOrder` version. -/
 lemma csSup_mem_of_not_isSuccPrelimit'
-    (hbdd : BddAbove s) (hlim : ¬ IsSuccPrelimit (sSup s)) :
-    sSup s ∈ s := by
-  obtain (rfl|hs) := s.eq_empty_or_nonempty
+    (hbdd : BddAbove s) (hlim : ¬ IsSuccPrelimit (sSup s)) : sSup s ∈ s := by
+  obtain rfl | hs := s.eq_empty_or_nonempty
   · simp [isSuccPrelimit_bot] at hlim
   · exact csSup_mem_of_not_isSuccPrelimit hs hbdd hlim
 
@@ -122,24 +117,23 @@ alias csSup_mem_of_not_isSuccLimit' := csSup_mem_of_not_isSuccPrelimit'
 /-- See `exists_eq_ciSup_of_not_isSuccPrelimit` for the
 `ConditionallyCompleteLinearOrder` version. -/
 lemma exists_eq_ciSup_of_not_isSuccPrelimit'
-    (hf : BddAbove (Set.range f)) (hf' : ¬ IsSuccPrelimit (⨆ i, f i)) :
-    ∃ i, f i = ⨆ i, f i :=
+    (hf : BddAbove (range f)) (hf' : ¬ IsSuccPrelimit (⨆ i, f i)) : ∃ i, f i = ⨆ i, f i :=
   csSup_mem_of_not_isSuccPrelimit' hf hf'
 
 @[deprecated exists_eq_ciSup_of_not_isSuccPrelimit' (since := "2024-09-05")]
 alias exists_eq_ciSup_of_not_isSuccLimit' := exists_eq_ciSup_of_not_isSuccPrelimit'
 
-lemma IsLUB.mem_of_not_isSuccPrelimit (hs : IsLUB s x) (hx : ¬ IsSuccPrelimit x) :
-    x ∈ s := by
-  obtain (rfl|hs') := s.eq_empty_or_nonempty
+lemma IsLUB.mem_of_not_isSuccPrelimit (hs : IsLUB s x) (hx : ¬ IsSuccPrelimit x) : x ∈ s := by
+  obtain rfl | hs' := s.eq_empty_or_nonempty
   · simp [show x = ⊥ by simpa using hs, isSuccPrelimit_bot] at hx
   · exact hs.mem_of_nonempty_of_not_isSuccPrelimit hs' hx
 
 @[deprecated IsLUB.mem_of_not_isSuccPrelimit (since := "2024-09-05")]
 alias IsLUB.mem_of_not_isSuccLimit := IsLUB.mem_of_not_isSuccPrelimit
 
-lemma IsLUB.exists_of_not_isSuccPrelimit (hf : IsLUB (Set.range f) x) (hx : ¬ IsSuccPrelimit x) :
-    ∃ i, f i = x := hf.mem_of_not_isSuccPrelimit hx
+lemma IsLUB.exists_of_not_isSuccPrelimit (hf : IsLUB (range f) x) (hx : ¬ IsSuccPrelimit x) :
+    ∃ i, f i = x :=
+  hf.mem_of_not_isSuccPrelimit hx
 
 @[deprecated IsLUB.exists_of_not_isSuccPrelimit (since := "2024-09-05")]
 alias IsLUB.exists_of_not_isSuccLimit := IsLUB.exists_of_not_isSuccPrelimit
@@ -175,17 +169,15 @@ end ConditionallyCompleteLinearOrderBot
 section CompleteLinearOrder
 variable [CompleteLinearOrder α] {s : Set α} {f : ι → α} {x : α}
 
-lemma sSup_mem_of_not_isSuccPrelimit (hlim : ¬ IsSuccPrelimit (sSup s)) :
-    sSup s ∈ s := by
+lemma sSup_mem_of_not_isSuccPrelimit (hlim : ¬ IsSuccPrelimit (sSup s)) : sSup s ∈ s := by
   obtain ⟨y, hy⟩ := not_forall_not.mp hlim
   obtain ⟨i, his, hi⟩ := lt_sSup_iff.mp hy.lt
   exact eq_of_le_of_not_lt (le_sSup his) (hy.2 hi) ▸ his
 
 @[deprecated sSup_mem_of_not_isSuccPrelimit (since := "2024-09-05")]
 alias sSup_mem_of_not_isSuccLimit := sSup_mem_of_not_isSuccPrelimit
 
-lemma sInf_mem_of_not_isPredPrelimit (hlim : ¬ IsPredPrelimit (sInf s)) :
-    sInf s ∈ s := by
+lemma sInf_mem_of_not_isPredPrelimit (hlim : ¬ IsPredPrelimit (sInf s)) : sInf s ∈ s := by
   obtain ⟨y, hy⟩ := not_forall_not.mp hlim
   obtain ⟨i, his, hi⟩ := sInf_lt_iff.mp hy.lt
   exact eq_of_le_of_not_lt (sInf_le his) (hy.2 · hi) ▸ his
@@ -207,15 +199,15 @@ lemma exists_eq_iInf_of_not_isPredPrelimit (hf : ¬ IsPredPrelimit (⨅ i, f i))
 @[deprecated exists_eq_iInf_of_not_isPredPrelimit (since := "2024-09-05")]
 alias exists_eq_iInf_of_not_isPredLimit := exists_eq_iInf_of_not_isPredPrelimit
 
-lemma IsGLB.mem_of_not_isPredPrelimit (hs : IsGLB s x) (hx : ¬ IsPredPrelimit x) :
-    x ∈ s :=
+lemma IsGLB.mem_of_not_isPredPrelimit (hs : IsGLB s x) (hx : ¬ IsPredPrelimit x) : x ∈ s :=
   hs.sInf_eq ▸ sInf_mem_of_not_isPredPrelimit (hs.sInf_eq ▸ hx)
 
 @[deprecated IsGLB.mem_of_not_isPredPrelimit (since := "2024-09-05")]
 alias IsGLB.mem_of_not_isPredLimit := IsGLB.mem_of_not_isPredPrelimit
 
-lemma IsGLB.exists_of_not_isPredPrelimit (hf : IsGLB (Set.range f) x) (hx : ¬ IsPredPrelimit x) :
-    ∃ i, f i = x := hf.mem_of_not_isPredPrelimit hx
+lemma IsGLB.exists_of_not_isPredPrelimit (hf : IsGLB (range f) x) (hx : ¬ IsPredPrelimit x) :
+    ∃ i, f i = x :=
+  hf.mem_of_not_isPredPrelimit hx
 
 @[deprecated IsGLB.exists_of_not_isPredPrelimit (since := "2024-09-05")]
 alias IsGLB.exists_of_not_isPredLimit := IsGLB.exists_of_not_isPredPrelimit