Theorem: contains_alternating_of_index_le_2' (Jordan/IndexNormal.lean)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G ≤ 2
⊢ alternatingGroup α ≤ G
Tactic:
apply large_subgroup_of_perm_contains_alternating
State after:
case hG
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G ≤ 2
⊢ Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G

State before:
case hG
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G ≤ 2
⊢ Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
Tactic:
rw [← Subgroup.index_mul_card G]
State after:
case hG
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G ≤ 2
⊢ Subgroup.index G * Fintype.card ↥G ≤ 2 * Fintype.card ↥G

State before:
case hG
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G ≤ 2
⊢ Subgroup.index G * Fintype.card ↥G ≤ 2 * Fintype.card ↥G
Tactic:
apply Nat.mul_le_mul_right _ hG
State after:
no goals