Using conditions of an if statement in defining a function

Stream: new members

[Aeacus Sheng]

Hi, I'm trying to define a function that behaves like this:

theorem finLt (a : Fin n) (b : ℕ) (h : n ≥ 1): b < a.val → b < n-1 := by omega

def foo  (h: n ≥ 1) (m : Fin n) (x: Fin 2): (Fin (n-1) → Fin 2) → (Fin n → Fin 2) :=
  fun i => fun j =>
    match Nat.lt_trichotomy j.val m.val with
    | Or.inl h1 => i ⟨j.val, finLt m j.val h h1⟩
    | Or.inr (Or.inl h2) => x
    | Or.inr (Or.inr h3) => 0

And I got the following error: tactic 'cases' failed, nested error:
tactic 'induction' failed, recursor 'Or.casesOn' can only eliminate into Prop.

I suppose this suggests that I can only use the h1, h2, h3s to prove Props? Anyway, if I can access the 'if condition' in defining a function then I don't need match: I can simply write

if j.val < m.val then i ⟨j.val, finLt m j.val h 'if condition'⟩ else if ...

Does anyone know if this is possible, and if not, are there other ways to define the function? Thank you!

[Ruben Van de Velde]

if h : ...

[Aeacus Sheng]

Ruben Van de Velde said:

if h : ...

Thank you so much! I couldn't imagine it's so simple lmao

[Ruben Van de Velde]

Simple once you know it :)

[Eric Wieser]

Or docs#ltByCases