more adjustments

Author: AntoineChambert-Loir

Mathlib/GroupTheory/SpecificGroups/Alternating.lean

@@ -155,7 +155,35 @@ theorem isCyclic_of_card_le_three (hα : Nat.card α ≤ 3) :
 
 theorem isMulCommutative_of_card_le_three (hα : Nat.card α ≤ 3) :
     IsMulCommutative (alternatingGroup α) :=
-  ⟨(isCyclic_of_card_le_three hα).commutative⟩
+  (isCyclic_of_card_le_three hα).isMulCommutative
+
+theorem isMulCommutative_iff_card_le_three :
+    IsMulCommutative (alternatingGroup α) ↔ Nat.card α ≤ 3 := by
+  refine ⟨fun ⟨⟨H⟩⟩ ↦ ?_, fun h ↦ (isCyclic_of_card_le_three h).isMulCommutative⟩
+  rw [← not_lt, ← Set.ncard_univ, Set.three_lt_ncard_iff]
+  push Not
+  intro a b c d _ _ _ _ hab hac had hbc hbd
+  by_contra hcd
+  apply Ne.symm hcd
+  let g : alternatingGroup α := ⟨swap a b * swap a c, by
+    rw [mem_alternatingGroup]
+    exact (isThreeCycle_swap_mul_swap_same hab hac hbc).sign⟩
+  let h : alternatingGroup α := ⟨swap a b * swap a d, by
+    rw [mem_alternatingGroup]
+    exact (isThreeCycle_swap_mul_swap_same hab had hbd).sign⟩
+  specialize H g h
+  simp only [MulMemClass.mk_mul_mk, Subtype.mk.injEq, Perm.ext_iff, Perm.coe_mul,
+    Function.comp_apply, EmbeddingLike.apply_eq_iff_eq, g, h] at H
+  simpa only [swap_apply_left,
+    swap_apply_of_ne_of_ne (Ne.symm had) (Ne.symm hbd),
+    swap_apply_of_ne_of_ne (Ne.symm hac) (Ne.symm hbc),
+    swap_apply_of_ne_of_ne (Ne.symm hac) hcd,
+    swap_apply_of_ne_of_ne (Ne.symm had) (Ne.symm hcd)] using H a
+
+theorem isCyclic_iff_card_le_three :
+    IsCyclic (alternatingGroup α) ↔ Nat.card α ≤ 3 :=
+  ⟨fun _ ↦ by rw [← isMulCommutative_iff_card_le_three]; exact IsCyclic.isMulCommutative,
+   isCyclic_of_card_le_three⟩
 
 open Equiv.Perm
 

Mathlib/GroupTheory/SpecificGroups/Alternating/Simple.lean

@@ -53,26 +53,15 @@ open MulAction Equiv.Perm Equiv Set.powersetCard
 
 namespace Equiv.Perm
 
-variable {α : Type*} [Finite α]
-
-theorem isCyclic_of_card_le_two (hα : Nat.card α ≤ 2) :
-    IsCyclic (Perm α) := by
-  apply isCyclic_of_card_dvd_prime (p := 2)
-  rw [Nat.card_perm]
-  interval_cases (Nat.card α) <;> simp
-
-theorem isMulCommutative_of_card_le_two (hα : Nat.card α ≤ 2) :
-    IsMulCommutative (Perm α) :=
-  ⟨(isCyclic_of_card_le_two hα).commutative⟩
-
-variable [DecidableEq α]
+variable {α : Type*} [Finite α] [DecidableEq α]
 
 /-- The Iwasawa structure of `Perm α` acting on `Set.powersetCard α 2`. -/
 def iwasawaStructure_two [∀ s : Set α, DecidablePred fun x ↦ x ∈ s] :
     IwasawaStructure (Perm α) (Set.powersetCard α 2) where
   T s := (ofSubtype : Perm (s : Set α) →* Perm α).range
   is_comm s := by
-    have : IsMulCommutative (Perm s) := isMulCommutative_of_card_le_two (by simp)
+    have : IsMulCommutative (Perm s) :=
+      isMulCommutative_iff_card_le_two.mpr (by simp)
     rw [MonoidHom.range_eq_map]
     apply Subgroup.map_isMulCommutative
   is_conj g s := by