chore: fix junk value for sInf on WithTop (#13717)

As pointed out in https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Definition.20of.20.60WithTop.2EinstInfSet.60/near/443609808, the current choice of junk value for `sInf s` when `s : Set (WithTop α)` is not bounded below does not coincide with `sInf ∅`. This makes it impossible to get a `ConditionallyCompleteLinearOrder` structure on `WithTop α` as we require the junk values to coincide.

This PR fixes the choice of junk value for  `sInf s` when `s : Set (WithTop α)` is not bounded below, making it equal to `⊤ = sInf ∅`.

Author: sgouezel

Mathlib/Data/ENNReal/Basic.lean

@@ -753,8 +753,8 @@ theorem coe_sSup {s : Set ℝ≥0} : BddAbove s → (↑(sSup s) : ℝ≥0∞) =
   WithTop.coe_sSup
 #align ennreal.coe_Sup ENNReal.coe_sSup
 
-theorem coe_sInf {s : Set ℝ≥0} : s.Nonempty → (↑(sInf s) : ℝ≥0∞) = ⨅ a ∈ s, ↑a :=
-  WithTop.coe_sInf
+theorem coe_sInf {s : Set ℝ≥0} (hs : s.Nonempty) : (↑(sInf s) : ℝ≥0∞) = ⨅ a ∈ s, ↑a :=
+  WithTop.coe_sInf hs (OrderBot.bddBelow s)
 #align ennreal.coe_Inf ENNReal.coe_sInf
 
 theorem coe_iSup {ι : Sort*} {f : ι → ℝ≥0} (hf : BddAbove (range f)) :
@@ -764,7 +764,7 @@ theorem coe_iSup {ι : Sort*} {f : ι → ℝ≥0} (hf : BddAbove (range f)) :
 
 @[norm_cast]
 theorem coe_iInf {ι : Sort*} [Nonempty ι] (f : ι → ℝ≥0) : (↑(iInf f) : ℝ≥0∞) = ⨅ a, ↑(f a) :=
-  WithTop.coe_iInf f
+  WithTop.coe_iInf (OrderBot.bddBelow _)
 #align ennreal.coe_infi ENNReal.coe_iInf
 
 theorem coe_mem_upperBounds {s : Set ℝ≥0} :

Mathlib/Data/ENat/Lattice.lean

@@ -36,8 +36,13 @@ lemma iInf_coe_ne_top : ⨅ i, (f i : ℕ∞) ≠ ⊤ ↔ Nonempty ι := by
 lemma iInf_coe_lt_top : ⨅ i, (f i : ℕ∞) < ⊤ ↔ Nonempty ι := WithTop.iInf_coe_lt_top
 
 lemma coe_sSup : BddAbove s → ↑(sSup s) = ⨆ a ∈ s, (a : ℕ∞) := WithTop.coe_sSup
-lemma coe_sInf : s.Nonempty → ↑(sInf s) = ⨅ a ∈ s, (a : ℕ∞) := WithTop.coe_sInf
+
+lemma coe_sInf (hs : s.Nonempty) : ↑(sInf s) = ⨅ a ∈ s, (a : ℕ∞) :=
+  WithTop.coe_sInf hs (OrderBot.bddBelow s)
+
 lemma coe_iSup : BddAbove (range f) → ↑(⨆ i, f i) = ⨆ i, (f i : ℕ∞) := WithTop.coe_iSup _
-@[norm_cast] lemma coe_iInf [Nonempty ι] : ↑(⨅ i, f i) = ⨅ i, (f i : ℕ∞) := WithTop.coe_iInf _
+
+@[norm_cast] lemma coe_iInf [Nonempty ι] : ↑(⨅ i, f i) = ⨅ i, (f i : ℕ∞) :=
+  WithTop.coe_iInf (OrderBot.bddBelow _)
 
 end ENat

Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

@@ -42,74 +42,78 @@ section
 Extension of `sSup` and `sInf` from a preorder `α` to `WithTop α` and `WithBot α`
 -/
 
+variable [Preorder α]
 
 open scoped Classical
 
-noncomputable instance WithTop.instSupSet {α : Type*} [Preorder α] [SupSet α] :
+noncomputable instance WithTop.instSupSet [SupSet α] :
     SupSet (WithTop α) :=
   ⟨fun S =>
     if ⊤ ∈ S then ⊤ else if BddAbove ((fun (a : α) ↦ ↑a) ⁻¹' S : Set α) then
       ↑(sSup ((fun (a : α) ↦ (a : WithTop α)) ⁻¹' S : Set α)) else ⊤⟩
 
-noncomputable instance WithTop.instInfSet {α : Type*} [InfSet α] : InfSet (WithTop α) :=
-  ⟨fun S => if S ⊆ {⊤} then ⊤ else ↑(sInf ((fun (a : α) ↦ ↑a) ⁻¹' S : Set α))⟩
+noncomputable instance WithTop.instInfSet [InfSet α] : InfSet (WithTop α) :=
+  ⟨fun S => if S ⊆ {⊤} ∨ ¬BddBelow S then ⊤ else ↑(sInf ((fun (a : α) ↦ ↑a) ⁻¹' S : Set α))⟩
 
-noncomputable instance WithBot.instSupSet {α : Type*} [SupSet α] : SupSet (WithBot α) :=
+noncomputable instance WithBot.instSupSet [SupSet α] : SupSet (WithBot α) :=
   ⟨(WithTop.instInfSet (α := αᵒᵈ)).sInf⟩
 
-noncomputable instance WithBot.instInfSet {α : Type*} [Preorder α] [InfSet α] :
+noncomputable instance WithBot.instInfSet [InfSet α] :
     InfSet (WithBot α) :=
   ⟨(WithTop.instSupSet (α := αᵒᵈ)).sSup⟩
 
-theorem WithTop.sSup_eq [Preorder α] [SupSet α] {s : Set (WithTop α)} (hs : ⊤ ∉ s)
+theorem WithTop.sSup_eq [SupSet α] {s : Set (WithTop α)} (hs : ⊤ ∉ s)
     (hs' : BddAbove ((↑) ⁻¹' s : Set α)) : sSup s = ↑(sSup ((↑) ⁻¹' s) : α) :=
   (if_neg hs).trans <| if_pos hs'
 #align with_top.Sup_eq WithTop.sSup_eq
 
-theorem WithTop.sInf_eq [InfSet α] {s : Set (WithTop α)} (hs : ¬s ⊆ {⊤}) :
+theorem WithTop.sInf_eq [InfSet α] {s : Set (WithTop α)} (hs : ¬s ⊆ {⊤}) (h's : BddBelow s) :
     sInf s = ↑(sInf ((↑) ⁻¹' s) : α) :=
-  if_neg hs
+  if_neg <| by simp [hs, h's]
 #align with_top.Inf_eq WithTop.sInf_eq
 
-theorem WithBot.sInf_eq [Preorder α] [InfSet α] {s : Set (WithBot α)} (hs : ⊥ ∉ s)
+theorem WithBot.sInf_eq [InfSet α] {s : Set (WithBot α)} (hs : ⊥ ∉ s)
     (hs' : BddBelow ((↑) ⁻¹' s : Set α)) : sInf s = ↑(sInf ((↑) ⁻¹' s) : α) :=
   (if_neg hs).trans <| if_pos hs'
 #align with_bot.Inf_eq WithBot.sInf_eq
 
-theorem WithBot.sSup_eq [SupSet α] {s : Set (WithBot α)} (hs : ¬s ⊆ {⊥}) :
+theorem WithBot.sSup_eq [SupSet α] {s : Set (WithBot α)} (hs : ¬s ⊆ {⊥}) (h's : BddAbove s) :
     sSup s = ↑(sSup ((↑) ⁻¹' s) : α) :=
-  if_neg hs
+  WithTop.sInf_eq (α := αᵒᵈ) hs h's
 #align with_bot.Sup_eq WithBot.sSup_eq
 
 @[simp]
-theorem WithTop.sInf_empty {α : Type*} [InfSet α] : sInf (∅ : Set (WithTop α)) = ⊤ :=
-  if_pos <| Set.empty_subset _
+theorem WithTop.sInf_empty [InfSet α] : sInf (∅ : Set (WithTop α)) = ⊤ :=
+  if_pos <| by simp
 #align with_top.cInf_empty WithTop.sInf_empty
 
 @[simp]
-theorem WithTop.iInf_empty {α : Type*} [IsEmpty ι] [InfSet α] (f : ι → WithTop α) :
+theorem WithTop.iInf_empty [IsEmpty ι] [InfSet α] (f : ι → WithTop α) :
     ⨅ i, f i = ⊤ := by rw [iInf, range_eq_empty, WithTop.sInf_empty]
 #align with_top.cinfi_empty WithTop.iInf_empty
 
-theorem WithTop.coe_sInf' [InfSet α] {s : Set α} (hs : s.Nonempty) :
+theorem WithTop.coe_sInf' [InfSet α] {s : Set α} (hs : s.Nonempty) (h's : BddBelow s) :
     ↑(sInf s) = (sInf ((fun (a : α) ↦ ↑a) '' s) : WithTop α) := by
   obtain ⟨x, hx⟩ := hs
   change _ = ite _ _ _
   split_ifs with h
-  · cases h (mem_image_of_mem _ hx)
+  · rcases h with h1 | h2
+    · cases h1 (mem_image_of_mem _ hx)
+    · exact (h2 (Monotone.map_bddBelow coe_mono h's)).elim
   · rw [preimage_image_eq]
     exact Option.some_injective _
 #align with_top.coe_Inf' WithTop.coe_sInf'
 
 -- Porting note: the mathlib3 proof uses `range_comp` in the opposite direction and
 -- does not need `rfl`.
 @[norm_cast]
-theorem WithTop.coe_iInf [Nonempty ι] [InfSet α] (f : ι → α) :
+theorem WithTop.coe_iInf [Nonempty ι] [InfSet α] {f : ι → α} (hf : BddBelow (range f)) :
     ↑(⨅ i, f i) = (⨅ i, f i : WithTop α) := by
-  rw [iInf, iInf, WithTop.coe_sInf' (range_nonempty f), ← range_comp]; rfl
+  rw [iInf, iInf, WithTop.coe_sInf' (range_nonempty f) hf, ← range_comp]
+  rfl
 #align with_top.coe_infi WithTop.coe_iInf
 
-theorem WithTop.coe_sSup' [Preorder α] [SupSet α] {s : Set α} (hs : BddAbove s) :
+theorem WithTop.coe_sSup' [SupSet α] {s : Set α} (hs : BddAbove s) :
     ↑(sSup s) = (sSup ((fun (a : α) ↦ ↑a) '' s) : WithTop α) := by
   change _ = ite _ _ _
   rw [if_neg, preimage_image_eq, if_pos hs]
@@ -120,42 +124,44 @@ theorem WithTop.coe_sSup' [Preorder α] [SupSet α] {s : Set α} (hs : BddAbove
 -- Porting note: the mathlib3 proof uses `range_comp` in the opposite direction and
 -- does not need `rfl`.
 @[norm_cast]
-theorem WithTop.coe_iSup [Preorder α] [SupSet α] (f : ι → α) (h : BddAbove (Set.range f)) :
+theorem WithTop.coe_iSup [SupSet α] (f : ι → α) (h : BddAbove (Set.range f)) :
     ↑(⨆ i, f i) = (⨆ i, f i : WithTop α) := by
     rw [iSup, iSup, WithTop.coe_sSup' h, ← range_comp]; rfl
 #align with_top.coe_supr WithTop.coe_iSup
 
 @[simp]
-theorem WithBot.csSup_empty {α : Type*} [SupSet α] : sSup (∅ : Set (WithBot α)) = ⊥ :=
-  if_pos <| Set.empty_subset _
-#align with_bot.cSup_empty WithBot.csSup_empty
+theorem WithBot.sSup_empty [SupSet α] : sSup (∅ : Set (WithBot α)) = ⊥ :=
+  WithTop.sInf_empty (α := αᵒᵈ)
+#align with_bot.cSup_empty WithBot.sSup_empty
+
+@[deprecated (since := "2024-06-10")] alias WithBot.csSup_empty := WithBot.sSup_empty
 
 @[simp]
-theorem WithBot.ciSup_empty {α : Type*} [IsEmpty ι] [SupSet α] (f : ι → WithBot α) :
+theorem WithBot.ciSup_empty [IsEmpty ι] [SupSet α] (f : ι → WithBot α) :
     ⨆ i, f i = ⊥ :=
   WithTop.iInf_empty (α := αᵒᵈ) _
 #align with_bot.csupr_empty WithBot.ciSup_empty
 
 @[norm_cast]
-theorem WithBot.coe_sSup' [SupSet α] {s : Set α} (hs : s.Nonempty) :
+theorem WithBot.coe_sSup' [SupSet α] {s : Set α} (hs : s.Nonempty) (h's : BddAbove s) :
     ↑(sSup s) = (sSup ((fun (a : α) ↦ ↑a) '' s) : WithBot α) :=
-  WithTop.coe_sInf' (α := αᵒᵈ) hs
+  WithTop.coe_sInf' (α := αᵒᵈ) hs h's
 #align with_bot.coe_Sup' WithBot.coe_sSup'
 
 @[norm_cast]
-theorem WithBot.coe_iSup [Nonempty ι] [SupSet α] (f : ι → α) :
+theorem WithBot.coe_iSup [Nonempty ι] [SupSet α] {f : ι → α} (hf : BddAbove (range f)) :
     ↑(⨆ i, f i) = (⨆ i, f i : WithBot α) :=
-  WithTop.coe_iInf (α := αᵒᵈ) _
+  WithTop.coe_iInf (α := αᵒᵈ) hf
 #align with_bot.coe_supr WithBot.coe_iSup
 
 @[norm_cast]
-theorem WithBot.coe_sInf' [Preorder α] [InfSet α] {s : Set α} (hs : BddBelow s) :
+theorem WithBot.coe_sInf' [InfSet α] {s : Set α} (hs : BddBelow s) :
     ↑(sInf s) = (sInf ((fun (a : α) ↦ ↑a) '' s) : WithBot α) :=
   WithTop.coe_sSup' (α := αᵒᵈ) hs
 #align with_bot.coe_Inf' WithBot.coe_sInf'
 
 @[norm_cast]
-theorem WithBot.coe_iInf [Preorder α] [InfSet α] (f : ι → α) (h : BddBelow (Set.range f)) :
+theorem WithBot.coe_iInf [InfSet α] (f : ι → α) (h : BddBelow (Set.range f)) :
     ↑(⨅ i, f i) = (⨅ i, f i : WithBot α) :=
   WithTop.coe_iSup (α := αᵒᵈ) _ h
 #align with_bot.coe_infi WithBot.coe_iInf
@@ -1335,6 +1341,7 @@ theorem isGLB_sInf' {β : Type*} [ConditionallyCompleteLattice β] {s : Set (Wit
     (hs : BddBelow s) : IsGLB s (sInf s) := by
   constructor
   · show ite _ _ _ ∈ _
+    simp only [hs, not_true_eq_false, or_false]
     split_ifs with h
     · intro a ha
       exact top_le_iff.2 (Set.mem_singleton_iff.1 (h ha))
@@ -1351,6 +1358,7 @@ theorem isGLB_sInf' {β : Type*} [ConditionallyCompleteLattice β] {s : Set (Wit
       intro c hc
       exact coe_le_coe.1 (hb hc)
   · show ite _ _ _ ∈ _
+    simp only [hs, not_true_eq_false, or_false]
     split_ifs with h
     · intro _ _
       exact le_top
@@ -1397,8 +1405,9 @@ theorem coe_sSup {s : Set α} (hb : BddAbove s) : ↑(sSup s) = (⨆ a ∈ s, 
 
 /-- A version of `WithTop.coe_sInf'` with a more convenient but less general statement. -/
 @[norm_cast]
-theorem coe_sInf {s : Set α} (hs : s.Nonempty) : ↑(sInf s) = (⨅ a ∈ s, ↑a : WithTop α) := by
-  rw [coe_sInf' hs, sInf_image]
+theorem coe_sInf {s : Set α} (hs : s.Nonempty) (h's : BddBelow s) :
+    ↑(sInf s) = (⨅ a ∈ s, ↑a : WithTop α) := by
+  rw [coe_sInf' hs h's, sInf_image]
 #align with_top.coe_Inf WithTop.coe_sInf
 
 end WithTop
@@ -1658,7 +1667,7 @@ noncomputable instance WithTop.WithBot.completeLattice {α : Type*}
           -- Porting note: previous proof relied on convert unfolding
           -- the definition of ⊥
           apply congr_arg
-          simp only [h, preimage_empty, WithBot.csSup_empty]
+          simp only [h, preimage_empty, WithBot.sSup_empty]
         · exfalso
           apply h₂
           use ⊥
@@ -1667,6 +1676,7 @@ noncomputable instance WithTop.WithBot.completeLattice {α : Type*}
       · exact (WithTop.isLUB_sSup' h).2 ha
     sInf_le := fun S a haS =>
       show ite _ _ _ ≤ a by
+        simp only [OrderBot.bddBelow, not_true_eq_false, or_false]
         split_ifs with h₁
         · cases' a with a
           · exact le_rfl