Theorem: large_subgroup_of_perm_contains_alternating (Jordan/IndexNormal.lean)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
⊢ alternatingGroup α ≤ G
Tactic:
cases' Nat.eq_zero_or_pos G.index with h h
State after:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h : Subgroup.index G = 0
⊢ alternatingGroup α ≤ G

case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h : Subgroup.index G > 0
⊢ alternatingGroup α ≤ G

State before:
case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h : Subgroup.index G > 0
⊢ alternatingGroup α ≤ G
Tactic:
cases' eq_or_gt_of_le (Nat.succ_le_iff.mpr h) with h h
State after:
case inr.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : Subgroup.index G = Nat.succ 0
⊢ alternatingGroup α ≤ G

case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : Nat.succ 0 < Subgroup.index G
⊢ alternatingGroup α ≤ G

State before:
case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : Nat.succ 0 < Subgroup.index G
⊢ alternatingGroup α ≤ G
Tactic:
rw [← Nat.succ_le_iff] at h
State after:
case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : Nat.succ (Nat.succ 0) ≤ Subgroup.index G
⊢ alternatingGroup α ≤ G

State before:
case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : Nat.succ (Nat.succ 0) ≤ Subgroup.index G
⊢ alternatingGroup α ≤ G
Tactic:
norm_num at h
State after:
case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ alternatingGroup α ≤ G

State before:
case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ alternatingGroup α ≤ G
Tactic:
apply le_of_eq
State after:
case inr.inr.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ alternatingGroup α = G

State before:
case inr.inr.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ alternatingGroup α = G
Tactic:
apply is_alternating_of_index_2
State after:
case inr.inr.a.hG
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ Subgroup.index G = 2

State before:
case inr.inr.a.hG
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ Subgroup.index G = 2
Tactic:
refine' le_antisymm _ h
State after:
case inr.inr.a.hG
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ Subgroup.index G ≤ 2

State before:
case inr.inr.a.hG
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ Subgroup.index G ≤ 2
Tactic:
refine' Nat.le_of_mul_le_mul_left _ _
State after:
case inr.inr.a.hG.refine'_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ ℕ

case inr.inr.a.hG.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ ?inr.inr.a.hG.refine'_1 * Subgroup.index G ≤ ?inr.inr.a.hG.refine'_1 * 2

case inr.inr.a.hG.refine'_3
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ 0 < ?inr.inr.a.hG.refine'_1

State before:
case inr.inr.a.hG.refine'_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ ℕ

case inr.inr.a.hG.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ ?inr.inr.a.hG.refine'_1 * Subgroup.index G ≤ ?inr.inr.a.hG.refine'_1 * 2

case inr.inr.a.hG.refine'_3
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ 0 < ?inr.inr.a.hG.refine'_1
Tactic:
swap
State after:
case inr.inr.a.hG.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ ?inr.inr.a.hG.refine'_1 * Subgroup.index G ≤ ?inr.inr.a.hG.refine'_1 * 2

case inr.inr.a.hG.refine'_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ ℕ

case inr.inr.a.hG.refine'_3
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ 0 < ?inr.inr.a.hG.refine'_1

State before:
case inr.inr.a.hG.refine'_3
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ 0 < Fintype.card ↥G
Tactic:
exact Fintype.card_pos
State after:
no goals

State before:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h : Subgroup.index G = 0
⊢ alternatingGroup α ≤ G
Tactic:
exfalso
State after:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h : Subgroup.index G = 0
⊢ False

State before:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h : Subgroup.index G = 0
⊢ False
Tactic:
exact Subgroup.index_ne_zero_of_finite h
State after:
no goals

State before:
case inr.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : Subgroup.index G = Nat.succ 0
⊢ alternatingGroup α ≤ G
Tactic:
rw [Subgroup.index_eq_one] at h
State after:
case inr.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : G = ⊤
⊢ alternatingGroup α ≤ G

State before:
case inr.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : G = ⊤
⊢ alternatingGroup α ≤ G
Tactic:
rw [h]
State after:
case inr.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : G = ⊤
⊢ alternatingGroup α ≤ ⊤

State before:
case inr.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : G = ⊤
⊢ alternatingGroup α ≤ ⊤
Tactic:
exact le_top
State after:
no goals

State before:
case inr.inr.a.hG.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ ?inr.inr.a.hG.refine'_1 * Subgroup.index G ≤ ?inr.inr.a.hG.refine'_1 * 2
Tactic:
rw [mul_comm, Subgroup.index_mul_card, mul_comm]
State after:
case inr.inr.a.hG.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G

State before:
case inr.inr.a.hG.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
Tactic:
exact hG
State after:
no goals