The Feit–Thompson odd order theorem in Lean 4, with the finite group theory library it required — Hall, Fitting, Frobenius groups, transfer, ZJ, Dade isometry, coherence