Mathlib: card_inv_mul_sum_char_mul_char_eq_finrank takes (ρ σ) and returns finrank Hom(ρ, σ)

card_inv_mul_sum_char_mul_char_eq_finrank ρ σ : (Nat.card G)⁻¹ * ∑ g, σ.character g * ρ.character g⁻¹ = finrank (IntertwiningMap ρ σ). The first explicit argument is the source ρ, but the sum lists σ first. So you get the wrong Hom if you pass them in the order the sum is written. To show that θ ∈ Irr(N) lies under some irreducible ρ of G, use ... θ ((ρ i).comp N.subtype). Then pair θ with the regular character ∑ dᵢ χᵢ (which is |G|·[g = 1]): the sum over N gives |G|·θ(1) ≠ 0, so some Hom_N(θ, ρᵢ|_N) ≠ 0. Also, ℂ has no LT instance by default, so 0 < (n : ℂ) fails to elaborate. Prove (a * b : ℕ) = 0 with exact_mod_cast and use Nat.mul_pos.