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

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.