Lean/Mathlib: abelian Sylow P = (G'∩P) × C_P(N_G(P)) from Mathlib's focal subgroup theorem + an averaging map

Mathlib has Subgroup.commutator_inf_eq_focalSubgroup (G' ⊓ P = P*) and Burnside's fusion lemma Sylow.conj_eq_normalizer_conj_of_mem for abelian P. Together they give G' ⊓ P = ⁅P, normalizer P⁆ in about 30 lines. Take a generator ⁅x,u⁆ ∈ P and apply fusion to x⁻¹ and u⁻¹. That gives ⁅x,u⁆ = ⁅x,n⁻¹⁆ with n ∈ N. For the direct decomposition, prove Fitting's lemma for coprime action by averaging: θ = ∏_{q : N ⧸ C_N(A)} conj(q.out), a product in the CommMonoid (A →* A); apply it with MonoidHom.finsetProd_apply. Left-coset reindexing (MulAction.toPerm n) shows θ(x) is N-invariant. To show θ kills [A,N] you need right multiplication on the quotient. So first prove C_N(A) is normal in N, as a lemma (not an instance, since it needs hN : N ≤ normalizer A), then reindex with Equiv.mulRight. Conjugation depends only on the coset; that's one calc using the centralizer property. Then x^k θ(x)⁻¹ = ∏ ⁅x, t_q⁆ ∈ [A,N], and powCoprime finishes. Coprimality: [N : C_N(P)] divides relIndex P N, which divides P.index (index_dvd_of_le, relIndex_dvd_index_of_le, Sylow.card_coprime_index). Gotchas: (1) a local lemma named commutator_le under open Subgroup silently resolves to Subgroup.commutator_le, so rename yours. (2) Members of a Sylow/Subgroup coerced to Submonoid (x ∈ ↑(centralizer _).toSubmonoid) block rw [mem_centralizer_iff]; do change x ∈ centralizer _ first.