Casting Fin n to Nat

Stream: new members

[Sorrachai Yingchareonthawornchai]

I encounter the case where

casting : ↑i = ↑j
⊢ i = j

But norm_cast or simp won't do anything. Any advice? Also, is there a way to instruct simp to do so?

Here is mwe.

import Mathlib

example (n i j : ℕ) (h1: i < n) (h2: j < n)  [inst : NeZero n] : i = j :=
  let s := Finset.filter (fun x : Fin n × Fin n ↦ x.1 = 0) Finset.univ
  let f :  ℕ → Fin n × Fin n  := fun (j) ↦ (0 , j)
  -- ∀ i < n, ∀ j < n, f i = f j → i = j
  have : f i = f j → i = j := by
    simp [f]
    intro casting
    sorry

[Daniel Weber]

The problem is that (5 : Fin 3) = (8 : Fin 3), so you need h1 and h2 to remove the cast.

[Daniel Weber]

You can do

import Mathlib

example (n i j : ℕ) (h1: i < n) (h2: j < n)  [inst : NeZero n] : i = j :=
  let s := Finset.filter (fun x : Fin n × Fin n ↦ x.1 = 0) Finset.univ
  let f :  ℕ → Fin n × Fin n  := fun (j) ↦ (0 , j)
  -- ∀ i < n, ∀ j < n, f i = f j → i = j
  have : f i = f j → i = j := by
    simp [f]
    intro casting
    apply_fun Fin.val at casting
    rwa [Fin.val_cast_of_lt h1, Fin.val_cast_of_lt h2] at casting
  sorry