How to demonstrate that OrderedAddCommMonoid is a SupSet?

Stream: mathlib4

[张守信(Shouxin Zhang)]

I have been recently studying Filtration, which can have a corresponding valuation. Therefore, I am attempting to define valuation in Lean 4. During this definition process, I encountered a part that is mathematically obvious but somewhat strange in Lean 4, which is what the title refers to. The code is as follows:

noncomputable section temp1
namespace temp1

open BigOperators ENNReal

variable (G : Type*) [Group G]
variable (Λ : Type*)

class GroupFiltration [CanonicallyOrderedAddCommMonoid Λ] where

    orderMap : Λ → Subgroup G

    union_eq_top : (⨆ i > (0 : Λ), orderMap i) = ⊤

    commutator_mem : ∀ (i j : Λ), i > 0 → j > 0 → ∀ x ∈ orderMap i, ∀ y ∈ orderMap j, (x⁻¹ * y⁻¹ * x * y) ∈ orderMap (i + j)

    inter_eq : ∀ (i : Λ), i > 0 → orderMap i = (⨅ j < i, orderMap j)

variable [CanonicallyLinearOrderedAddCommMonoid Λ] (fil : GroupFiltration G ℝ≥0∞) (test : GroupFiltration G (WithTop Λ))

def valuation : G → ℝ≥0∞ := by
    intro x
    let y := {i : ℝ≥0∞ | x ∈ fil.orderMap i}
    let z := sSup y
    use z

instance : SupSet (WithTop Λ) := by
  by_cases h : ∀ b < (⊤ : (WithTop Λ)), ∃ a : (WithTop Λ), b < a
  . refine { sSup := ?_ }
    exact fun _ => (⊤ : (WithTop Λ))
  . simp only [not_forall, Classical.not_imp, not_exists, not_lt] at h
    -- replace h : ∃ x, ∃ (_ : x < ⊤), ∀ (x_1 : WithTop Λ), x_1 ≤ x
    refine { sSup := ?_ }
    exact fun _ => Classical.choose h

def valuation_test : G → WithTop Λ := by
    intro x
    let y := {i : WithTop Λ | x ∈ test.orderMap i}
    let z := sSup y
    use z

end temp1
end temp1

Since sSup requires the precondition of SupSet, I need to start proving it. For ℝ≥0∞, it being a SupSet is automatically established in Lean. Therefore, I believe this also holds true for a general WithTop Λ. In the instance : SupSet (WithTop Λ) here, I used my natural intuition, but I feel this seems too strange. There should be some natural API that can be directly used with exact. What should I do?

[Yaël Dillies]

No, CanonicallyLinearOrderedAddCommMonoid Λ does not imply the existence of arbitrary suprema. Take eg ℚ≥0 and the set s = {q : ℚ≥0 | q ^ 2 < 2}.