Implementing supremum from proof that a lub exists

Stream: general

[Kevin Fisher]

So, as an exercise for my own self enrichment I'm trying to implement as much of "baby rudin" (the analysis book). I have the following defined, for reference

import Mathlib.Init.Set
import Mathlib.Data.Set.Basic
import Mathlib.Init.Algebra.Order

variable [LinearOrder α]

def upper_bound (b : α) (s : Set α) := ∀ x ∈ s, x ≤ b

def lower_bound (b : α) (s : Set α) := ∀ x ∈ s, b ≤ x

def bounded_above (s : Set α) := ∃ b, upper_bound b s

def bounded_below (s : Set α) := ∃ b, lower_bound b s

def lub (b : α) (s : Set α) :=
  upper_bound b s ∧ (∀ x, x < b → ¬upper_bound x s)

def glb (b : α) (s : Set α) :=
  lower_bound b s ∧ (∀ x, b < x → ¬lower_bound x s)

anyway, I want to define a sup function that obeys the properties of the supremum function, for use in equational theorems involving sup, which are quite common in Rudin. However, I'm having trouble with that, since Exists can only eliminate into Prop, which makes sense, but is somewhat annoying since it prevents what I want. Here is my attempt, for reference

def sup (s : Set α) : (∃ b, lub b s) → α
  | ⟨b, hb⟩ => _

Is there a way to do what I want? Or am I going about this completely wrong?

[Alistair Tucker]

You can use docs4#Exists.choose

[Kevin Buzzard]

In mathlib3, sup is defined for all subsets of \R and returns junk values for subsets that don't have a sup. This makes it much easier to use. It might not be mathematically "normal" but it's a more effective way of implementing the idea within lean's type theory.

[Kevin Fisher]

Thanks for the options, I'll think about it