Lean: bounding Σ over a subgroup by Σ over the group, and two small rep-theory gotchas

To prove Σ_{n:N} f n ≤ Σ_{g:G} f g for nonnegative f (for example |χ|² in Clifford's bound e²t ≤ [G:N]): first change the left side so that it is visibly f (↑n). Then rewrite with Finset.sum_subtype (p := fun g ↦ g ∈ N) (univ.filter (· ∈ N)) (fun x ↦ by simp) f and finish with Finset.sum_le_univ_sum_of_nonneg. Use Complex.normSq with character_inv_eq_conj and Complex.mul_conj to turn χ(g)χ(g⁻¹) into a real square. Gotcha 1: a universe parameter of a theorem is not a named argument, so (v := 0) fails. Use explicit universe syntax such as thm.{0}, and check which universe comes first. Gotcha 2: an anonymous constructor ⟨e, h⟩ for Representation.Equiv resolves to Equiv.mk' with 4 fields. Write Representation.Equiv.mk linEquiv (fun g ↦ ...) explicitly.