val_cast_of_lt

Stream: mathlib4

[Enrico Borba]

Why in val_cast_of_lt is [NeZero n] needed?

theorem val_cast_of_lt {n : ℕ} [NeZero n] {a : ℕ} (h : a < n) : (a : Fin n).val = a :=
  Nat.mod_eq_of_lt h

I can see that if I remove it, there is an error on (a : Fin n), however isn't NeZero n implied by a < n? Is there no way to craft this instance in the signature of this theorem?

[Enrico Borba]

Whoops, meant to post this in #mathlib4

[Ruben Van de Velde]

import Mathlib
open Nat
theorem val_cast_of_lt {n : ℕ} {a : ℕ} (h : a < n) : have : NeZero n := ⟨(pos_of_gt h).ne'⟩; (a : Fin n).val = a :=
  Nat.mod_eq_of_lt h

Not sure that's better

[Enrico Borba]

I see. It's not visually better, but it's nice to not have it require the instance when using val_cast_of_lt.

[Notification Bot]

This topic was moved here from #lean4 > val_cast_of_lt by Eric Wieser.