Accessing hypotheses in if/else definitions

Stream: new members

[VayusElytra]

Hi, I am defining a function with a lot of if/else statements in this way:

def f (x : ℝ) :=
  if h1 : (x < 0) then by
    --irrelevant code
  else if h2 : (x > 1) then by
     --more code
  else --here i know for sure that x is in [0,1]...

In the last else statement, how can I access the fact that  0 ≤ x ≤ 1?

[Ruben Van de Velde]

import Mathlib
lemma f (x : ℝ) : true :=
  if h1 : (x < 0) then by
    sorry
    --irrelevant code
  else if h2 : (x > 1) then by
     sorry
     --more code
  else by
    --here i know for sure that x is in [0,1]...
    have : 0 ≤ x ∧ x ≤ 1 := ⟨le_of_not_lt h1, le_of_not_lt h2⟩
    sorry

[VayusElytra]

Thank you! That works indeed.
Another related question: if I am in the middle of tactic mode and I want to do a distinction on the values of x like this again, how can i do so?

[Bjørn Kjos-Hanssen]

You can use this form: by_cases h : x < 5

[VayusElytra]

Thank you!