-- Mathlib/GroupTheory/SpecificGroups/Alternating.lean
theorem eq_alternatingGroup_of_index_eq_two {G : Subgroup (Equiv.Perm α)} (hG : G.index = 2) :
    G = alternatingGroup α

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
a✝ : Nontrivial α
h : ∀ (g : Perm α), g.IsSwap → g ∈ G
⊢ G = ⊤

Tactic:
rwa [eq_top_iff, ← closure_isSwap, G.closure_le]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
a✝ : Nontrivial α
h : ∀ (g : Perm α), g.IsSwap → g ∈ G
⊢ False

Tactic:
suffices G = ⊤ by rw [this, Subgroup.index_top] at hG; cases hG

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
a✝ : Nontrivial α
h : ∀ (g : Perm α), g.IsSwap → g ∈ G
⊢ G = ⊤

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
a✝ : Nontrivial α
a b : α
hab : a ≠ b
habG : swap a b ∉ G
⊢ G = alternatingGroup α

Tactic:
ext g

Result:
case intro.intro.intro.intro.intro.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
a✝ : Nontrivial α
a b : α
hab : a ≠ b
habG : swap a b ∉ G
g : Perm α
⊢ g ∈ G ↔ g ∈ alternatingGroup α

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
a✝ : Nontrivial α
⊢ G = alternatingGroup α

Tactic:
obtain ⟨_, ⟨a, b, hab, rfl⟩, habG⟩ : ∃ g : Perm α, g.IsSwap ∧ g ∉ G := by
  by_contra! h
  suffices G = ⊤ by rw [this, Subgroup.index_top] at hG; cases hG
  rwa [eq_top_iff, ← closure_isSwap, G.closure_le]

Result:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
a✝ : Nontrivial α
a b : α
hab : a ≠ b
habG : swap a b ∉ G
⊢ G = alternatingGroup α

Proof state:
case intro.intro.intro.intro.intro.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
a✝ : Nontrivial α
a b : α
hab : a ≠ b
habG : swap a b ∉ G
g✝ g : Perm α
x y : α
hxy : x ≠ y
ih : g ∈ G ↔ g ∈ alternatingGroup α
⊢ swap x y ∉ G

Tactic:
contrapose! habG

Result:
case intro.intro.intro.intro.intro.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
a✝ : Nontrivial α
a b : α
hab : a ≠ b
g✝ g : Perm α
x y : α
hxy : x ≠ y
ih : g ∈ G ↔ g ∈ alternatingGroup α
habG : swap x y ∈ G
⊢ swap a b ∈ G

Proof state:
case intro.intro.intro.intro.intro.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
a✝ : Nontrivial α
a b : α
hab : a ≠ b
g✝ g : Perm α
x y : α
hxy : x ≠ y
ih : g ∈ G ↔ g ∈ alternatingGroup α
habG : swap x y ∈ G
⊢ ⋯.choose * swap x y * ⋯.choose⁻¹ ∈ G

Tactic:
exact (normal_of_index_eq_two hG).conj_mem _ habG _

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
a✝ : Nontrivial α
a b : α
hab : a ≠ b
habG : swap a b ∉ G
g✝ g : Perm α
x y : α
hxy : x ≠ y
ih : g ∈ G ↔ g ∈ alternatingGroup α
⊢ swap x y * g ∈ G ↔ swap x y * g ∈ alternatingGroup α

Tactic:
rw [mul_mem_iff_of_index_two hG, mul_mem_iff_of_index_two alternatingGroup.index_eq_two, ih]

Result:
case intro.intro.intro.intro.intro.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
a✝ : Nontrivial α
a b : α
hab : a ≠ b
habG : swap a b ∉ G
g✝ g : Perm α
x y : α
hxy : x ≠ y
ih : g ∈ G ↔ g ∈ alternatingGroup α
⊢ (swap x y ∈ G ↔ g ∈ alternatingGroup α) ↔ (swap x y ∈ alternatingGroup α ↔ g ∈ alternatingGroup α)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
a✝ : Nontrivial α
h : ∀ (g : Perm α), g.IsSwap → g ∈ G
this : G = ⊤
⊢ False

Tactic:
rw [this, Subgroup.index_top] at hG

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : 1 = 2
a✝ : Nontrivial α
h : ∀ (g : Perm α), g.IsSwap → g ∈ G
this : G = ⊤
⊢ False

Proof state:
case intro.intro.intro.intro.intro.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
a✝ : Nontrivial α
a b : α
hab : a ≠ b
g✝ g : Perm α
x y : α
hxy : x ≠ y
ih : g ∈ G ↔ g ∈ alternatingGroup α
habG : swap x y ∈ G
⊢ swap a b ∈ G

Tactic:
rw [← (isConj_iff.mp <| isConj_swap hxy hab).choose_spec]

Result:
case intro.intro.intro.intro.intro.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
a✝ : Nontrivial α
a b : α
hab : a ≠ b
g✝ g : Perm α
x y : α
hxy : x ≠ y
ih : g ∈ G ↔ g ∈ alternatingGroup α
habG : swap x y ∈ G
⊢ ⋯.choose * swap x y * ⋯.choose⁻¹ ∈ G

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
⊢ G = alternatingGroup α

Tactic:
nontriviality α

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
a✝ : Nontrivial α
⊢ G = alternatingGroup α

Proof state:
case intro.intro.intro.intro.intro.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
a✝ : Nontrivial α
a b : α
hab : a ≠ b
habG : swap a b ∉ G
g : Perm α
⊢ g ∈ G ↔ g ∈ alternatingGroup α

Tactic:
refine swap_induction_on g (iff_of_true G.one_mem <| map_one _) fun g x y hxy ih ↦ ?_

Result:
case intro.intro.intro.intro.intro.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
a✝ : Nontrivial α
a b : α
hab : a ≠ b
habG : swap a b ∉ G
g✝ g : Perm α
x y : α
hxy : x ≠ y
ih : g ∈ G ↔ g ∈ alternatingGroup α
⊢ swap x y * g ∈ G ↔ swap x y * g ∈ alternatingGroup α

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : 1 = 2
a✝ : Nontrivial α
h : ∀ (g : Perm α), g.IsSwap → g ∈ G
this : G = ⊤
⊢ False

Tactic:
cases hG

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
a✝ : Nontrivial α
⊢ ∃ g, g.IsSwap ∧ g ∉ G

Tactic:
by_contra! h

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
a✝ : Nontrivial α
h : ∀ (g : Perm α), g.IsSwap → g ∈ G
⊢ False