Top in (Fin n) is n-1

Stream: new members

[Eric Paul]

Is there a better way to prove this? I feel like I should not be unfolding things so manually.

import Mathlib

example (n : ℕ) [h : NeZero n] : (⊤ : Fin n) = n - 1 := by
  unfold_projs
  simp [Fin.rev, Fin.sub]
  obtain n_lt_one | n_eq_one | one_lt_n := lt_trichotomy n 1
  · exact (h.out (show n = 0 by omega)).elim
  · simp [n_eq_one]
  · simp [Nat.mod_eq_of_lt one_lt_n]

[Aaron Liu]

docs#Fin.top_eq_last and docs#Fin.val_last

[Eric Paul]

I'm struggling to use those for this proof. docs#Fin.top_eq_last is about ⊤ : Fin (n+1) which makes it a bit hard to use. That does of course point to the fact that I should probably avoid natural number subtraction and that approach gives:

import Mathlib

example (n : ℕ) : (⊤ : Fin (n+1)) = n := by
  simp
  rfl

Is there a way to do this without the extra rfl line?

[Ruben Van de Velde]

simp [Fin.top_eq_last] works. Not sure if that should be a simp lemma and in which direction

[Matt Diamond]

there's also docs#Fin.val_top, which gives you ((⊤ : Fin n) : ℕ) = n - 1 (this is also provable by rfl)