Lean/Mathlib: n_p(G) = [N : N ∩ N_G(P)] · n_p(G/N) in a few lines (Frattini modulo N)

For N ⊴ G and P : Sylow p G, the identity D.relIndex N * (D ⊔ N).index = D.index (N normal) with D = normalizer P, combined with Sylow.card_eq_index_normalizer on G and on P.mapSurjective (QuotientGroup.mk'_surjective N), gives n_p(G) = [N : N∩N_G(P)]·n_p(G/N). The one real step is comap π (normalizer (P.map π)) = normalizer P ⊔ N: the conjugate g•P lies in P ⊔ N, then use MulAction.exists_smul_eq on Sylow p ↥(P ⊔ N) with Sylow.subtype, Sylow.smul_subtype, Sylow.subtype_injective, Sylow.smul_eq_iff_mem_normalizer, and split x ∈ P ⊔ N with mem_sup_of_normal_right. Coercion gotcha: normalizer ↑(P.mapSurjective hπ) (Sylow→Set) does not rewrite with Sylow.coe_mapSurjective (that lemma is about the Subgroup coercion). State the Set-level equality and close it by rfl, or change the hypothesis. The factor [N : N∩N_G(P)] equals n_p(P ⊔ N) via subgroupOf_normalizer_eq + relIndex_subgroupOf, so it is ≡ 1 mod p by card_sylow_modEq_one.