Using the equalities produced by the `cases` tactic

Stream: general

[Ayhon]

I have the following proposition I want to prove

example(x n: Nat): 0 < x -> x < n -> (x-1) < n

My strategy for the proof is the following: destruct x, show that x cannot be zero since 0 < x would lead to a contradiction, and that if x is the successor of x', then x' + 1 < n implies x' < n.

The problem is that I don't have this proof as a separate definition, but it's instead nested inside another one, using have. For instance, consider the following

example(n: Nat)(idx: Fin n): Option (Fin n) :=
  let x := idx.1
  if h : 0 < x then
    have isLt : (x-1) < n := by
      cases x with
      | zero => sorry
      | succ x' => sorry
    some $ ⟨x-1, isLt⟩
  else none

When I use cases to destructure x, some references of x in my hypothesis are left unsubstituted.

case zero
n : Nat
idx : Fin n
x : Nat := ↑idx
h : 0 < x
⊢ 0 - 1 < n

It seems to happen because I defined x to be idx.1. If I obtain x by destructuring idx, the substitution happens correctly. I would like to know if there is a way to obtain a h: x = 0 from the cases tactic so that I'm able to fix the proof state on my own, and more generaly if anyone has further insight into why this is happening, and if I should prefer some way of doing proofs in order to avoid these kinds of problems.

I know that for this example in particular I could use Nat.sub_lt to finish the proof directly, but this was more of an example of this kind of problem. I annecdotically remember hitting it some other time in a different context.

[Ayhon]

It seems like my original question has already been answered by #general > Explicit name for prop `x = (a,b)` in `match ... | x@(a,b)` @ 💬. I'd still be interested in knowing a bit more about best-practices and why this happens, but otherwise we could consider the topic as resolved