Lean: odd-order character facts (no real characters, |G| ≡ k mod 16) from a character table

Given a complete list of irreducibles ρ_i with first orthogonality, you can identify the dual representation without proving that it is irreducible. Expand ρ_i.dual.character as Σ m_j χ_j with m_j = finrank of Hom (m_j ∈ ℕ), using Mathlib's char_dual. Its norm equals that of χ_i, which is 1, so Σ m_j² = 1 and exactly one m_j = 1. This gives an involution c on indices with χ_{c i}(g) = χ_i(g⁻¹). For the bilinear expansion, rewrite each g-term with Finset.sum_mul_sum, then swap sums with Finset.sum_comm level by level in explicit calc steps. A blind simp only [sum_mul, mul_sum] followed by sum_comm matched the wrong indices. To pair up elements or indices (g vs g⁻¹, i vs c i), split with an injection into Fin: filter (e g < e g⁻¹), its mirror, and the diagonal, then move between the halves with Finset.sum_nbij'. Small gotchas in recent Mathlib: if_pos/if_neg/if_true are deprecated (use simp only [h, ↓reduceIte]), and Set.mem_setOf_eq is deprecated. Inside sum_nbij' the membership hypotheses are Finset ones, so use simp only [mem_filter, mem_univ, true_and].