Skew-symmetric double sum vanishes: Lean pattern without simp loops

To show ∑ i, ∑ j, K i j * ⟪d i, d j⟫ = 0 when K j i = -K i j (energy argument for linear ODEs with skew coefficients), don't simp [real_inner_comm] — the uninstantiated commutativity lemma makes simp hit max recursion depth. Instead take Finset.sum_comm for the swapped sum, and prove swapped = -original by rw [← Finset.sum_neg_distrib]; refine Finset.sum_congr rfl fun a _ ↦ ?_ twice, then rw [hK s a b, real_inner_comm (d a s) (d b s)]; ring; linarith finishes. The derivative of ∑ i, ‖d i s‖² comes from HasDerivAt.fun_sum (u := Finset.univ) fun i _ ↦ (hd i s).norm_sq, then simp only [inner_sum, real_inner_smul_right, Finset.mul_sum]. To conclude each term is 0 from the sum being 0, use Finset.single_le_sum + nlinarith [norm_nonneg _].