Theorem: eq_s2_of_nontrivial (Jordan/Jordan.lean)

State before:
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ G = ⊤
Tactic:
classical
apply Subgroup.eq_top_of_card_eq
apply le_antisymm
apply Fintype.card_subtype_le
rw [Fintype.card_equiv (Equiv.cast rfl)]
refine' le_trans _ _
exact (2 : ℕ).factorial
exact Nat.factorial_le hα
rw [Nat.factorial_two]
rw [← Fintype.one_lt_card_iff_nontrivial] at hG
exact hG
State after:
no goals

State before:
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ G = ⊤
Tactic:
apply Subgroup.eq_top_of_card_eq
State after:
case h
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ Fintype.card ↥G = Fintype.card (Equiv.Perm α)

State before:
case h
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ Fintype.card ↥G = Fintype.card (Equiv.Perm α)
Tactic:
apply le_antisymm
State after:
case h.a
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ Fintype.card ↥G ≤ Fintype.card (Equiv.Perm α)

case h.a
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ Fintype.card (Equiv.Perm α) ≤ Fintype.card ↥G

State before:
case h.a
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ Fintype.card ↥G ≤ Fintype.card (Equiv.Perm α)

case h.a
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ Fintype.card (Equiv.Perm α) ≤ Fintype.card ↥G
Tactic:
apply Fintype.card_subtype_le
State after:
case h.a
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ Fintype.card (Equiv.Perm α) ≤ Fintype.card ↥G

State before:
case h.a
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ Fintype.card (Equiv.Perm α) ≤ Fintype.card ↥G
Tactic:
rw [Fintype.card_equiv (Equiv.cast rfl)]
State after:
case h.a
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ Nat.factorial (Fintype.card α) ≤ Fintype.card ↥G

State before:
case h.a
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ Nat.factorial (Fintype.card α) ≤ Fintype.card ↥G
Tactic:
refine' le_trans _ _
State after:
case h.a.refine'_1
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ ℕ

case h.a.refine'_2
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ Nat.factorial (Fintype.card α) ≤ ?h.a.refine'_1

case h.a.refine'_3
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ ?h.a.refine'_1 ≤ Fintype.card ↥G

State before:
case h.a.refine'_1
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ ℕ

case h.a.refine'_2
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ Nat.factorial (Fintype.card α) ≤ ?h.a.refine'_1

case h.a.refine'_3
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ ?h.a.refine'_1 ≤ Fintype.card ↥G
Tactic:
exact (2 : ℕ).factorial
State after:
case h.a.refine'_2
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ Nat.factorial (Fintype.card α) ≤ Nat.factorial 2

case h.a.refine'_3
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ Nat.factorial 2 ≤ Fintype.card ↥G

State before:
case h.a.refine'_2
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ Nat.factorial (Fintype.card α) ≤ Nat.factorial 2

case h.a.refine'_3
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ Nat.factorial 2 ≤ Fintype.card ↥G
Tactic:
exact Nat.factorial_le hα
State after:
case h.a.refine'_3
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ Nat.factorial 2 ≤ Fintype.card ↥G

State before:
case h.a.refine'_3
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ Nat.factorial 2 ≤ Fintype.card ↥G
Tactic:
rw [Nat.factorial_two]
State after:
case h.a.refine'_3
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ 2 ≤ Fintype.card ↥G

State before:
case h.a.refine'_3
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : Nontrivial ↥G
⊢ 2 ≤ Fintype.card ↥G
Tactic:
rw [← Fintype.one_lt_card_iff_nontrivial] at hG
State after:
case h.a.refine'_3
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : 1 < Fintype.card ↥G
⊢ 2 ≤ Fintype.card ↥G

State before:
case h.a.refine'_3
α : Type u_1
inst✝ : Fintype α
G : Subgroup (Equiv.Perm α)
hα : Fintype.card α ≤ 2
hG : 1 < Fintype.card ↥G
⊢ 2 ≤ Fintype.card ↥G
Tactic:
exact hG
State after:
no goals