From dd71334db81d0bd444af1ee339a29298bef40734 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 9 Jan 2023 16:42:09 +0000
Subject: [PATCH] feat(order/partial_sups): add csupr lemmas (#18053)

---
 src/order/partial_sups.lean | 49 ++++++++++++++++++++++++++++---------
 1 file changed, 37 insertions(+), 12 deletions(-)

diff --git a/src/order/partial_sups.lean b/src/order/partial_sups.lean
index fa4a0a5b400b3..41e97ca76bed3 100644
--- a/src/order/partial_sups.lean
+++ b/src/order/partial_sups.lean
@@ -5,13 +5,15 @@ Authors: Scott Morrison
 -/
 import data.finset.lattice
 import order.hom.basic
+import order.conditionally_complete_lattice.finset
 
 /-!
 # The monotone sequence of partial supremums of a sequence
 
 We define `partial_sups : (ℕ → α) → ℕ →o α` inductively. For `f : ℕ → α`, `partial_sups f` is
 the sequence `f 0 `, `f 0 ⊔ f 1`, `f 0 ⊔ f 1 ⊔ f 2`, ... The point of this definition is that
-* it doesn't need a `⨆`, as opposed to `⨆ (i ≤ n), f i`.
+* it doesn't need a `⨆`, as opposed to `⨆ (i ≤ n), f i` (which also means the wrong thing on
+  `conditionally_complete_lattice`s).
 * it doesn't need a `⊥`, as opposed to `(finset.range (n + 1)).sup f`.
 * it avoids needing to prove that `finset.range (n + 1)` is nonempty to use `finset.sup'`.
 
@@ -67,6 +69,17 @@ begin
   { exact sup_le (ih (λ m p, w m (nat.le_succ_of_le p))) (w (n + 1) le_rfl) }
 end
 
+@[simp] lemma bdd_above_range_partial_sups {f : ℕ → α} :
+  bdd_above (set.range (partial_sups f)) ↔ bdd_above (set.range f) :=
+begin
+  apply exists_congr (λ a, _),
+  split,
+  { rintros h b ⟨i, rfl⟩,
+    exact (le_partial_sups _ _).trans (h (set.mem_range_self i)) },
+  { rintros h b ⟨i, rfl⟩,
+    exact (partial_sups_le _ _ _ $ λ _ _, h (set.mem_range_self _)), },
+end
+
 lemma monotone.partial_sups_eq {f : ℕ → α} (hf : monotone f) :
   (partial_sups f : ℕ → α) = f :=
 begin
@@ -132,25 +145,37 @@ begin
     exact ⟨ih (nat.lt_of_succ_lt hmn), h hmn.ne⟩ }
 end
 
+section conditionally_complete_lattice
+variables [conditionally_complete_lattice α]
+
+lemma partial_sups_eq_csupr_Iic (f : ℕ → α) (n : ℕ) : partial_sups f n = ⨆ i : set.Iic n, f i :=
+begin
+  have : set.Iio (n + 1) = set.Iic n := set.ext (λ _, nat.lt_succ_iff),
+  rw [partial_sups_eq_sup'_range, finset.sup'_eq_cSup_image, finset.coe_range,
+    supr, set.range_comp, subtype.range_coe, this],
+end
+
+@[simp] lemma csupr_partial_sups_eq {f : ℕ → α} (h : bdd_above (set.range f)) :
+  (⨆ n, partial_sups f n) = ⨆ n, f n :=
+begin
+  refine (csupr_le $ λ n, _).antisymm (csupr_mono _ $ le_partial_sups f),
+  { rw partial_sups_eq_csupr_Iic,
+    exact csupr_le (λ i, le_csupr h _), },
+  { rwa bdd_above_range_partial_sups },
+end
+
+end conditionally_complete_lattice
+
 section complete_lattice
 variables [complete_lattice α]
 
 lemma partial_sups_eq_bsupr (f : ℕ → α) (n : ℕ) :
   partial_sups f n = ⨆ (i ≤ n), f i :=
-begin
-  rw [partial_sups_eq_sup_range, finset.sup_eq_supr],
-  congr,
-  ext a,
-  exact supr_congr_Prop (by rw [finset.mem_range, nat.lt_succ_iff]) (λ _, rfl),
-end
+by simpa only [supr_subtype] using partial_sups_eq_csupr_Iic f n
 
 @[simp] lemma supr_partial_sups_eq (f : ℕ → α) :
   (⨆ n, partial_sups f n) = ⨆ n, f n :=
-begin
-  refine (supr_le $ λ n, _).antisymm (supr_mono $ le_partial_sups f),
-  rw partial_sups_eq_bsupr,
-  exact supr₂_le_supr _ _,
-end
+csupr_partial_sups_eq $ order_top.bdd_above _
 
 lemma supr_le_supr_of_partial_sups_le_partial_sups {f g : ℕ → α}
   (h : partial_sups f ≤ partial_sups g) :