English
If hmt: IsMultiplyPretransitive G α (|α|−2), then alternatingGroup α ≤ G.
Русский
Если hmt: IsMultiplyPretransitive G α (|α|−2), то alternatingGroup α ⊆ G.
LaTeX
$$alternatingGroup α \le G$$
Lean4
/-- A subgroup of `Equiv.Perm α` which is (card α - 2)-pretransitive
contains `alternatingGroup α`. -/
theorem _root_.IsMultiplyPretransitive.alternatingGroup_le (G : Subgroup (Equiv.Perm α))
(hmt : IsMultiplyPretransitive G α (Nat.card α - 2)) : alternatingGroup α ≤ G :=
by
rcases Nat.lt_or_ge (Nat.card α) 2 with hα1 | hα
· -- Nat.card α < 2
rw [Nat.card_eq_fintype_card] at hα1
rw [alternatingGroup.eq_bot_of_card_le_two hα1.le]
exact bot_le
apply Equiv.Perm.alternatingGroup_le_of_index_le_two
obtain ⟨s, _, hs⟩ :=
Set.exists_subset_card_eq (s := (Set.univ : Set α)) (n := Nat.card α - 2)
(by rw [Set.ncard_univ]; exact sub_le (Nat.card α) 2)
rw [← hs] at hmt
have := hmt.index_of_fixingSubgroup_mul rfl
rw [hs, Nat.sub_sub_self hα, factorial_two] at this
rw [← mul_le_mul_iff_of_pos_left (a := Nat.card G) card_pos, Subgroup.card_mul_index, ←
(fixingSubgroup G s).index_mul_card, mul_assoc, mul_comm _ 2, ← mul_assoc]
rw [this, Nat.card_perm]
refine Nat.le_mul_of_pos_right (Nat.card α)! card_pos
