This happens because the coercion is in an unexpected place: The h here is interpreted as h : ((i.val : Fin 3) / 3).val = i.val / 3, so you get ((6 : Fin 3) / 3).val = (0 / 3).val = 0. On newer versions of Mathlib, the coercion from Nat to Fin is disabled by default to avoid such unintuitive behavior (but you can enable it using open scoped Fin.NatCast).