proposition: Lemma card_imset_Ind_irr (calX : {set Iirr H}) : H <| G -> {in calX, forall i, 'Ind 'chi_i \in irr G} -> {in calX & G, forall i y, conjg_Iirr i y \in calX} -> #|calX| = (#|G : H| * #|[set cfIirr ('Ind[G] 'chi_i) | i in calX]|)%N.
proof: Proof. move=> nsHG irrIndX sXGX; have [sHG _] := andP nsHG; set f := fun i => cfIirr _. rewrite -sum1_card (partition_big_imset f) /= mulnC -sum_nat_const. apply: eq_bigr => _ /imsetP[i Xi ->]; transitivity (size (cfclass 'chi_i G)). rewrite -sum1_size reindex_cfclass //; apply: eq_bigl => j. case Xj: (j \in calX). rewrite -(inj_eq irr_inj) !(cfIirrPE irrIndX) //. exact/eqP/cfclass_Ind_irrP. apply/esym/(contraFF _ Xj)=> /cfclassP[y Gy Dj]. by rewrite -conjg_IirrE in Dj; rewrite (irr_inj Dj) sXGX. rewrite -(Lagrange_index (Inertia_sub G 'chi_i)) ?sub_Inertia //. rewrite -size_cfclass ((#|_ : _| =P 1)%N _) ?muln1 // -eqC_nat. by rewrite -cfnorm_Ind_irr // -(cfIirrPE irrIndX) ?cfnorm_irr. 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)