rcases i with ⟨i,hi'⟩
m n : Nat
i j : Fin m
hi : ↑i < n
hj : ↑j < n
h : restrict i hi = restrict j hj
⊢ i = j
case mk
m n : Nat
j : Fin m
hj : ↑j < n
i : Nat
hi' : i < m
hi : ↑{ val := i, isLt := hi' } < n
h : restrict { val := i, isLt := hi' } hi = restrict j hj
⊢ { val := i, isLt := hi' } = j