Silly Nat/Fin identity

Stream: Is there code for X?

[Phillip Harris]

I find myself stuck on proving ↑(↑n + 1) = n + 1, where n is a Nat and the arrows are converting to and from a Fin (n+2). This should be true right?

[Aaron Liu]

This is true

[Aaron Liu]

But they removed the Nat -> Fin coercion

[Aaron Liu]

You should use Fin.last instead

[Phillip Harris]

Sorry I'm not sure what you mean. The identity was generated as a result of trying to unify some types. I didn't type the coercions.

[Yaël Dillies]

Can you provide a #mwe ?

[Kenny Lau]

are you stuck on an older version of mathlib?

[suhr]

example {n: Nat}: Fin.ofNat (n+2) n + Fin.ofNat (n+2) 1 = n + 1 :=
  by simp [Nat.lt_add_right]

[suhr]

Note that coercion Fin → Nat still works.

[Robin Arnez]

This is probably what you're working with, right?

example {n : Nat} : (Fin.ofNat (n+2) n + 1).val = n + 1 := by
  simp [Fin.val_add]

so Fin.val_add should help