How to turn an exists_unique into a function?

Stream: new members

[Kent Van Vels]

I am interested in proving a few simple things about the floor and ceiling functions.

In mathlib there is a function/proof that the floor exists called Real.exists_floor.

I have done straightforward task of showing that this floor is unique and now I want to turn this into a function. What follows is minimal working example.

import Mathlib.Tactic

theorem exists_unique_floor (x : ℝ): ∃! ub : ℤ, (ub : ℝ) ≤ x ∧ ∀ z : ℤ, (z : ℝ) ≤ x → z ≤ ub := by
  rcases Real.exists_floor x with ⟨fl,⟨hfl0,hfl1⟩⟩
  use fl
  apply And.intro
  exact ⟨hfl0,hfl1⟩
  intro y ⟨hy0,hy1⟩
  apply le_antisymm (hfl1 y hy0) (hy1 fl hfl0)

--noncomputable?
def myFloor (x : ℝ) : ℤ := by
  sorry
  --choose i using Real.exists_floor x doesn't work
  --what do I do here?

[Matt Diamond]

Just to be clear, you want to use your own lemma here and not the existing integer Floor function (i.e. docs#Int.floor) in mathlib, right?

[Kent Van Vels]

Well... I will use those. But I didn't know about them. :smile:

Even so, I still would like to know if it is possible to turn a "exists_unique" into a function somehow.

[Matt Diamond]

Sure... you can write (exists_unique_floor x).choose and mark the function as noncomputable

[Matt Diamond]

docs#Exists.choose and docs#Exists.choose_spec are available whenever you want to pick a value from an Exists statement

[Kent Van Vels]

Ok. Thank you! I appreciate it and I appreciate the tip on the existing (ha) functions.

[Matt Diamond]

no problem!