feat(GroupTheory/Perm/ClosureSwap): add slight generalization (#31570)

This PR adds a slight generalization of `surjective_of_isSwap_of_isPretransitive` that is needed to compute the Galois group of `x^n - x  - 1`.

Co-authored-by: tb65536 <thomas.l.browning@gmail.com>

Author: tb65536

Mathlib/GroupTheory/Perm/ClosureSwap.lean

@@ -140,11 +140,21 @@ theorem closure_of_isSwap_of_isPretransitive [Finite α] {S : Set (Perm α)} (hS
     [MulAction.IsPretransitive (Subgroup.closure S) α] : Subgroup.closure S = ⊤ := by
   simp [eq_top_iff', mem_closure_isSwap hS, orbit_eq_univ, Set.toFinite]
 
+/-- A transitive permutation group generated by transpositions must be the whole symmetric group -/
+theorem surjective_of_isSwap_of_isPretransitive' [Finite α] (S : Set G)
+    (hS1 : ∀ σ ∈ S, MulAction.toPermHom G α σ = 1 ∨ Perm.IsSwap (MulAction.toPermHom G α σ))
+    (hS2 : Subgroup.closure S = ⊤) [h : MulAction.IsPretransitive G α] :
+    Function.Surjective (MulAction.toPermHom G α) := by
+  have h : closure ((toPermHom G α '' S) \ {1}) = (toPermHom G α).range := by
+    rw [closure_diff_one, ← MonoidHom.map_closure, hS2, ← MonoidHom.range_eq_map]
+  have := IsPretransitive.of_compHom (α := α) (toPermHom G α).rangeRestrict
+  rw [← h] at this
+  rw [← MonoidHom.range_eq_top, ← h, closure_of_isSwap_of_isPretransitive]
+  rintro - ⟨⟨σ, hσ, rfl⟩, hσ1⟩
+  exact (hS1 σ hσ).resolve_left hσ1
+
 /-- A transitive permutation group generated by transpositions must be the whole symmetric group -/
 theorem surjective_of_isSwap_of_isPretransitive [Finite α] (S : Set G)
     (hS1 : ∀ σ ∈ S, Perm.IsSwap (MulAction.toPermHom G α σ)) (hS2 : Subgroup.closure S = ⊤)
-    [h : MulAction.IsPretransitive G α] : Function.Surjective (MulAction.toPermHom G α) := by
-  rw [← MonoidHom.range_eq_top]
-  have := MulAction.IsPretransitive.of_compHom (α := α) (MulAction.toPermHom G α).rangeRestrict
-  rw [MonoidHom.range_eq_map, ← hS2, MonoidHom.map_closure] at this ⊢
-  exact closure_of_isSwap_of_isPretransitive (Set.forall_mem_image.2 hS1)
+  [h : MulAction.IsPretransitive G α] : Function.Surjective (MulAction.toPermHom G α) :=
+  surjective_of_isSwap_of_isPretransitive' S (fun σ hσ ↦ Or.inr (hS1 σ hσ)) hS2