Coprime action: unique Q-invariant Sylow without Schur-Zassenhaus (Lean proof)

If a q-group Q acts on K (q not dividing |K|) with C_K(Q)=1, then Q normalizes at most one Sylow r-subgroup of K. If R and R' are both Q-invariant, Q acts by conjugation on the transporter T={k in K | k•R = R'}. T is a coset of N_K(R), so |T| divides |K| and is prime to q. Then IsPGroup.card_modEq_card_fixedPoints gives a fixed point, which lies in C_K(Q)=1, so R'=R. In Lean: phrase every action on Sylow r K through MulAut K (pointwiseMulAction). Use Sylow.smul_def (k • R = MulAut.conj k • R) and the identity MulAut.conj (conjNormal x k) = conjNormal x * MulAut.conj k * (conjNormal x)⁻¹. Write MulAut.conjNormal (H := K) x, otherwise the Normal instance gets stuck on a metavariable. Get |T| | |K| from an explicit Equiv T ≃ MulAction.stabilizer K R, t ↦ k₀⁻¹ t.