-- Mathlib/GroupTheory/SpecificGroups/Alternating.lean
theorem normalClosure_swap_mul_swap_five :
    normalClosure
        ({⟨swap 0 4 * swap 1 3, mem_alternatingGroup.2 (by decide)⟩} :
          Set (alternatingGroup (Fin 5))) =
      ⊤

Proof state:
⊢ normalClosure {⟨swap 0 4 * swap 1 3, ⋯⟩} = ⊤

Tactic:
let g1 := (⟨swap 0 2 * swap 0 1, mem_alternatingGroup.2 (by decide)⟩ : alternatingGroup (Fin 5))

Result:
g1 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 2 * swap 0 1, ⋯⟩
⊢ normalClosure {⟨swap 0 4 * swap 1 3, ⋯⟩} = ⊤

Proof state:
g1 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 2 * swap 0 1, ⋯⟩
g2 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 4 * swap 1 3, ⋯⟩
⊢ ↑g1 * ↑g2 * (↑g1)⁻¹ * (↑g2)⁻¹ = finRotate 5

Tactic:
decide

Result:
no goals

Proof state:
g1 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 2 * swap 0 1, ⋯⟩
g2 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 4 * swap 1 3, ⋯⟩
⊢ normalClosure {⟨swap 0 4 * swap 1 3, ⋯⟩} = ⊤

Tactic:
have h5 : g1 * g2 * g1⁻¹ * g2⁻¹ =
    ⟨finRotate 5, finRotate_bit1_mem_alternatingGroup (n := 2)⟩ := by
  rw [Subtype.ext_iff]
  simp only [Fin.val_mk, Subgroup.coe_mul, Subgroup.coe_inv, Fin.val_mk]
  decide

Result:
g1 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 2 * swap 0 1, ⋯⟩
g2 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 4 * swap 1 3, ⋯⟩
h5 : g1 * g2 * g1⁻¹ * g2⁻¹ = ⟨finRotate 5, ⋯⟩
⊢ normalClosure {⟨swap 0 4 * swap 1 3, ⋯⟩} = ⊤

Proof state:
g1 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 2 * swap 0 1, ⋯⟩
g2 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 4 * swap 1 3, ⋯⟩
h5 : g1 * g2 * g1⁻¹ * g2⁻¹ = ⟨finRotate 5, ⋯⟩
⊢ normalClosure {⟨swap 0 4 * swap 1 3, ⋯⟩} = ⊤

Tactic:
rw [eq_top_iff, ← normalClosure_finRotate_five]

Result:
g1 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 2 * swap 0 1, ⋯⟩
g2 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 4 * swap 1 3, ⋯⟩
h5 : g1 * g2 * g1⁻¹ * g2⁻¹ = ⟨finRotate 5, ⋯⟩
⊢ normalClosure {⟨finRotate 5, ⋯⟩} ≤ normalClosure {⟨swap 0 4 * swap 1 3, ⋯⟩}

Proof state:
g1 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 2 * swap 0 1, ⋯⟩
g2 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 4 * swap 1 3, ⋯⟩
h5 : g1 * g2 * g1⁻¹ * g2⁻¹ = ⟨finRotate 5, ⋯⟩
⊢ normalClosure {⟨finRotate 5, ⋯⟩} ≤ normalClosure {⟨swap 0 4 * swap 1 3, ⋯⟩}

Tactic:
refine normalClosure_le_normal ?_

Result:
g1 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 2 * swap 0 1, ⋯⟩
g2 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 4 * swap 1 3, ⋯⟩
h5 : g1 * g2 * g1⁻¹ * g2⁻¹ = ⟨finRotate 5, ⋯⟩
⊢ {⟨finRotate 5, ⋯⟩} ⊆ ↑(normalClosure {⟨swap 0 4 * swap 1 3, ⋯⟩})

Proof state:
g1 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 2 * swap 0 1, ⋯⟩
⊢ sign (swap 0 4 * swap 1 3) = 1

Tactic:
decide

Result:
no goals

Proof state:
g1 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 2 * swap 0 1, ⋯⟩
⊢ normalClosure {⟨swap 0 4 * swap 1 3, ⋯⟩} = ⊤

Tactic:
let g2 := (⟨swap 0 4 * swap 1 3, mem_alternatingGroup.2 (by decide)⟩ : alternatingGroup (Fin 5))

Result:
g1 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 2 * swap 0 1, ⋯⟩
g2 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 4 * swap 1 3, ⋯⟩
⊢ normalClosure {⟨swap 0 4 * swap 1 3, ⋯⟩} = ⊤

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ sign (swap 0 4 * swap 1 3) = 1

Tactic:
decide

Result:
no goals

Proof state:
g1 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 2 * swap 0 1, ⋯⟩
g2 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 4 * swap 1 3, ⋯⟩
h5 : g1 * g2 * g1⁻¹ * g2⁻¹ = ⟨finRotate 5, ⋯⟩
⊢ {⟨finRotate 5, ⋯⟩} ⊆ ↑(normalClosure {⟨swap 0 4 * swap 1 3, ⋯⟩})

Tactic:
rw [Set.singleton_subset_iff, SetLike.mem_coe, ← h5]

Result:
g1 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 2 * swap 0 1, ⋯⟩
g2 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 4 * swap 1 3, ⋯⟩
h5 : g1 * g2 * g1⁻¹ * g2⁻¹ = ⟨finRotate 5, ⋯⟩
⊢ g1 * g2 * g1⁻¹ * g2⁻¹ ∈ normalClosure {⟨swap 0 4 * swap 1 3, ⋯⟩}

Proof state:
g1 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 2 * swap 0 1, ⋯⟩
g2 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 4 * swap 1 3, ⋯⟩
h5 : g1 * g2 * g1⁻¹ * g2⁻¹ = ⟨finRotate 5, ⋯⟩
h : g2 ∈ normalClosure {g2}
⊢ g1 * g2 * g1⁻¹ * g2⁻¹ ∈ normalClosure {⟨swap 0 4 * swap 1 3, ⋯⟩}

Tactic:
exact mul_mem (Subgroup.normalClosure_normal.conj_mem _ h g1) (inv_mem h)

Result:
no goals

Proof state:
g1 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 2 * swap 0 1, ⋯⟩
g2 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 4 * swap 1 3, ⋯⟩
h5 : g1 * g2 * g1⁻¹ * g2⁻¹ = ⟨finRotate 5, ⋯⟩
⊢ g1 * g2 * g1⁻¹ * g2⁻¹ ∈ normalClosure {⟨swap 0 4 * swap 1 3, ⋯⟩}

Tactic:
have h : g2 ∈ normalClosure {g2} :=
  SetLike.mem_coe.1 (subset_normalClosure (Set.mem_singleton _))

Result:
g1 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 2 * swap 0 1, ⋯⟩
g2 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 4 * swap 1 3, ⋯⟩
h5 : g1 * g2 * g1⁻¹ * g2⁻¹ = ⟨finRotate 5, ⋯⟩
h : g2 ∈ normalClosure {g2}
⊢ g1 * g2 * g1⁻¹ * g2⁻¹ ∈ normalClosure {⟨swap 0 4 * swap 1 3, ⋯⟩}

Proof state:
g1 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 2 * swap 0 1, ⋯⟩
g2 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 4 * swap 1 3, ⋯⟩
⊢ g1 * g2 * g1⁻¹ * g2⁻¹ = ⟨finRotate 5, ⋯⟩

Tactic:
rw [Subtype.ext_iff]

Result:
g1 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 2 * swap 0 1, ⋯⟩
g2 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 4 * swap 1 3, ⋯⟩
⊢ ↑(g1 * g2 * g1⁻¹ * g2⁻¹) = ↑⟨finRotate 5, ⋯⟩

Proof state:
g1 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 2 * swap 0 1, ⋯⟩
g2 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 4 * swap 1 3, ⋯⟩
⊢ ↑(g1 * g2 * g1⁻¹ * g2⁻¹) = ↑⟨finRotate 5, ⋯⟩

Tactic:
simp only [Fin.val_mk, Subgroup.coe_mul, Subgroup.coe_inv, Fin.val_mk]

Result:
g1 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 2 * swap 0 1, ⋯⟩
g2 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 4 * swap 1 3, ⋯⟩
⊢ ↑g1 * ↑g2 * (↑g1)⁻¹ * (↑g2)⁻¹ = finRotate 5

Proof state:
⊢ sign (swap 0 2 * swap 0 1) = 1

Tactic:
decide

Result:
no goals