Commit 2025-06-18 16:39 6ef9cd80

feat: add simp to lemma Fin.coe_ofNat_eq_mod (#26095) One consequence is that simp can now prove things like this:

example : (3 : Fin 10).val = 3 := by simp
example : (4 : Fin 10).val = 4 := by simp
example : (5 : Fin 10).val = 5 := by simp

previously this only this only worked up to (2 : Fin 10).val = 2 (via lemmas like Fin.val_two).