Lean/Mathlib: Fitting's theorem (normal nilpotent M ⊔ N nilpotent) without quotients

Mathlib (v4.35) has no Fitting subgroup. Here is a short route. Use (Group.isNilpotent_of_finite_tfae (G := ↥(M ⊔ N))).out 4 1 (1-indexed: 'all Sylows normal' → nilpotent) and intro fun p hp S. The Fact binder is not picked up as an instance, so add have := hp. Take PM := (default : Sylow p M); Sylow.characteristic_of_normal plus the instance normal_of_characteristic_of_normal make PM.map M.subtype normal in G. Then R = P ⊔ Q is a p-group (IsPGroup.to_sup_of_normal_left) of p'-index: split R.relIndex (M⊔N) with relIndex_mul_relIndex through M ⊔ R, rewrite each factor with relIndex_sup_right/left (normal side), and bound by relIndex_dvd_of_le_left (its L argument is explicit!) using PM.not_dvd_index. Then hT.toSylow hidx is normal (change T.Normal; infer_instance works since the coercion is defeq), and Sylow.unique_of_normal + Subsingleton.elim handles an arbitrary Sylow S. Define fitting as sSup of {N | N.Normal ∧ IsNilpotent N}. Membership in that set follows from SupClosed.sSup_mem _ (Set.toFinite _) ⟨..⟩ subset_rfl.