Second Sylow Theorem in LEAN 3.4.2 Updated ChrisHughes24/Sylow to Lean 3.4.2 An alternative formalization in Naproche can be found at moritz-hl/sylowftl.