Theorem: MulAction.IsMultiplyPretransitive.alternatingGroup_le_of_sub_two (Jordan/MultipleTransitivity.lean)

State before:
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
⊢ alternatingGroup α ≤ G
Tactic:
cases' Nat.lt_or_ge (Fintype.card α) 2 with hα1 hα
State after:
case inl
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα1 : Fintype.card α < 2
⊢ alternatingGroup α ≤ G

case inr
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα : Fintype.card α ≥ 2
⊢ alternatingGroup α ≤ G

State before:
case inr
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα : Fintype.card α ≥ 2
⊢ alternatingGroup α ≤ G
Tactic:
apply large_subgroup_of_perm_contains_alternating
State after:
case inr.hG
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα : Fintype.card α ≥ 2
⊢ Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G

State before:
case inr.hG
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα : Fintype.card α ≥ 2
⊢ Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
Tactic:
rw [Fintype.card_equiv (Equiv.refl _)]
State after:
case inr.hG
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα : Fintype.card α ≥ 2
⊢ (Fintype.card α)! ≤ 2 * Fintype.card ↥G

State before:
case inr.hG
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα : Fintype.card α ≥ 2
⊢ (Fintype.card α)! ≤ 2 * Fintype.card ↥G
Tactic:
obtain ⟨s, _, hs⟩ := Set.exists_smaller_set (Set.univ : Set α) (Fintype.card α - 2)
  (by
    rw [Set.ncard_univ, Nat.card_eq_fintype_card]
    exact sub_le (Fintype.card α) 2)
State after:
case inr.hG.intro.intro
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα : Fintype.card α ≥ 2
s : Set α
left✝ : s ⊆ Set.univ
hs : Set.ncard s = Fintype.card α - 2
⊢ (Fintype.card α)! ≤ 2 * Fintype.card ↥G

State before:
case inr.hG.intro.intro
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα : Fintype.card α ≥ 2
s : Set α
left✝ : s ⊆ Set.univ
hs : Set.ncard s = Fintype.card α - 2
⊢ (Fintype.card α)! ≤ 2 * Fintype.card ↥G
Tactic:
rw [← hs] at hmt
State after:
case inr.hG.intro.intro
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≥ 2
s : Set α
hmt : IsMultiplyPretransitive (↥G) α (Set.ncard s)
left✝ : s ⊆ Set.univ
hs : Set.ncard s = Fintype.card α - 2
⊢ (Fintype.card α)! ≤ 2 * Fintype.card ↥G

State before:
case inr.hG.intro.intro
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≥ 2
s : Set α
hmt : IsMultiplyPretransitive (↥G) α (Set.ncard s)
left✝ : s ⊆ Set.univ
hs : Set.ncard s = Fintype.card α - 2
⊢ (Fintype.card α)! ≤ 2 * Fintype.card ↥G
Tactic:
rw [← hmt.index_of_fixingSubgroup G α s, hs, Nat.sub_sub_self hα,
  Nat.factorial_two, mul_comm]
State after:
case inr.hG.intro.intro
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≥ 2
s : Set α
hmt : IsMultiplyPretransitive (↥G) α (Set.ncard s)
left✝ : s ⊆ Set.univ
hs : Set.ncard s = Fintype.card α - 2
⊢ 2 * Subgroup.index (fixingSubgroup (↥G) s) ≤ 2 * Fintype.card ↥G

State before:
case inr.hG.intro.intro
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≥ 2
s : Set α
hmt : IsMultiplyPretransitive (↥G) α (Set.ncard s)
left✝ : s ⊆ Set.univ
hs : Set.ncard s = Fintype.card α - 2
⊢ 2 * Subgroup.index (fixingSubgroup (↥G) s) ≤ 2 * Fintype.card ↥G
Tactic:
apply Nat.mul_le_mul_left
State after:
case inr.hG.intro.intro.h
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≥ 2
s : Set α
hmt : IsMultiplyPretransitive (↥G) α (Set.ncard s)
left✝ : s ⊆ Set.univ
hs : Set.ncard s = Fintype.card α - 2
⊢ Subgroup.index (fixingSubgroup (↥G) s) ≤ Fintype.card ↥G

State before:
case inr.hG.intro.intro.h
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≥ 2
s : Set α
hmt : IsMultiplyPretransitive (↥G) α (Set.ncard s)
left✝ : s ⊆ Set.univ
hs : Set.ncard s = Fintype.card α - 2
⊢ Subgroup.index (fixingSubgroup (↥G) s) ≤ Fintype.card ↥G
Tactic:
apply Nat.le_of_dvd (Fintype.card_pos)
State after:
case inr.hG.intro.intro.h
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≥ 2
s : Set α
hmt : IsMultiplyPretransitive (↥G) α (Set.ncard s)
left✝ : s ⊆ Set.univ
hs : Set.ncard s = Fintype.card α - 2
⊢ Subgroup.index (fixingSubgroup (↥G) s) ∣ Fintype.card ↥G

State before:
case inr.hG.intro.intro.h
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≥ 2
s : Set α
hmt : IsMultiplyPretransitive (↥G) α (Set.ncard s)
left✝ : s ⊆ Set.univ
hs : Set.ncard s = Fintype.card α - 2
⊢ Subgroup.index (fixingSubgroup (↥G) s) ∣ Fintype.card ↥G
Tactic:
apply Subgroup.index_dvd_card
State after:
no goals

State before:
case inl
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα1 : Fintype.card α < 2
⊢ alternatingGroup α ≤ G
Tactic:
rw [Nat.lt_succ_iff] at hα1
State after:
case inl
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα1 : Fintype.card α ≤ 1
⊢ alternatingGroup α ≤ G

State before:
case inl
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα1 : Fintype.card α ≤ 1
⊢ alternatingGroup α ≤ G
Tactic:
suffices alternatingGroup α = ⊥ by
  rw [this]; exact bot_le
State after:
case inl
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα1 : Fintype.card α ≤ 1
⊢ alternatingGroup α = ⊥

State before:
case inl
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα1 : Fintype.card α ≤ 1
⊢ alternatingGroup α = ⊥
Tactic:
rw [← Subgroup.card_le_one_iff_eq_bot]
State after:
case inl
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα1 : Fintype.card α ≤ 1
⊢ Fintype.card ↥(alternatingGroup α) ≤ 1

State before:
case inl
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα1 : Fintype.card α ≤ 1
⊢ Fintype.card ↥(alternatingGroup α) ≤ 1
Tactic:
suffices Fintype.card (alternatingGroup α) ≤ Fintype.card (Equiv.Perm α) by
  apply le_trans this
  rw [Fintype.card_perm]
  exact Nat.factorial_le hα1
State after:
case inl
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα1 : Fintype.card α ≤ 1
⊢ Fintype.card ↥(alternatingGroup α) ≤ Fintype.card (Equiv.Perm α)

State before:
case inl
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα1 : Fintype.card α ≤ 1
⊢ Fintype.card ↥(alternatingGroup α) ≤ Fintype.card (Equiv.Perm α)
Tactic:
convert Fintype.card_subtype_le (fun x ↦ x ∈ alternatingGroup α)
State after:
no goals

State before:
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα1 : Fintype.card α ≤ 1
this : alternatingGroup α = ⊥
⊢ alternatingGroup α ≤ G
Tactic:
rw [this]
State after:
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα1 : Fintype.card α ≤ 1
this : alternatingGroup α = ⊥
⊢ ⊥ ≤ G

State before:
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα1 : Fintype.card α ≤ 1
this : alternatingGroup α = ⊥
⊢ ⊥ ≤ G
Tactic:
exact bot_le
State after:
no goals

State before:
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα1 : Fintype.card α ≤ 1
this : Fintype.card ↥(alternatingGroup α) ≤ Fintype.card (Equiv.Perm α)
⊢ Fintype.card ↥(alternatingGroup α) ≤ 1
Tactic:
apply le_trans this
State after:
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα1 : Fintype.card α ≤ 1
this : Fintype.card ↥(alternatingGroup α) ≤ Fintype.card (Equiv.Perm α)
⊢ Fintype.card (Equiv.Perm α) ≤ 1

State before:
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα1 : Fintype.card α ≤ 1
this : Fintype.card ↥(alternatingGroup α) ≤ Fintype.card (Equiv.Perm α)
⊢ Fintype.card (Equiv.Perm α) ≤ 1
Tactic:
rw [Fintype.card_perm]
State after:
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα1 : Fintype.card α ≤ 1
this : Fintype.card ↥(alternatingGroup α) ≤ Fintype.card (Equiv.Perm α)
⊢ (Fintype.card α)! ≤ 1

State before:
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα1 : Fintype.card α ≤ 1
this : Fintype.card ↥(alternatingGroup α) ≤ Fintype.card (Equiv.Perm α)
⊢ (Fintype.card α)! ≤ 1
Tactic:
exact Nat.factorial_le hα1
State after:
no goals

State before:
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα : Fintype.card α ≥ 2
⊢ Fintype.card α - 2 ≤ Set.ncard Set.univ
Tactic:
rw [Set.ncard_univ, Nat.card_eq_fintype_card]
State after:
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα : Fintype.card α ≥ 2
⊢ Fintype.card α - 2 ≤ Fintype.card α

State before:
M : Type ?u.274186
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
hα : Fintype.card α ≥ 2
⊢ Fintype.card α - 2 ≤ Fintype.card α
Tactic:
exact sub_le (Fintype.card α) 2
State after:
no goals