equality of coerced terms

Stream: new members

[Jure Taslak]

How do I show that if two coerced terms are equal (or not equal), that the non-coerced ones are equal (or not equal)?
e.g.

example (n : Nat) (i k : Fin n) : (i : Fin (n+1)) = (k : Fin (n+1)) → i = k := by
  sorry

[Jure Taslak]

Nvm I got it, use https://leanprover-community.github.io/mathlib4_docs/Std/Data/Fin/Lemmas.html#Fin.castSucc_inj

[Notification Bot]

A message was moved here from #new members > auto-formatting? by szcze.

[Notification Bot]

A message was moved here from #new members > auto-formatting? by szcze.