feat(ConditionallyCompleteLattice): ciSup_image, ciSup_or', and other iSup-like lemmas (#15271)

Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>

Author: pechersky

Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

@@ -861,6 +861,94 @@ lemma sup_eq_top_of_top_mem [OrderTop α] (h : ⊤ ∈ s) : sSup s = ⊤ :=
 lemma inf_eq_bot_of_bot_mem [OrderBot α] (h : ⊥ ∈ s) : sInf s = ⊥ :=
   bot_unique <| csInf_le (OrderBot.bddBelow s) h
 
+theorem ciSup_subtype [Nonempty ι] {p : ι → Prop} [Nonempty (Subtype p)] {f : Subtype p → α}
+    (hf : BddAbove (Set.range f)) (hf' : sSup ∅ ≤ iSup f) :
+    iSup f = ⨆ (i) (h : p i), f ⟨i, h⟩ := by
+  classical
+  refine le_antisymm (ciSup_le ?_) ?_
+  · intro ⟨i, h⟩
+    have : f ⟨i, h⟩ = (fun i : ι ↦ ⨆ (h : p i), f ⟨i, h⟩) i := by simp [h]
+    rw [this]
+    refine le_ciSup (f := (fun i : ι ↦ ⨆ (h : p i), f ⟨i, h⟩)) ?_ i
+    simp_rw [ciSup_eq_ite]
+    refine (hf.union (bddAbove_singleton (a := sSup ∅))).mono ?_
+    intro
+    simp only [Set.mem_range, Set.union_singleton, Set.mem_insert_iff, Subtype.exists,
+      forall_exists_index]
+    intro b hb
+    split_ifs at hb
+    · exact Or.inr ⟨_, _, hb⟩
+    · simp_all
+  · refine ciSup_le fun i ↦ ?_
+    simp_rw [ciSup_eq_ite]
+    split_ifs
+    · exact le_ciSup hf ?_
+    · exact hf'
+
+theorem ciInf_subtype [Nonempty ι] {p : ι → Prop} [Nonempty (Subtype p)] {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 → α}
+    (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 → α}
+    (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 : ι → α}
+    (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 : ι → α}
+    (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 : β → α}
+    (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]
+
+theorem csInf_image [Nonempty β] {s : Set β} (hs : s.Nonempty) {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'
+
+lemma ciSup_image {α ι ι' : Type*} [ConditionallyCompleteLattice α] [Nonempty ι] [Nonempty ι']
+    {s : Set ι} (hs : s.Nonempty) {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
+  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
+    refine hg'.trans ?_
+    have : Nonempty s := Set.Nonempty.to_subtype hs
+    refine ciSup_le ?_
+    intro ⟨i, h⟩
+    obtain ⟨t, ht⟩ : ∃ t : f '' s, g t = g (f (Subtype.mk i h)) := by
+      have : f i ∈ f '' s := Set.mem_image_of_mem _ h
+      exact ⟨⟨f i, this⟩, by simp [this]⟩
+    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]
+
+lemma ciInf_image {α ι ι' : Type*} [ConditionallyCompleteLattice α] [Nonempty ι] [Nonempty ι']
+    {s : Set ι} (hs : s.Nonempty) {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'
+
 end ConditionallyCompleteLattice
 
 instance Pi.conditionallyCompleteLattice {ι : Type*} {α : ι → Type*}
@@ -992,7 +1080,7 @@ theorem cbiSup_eq_of_not_forall {p : ι → Prop} {f : Subtype p → α} (hp : 
       · simp [hi]
     · apply sup_le
       · rcases isEmpty_or_nonempty (Subtype p) with hp|hp
-        · simp only [iSup_of_empty']
+        · rw [iSup_of_empty']
           convert le_ciSup B i₀
           simp [hi₀]
         · apply ciSup_le
@@ -1123,6 +1211,14 @@ theorem ciSup_mono' {ι'} {f : ι → α} {g : ι' → α} (hg : BddAbove (range
 theorem csInf_le_csInf' {s t : Set α} (h₁ : t.Nonempty) (h₂ : t ⊆ s) : sInf s ≤ sInf t :=
   csInf_le_csInf (OrderBot.bddBelow s) h₁ h₂
 
+lemma ciSup_or' (p q : Prop) (f : p ∨ q → α) :
+    ⨆ (h : p ∨ q), f h = (⨆ h : p, f (.inl h)) ⊔ ⨆ h : q, f (.inr h) := by
+  by_cases hp : p <;> by_cases hq : q
+  · simp [hp, hq]
+  · simp [hp, hq]
+  · simp [hp, hq]
+  · simp [hp, hq]
+
 end ConditionallyCompleteLinearOrderBot
 
 namespace WithTop