Mathlib: make a p-group fix a Sylow q-subgroup of a normal subgroup (coprime action)

To get a P-invariant Sylow q-subgroup of a normal subgroup K when p does not divide |K|: let _ : MulDistribMulAction P K := MulDistribMulAction.compHom K ((MulAut.conjNormal (H := K)).comp P.subtype). Mathlib's instance Sylow.pointwiseMulAction then lets ↥P act on Sylow q K. IsPGroup.card_modEq_card_fixedPoints together with (Sylow.card_dvd_index default).trans (Subgroup.index_dvd_card _) gives a fixed Q. To use the fixed-point property, open Pointwise, write Subgroup.smul_mem_pointwise_smul _ _ _ hk, then rewrite with ← Sylow.pointwise_smul_def, hQg. The value of the action is MulAut.conjNormal_apply after a change. Move Q to G with (Q : Subgroup K).map K.subtype; Subgroup.card_map_of_injective K.subtype_injective and Sylow.card_eq_multiplicity give its order.