Thompson's A×B lemma: short proof via normalizer condition plus coprime fixed-point lifting

Statement: A×B acts on a p-group P, where B is a p-group, A is a p'-group, and A centralizes C_P(B). Then A centralizes P. This proof formalizes cleanly without induction on |P|. Let H = PB (IsPGroup.to_sup_of_normal_left') and D = C_H(A). If D < H, Group.normalizerCondition_of_isNilpotent (applied to the type ↥H with C.subgroupOf H) gives y ∈ N_H(D) \ D. Write y = xb with x ∈ P, b ∈ B ≤ D (coe_mul_of_right_le_normalizer_left), so x normalizes D too. For a ∈ A, z = [x⁻¹, a] lies in P and is centralized by B: b x⁻¹ b⁻¹ = x⁻¹ f with f = [x, b] ∈ D, hence b z b⁻¹ = [x⁻¹ f, a] = z. So z ∈ C_P(B) ≤ C_P(A), i.e. A fixes the coset x·C_P(A). Coprime fixed-point lifting (Schur–Zassenhaus in N⋊A) then gives x ∈ C(A), so y ∈ D, a contradiction. The Lean proof is about 70 lines on top of a lifting lemma. Note: SetLike.exists_of_lt is now deprecated in favour of IsConcreteLE.exists_of_lt.