feat(Order/ConditionallyCompleteLattice): Generalize and add cbiSup/cbiInf theorems (leanprover-community#37526)

Generalize some theorems concerning cbiSup (`⨆ i, ⨆ h : p i, f i h`) by removing superfluous `Nonempty` typeclasses and parameters. It would be nice to also remove the `BoundedAbove` typeclass, but this can only be done with linear orders because junk values of lattices are not currently specified[0].

[0]: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Moving.20.60csSup.60.20junk.20into.20.60ConditionallyCompleteLattice.60/near/583143345

In the absence of that, we provide the theorem `cbiSup_of_not_bddAbove` defining the junk values of `cbiSup` in the linear order case.

Add theorem `cbiSup_id`, showing that `⨆ i ∈ s, i = sSup s`.

Add theorem `cbiSup_eq_of_forall_not` as a counterpart to `cbiSup_eq_of_forall` when the condition is never true, and a corollary `cbiSup_empty` for the obvious empty set case.

Use the new theorems to shorten the proof of `cbiSup_eq_of_not_forall`.

Give proper names to the prime versions of `ciSup_subtype` and `ciInf_subtype`.

Moves:
- `ciSup_subtype'` -> `cbiSup_eq_ciSup_subtype`
- `ciInf_subtype'` -> `cbiInf_eq_ciInf_subtype`
- `ciSup_subtype''` -> `ciSup_subtype_fun`
- `ciInf_subtype''` -> `ciInf_subtype_fun`

Co-authored-by: SabrinaJewson <sejewson@gmail.com>

Author: SabrinaJewson

Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean

@@ -259,9 +259,12 @@ lemma Set.Ici_ciSup [Nonempty ι] {f : ι → α} (hf : BddAbove (range f)) :
     Ici (⨆ i, f i) = ⋂ i, Ici (f i) :=
   Iic_ciInf (α := αᵒᵈ) hf
 
-theorem ciSup_subtype [Nonempty ι] {p : ι → Prop} [Nonempty (Subtype p)] {f : Subtype p → α}
+theorem ciSup_subtype {p : ι → Prop} {f : Subtype p → α}
     (hf : BddAbove (Set.range f)) (hf' : sSup ∅ ≤ iSup f) :
     iSup f = ⨆ (i) (h : p i), f ⟨i, h⟩ := by
+  cases isEmpty_or_nonempty (Subtype p)
+  · rw [iSup_of_empty', cbiSup_eq_of_forall_not fun i h ↦ isEmptyElim (⟨i, h⟩ : Subtype p)]
+  have : Nonempty ι := (nonempty_subtype.mp ‹_›).nonempty
   classical
   refine le_antisymm (ciSup_le ?_) ?_
   · intro ⟨i, h⟩
@@ -277,49 +280,66 @@ theorem ciSup_subtype [Nonempty ι] {p : ι → Prop} [Nonempty (Subtype p)] {f
     · exact le_ciSup hf ?_
     · exact hf'
 
-theorem ciInf_subtype [Nonempty ι] {p : ι → Prop} [Nonempty (Subtype p)] {f : Subtype p → α}
+theorem ciInf_subtype {p : ι → Prop} {f : Subtype p → α}
     (hf : BddBelow (Set.range f)) (hf' : iInf f ≤ sInf ∅) :
     iInf f = ⨅ (i) (h : p i), f ⟨i, h⟩ :=
   ciSup_subtype (α := αᵒᵈ) hf hf'
 
-theorem ciSup_subtype' [Nonempty ι] {p : ι → Prop} [Nonempty (Subtype p)] {f : ∀ i, p i → α}
+theorem cbiSup_eq_ciSup_subtype {p : ι → Prop} {f : ∀ i, p i → α}
     (hf : BddAbove (Set.range (fun i : Subtype p ↦ f i i.prop)))
     (hf' : sSup ∅ ≤ ⨆ (i : Subtype p), f i i.prop) :
     ⨆ (i) (h), f i h = ⨆ x : Subtype p, f x x.property :=
   (ciSup_subtype (f := fun x => f x.val x.property) hf hf').symm
 
-theorem ciInf_subtype' [Nonempty ι] {p : ι → Prop} [Nonempty (Subtype p)] {f : ∀ i, p i → α}
+@[deprecated (since := "2026-04-04")] alias ciSup_subtype' := cbiSup_eq_ciSup_subtype
+
+theorem cbiInf_eq_ciInf_subtype {p : ι → Prop} {f : ∀ i, p i → α}
     (hf : BddBelow (Set.range (fun i : Subtype p ↦ f i i.prop)))
     (hf' : ⨅ (i : Subtype p), f i i.prop ≤ sInf ∅) :
     ⨅ (i) (h), f i h = ⨅ x : Subtype p, f x x.property :=
   (ciInf_subtype (f := fun x => f x.val x.property) hf hf').symm
 
-theorem ciSup_subtype'' {ι} [Nonempty ι] {s : Set ι} (hs : s.Nonempty) {f : ι → α}
+@[deprecated (since := "2026-04-04")] alias ciInf_subtype' := cbiInf_eq_ciInf_subtype
+
+theorem ciSup_subtype_fun {ι} {s : Set ι} {f : ι → α}
     (hf : BddAbove (Set.range fun i : s ↦ f i)) (hf' : sSup ∅ ≤ ⨆ i : s, f i) :
     ⨆ i : s, f i = ⨆ (t : ι) (_ : t ∈ s), f t :=
-  haveI : Nonempty s := Set.Nonempty.to_subtype hs
   ciSup_subtype hf hf'
 
-theorem ciInf_subtype'' {ι} [Nonempty ι] {s : Set ι} (hs : s.Nonempty) {f : ι → α}
+@[deprecated (since := "2026-04-04")] alias ciSup_subtype'' := ciSup_subtype_fun
+
+theorem ciInf_subtype_fun {ι} {s : Set ι} {f : ι → α}
     (hf : BddBelow (Set.range fun i : s ↦ f i)) (hf' : ⨅ i : s, f i ≤ sInf ∅) :
     ⨅ i : s, f i = ⨅ (t : ι) (_ : t ∈ s), f t :=
-  haveI : Nonempty s := Set.Nonempty.to_subtype hs
   ciInf_subtype hf hf'
 
-theorem csSup_image [Nonempty β] {s : Set β} (hs : s.Nonempty) {f : β → α}
+@[deprecated (since := "2026-04-04")] alias ciInf_subtype'' := ciInf_subtype_fun
+
+theorem csSup_image {s : Set β} {f : β → α}
     (hf : BddAbove (Set.range fun i : s ↦ f i)) (hf' : sSup ∅ ≤ ⨆ i : s, f i) :
     sSup (f '' s) = ⨆ a ∈ s, f a := by
-  rw [← ciSup_subtype'' hs hf hf', iSup, Set.image_eq_range]
+  rw [← ciSup_subtype_fun hf hf', iSup, Set.image_eq_range]
 
-theorem csInf_image [Nonempty β] {s : Set β} (hs : s.Nonempty) {f : β → α}
+theorem csInf_image {s : Set β} {f : β → α}
     (hf : BddBelow (Set.range fun i : s ↦ f i)) (hf' : ⨅ i : s, f i ≤ sInf ∅) :
     sInf (f '' s) = ⨅ a ∈ s, f a :=
-  csSup_image (α := αᵒᵈ) hs hf hf'
+  csSup_image (α := αᵒᵈ) hf hf'
+
+theorem cbiSup_id {s : Set α} (hs : BddAbove s) (h : sSup ∅ ≤ sSup s) : ⨆ i ∈ s, i = sSup s := by
+  rw [← csSup_image (Subtype.range_coe ▸ hs), Set.image_id']
+  · convert h
+    rw [← sSup_range, Subtype.range_coe]
 
-lemma ciSup_image {α ι ι' : Type*} [ConditionallyCompleteLattice α] [Nonempty ι] [Nonempty ι']
-    {s : Set ι} (hs : s.Nonempty) {f : ι → ι'} {g : ι' → α}
+theorem cbiInf_id {s : Set α} (hs : BddBelow s) (h : sInf s ≤ sInf ∅) : ⨅ i ∈ s, i = sInf s := by
+  rw [← csInf_image (Subtype.range_coe ▸ hs), Set.image_id']
+  · convert h
+    rw [← sInf_range, Subtype.range_coe]
+
+lemma ciSup_image {ι ι' : Type*} {s : Set ι} {f : ι → ι'} {g : ι' → α}
     (hf : BddAbove (Set.range fun i : s ↦ g (f i))) (hg' : sSup ∅ ≤ ⨆ i : s, g (f i)) :
     ⨆ i ∈ (f '' s), g i = ⨆ x ∈ s, g (f x) := by
+  rcases s.eq_empty_or_nonempty with (rfl | hs)
+  · rw [Set.image_empty, cbiSup_empty, cbiSup_empty]
   have hg : BddAbove (Set.range fun i : f '' s ↦ g i) := by
     simpa [bddAbove_def] using hf
   have hf' : sSup ∅ ≤ ⨆ i : f '' s, g i := by
@@ -333,13 +353,12 @@ lemma ciSup_image {α ι ι' : Type*} [ConditionallyCompleteLattice α] [Nonempt
     rw [← ht]
     refine le_ciSup_set ?_ t.prop
     simpa [bddAbove_def] using hf
-  rw [← csSup_image (by simpa using hs) hg hf', ← csSup_image hs hf hg', ← Set.image_comp, comp_def]
+  rw [← csSup_image hg hf', ← csSup_image hf hg', ← Set.image_comp, comp_def]
 
-lemma ciInf_image {α ι ι' : Type*} [ConditionallyCompleteLattice α] [Nonempty ι] [Nonempty ι']
-    {s : Set ι} (hs : s.Nonempty) {f : ι → ι'} {g : ι' → α}
+lemma ciInf_image {ι ι' : Type*} {s : Set ι} {f : ι → ι'} {g : ι' → α}
     (hf : BddBelow (Set.range fun i : s ↦ g (f i))) (hg' : ⨅ i : s, g (f i) ≤ sInf ∅) :
     ⨅ i ∈ (f '' s), g i = ⨅ x ∈ s, g (f x) :=
-  ciSup_image (α := αᵒᵈ) hs hf hg'
+  ciSup_image (α := αᵒᵈ) hf hg'
 
 end ConditionallyCompleteLattice
 
@@ -368,46 +387,32 @@ theorem ciInf_lt_iff [Nonempty ι] {f : ι → α} (hb : BddBelow (range f)) :
     iInf f < a ↔ ∃ i, f i < a := by
   simpa only [mem_range, exists_exists_eq_and] using csInf_lt_iff hb (range_nonempty _)
 
+theorem cbiSup_of_not_bddAbove {p : ι → Prop} {f : ∀ i, p i → α}
+    (h : ¬BddAbove (range fun i : Subtype p ↦ f i i.prop)) :
+    ⨆ (i : ι), ⨆ (h : p i), f i h = sSup ∅ :=
+  ciSup_of_not_bddAbove fun ⟨u, hu⟩ ↦ h ⟨u, fun _ ⟨x, hx⟩ ↦ hx ▸ hu ⟨x, ciSup_pos x.prop⟩⟩
+
+theorem cbiInf_of_not_bddBelow {p : ι → Prop} {f : ∀ i, p i → α}
+    (h : ¬BddBelow (range fun i : Subtype p ↦ f i i.prop)) :
+    ⨅ (i : ι), ⨅ (h : p i), f i h = sInf ∅ :=
+  ciInf_of_not_bddBelow fun ⟨u, hu⟩ ↦ h ⟨u, fun _ ⟨x, hx⟩ ↦ hx ▸ hu ⟨x, ciInf_pos x.prop⟩⟩
+
 theorem cbiSup_eq_of_not_forall {p : ι → Prop} {f : Subtype p → α} (hp : ¬ (∀ i, p i)) :
     ⨆ (i) (h : p i), f ⟨i, h⟩ = iSup f ⊔ sSup ∅ := by
-  classical
-  rcases not_forall.1 hp with ⟨i₀, hi₀⟩
-  have : Nonempty ι := ⟨i₀⟩
-  simp only [ciSup_eq_ite]
-  by_cases H : BddAbove (range f)
-  · have B : BddAbove (range fun i ↦ if h : p i then f ⟨i, h⟩ else sSup ∅) := by
-      rcases H with ⟨c, hc⟩
-      refine ⟨c ⊔ sSup ∅, ?_⟩
-      rintro - ⟨i, rfl⟩
-      by_cases hi : p i
-      · simp only [hi, dite_true, le_sup_iff, hc (mem_range_self _), true_or]
-      · simp only [hi, dite_false, le_sup_right]
-    apply le_antisymm
-    · apply ciSup_le (fun i ↦ ?_)
-      by_cases hi : p i
-      · simp only [hi, dite_true, le_sup_iff]
-        left
-        exact le_ciSup H _
-      · simp [hi]
-    · apply sup_le
-      · rcases isEmpty_or_nonempty (Subtype p) with hp | hp
-        · rw [iSup_of_empty']
-          convert le_ciSup B i₀
-          simp [hi₀]
-        · apply ciSup_le
-          rintro ⟨i, hi⟩
-          convert le_ciSup B i
-          simp [hi]
-      · convert le_ciSup B i₀
-        simp [hi₀]
-  · have : iSup f = sSup (∅ : Set α) := csSup_of_not_bddAbove H
-    simp only [this, le_refl, sup_of_le_left]
-    apply csSup_of_not_bddAbove
-    contrapose! H
-    apply H.mono
-    rintro - ⟨i, rfl⟩
-    convert mem_range_self i.1
-    simp [i.2]
+  rcases le_or_gt (sSup ∅) (iSup f) with le|gt
+  · rw [max_eq_left le]
+    by_cases bdd : BddAbove (range f)
+    · rw [← ciSup_subtype bdd le]
+    · rw [ciSup_of_not_bddAbove bdd, cbiSup_of_not_bddAbove bdd]
+  have ⟨i, hi⟩ := not_forall.mp hp
+  have : Nonempty ι := ⟨i⟩
+  have bdd : BddAbove (range f) := not_not.mp fun h ↦ gt.ne (ciSup_of_not_bddAbove h)
+  rw [max_eq_right gt.le]
+  refine ciSup_eq_of_forall_le_of_forall_lt_exists_gt (fun j ↦ ?_) ?_
+  · by_cases hj : p j
+    · exact ((ciSup_pos hj).trans_le (le_ciSup bdd ⟨j, hj⟩)).trans gt.le
+    · exact (ciSup_neg hj).le
+  · exact fun w hw ↦ ⟨i, hw.trans_eq (ciSup_neg hi).symm⟩
 
 theorem cbiInf_eq_of_not_forall {p : ι → Prop} {f : Subtype p → α} (hp : ¬ (∀ i, p i)) :
     ⨅ (i) (h : p i), f ⟨i, h⟩ = iInf f ⊓ sInf ∅ :=

Mathlib/Order/ConditionallyCompletePartialOrder/Indexed.lean

@@ -119,6 +119,18 @@ theorem cbiSup_eq_of_forall {p : ι → Prop} {f : Subtype p → α} (hp : ∀ i
   · rintro - ⟨i, rfl⟩
     simp
 
+@[to_dual]
+lemma cbiSup_eq_of_forall_not {p : ι → Prop} {f : ∀ i, p i → α} (hp : ∀ i, ¬p i) :
+    ⨆ (i) (h : p i), f i h = sSup ∅ := by
+  cases isEmpty_or_nonempty ι
+  · rw [iSup_of_empty']
+  · have (i : ι) : IsEmpty (p i) := ⟨hp i⟩
+    simp only [iSup_of_empty', ciSup_const]
+
+@[to_dual]
+theorem cbiSup_empty {f : β → α} : ⨆ i ∈ (∅ : Set β), f i = sSup ∅ :=
+  cbiSup_eq_of_forall_not Set.notMem_empty
+
 /-- Introduction rule to prove that `b` is the supremum of `f`: it suffices to check that `b`
 is larger than `f i` for all `i`, and that this is not the case of any `w<b`.
 See `iSup_eq_of_forall_le_of_forall_lt_exists_gt` for a version in complete lattices. -/

scripts/nolints_prime_decls.txt

@@ -593,8 +593,6 @@ ChartedSpaceCore.open_source'
 CharTwo.neg_eq'
 ciInf_le'
 ciInf_le_of_le'
-ciInf_subtype'
-ciInf_subtype''
 CircleDeg1Lift.tendsto_translation_number'
 CircleDeg1Lift.tendsto_translation_number₀'
 CircleDeg1Lift.translationNumber_conj_eq'
@@ -605,8 +603,6 @@ ciSup_le'
 ciSup_le_iff'
 ciSup_mono'
 ciSup_or'
-ciSup_subtype'
-ciSup_subtype''
 Classical.choose_eq'
 CliffordAlgebra.instAlgebra'
 CliffordAlgebra.star_def'