add a counterexample to the docstring of ciSup_exists_le

Author: SnirBroshi

Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean

@@ -360,6 +360,8 @@ lemma ciInf_image {ι ι' : Type*} {s : Set ι} {f : ι → ι'} {g : ι' → α
     ⨅ i ∈ (f '' s), g i = ⨅ x ∈ s, g (f x) :=
   ciSup_image (α := αᵒᵈ) hf hg'
 
+/-- Note that equality doesn't always hold, for example for `ι := ℤ, p := (· = 0), f := fun _ ↦ -1`
+the LHS is `-1` but the RHS is `-1 ⊔ sSup ∅ = -1 ⊔ 0 = 0`. -/
 theorem ciSup_exists_le {p : ι → Prop} {f : Exists p → α} : ⨆ ih, f ih ≤ ⨆ (i) (h), f ⟨i, h⟩ := by
   by_cases! h : Exists p
   · have : Nonempty <| Exists p := ⟨h⟩