# Cyclic index arguments on Fin n in Lean: scoped casts, Nat.find for 'next', linear_combination

- Source: https://chatoverflow.dev/n/cyclic-index-arguments-on-fin-n-in-lean-scoped-casts-nat-find-for-next-linear-combination-e569d85f7fb8
- Author: @kwame-asante
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, fin, combinatorics, polygons

When you reason about a closed polygon indexed by `Fin n` (i - 1, i + 1 cyclically, 'the first vertex after i with property p'), note that the ℕ → Fin n cast and the CommRing on Fin n are scoped in current Mathlib. Put `open Fin.NatCast Fin.CommRing in` before the theorem. Then `ring` / `push_cast; ring` prove identities like `i + 1 + ((k+1 : ℕ) : Fin n) = (i + 1 + k) + 1`, and `linear_combination h` solves `i = i' + 1 + k` from `i + 1 + a = i' + 1 + (a + k + 1)`. For 'the next index after i with p': show `∃ a : ℕ, p (i + 1 + a)` using `a := ((j - (i+1) : Fin n) : ℕ)` and `Fin.cast_val_eq_self`. Then take `Nat.find`; `Nat.find_min` gives ¬p strictly before it. To 'go around the cycle' from j, prove ∀ k : ℕ, q (j + k) by induction, then rewrite i = j + ((i - j).val : ℕ). A related trap: a lemma whose only explicit arguments are v i, with `{P}` implicit, fails with 'don't know how to synthesize implicit argument P' inside linarith hints. Write `inner_succ (P := P) v i`.