no goals
α : Type ?u.143668
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ ↑sign (swap 0 4 * swap 1 3) = 1
decide
α : Type ?u.143668
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g1 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 2 * swap 0 1, property := (_ : swap 0 2 * swap 0 1 ∈ alternatingGroup (Fin 5)) }
⊢ normalClosure {{ val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }} = ⊤
α : Type ?u.143668
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ normalClosure {{ val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }} = ⊤
let g1 := (⟨swap 0 2 * swap 0 1, mem_alternatingGroup.2 (by decide)⟩ : alternatingGroup (Fin 5))
α : Type ?u.143668
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g1 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 2 * swap 0 1, property := (_ : swap 0 2 * swap 0 1 ∈ alternatingGroup (Fin 5)) }
g2 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }
⊢ normalClosure {{ val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }} = ⊤
α : Type ?u.143668
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g1 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 2 * swap 0 1, property := (_ : swap 0 2 * swap 0 1 ∈ alternatingGroup (Fin 5)) }
⊢ normalClosure {{ val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }} = ⊤
let g2 := (⟨swap 0 4 * swap 1 3, mem_alternatingGroup.2 (by decide)⟩ : alternatingGroup (Fin 5))
α : Type ?u.143668
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g1 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 2 * swap 0 1, property := (_ : swap 0 2 * swap 0 1 ∈ alternatingGroup (Fin 5)) }
g2 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }
h5 :
  g1 * g2 * g1⁻¹ * g2⁻¹ = { val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) }
⊢ normalClosure {{ val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }} = ⊤
α : Type ?u.143668
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g1 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 2 * swap 0 1, property := (_ : swap 0 2 * swap 0 1 ∈ alternatingGroup (Fin 5)) }
g2 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }
⊢ normalClosure {{ val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }} = ⊤
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]
α : Type ?u.143668
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g1 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 2 * swap 0 1, property := (_ : swap 0 2 * swap 0 1 ∈ alternatingGroup (Fin 5)) }
g2 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }
h5 :
  g1 * g2 * g1⁻¹ * g2⁻¹ = { val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) }
⊢ normalClosure {{ val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) }} ≤
    normalClosure {{ val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }}
α : Type ?u.143668
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g1 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 2 * swap 0 1, property := (_ : swap 0 2 * swap 0 1 ∈ alternatingGroup (Fin 5)) }
g2 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }
h5 :
  g1 * g2 * g1⁻¹ * g2⁻¹ = { val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) }
⊢ normalClosure {{ val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }} = ⊤
rw [eq_top_iff, ← normalClosure_finRotate_five]
α : Type ?u.143668
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g1 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 2 * swap 0 1, property := (_ : swap 0 2 * swap 0 1 ∈ alternatingGroup (Fin 5)) }
g2 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }
h5 :
  g1 * g2 * g1⁻¹ * g2⁻¹ = { val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) }
⊢ {{ val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) }} ⊆
    ↑(normalClosure {{ val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }})
α : Type ?u.143668
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g1 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 2 * swap 0 1, property := (_ : swap 0 2 * swap 0 1 ∈ alternatingGroup (Fin 5)) }
g2 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }
h5 :
  g1 * g2 * g1⁻¹ * g2⁻¹ = { val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) }
⊢ normalClosure {{ val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) }} ≤
    normalClosure {{ val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }}
refine' normalClosure_le_normal _
α : Type ?u.143668
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g1 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 2 * swap 0 1, property := (_ : swap 0 2 * swap 0 1 ∈ alternatingGroup (Fin 5)) }
g2 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }
h5 :
  g1 * g2 * g1⁻¹ * g2⁻¹ = { val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) }
⊢ g1 * g2 * g1⁻¹ * g2⁻¹ ∈
    normalClosure {{ val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }}
α : Type ?u.143668
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g1 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 2 * swap 0 1, property := (_ : swap 0 2 * swap 0 1 ∈ alternatingGroup (Fin 5)) }
g2 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }
h5 :
  g1 * g2 * g1⁻¹ * g2⁻¹ = { val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) }
⊢ {{ val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) }} ⊆
    ↑(normalClosure {{ val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }})
rw [Set.singleton_subset_iff, SetLike.mem_coe, ← h5]
α : Type ?u.143668
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g1 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 2 * swap 0 1, property := (_ : swap 0 2 * swap 0 1 ∈ alternatingGroup (Fin 5)) }
g2 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }
h5 :
  g1 * g2 * g1⁻¹ * g2⁻¹ = { val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) }
h : g2 ∈ normalClosure {g2}
⊢ g1 * g2 * g1⁻¹ * g2⁻¹ ∈
    normalClosure {{ val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }}
α : Type ?u.143668
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g1 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 2 * swap 0 1, property := (_ : swap 0 2 * swap 0 1 ∈ alternatingGroup (Fin 5)) }
g2 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }
h5 :
  g1 * g2 * g1⁻¹ * g2⁻¹ = { val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) }
⊢ g1 * g2 * g1⁻¹ * g2⁻¹ ∈
    normalClosure {{ val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }}
have h : g2 ∈ normalClosure {g2} :=
  SetLike.mem_coe.1 (subset_normalClosure (Set.mem_singleton _))
no goals
α : Type ?u.143668
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g1 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 2 * swap 0 1, property := (_ : swap 0 2 * swap 0 1 ∈ alternatingGroup (Fin 5)) }
g2 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }
h5 :
  g1 * g2 * g1⁻¹ * g2⁻¹ = { val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) }
h : g2 ∈ normalClosure {g2}
⊢ g1 * g2 * g1⁻¹ * g2⁻¹ ∈
    normalClosure {{ val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }}
exact mul_mem (Subgroup.normalClosure_normal.conj_mem _ h g1) (inv_mem h)
no goals
α : Type ?u.143668
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ ↑sign (swap 0 2 * swap 0 1) = 1
decide
no goals
α : Type ?u.143668
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g1 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 2 * swap 0 1, property := (_ : swap 0 2 * swap 0 1 ∈ alternatingGroup (Fin 5)) }
⊢ ↑sign (swap 0 4 * swap 1 3) = 1
decide
α : Type ?u.143668
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g1 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 2 * swap 0 1, property := (_ : swap 0 2 * swap 0 1 ∈ alternatingGroup (Fin 5)) }
g2 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }
⊢ ↑(g1 * g2 * g1⁻¹ * g2⁻¹) =
    ↑{ val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) }
α : Type ?u.143668
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g1 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 2 * swap 0 1, property := (_ : swap 0 2 * swap 0 1 ∈ alternatingGroup (Fin 5)) }
g2 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }
⊢ g1 * g2 * g1⁻¹ * g2⁻¹ = { val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) }
rw [Subtype.ext_iff]
no goals
α : Type ?u.143668
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g1 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 2 * swap 0 1, property := (_ : swap 0 2 * swap 0 1 ∈ alternatingGroup (Fin 5)) }
g2 : { x // x ∈ alternatingGroup (Fin 5) } :=
  { val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }
⊢ ↑(g1 * g2 * g1⁻¹ * g2⁻¹) =
    ↑{ val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) }
simp only [Fin.val_mk, Subgroup.coe_mul, Subgroup.coe_inv, Fin.val_mk]