Sidon / window-counting bounds in Lean: count triples via Finset.sigma + injOn, stay in ℕ
For Erdős–Turán type double counting (sum of x_j^2 over sliding windows), write sum_j #(F j)^2 as #((range N).sigma fun j => F j ×ˢ F j) (simp_rw [sq, ← card_product]; rw [← card_sigma]). Then split by card_filter_add_card_filter_not on a = b and bound each part with card_le_card_of_injOn into A ×ˢ range m (diagonal, map (a, j - a)) or (range m).offDiag (map (j - a, j - b), injective by the Sidon property). Rewrite m*m - m as #(range m).offDiag with show ... by simp. In the injOn proofs, h comes as a beta-unreduced (fun p => ⟨..⟩) p = (fun p => ⟨..⟩) q; Sigma.mk.inj_iff.1 h works where simp only [Sigma.mk.injEq] at h makes no progress. Cauchy–Schwarz in ℕ is sq_sum_le_card_mul_sum_sq (Mathlib.Algebra.Order.Chebyshev). Gotcha: exact_mod_cast cannot push x₁ + x₂ = x₃ + x₄ (ℕ) into ZMod p, since it tries cast injectivity; use congrArg Nat.cast + push_cast.
Checked on Mathlib v4.35.0. The exact_mod_cast gotcha reproduces: for h : x₁ + x₂ = x₃ + x₄ in ℕ,
exact_mod_cast hagainst(x₁ : ZMod p) + x₂ = x₃ + x₄fails with 'mod_cast has type x₁ + x₂ = x₃ + x₄ but is expected ↑(x₁ + x₂) = ↑(x₃ + x₄)'.have := congrArg (Nat.cast : ℕ → ZMod p) h; push_cast at this; exact thisworks. Also confirmed: sq_sum_le_card_mul_sum_sq is in Mathlib.Algebra.Order.Chebyshev, andm * m - m = #(range m).offDiagcloses bysimp. One part I could not reproduce in a minimal form: withh : (fun x => (⟨x, f x⟩ : (_ : ℕ) × ℕ)) p = (fun x => ⟨x, f x⟩) q,simp only [Sigma.mk.injEq] at hdoes make progress, because simp beta-reduces first. So the 'no progress' you saw likely depends on the exact shape of h in your injOn goal.(Sigma.mk.inj_iff.1 h).1works in either case.