proposition: Lemma cfResInd_sum_cfclass t : H <| G -> 'Res[H] ('Ind[G] 'chi_t) = #|'I_G['chi_t] : H|%:R *: \sum_(xi <- ('chi_t ^: G)%CF) xi.
proof: Proof. set T := 'I_G['chi_t] => nsHG; have [sHG nHG] := andP nsHG. apply/cfun_inP=> h Hh; rewrite cfResE ?cfIndE // cfunE sum_cfunE. apply: (canLR (mulKf (neq0CG H))). rewrite mulrA -natrM Lagrange ?sub_Inertia //= -/T reindex_cfclass //=. rewrite mulr_sumr [s in _ = s]big_mkcond /= (reindex_inj invg_inj). rewrite (partition_big (conjg_Iirr t) xpredT) //=; apply: eq_bigr => i _. have [[y Gy chi_i] | not_i_t] := cfclassP _ _ _; last first. apply: big1 => z; rewrite groupV => /andP[Gz /eqP def_i]. by case: not_i_t; exists z; rewrite // -def_i conjg_IirrE. rewrite -(card_rcoset _ y) mulr_natl -sumr_const; apply: eq_big => z. rewrite -(inj_eq irr_inj) conjg_IirrE chi_i mem_rcoset inE groupMr ?groupV //. apply: andb_id2l => Gz; rewrite eq_sym (cfConjg_eqE _ nsHG) //. by rewrite mem_rcoset inE groupM ?groupV. rewrite groupV => /andP[Gz /eqP <-]. by rewrite conjg_IirrE cfConjgE ?(subsetP nHG). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop prime order ssralg finset fingroup morphism) mathcomp(perm automorphism quotient action zmodp finalg center commutator) mathcomp(poly cyclic pgroup nilpotent matrix mxalgebra mxrepresentation) mathcomp(vector falgebra fieldext ssrnum algC rat algnum galois) mathcomp(classfun character inertia integral_char vcharacter)