[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ l → IsSwap g
⊢ List.prod l ∈ alternatingGroup α ↔ Even (List.length l)
[PROOFSTEP]
rw [mem_alternatingGroup, sign_prod_list_swap hl, ← Units.val_eq_one, Units.val_pow_eq_pow_val, Units.coe_neg_one,
  neg_one_pow_eq_one_iff_even]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ l → IsSwap g
⊢ -1 ≠ 1
[PROOFSTEP]
decide
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
⊢ finRotate (bit1 n) ∈ alternatingGroup (Fin (bit1 n))
[PROOFSTEP]
rw [mem_alternatingGroup, bit1, sign_finRotate, pow_bit0', Int.units_mul_self, one_pow]
[GOAL]
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nontrivial α
⊢ 2 * card { x // x ∈ alternatingGroup α } = card (Perm α)
[PROOFSTEP]
let this := (QuotientGroup.quotientKerEquivOfSurjective _ (sign_surjective α)).toEquiv
[GOAL]
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nontrivial α
this : Perm α ⧸ MonoidHom.ker sign ≃ ℤˣ :=
  (QuotientGroup.quotientKerEquivOfSurjective sign (_ : Function.Surjective ↑sign)).toEquiv
⊢ 2 * card { x // x ∈ alternatingGroup α } = card (Perm α)
[PROOFSTEP]
rw [← Fintype.card_units_int, ← Fintype.card_congr this]
[GOAL]
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nontrivial α
this : Perm α ⧸ MonoidHom.ker sign ≃ ℤˣ :=
  (QuotientGroup.quotientKerEquivOfSurjective sign (_ : Function.Surjective ↑sign)).toEquiv
⊢ card (Perm α ⧸ MonoidHom.ker sign) * card { x // x ∈ alternatingGroup α } = card (Perm α)
[PROOFSTEP]
apply (Subgroup.card_eq_card_quotient_mul_card_subgroup _).symm
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : { x // x ∈ alternatingGroup α }
hc : IsConj ↑σ ↑τ
hσ : Finset.card (support ↑σ) + 2 ≤ card α
⊢ IsConj σ τ
[PROOFSTEP]
obtain ⟨σ, hσ⟩ := σ
[GOAL]
case mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
τ : { x // x ∈ alternatingGroup α }
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hc : IsConj ↑{ val := σ, property := hσ✝ } ↑τ
hσ : Finset.card (support ↑{ val := σ, property := hσ✝ }) + 2 ≤ card α
⊢ IsConj { val := σ, property := hσ✝ } τ
[PROOFSTEP]
obtain ⟨τ, hτ⟩ := τ
[GOAL]
case mk.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : Finset.card (support ↑{ val := σ, property := hσ✝ }) + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑{ val := σ, property := hσ✝ } ↑{ val := τ, property := hτ }
⊢ IsConj { val := σ, property := hσ✝ } { val := τ, property := hτ }
[PROOFSTEP]
obtain ⟨π, hπ⟩ := isConj_iff.1 hc
[GOAL]
case mk.mk.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : Finset.card (support ↑{ val := σ, property := hσ✝ }) + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑{ val := σ, property := hσ✝ } ↑{ val := τ, property := hτ }
π : Perm α
hπ : π * ↑{ val := σ, property := hσ✝ } * π⁻¹ = ↑{ val := τ, property := hτ }
⊢ IsConj { val := σ, property := hσ✝ } { val := τ, property := hτ }
[PROOFSTEP]
rw [Subtype.coe_mk, Subtype.coe_mk] at hπ 
[GOAL]
case mk.mk.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : Finset.card (support ↑{ val := σ, property := hσ✝ }) + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑{ val := σ, property := hσ✝ } ↑{ val := τ, property := hτ }
π : Perm α
hπ : π * σ * π⁻¹ = τ
⊢ IsConj { val := σ, property := hσ✝ } { val := τ, property := hτ }
[PROOFSTEP]
cases' Int.units_eq_one_or (Perm.sign π) with h h
[GOAL]
case mk.mk.intro.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : Finset.card (support ↑{ val := σ, property := hσ✝ }) + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑{ val := σ, property := hσ✝ } ↑{ val := τ, property := hτ }
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : ↑sign π = 1
⊢ IsConj { val := σ, property := hσ✝ } { val := τ, property := hτ }
[PROOFSTEP]
rw [isConj_iff]
[GOAL]
case mk.mk.intro.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : Finset.card (support ↑{ val := σ, property := hσ✝ }) + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑{ val := σ, property := hσ✝ } ↑{ val := τ, property := hτ }
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : ↑sign π = 1
⊢ ∃ c, c * { val := σ, property := hσ✝ } * c⁻¹ = { val := τ, property := hτ }
[PROOFSTEP]
refine' ⟨⟨π, mem_alternatingGroup.mp h⟩, Subtype.val_injective _⟩
[GOAL]
case mk.mk.intro.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : Finset.card (support ↑{ val := σ, property := hσ✝ }) + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑{ val := σ, property := hσ✝ } ↑{ val := τ, property := hτ }
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : ↑sign π = 1
⊢ ↑({ val := π, property := (_ : ↑sign π = 1) } * { val := σ, property := hσ✝ } *
        { val := π, property := (_ : ↑sign π = 1) }⁻¹) =
    ↑{ val := τ, property := hτ }
[PROOFSTEP]
simpa only [Subtype.val, Subgroup.coe_mul, coe_inv, coe_mk] using hπ
[GOAL]
case mk.mk.intro.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : Finset.card (support ↑{ val := σ, property := hσ✝ }) + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑{ val := σ, property := hσ✝ } ↑{ val := τ, property := hτ }
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : ↑sign π = -1
⊢ IsConj { val := σ, property := hσ✝ } { val := τ, property := hτ }
[PROOFSTEP]
have h2 : 2 ≤ σ.supportᶜ.card :=
  by
  rw [Finset.card_compl, le_tsub_iff_left σ.support.card_le_univ]
  exact hσ
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : Finset.card (support ↑{ val := σ, property := hσ✝ }) + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑{ val := σ, property := hσ✝ } ↑{ val := τ, property := hτ }
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : ↑sign π = -1
⊢ 2 ≤ Finset.card (support σ)ᶜ
[PROOFSTEP]
rw [Finset.card_compl, le_tsub_iff_left σ.support.card_le_univ]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : Finset.card (support ↑{ val := σ, property := hσ✝ }) + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑{ val := σ, property := hσ✝ } ↑{ val := τ, property := hτ }
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : ↑sign π = -1
⊢ Finset.card (support σ) + 2 ≤ card α
[PROOFSTEP]
exact hσ
[GOAL]
case mk.mk.intro.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : Finset.card (support ↑{ val := σ, property := hσ✝ }) + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑{ val := σ, property := hσ✝ } ↑{ val := τ, property := hτ }
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : ↑sign π = -1
h2 : 2 ≤ Finset.card (support σ)ᶜ
⊢ IsConj { val := σ, property := hσ✝ } { val := τ, property := hτ }
[PROOFSTEP]
obtain ⟨a, ha, b, hb, ab⟩ := Finset.one_lt_card.1 h2
[GOAL]
case mk.mk.intro.inr.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : Finset.card (support ↑{ val := σ, property := hσ✝ }) + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑{ val := σ, property := hσ✝ } ↑{ val := τ, property := hτ }
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : ↑sign π = -1
h2 : 2 ≤ Finset.card (support σ)ᶜ
a : α
ha : a ∈ (support σ)ᶜ
b : α
hb : b ∈ (support σ)ᶜ
ab : a ≠ b
⊢ IsConj { val := σ, property := hσ✝ } { val := τ, property := hτ }
[PROOFSTEP]
refine' isConj_iff.2 ⟨⟨π * swap a b, _⟩, Subtype.val_injective _⟩
[GOAL]
case mk.mk.intro.inr.intro.intro.intro.intro.refine'_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : Finset.card (support ↑{ val := σ, property := hσ✝ }) + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑{ val := σ, property := hσ✝ } ↑{ val := τ, property := hτ }
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : ↑sign π = -1
h2 : 2 ≤ Finset.card (support σ)ᶜ
a : α
ha : a ∈ (support σ)ᶜ
b : α
hb : b ∈ (support σ)ᶜ
ab : a ≠ b
⊢ π * swap a b ∈ alternatingGroup α
[PROOFSTEP]
rw [mem_alternatingGroup, MonoidHom.map_mul, h, sign_swap ab, Int.units_mul_self]
[GOAL]
case mk.mk.intro.inr.intro.intro.intro.intro.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : Finset.card (support ↑{ val := σ, property := hσ✝ }) + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑{ val := σ, property := hσ✝ } ↑{ val := τ, property := hτ }
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : ↑sign π = -1
h2 : 2 ≤ Finset.card (support σ)ᶜ
a : α
ha : a ∈ (support σ)ᶜ
b : α
hb : b ∈ (support σ)ᶜ
ab : a ≠ b
⊢ ↑({ val := π * swap a b, property := (_ : π * swap a b ∈ alternatingGroup α) } * { val := σ, property := hσ✝ } *
        { val := π * swap a b, property := (_ : π * swap a b ∈ alternatingGroup α) }⁻¹) =
    ↑{ val := τ, property := hτ }
[PROOFSTEP]
simp only [← hπ, coe_mk, Subgroup.coe_mul, Subtype.val]
[GOAL]
case mk.mk.intro.inr.intro.intro.intro.intro.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : Finset.card (support ↑{ val := σ, property := hσ✝ }) + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑{ val := σ, property := hσ✝ } ↑{ val := τ, property := hτ }
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : ↑sign π = -1
h2 : 2 ≤ Finset.card (support σ)ᶜ
a : α
ha : a ∈ (support σ)ᶜ
b : α
hb : b ∈ (support σ)ᶜ
ab : a ≠ b
⊢ π * swap a b * σ * ↑{ val := π * swap a b, property := (_ : π * swap a b ∈ alternatingGroup α) }⁻¹ = π * σ * π⁻¹
[PROOFSTEP]
have hd : Disjoint (swap a b) σ :=
  by
  rw [disjoint_iff_disjoint_support, support_swap ab, Finset.disjoint_insert_left, Finset.disjoint_singleton_left]
  exact ⟨Finset.mem_compl.1 ha, Finset.mem_compl.1 hb⟩
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : Finset.card (support ↑{ val := σ, property := hσ✝ }) + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑{ val := σ, property := hσ✝ } ↑{ val := τ, property := hτ }
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : ↑sign π = -1
h2 : 2 ≤ Finset.card (support σ)ᶜ
a : α
ha : a ∈ (support σ)ᶜ
b : α
hb : b ∈ (support σ)ᶜ
ab : a ≠ b
⊢ Perm.Disjoint (swap a b) σ
[PROOFSTEP]
rw [disjoint_iff_disjoint_support, support_swap ab, Finset.disjoint_insert_left, Finset.disjoint_singleton_left]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : Finset.card (support ↑{ val := σ, property := hσ✝ }) + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑{ val := σ, property := hσ✝ } ↑{ val := τ, property := hτ }
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : ↑sign π = -1
h2 : 2 ≤ Finset.card (support σ)ᶜ
a : α
ha : a ∈ (support σ)ᶜ
b : α
hb : b ∈ (support σ)ᶜ
ab : a ≠ b
⊢ ¬a ∈ support σ ∧ ¬b ∈ support σ
[PROOFSTEP]
exact ⟨Finset.mem_compl.1 ha, Finset.mem_compl.1 hb⟩
[GOAL]
case mk.mk.intro.inr.intro.intro.intro.intro.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : Finset.card (support ↑{ val := σ, property := hσ✝ }) + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑{ val := σ, property := hσ✝ } ↑{ val := τ, property := hτ }
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : ↑sign π = -1
h2 : 2 ≤ Finset.card (support σ)ᶜ
a : α
ha : a ∈ (support σ)ᶜ
b : α
hb : b ∈ (support σ)ᶜ
ab : a ≠ b
hd : Perm.Disjoint (swap a b) σ
⊢ π * swap a b * σ * ↑{ val := π * swap a b, property := (_ : π * swap a b ∈ alternatingGroup α) }⁻¹ = π * σ * π⁻¹
[PROOFSTEP]
rw [mul_assoc π _ σ, hd.commute.eq, coe_inv, coe_mk]
[GOAL]
case mk.mk.intro.inr.intro.intro.intro.intro.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : Finset.card (support ↑{ val := σ, property := hσ✝ }) + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑{ val := σ, property := hσ✝ } ↑{ val := τ, property := hτ }
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : ↑sign π = -1
h2 : 2 ≤ Finset.card (support σ)ᶜ
a : α
ha : a ∈ (support σ)ᶜ
b : α
hb : b ∈ (support σ)ᶜ
ab : a ≠ b
hd : Perm.Disjoint (swap a b) σ
⊢ π * (σ * swap a b) * (π * swap a b)⁻¹ = π * σ * π⁻¹
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ card α
σ τ : { x // x ∈ alternatingGroup α }
hσ : IsThreeCycle ↑σ
hτ : IsThreeCycle ↑τ
⊢ Finset.card (support ↑σ) + 2 ≤ card α
[PROOFSTEP]
rwa [hσ.card_support]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
⊢ σ ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
suffices hind :
  ∀ (n : ℕ) (l : List (Perm α)) (_ : ∀ g, g ∈ l → IsSwap g) (_ : l.length = 2 * n),
    l.prod ∈ closure {σ : Perm α | IsThreeCycle σ}
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
hind :
  ∀ (n : ℕ) (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
⊢ σ ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
obtain ⟨l, rfl, hl⟩ := truncSwapFactors σ
[GOAL]
case mk.mk.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hind :
  ∀ (n : ℕ) (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ l → IsSwap g
hσ : List.prod l ∈ alternatingGroup α
x✝ : Trunc { l_1 // List.prod l_1 = List.prod l ∧ ∀ (g : Perm α), g ∈ l_1 → IsSwap g }
⊢ List.prod l ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
obtain ⟨n, hn⟩ := (prod_list_swap_mem_alternatingGroup_iff_even_length hl).1 hσ
[GOAL]
case mk.mk.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hind :
  ∀ (n : ℕ) (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ l → IsSwap g
hσ : List.prod l ∈ alternatingGroup α
x✝ : Trunc { l_1 // List.prod l_1 = List.prod l ∧ ∀ (g : Perm α), g ∈ l_1 → IsSwap g }
n : ℕ
hn : List.length l = n + n
⊢ List.prod l ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
rw [← two_mul] at hn 
[GOAL]
case mk.mk.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hind :
  ∀ (n : ℕ) (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ l → IsSwap g
hσ : List.prod l ∈ alternatingGroup α
x✝ : Trunc { l_1 // List.prod l_1 = List.prod l ∧ ∀ (g : Perm α), g ∈ l_1 → IsSwap g }
n : ℕ
hn : List.length l = 2 * n
⊢ List.prod l ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
exact hind n l hl hn
[GOAL]
case hind
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
⊢ ∀ (n : ℕ) (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
intro n
[GOAL]
case hind
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
⊢ ∀ (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
induction' n with n ih
[GOAL]
case hind.zero
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
⊢ ∀ (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * Nat.zero → List.prod l ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
intro l hl hn
[GOAL]
case hind.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih :
  ∀ (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
⊢ ∀ (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * Nat.succ n → List.prod l ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
intro l hl hn
[GOAL]
case hind.zero
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ l → IsSwap g
hn : List.length l = 2 * Nat.zero
⊢ List.prod l ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
simp [List.length_eq_zero.1 hn, one_mem]
[GOAL]
case hind.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih :
  ∀ (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ l → IsSwap g
hn : List.length l = 2 * Nat.succ n
⊢ List.prod l ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
rw [Nat.mul_succ] at hn 
[GOAL]
case hind.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih :
  ∀ (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ l → IsSwap g
hn : List.length l = 2 * n + 2
⊢ List.prod l ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
obtain ⟨a, l, rfl⟩ := l.exists_of_length_succ hn
[GOAL]
case hind.succ.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih :
  ∀ (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
a : Perm α
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ a :: l → IsSwap g
hn : List.length (a :: l) = 2 * n + 2
⊢ List.prod (a :: l) ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
rw [List.length_cons, Nat.succ_inj'] at hn 
[GOAL]
case hind.succ.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih :
  ∀ (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
a : Perm α
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ a :: l → IsSwap g
hn : List.length l = 2 * n + 1
⊢ List.prod (a :: l) ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
obtain ⟨b, l, rfl⟩ := l.exists_of_length_succ hn
[GOAL]
case hind.succ.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih :
  ∀ (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
a b : Perm α
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ a :: b :: l → IsSwap g
hn : List.length (b :: l) = 2 * n + 1
⊢ List.prod (a :: b :: l) ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
rw [List.prod_cons, List.prod_cons, ← mul_assoc]
[GOAL]
case hind.succ.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih :
  ∀ (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
a b : Perm α
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ a :: b :: l → IsSwap g
hn : List.length (b :: l) = 2 * n + 1
⊢ a * b * List.prod l ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
rw [List.length_cons, Nat.succ_inj'] at hn 
[GOAL]
case hind.succ.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih :
  ∀ (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
a b : Perm α
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ a :: b :: l → IsSwap g
hn : List.length l = 2 * n
⊢ a * b * List.prod l ∈ closure {σ | IsThreeCycle σ}
[PROOFSTEP]
exact
  mul_mem
    (IsSwap.mul_mem_closure_three_cycles (hl a (List.mem_cons_self a _))
      (hl b (List.mem_cons_of_mem a (l.mem_cons_self b))))
    (ih _ (fun g hg => hl g (List.mem_cons_of_mem _ (List.mem_cons_of_mem _ hg))) hn)
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ card α
f : Perm α
hf : IsThreeCycle f
⊢ ⊤ ≤ normalClosure {{ val := f, property := (_ : f ∈ alternatingGroup α) }}
[PROOFSTEP]
have hi : Function.Injective (alternatingGroup α).subtype := Subtype.coe_injective
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ card α
f : Perm α
hf : IsThreeCycle f
hi : Function.Injective ↑(Subgroup.subtype (alternatingGroup α))
⊢ ⊤ ≤ normalClosure {{ val := f, property := (_ : f ∈ alternatingGroup α) }}
[PROOFSTEP]
refine' eq_top_iff.1 (map_injective hi (le_antisymm (map_mono le_top) _))
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ card α
f : Perm α
hf : IsThreeCycle f
hi : Function.Injective ↑(Subgroup.subtype (alternatingGroup α))
⊢ map (Subgroup.subtype (alternatingGroup α)) ⊤ ≤
    map (Subgroup.subtype (alternatingGroup α)) (normalClosure {{ val := f, property := (_ : f ∈ alternatingGroup α) }})
[PROOFSTEP]
rw [← MonoidHom.range_eq_map, subtype_range, normalClosure, MonoidHom.map_closure]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ card α
f : Perm α
hf : IsThreeCycle f
hi : Function.Injective ↑(Subgroup.subtype (alternatingGroup α))
⊢ alternatingGroup α ≤
    closure
      (↑(Subgroup.subtype (alternatingGroup α)) ''
        Group.conjugatesOfSet {{ val := f, property := (_ : f ∈ alternatingGroup α) }})
[PROOFSTEP]
refine' (le_of_eq closure_three_cycles_eq_alternating.symm).trans (closure_mono _)
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ card α
f : Perm α
hf : IsThreeCycle f
hi : Function.Injective ↑(Subgroup.subtype (alternatingGroup α))
⊢ {σ | IsThreeCycle σ} ⊆
    ↑(Subgroup.subtype (alternatingGroup α)) ''
      Group.conjugatesOfSet {{ val := f, property := (_ : f ∈ alternatingGroup α) }}
[PROOFSTEP]
intro g h
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ card α
f : Perm α
hf : IsThreeCycle f
hi : Function.Injective ↑(Subgroup.subtype (alternatingGroup α))
g : Perm α
h : g ∈ {σ | IsThreeCycle σ}
⊢ g ∈
    ↑(Subgroup.subtype (alternatingGroup α)) ''
      Group.conjugatesOfSet {{ val := f, property := (_ : f ∈ alternatingGroup α) }}
[PROOFSTEP]
obtain ⟨c, rfl⟩ := isConj_iff.1 (isConj_iff_cycleType_eq.2 (hf.trans h.symm))
[GOAL]
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ card α
f : Perm α
hf : IsThreeCycle f
hi : Function.Injective ↑(Subgroup.subtype (alternatingGroup α))
c : Perm α
h : c * f * c⁻¹ ∈ {σ | IsThreeCycle σ}
⊢ c * f * c⁻¹ ∈
    ↑(Subgroup.subtype (alternatingGroup α)) ''
      Group.conjugatesOfSet {{ val := f, property := (_ : f ∈ alternatingGroup α) }}
[PROOFSTEP]
refine' ⟨⟨c * f * c⁻¹, h.mem_alternatingGroup⟩, _, rfl⟩
[GOAL]
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ card α
f : Perm α
hf : IsThreeCycle f
hi : Function.Injective ↑(Subgroup.subtype (alternatingGroup α))
c : Perm α
h : c * f * c⁻¹ ∈ {σ | IsThreeCycle σ}
⊢ { val := c * f * c⁻¹, property := (_ : c * f * c⁻¹ ∈ alternatingGroup α) } ∈
    Group.conjugatesOfSet {{ val := f, property := (_ : f ∈ alternatingGroup α) }}
[PROOFSTEP]
rw [Group.mem_conjugatesOfSet_iff]
[GOAL]
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ card α
f : Perm α
hf : IsThreeCycle f
hi : Function.Injective ↑(Subgroup.subtype (alternatingGroup α))
c : Perm α
h : c * f * c⁻¹ ∈ {σ | IsThreeCycle σ}
⊢ ∃ a,
    a ∈ {{ val := f, property := (_ : f ∈ alternatingGroup α) }} ∧
      IsConj a { val := c * f * c⁻¹, property := (_ : c * f * c⁻¹ ∈ alternatingGroup α) }
[PROOFSTEP]
exact ⟨⟨f, hf.mem_alternatingGroup⟩, Set.mem_singleton _, isThreeCycle_isConj h5 hf h⟩
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
h : 3 ∈ cycleType g
⊢ IsThreeCycle (g * g)
[PROOFSTEP]
obtain ⟨c, g', rfl, hd, _, h3⟩ := mem_cycleType_iff.1 h
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm (Fin 5)
h : 3 ∈ cycleType (c * g')
hd : Disjoint c g'
left✝ : IsCycle c
h3 : Finset.card (support c) = 3
⊢ IsThreeCycle (c * g' * (c * g'))
[PROOFSTEP]
simp only [mul_assoc]
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm (Fin 5)
h : 3 ∈ cycleType (c * g')
hd : Disjoint c g'
left✝ : IsCycle c
h3 : Finset.card (support c) = 3
⊢ IsThreeCycle (c * (g' * (c * g')))
[PROOFSTEP]
rw [hd.commute.eq, ← mul_assoc g']
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm (Fin 5)
h : 3 ∈ cycleType (c * g')
hd : Disjoint c g'
left✝ : IsCycle c
h3 : Finset.card (support c) = 3
⊢ IsThreeCycle (c * (g' * g' * c))
[PROOFSTEP]
suffices hg' : orderOf g' ∣ 2
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm (Fin 5)
h : 3 ∈ cycleType (c * g')
hd : Disjoint c g'
left✝ : IsCycle c
h3 : Finset.card (support c) = 3
hg' : orderOf g' ∣ 2
⊢ IsThreeCycle (c * (g' * g' * c))
[PROOFSTEP]
rw [← pow_two, orderOf_dvd_iff_pow_eq_one.1 hg', one_mul]
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm (Fin 5)
h : 3 ∈ cycleType (c * g')
hd : Disjoint c g'
left✝ : IsCycle c
h3 : Finset.card (support c) = 3
hg' : orderOf g' ∣ 2
⊢ IsThreeCycle (c * c)
[PROOFSTEP]
exact (card_support_eq_three_iff.1 h3).isThreeCycle_sq
[GOAL]
case hg'
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm (Fin 5)
h : 3 ∈ cycleType (c * g')
hd : Disjoint c g'
left✝ : IsCycle c
h3 : Finset.card (support c) = 3
⊢ orderOf g' ∣ 2
[PROOFSTEP]
rw [← lcm_cycleType, Multiset.lcm_dvd]
[GOAL]
case hg'
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm (Fin 5)
h : 3 ∈ cycleType (c * g')
hd : Disjoint c g'
left✝ : IsCycle c
h3 : Finset.card (support c) = 3
⊢ ∀ (b : ℕ), b ∈ cycleType g' → b ∣ 2
[PROOFSTEP]
intro n hn
[GOAL]
case hg'
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm (Fin 5)
h : 3 ∈ cycleType (c * g')
hd : Disjoint c g'
left✝ : IsCycle c
h3 : Finset.card (support c) = 3
n : ℕ
hn : n ∈ cycleType g'
⊢ n ∣ 2
[PROOFSTEP]
rw [le_antisymm (two_le_of_mem_cycleType hn) (le_trans (le_card_support_of_mem_cycleType hn) _)]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm (Fin 5)
h : 3 ∈ cycleType (c * g')
hd : Disjoint c g'
left✝ : IsCycle c
h3 : Finset.card (support c) = 3
n : ℕ
hn : n ∈ cycleType g'
⊢ Finset.card (support g') ≤ 2
[PROOFSTEP]
apply le_of_add_le_add_left
[GOAL]
case bc
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm (Fin 5)
h : 3 ∈ cycleType (c * g')
hd : Disjoint c g'
left✝ : IsCycle c
h3 : Finset.card (support c) = 3
n : ℕ
hn : n ∈ cycleType g'
⊢ ?a + Finset.card (support g') ≤ ?a + 2
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm (Fin 5)
h : 3 ∈ cycleType (c * g')
hd : Disjoint c g'
left✝ : IsCycle c
h3 : Finset.card (support c) = 3
n : ℕ
hn : n ∈ cycleType g'
⊢ ℕ
[PROOFSTEP]
rw [← hd.card_support_mul, h3]
[GOAL]
case bc
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c g' : Perm (Fin 5)
h : 3 ∈ cycleType (c * g')
hd : Disjoint c g'
left✝ : IsCycle c
h3 : Finset.card (support c) = 3
n : ℕ
hn : n ∈ cycleType g'
⊢ Finset.card (support (c * g')) ≤ 3 + 2
[PROOFSTEP]
exact (c * g').support.card_le_univ
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : 3 ≤ card α
⊢ Nontrivial { x // x ∈ alternatingGroup α }
[PROOFSTEP]
haveI := Fintype.one_lt_card_iff_nontrivial.1 (lt_trans (by decide) h3)
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : 3 ≤ card α
⊢ 1 < 2
[PROOFSTEP]
decide
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : 3 ≤ card α
this : Nontrivial α
⊢ Nontrivial { x // x ∈ alternatingGroup α }
[PROOFSTEP]
rw [← Fintype.one_lt_card_iff_nontrivial]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : 3 ≤ card α
this : Nontrivial α
⊢ 1 < card { x // x ∈ alternatingGroup α }
[PROOFSTEP]
refine' lt_of_mul_lt_mul_left _ (le_of_lt Nat.prime_two.pos)
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : 3 ≤ card α
this : Nontrivial α
⊢ 2 * 1 < 2 * card { x // x ∈ alternatingGroup α }
[PROOFSTEP]
rw [two_mul_card_alternatingGroup, card_perm, ← Nat.succ_le_iff]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : 3 ≤ card α
this : Nontrivial α
⊢ Nat.succ (2 * 1) ≤ Nat.factorial (card α)
[PROOFSTEP]
exact le_trans h3 (card α).self_le_factorial
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
⊢ 3 ≤ card (Fin (n + 3))
[PROOFSTEP]
rw [card_fin]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
⊢ 3 ≤ n + 3
[PROOFSTEP]
exact le_add_left (le_refl 3)
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ ⊤ ≤ normalClosure {{ val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) }}
[PROOFSTEP]
have h3 : IsThreeCycle (Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹) :=
  card_support_eq_three_iff.1 (by decide)
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ Finset.card (support (Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹)) = 3
[PROOFSTEP]
decide
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : IsThreeCycle (Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹)
⊢ ⊤ ≤ normalClosure {{ val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) }}
[PROOFSTEP]
rw [← h3.alternating_normalClosure (by rw [card_fin])]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : IsThreeCycle (Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹)
⊢ 5 ≤ card (Fin 5)
[PROOFSTEP]
rw [card_fin]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : IsThreeCycle (Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹)
⊢ normalClosure
      {{ val := Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹,
          property :=
            (_ :
              Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹ ∈ alternatingGroup (Fin 5)) }} ≤
    normalClosure {{ val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) }}
[PROOFSTEP]
refine' normalClosure_le_normal _
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : IsThreeCycle (Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹)
⊢ {{ val := Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹,
        property :=
          (_ : Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹ ∈ alternatingGroup (Fin 5)) }} ⊆
    ↑(normalClosure {{ val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) }})
[PROOFSTEP]
rw [Set.singleton_subset_iff, SetLike.mem_coe]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : IsThreeCycle (Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹)
⊢ { val := Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹,
      property :=
        (_ : Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹ ∈ alternatingGroup (Fin 5)) } ∈
    normalClosure {{ val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) }}
[PROOFSTEP]
have h : (⟨finRotate 5, finRotate_bit1_mem_alternatingGroup (n := 2)⟩ : alternatingGroup (Fin 5)) ∈ normalClosure _ :=
  SetLike.mem_coe.1 (subset_normalClosure (Set.mem_singleton _))
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : IsThreeCycle (Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹)
h :
  { val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) } ∈
    normalClosure {{ val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) }}
⊢ { val := Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹,
      property :=
        (_ : Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹ ∈ alternatingGroup (Fin 5)) } ∈
    normalClosure {{ val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) }}
[PROOFSTEP]
exact
  (mul_mem
      (Subgroup.normalClosure_normal.conj_mem _ h
        ⟨Fin.cycleRange 2, Fin.isThreeCycle_cycleRange_two.mem_alternatingGroup⟩)
      (inv_mem h)
        --Porting note : added `: _` :
    _)
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ ↑sign (swap 0 4 * swap 1 3) = 1
[PROOFSTEP]
decide
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ normalClosure {{ val := swap 0 4 * swap 1 3, property := (_ : swap 0 4 * swap 1 3 ∈ alternatingGroup (Fin 5)) }} = ⊤
[PROOFSTEP]
let g1 := (⟨swap 0 2 * swap 0 1, mem_alternatingGroup.2 (by decide)⟩ : alternatingGroup (Fin 5))
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ ↑sign (swap 0 2 * swap 0 1) = 1
[PROOFSTEP]
decide
[GOAL]
α : Type u_1
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)) }} = ⊤
[PROOFSTEP]
let g2 := (⟨swap 0 4 * swap 1 3, mem_alternatingGroup.2 (by decide)⟩ : alternatingGroup (Fin 5))
[GOAL]
α : Type u_1
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
[PROOFSTEP]
decide
[GOAL]
α : Type u_1
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)) }} = ⊤
[PROOFSTEP]
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]
[GOAL]
α : Type u_1
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))) }
[PROOFSTEP]
rw [Subtype.ext_iff]
[GOAL]
α : Type u_1
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))) }
[PROOFSTEP]
simp only [Fin.val_mk, Subgroup.coe_mul, Subgroup.coe_inv, Fin.val_mk]
[GOAL]
α : Type u_1
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)) }} = ⊤
[PROOFSTEP]
rw [eq_top_iff, ← normalClosure_finRotate_five]
[GOAL]
α : Type u_1
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)) }}
[PROOFSTEP]
refine' normalClosure_le_normal _
[GOAL]
α : Type u_1
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)) }})
[PROOFSTEP]
rw [Set.singleton_subset_iff, SetLike.mem_coe, ← h5]
[GOAL]
α : Type u_1
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)) }}
[PROOFSTEP]
have h : g2 ∈ normalClosure { g2 } := SetLike.mem_coe.1 (subset_normalClosure (Set.mem_singleton _))
[GOAL]
α : Type u_1
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)) }}
[PROOFSTEP]
exact mul_mem (Subgroup.normalClosure_normal.conj_mem _ h g1) (inv_mem h)
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
ha : g ∈ alternatingGroup (Fin 5)
h1 : g ≠ 1
h2 : ∀ (n : ℕ), n ∈ cycleType g → n = 2
⊢ IsConj (swap 0 4 * swap 1 3) g
[PROOFSTEP]
have h := g.support.card_le_univ
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
ha : g ∈ alternatingGroup (Fin 5)
h1 : g ≠ 1
h2 : ∀ (n : ℕ), n ∈ cycleType g → n = 2
h : Finset.card (support g) ≤ card (Fin 5)
⊢ IsConj (swap 0 4 * swap 1 3) g
[PROOFSTEP]
rw [← Multiset.eq_replicate_card] at h2 
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
ha : g ∈ alternatingGroup (Fin 5)
h1 : g ≠ 1
h2 : cycleType g = Multiset.replicate (↑Multiset.card (cycleType g)) 2
h : Finset.card (support g) ≤ card (Fin 5)
⊢ IsConj (swap 0 4 * swap 1 3) g
[PROOFSTEP]
rw [← sum_cycleType, h2, Multiset.sum_replicate, smul_eq_mul] at h 
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
ha : g ∈ alternatingGroup (Fin 5)
h1 : g ≠ 1
h2 : cycleType g = Multiset.replicate (↑Multiset.card (cycleType g)) 2
h : ↑Multiset.card (cycleType g) * 2 ≤ card (Fin 5)
⊢ IsConj (swap 0 4 * swap 1 3) g
[PROOFSTEP]
have h : Multiset.card g.cycleType ≤ 3 :=
  le_of_mul_le_mul_right (le_trans h (by simp only [card_fin]; ring_nf)) (by simp)
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
ha : g ∈ alternatingGroup (Fin 5)
h1 : g ≠ 1
h2 : cycleType g = Multiset.replicate (↑Multiset.card (cycleType g)) 2
h : ↑Multiset.card (cycleType g) * 2 ≤ card (Fin 5)
⊢ card (Fin 5) ≤ 3 * 2
[PROOFSTEP]
simp only [card_fin]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
ha : g ∈ alternatingGroup (Fin 5)
h1 : g ≠ 1
h2 : cycleType g = Multiset.replicate (↑Multiset.card (cycleType g)) 2
h : ↑Multiset.card (cycleType g) * 2 ≤ card (Fin 5)
⊢ 5 ≤ 3 * 2
[PROOFSTEP]
ring_nf
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
ha : g ∈ alternatingGroup (Fin 5)
h1 : g ≠ 1
h2 : cycleType g = Multiset.replicate (↑Multiset.card (cycleType g)) 2
h : ↑Multiset.card (cycleType g) * 2 ≤ card (Fin 5)
⊢ 0 < 2
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
ha : g ∈ alternatingGroup (Fin 5)
h1 : g ≠ 1
h2 : cycleType g = Multiset.replicate (↑Multiset.card (cycleType g)) 2
h✝ : ↑Multiset.card (cycleType g) * 2 ≤ card (Fin 5)
h : ↑Multiset.card (cycleType g) ≤ 3
⊢ IsConj (swap 0 4 * swap 1 3) g
[PROOFSTEP]
rw [mem_alternatingGroup, sign_of_cycleType, h2] at ha 
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
ha :
  (-1) ^
      (Multiset.sum (Multiset.replicate (↑Multiset.card (cycleType g)) 2) +
        ↑Multiset.card (Multiset.replicate (↑Multiset.card (cycleType g)) 2)) =
    1
h1 : g ≠ 1
h2 : cycleType g = Multiset.replicate (↑Multiset.card (cycleType g)) 2
h✝ : ↑Multiset.card (cycleType g) * 2 ≤ card (Fin 5)
h : ↑Multiset.card (cycleType g) ≤ 3
⊢ IsConj (swap 0 4 * swap 1 3) g
[PROOFSTEP]
norm_num at ha 
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
h1 : g ≠ 1
h2 : cycleType g = Multiset.replicate (↑Multiset.card (cycleType g)) 2
h✝ : ↑Multiset.card (cycleType g) * 2 ≤ card (Fin 5)
h : ↑Multiset.card (cycleType g) ≤ 3
ha : (-1) ^ (↑Multiset.card (cycleType g) * 2 + ↑Multiset.card (cycleType g)) = 1
⊢ IsConj (swap 0 4 * swap 1 3) g
[PROOFSTEP]
rw [pow_add, pow_mul, Int.units_pow_two, one_mul, Units.ext_iff, Units.val_one, Units.val_pow_eq_pow_val,
  Units.coe_neg_one, neg_one_pow_eq_one_iff_even _] at ha 
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
h1 : g ≠ 1
h2 : cycleType g = Multiset.replicate (↑Multiset.card (cycleType g)) 2
h✝ : ↑Multiset.card (cycleType g) * 2 ≤ card (Fin 5)
h : ↑Multiset.card (cycleType g) ≤ 3
ha : Even (↑Multiset.card (cycleType g))
⊢ IsConj (swap 0 4 * swap 1 3) g
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
h1 : g ≠ 1
h2 : cycleType g = Multiset.replicate (↑Multiset.card (cycleType g)) 2
h✝ : ↑Multiset.card (cycleType g) * 2 ≤ card (Fin 5)
h : ↑Multiset.card (cycleType g) ≤ 3
ha : (-1) ^ ↑Multiset.card (cycleType g) = 1
⊢ -1 ≠ 1
[PROOFSTEP]
swap
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
h1 : g ≠ 1
h2 : cycleType g = Multiset.replicate (↑Multiset.card (cycleType g)) 2
h✝ : ↑Multiset.card (cycleType g) * 2 ≤ card (Fin 5)
h : ↑Multiset.card (cycleType g) ≤ 3
ha : (-1) ^ ↑Multiset.card (cycleType g) = 1
⊢ -1 ≠ 1
[PROOFSTEP]
decide
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
h1 : g ≠ 1
h2 : cycleType g = Multiset.replicate (↑Multiset.card (cycleType g)) 2
h✝ : ↑Multiset.card (cycleType g) * 2 ≤ card (Fin 5)
h : ↑Multiset.card (cycleType g) ≤ 3
ha : Even (↑Multiset.card (cycleType g))
⊢ IsConj (swap 0 4 * swap 1 3) g
[PROOFSTEP]
rw [isConj_iff_cycleType_eq, h2]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
h1 : g ≠ 1
h2 : cycleType g = Multiset.replicate (↑Multiset.card (cycleType g)) 2
h✝ : ↑Multiset.card (cycleType g) * 2 ≤ card (Fin 5)
h : ↑Multiset.card (cycleType g) ≤ 3
ha : Even (↑Multiset.card (cycleType g))
⊢ cycleType (swap 0 4 * swap 1 3) = Multiset.replicate (↑Multiset.card (cycleType g)) 2
[PROOFSTEP]
interval_cases h_1 : Multiset.card g.cycleType
[GOAL]
case «0»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : ↑Multiset.card (cycleType g) = 0
h2 : cycleType g = Multiset.replicate 0 2
h✝ : 0 * 2 ≤ card (Fin 5)
h : 0 ≤ 3
ha : Even 0
⊢ cycleType (swap 0 4 * swap 1 3) = Multiset.replicate 0 2
[PROOFSTEP]
exact (h1 (card_cycleType_eq_zero.1 h_1)).elim
[GOAL]
case «1»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : ↑Multiset.card (cycleType g) = 1
h2 : cycleType g = Multiset.replicate 1 2
h✝ : 1 * 2 ≤ card (Fin 5)
h : 1 ≤ 3
ha : Even 1
⊢ cycleType (swap 0 4 * swap 1 3) = Multiset.replicate 1 2
[PROOFSTEP]
contrapose! ha
[GOAL]
case «1»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : ↑Multiset.card (cycleType g) = 1
h2 : cycleType g = Multiset.replicate 1 2
h✝ : 1 * 2 ≤ card (Fin 5)
h : 1 ≤ 3
ha : cycleType (swap 0 4 * swap 1 3) ≠ Multiset.replicate 1 2
⊢ ¬Even 1
[PROOFSTEP]
simp [h_1]
[GOAL]
case «2»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : ↑Multiset.card (cycleType g) = 2
h2 : cycleType g = Multiset.replicate 2 2
h✝ : 2 * 2 ≤ card (Fin 5)
h : 2 ≤ 3
ha : Even 2
⊢ cycleType (swap 0 4 * swap 1 3) = Multiset.replicate 2 2
[PROOFSTEP]
have h04 : (0 : Fin 5) ≠ 4 := by decide
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : ↑Multiset.card (cycleType g) = 2
h2 : cycleType g = Multiset.replicate 2 2
h✝ : 2 * 2 ≤ card (Fin 5)
h : 2 ≤ 3
ha : Even 2
⊢ 0 ≠ 4
[PROOFSTEP]
decide
[GOAL]
case «2»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : ↑Multiset.card (cycleType g) = 2
h2 : cycleType g = Multiset.replicate 2 2
h✝ : 2 * 2 ≤ card (Fin 5)
h : 2 ≤ 3
ha : Even 2
h04 : 0 ≠ 4
⊢ cycleType (swap 0 4 * swap 1 3) = Multiset.replicate 2 2
[PROOFSTEP]
have h13 : (1 : Fin 5) ≠ 3 := by decide
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : ↑Multiset.card (cycleType g) = 2
h2 : cycleType g = Multiset.replicate 2 2
h✝ : 2 * 2 ≤ card (Fin 5)
h : 2 ≤ 3
ha : Even 2
h04 : 0 ≠ 4
⊢ 1 ≠ 3
[PROOFSTEP]
decide
[GOAL]
case «2»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : ↑Multiset.card (cycleType g) = 2
h2 : cycleType g = Multiset.replicate 2 2
h✝ : 2 * 2 ≤ card (Fin 5)
h : 2 ≤ 3
ha : Even 2
h04 : 0 ≠ 4
h13 : 1 ≠ 3
⊢ cycleType (swap 0 4 * swap 1 3) = Multiset.replicate 2 2
[PROOFSTEP]
rw [Disjoint.cycleType, (isCycle_swap h04).cycleType, (isCycle_swap h13).cycleType, card_support_swap h04,
  card_support_swap h13]
[GOAL]
case «2»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : ↑Multiset.card (cycleType g) = 2
h2 : cycleType g = Multiset.replicate 2 2
h✝ : 2 * 2 ≤ card (Fin 5)
h : 2 ≤ 3
ha : Even 2
h04 : 0 ≠ 4
h13 : 1 ≠ 3
⊢ ↑[2] + ↑[2] = Multiset.replicate 2 2
[PROOFSTEP]
rfl
[GOAL]
case «2»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : ↑Multiset.card (cycleType g) = 2
h2 : cycleType g = Multiset.replicate 2 2
h✝ : 2 * 2 ≤ card (Fin 5)
h : 2 ≤ 3
ha : Even 2
h04 : 0 ≠ 4
h13 : 1 ≠ 3
⊢ Perm.Disjoint (swap 0 4) (swap 1 3)
[PROOFSTEP]
rw [disjoint_iff_disjoint_support, support_swap h04, support_swap h13]
[GOAL]
case «2»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : ↑Multiset.card (cycleType g) = 2
h2 : cycleType g = Multiset.replicate 2 2
h✝ : 2 * 2 ≤ card (Fin 5)
h : 2 ≤ 3
ha : Even 2
h04 : 0 ≠ 4
h13 : 1 ≠ 3
⊢ _root_.Disjoint {0, 4} {1, 3}
[PROOFSTEP]
decide
[GOAL]
case «3»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : ↑Multiset.card (cycleType g) = 3
h2 : cycleType g = Multiset.replicate 3 2
h✝ : 3 * 2 ≤ card (Fin 5)
h : 3 ≤ 3
ha : Even 3
⊢ cycleType (swap 0 4 * swap 1 3) = Multiset.replicate 3 2
[PROOFSTEP]
contrapose! ha
[GOAL]
case «3»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : ↑Multiset.card (cycleType g) = 3
h2 : cycleType g = Multiset.replicate 3 2
h✝ : 3 * 2 ≤ card (Fin 5)
h : 3 ≤ 3
ha : cycleType (swap 0 4 * swap 1 3) ≠ Multiset.replicate 3 2
⊢ ¬Even 3
[PROOFSTEP]
simp [h_1]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
⊢ Normal H → H = ⊥ ∨ H = ⊤
[PROOFSTEP]
intro Hn
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
⊢ H = ⊥ ∨ H = ⊤
[PROOFSTEP]
refine' or_not.imp id fun Hb => _
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
Hb : ¬H = ⊥
⊢ H = ⊤
[PROOFSTEP]
rw [eq_bot_iff_forall] at Hb 
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
Hb : ¬∀ (x : { x // x ∈ alternatingGroup (Fin 5) }), x ∈ H → x = 1
⊢ H = ⊤
[PROOFSTEP]
push_neg at Hb 
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
Hb : ∃ x, x ∈ H ∧ x ≠ 1
⊢ H = ⊤
[PROOFSTEP]
obtain ⟨⟨g, gA⟩, gH, g1⟩ : ∃ x : ↥(alternatingGroup (Fin 5)), x ∈ H ∧ x ≠ 1 := Hb
[GOAL]
case intro.mk.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : { val := g, property := gA } ∈ H
g1 : { val := g, property := gA } ≠ 1
⊢ H = ⊤
[PROOFSTEP]
rw [← SetLike.mem_coe, ← Set.singleton_subset_iff] at gH 
[GOAL]
case intro.mk.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
⊢ H = ⊤
[PROOFSTEP]
refine'
  eq_top_iff.2
    (le_trans (ge_of_eq _) (normalClosure_le_normal gH))
      -- It suffices to show that the normal closure of `g` in $A_5$ is $A_5$.
[GOAL]
case intro.mk.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
⊢ normalClosure {{ val := g, property := gA }} = ⊤
[PROOFSTEP]
by_cases h2 :
  ∀ n ∈ g.cycleType,
    n =
      2
        -- If the cycle decomposition of `g` consists entirely of swaps, then the cycle type is $(2,2)$.
            -- This means that it is conjugate to $(04)(13)$, whose normal closure is $A_5$.
[GOAL]
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
h2 : ∀ (n : ℕ), n ∈ cycleType g → n = 2
⊢ normalClosure {{ val := g, property := gA }} = ⊤
[PROOFSTEP]
rw [Ne.def, Subtype.ext_iff] at g1 
[GOAL]
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : ¬↑{ val := g, property := gA } = ↑1
h2 : ∀ (n : ℕ), n ∈ cycleType g → n = 2
⊢ normalClosure {{ val := g, property := gA }} = ⊤
[PROOFSTEP]
exact (isConj_swap_mul_swap_of_cycleType_two gA g1 h2).normalClosure_eq_top_of normalClosure_swap_mul_swap_five
[GOAL]
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
h2 : ¬∀ (n : ℕ), n ∈ cycleType g → n = 2
⊢ normalClosure {{ val := g, property := gA }} = ⊤
[PROOFSTEP]
push_neg at h2 
[GOAL]
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
h2 : ∃ n, n ∈ cycleType g ∧ n ≠ 2
⊢ normalClosure {{ val := g, property := gA }} = ⊤
[PROOFSTEP]
obtain ⟨n, ng, n2⟩ : ∃ n : ℕ, n ∈ g.cycleType ∧ n ≠ 2 := h2
[GOAL]
case neg.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : n ∈ cycleType g
n2 : n ≠ 2
⊢ normalClosure {{ val := g, property := gA }} = ⊤
[PROOFSTEP]
have n2' : 2 < n := lt_of_le_of_ne (two_le_of_mem_cycleType ng) n2.symm
[GOAL]
case neg.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : n ∈ cycleType g
n2 : n ≠ 2
n2' : 2 < n
⊢ normalClosure {{ val := g, property := gA }} = ⊤
[PROOFSTEP]
have n5 : n ≤ 5 := le_trans ?_ g.support.card_le_univ
[GOAL]
case neg.intro.intro.refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : n ∈ cycleType g
n2 : n ≠ 2
n2' : 2 < n
n5 : n ≤ 5
⊢ normalClosure {{ val := g, property := gA }} = ⊤
case neg.intro.intro.refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : n ∈ cycleType g
n2 : n ≠ 2
n2' : 2 < n
⊢ n ≤ Finset.card (support g)
[PROOFSTEP]
swap
[GOAL]
case neg.intro.intro.refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : n ∈ cycleType g
n2 : n ≠ 2
n2' : 2 < n
⊢ n ≤ Finset.card (support g)
[PROOFSTEP]
obtain ⟨m, hm⟩ := Multiset.exists_cons_of_mem ng
[GOAL]
case neg.intro.intro.refine_1.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : n ∈ cycleType g
n2 : n ≠ 2
n2' : 2 < n
m : Multiset ℕ
hm : cycleType g = n ::ₘ m
⊢ n ≤ Finset.card (support g)
[PROOFSTEP]
rw [← sum_cycleType, hm, Multiset.sum_cons]
[GOAL]
case neg.intro.intro.refine_1.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : n ∈ cycleType g
n2 : n ≠ 2
n2' : 2 < n
m : Multiset ℕ
hm : cycleType g = n ::ₘ m
⊢ n ≤ n + Multiset.sum m
[PROOFSTEP]
exact le_add_right le_rfl
[GOAL]
case neg.intro.intro.refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : n ∈ cycleType g
n2 : n ≠ 2
n2' : 2 < n
n5 : n ≤ 5
⊢ normalClosure {{ val := g, property := gA }} = ⊤
[PROOFSTEP]
interval_cases n
[GOAL]
case neg.intro.intro.refine_2.«3»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : 3 ∈ cycleType g
n2 : 3 ≠ 2
n2' : 2 < 3
n5 : 3 ≤ 5
⊢ normalClosure {{ val := g, property := gA }} = ⊤
[PROOFSTEP]
rw [eq_top_iff, ← (isThreeCycle_sq_of_three_mem_cycleType_five ng).alternating_normalClosure (by rw [card_fin])]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : 3 ∈ cycleType g
n2 : 3 ≠ 2
n2' : 2 < 3
n5 : 3 ≤ 5
⊢ 5 ≤ card (Fin 5)
[PROOFSTEP]
rw [card_fin]
[GOAL]
case neg.intro.intro.refine_2.«3»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : 3 ∈ cycleType g
n2 : 3 ≠ 2
n2' : 2 < 3
n5 : 3 ≤ 5
⊢ normalClosure {{ val := g * g, property := (_ : g * g ∈ alternatingGroup (Fin 5)) }} ≤
    normalClosure {{ val := g, property := gA }}
[PROOFSTEP]
refine' normalClosure_le_normal _
[GOAL]
case neg.intro.intro.refine_2.«3»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : 3 ∈ cycleType g
n2 : 3 ≠ 2
n2' : 2 < 3
n5 : 3 ≤ 5
⊢ {{ val := g * g, property := (_ : g * g ∈ alternatingGroup (Fin 5)) }} ⊆
    ↑(normalClosure {{ val := g, property := gA }})
[PROOFSTEP]
rw [Set.singleton_subset_iff, SetLike.mem_coe]
[GOAL]
case neg.intro.intro.refine_2.«3»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : 3 ∈ cycleType g
n2 : 3 ≠ 2
n2' : 2 < 3
n5 : 3 ≤ 5
⊢ { val := g * g, property := (_ : g * g ∈ alternatingGroup (Fin 5)) } ∈ normalClosure {{ val := g, property := gA }}
[PROOFSTEP]
have h := SetLike.mem_coe.1 (subset_normalClosure (G := alternatingGroup (Fin 5)) (Set.mem_singleton ⟨g, gA⟩))
[GOAL]
case neg.intro.intro.refine_2.«3»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : 3 ∈ cycleType g
n2 : 3 ≠ 2
n2' : 2 < 3
n5 : 3 ≤ 5
h : { val := g, property := gA } ∈ normalClosure {{ val := g, property := gA }}
⊢ { val := g * g, property := (_ : g * g ∈ alternatingGroup (Fin 5)) } ∈ normalClosure {{ val := g, property := gA }}
[PROOFSTEP]
exact mul_mem h h
[GOAL]
case neg.intro.intro.refine_2.«4»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : 4 ∈ cycleType g
n2 : 4 ≠ 2
n2' : 2 < 4
n5 : 4 ≤ 5
⊢ normalClosure {{ val := g, property := gA }} = ⊤
[PROOFSTEP]
have con := mem_alternatingGroup.1 gA
[GOAL]
case neg.intro.intro.refine_2.«4»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : 4 ∈ cycleType g
n2 : 4 ≠ 2
n2' : 2 < 4
n5 : 4 ≤ 5
con : ↑sign g = 1
⊢ normalClosure {{ val := g, property := gA }} = ⊤
[PROOFSTEP]
contrapose! con
[GOAL]
case neg.intro.intro.refine_2.«4»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : 4 ∈ cycleType g
n2 : 4 ≠ 2
n2' : 2 < 4
n5 : 4 ≤ 5
con : normalClosure {{ val := g, property := gA }} ≠ ⊤
⊢ ↑sign g ≠ 1
[PROOFSTEP]
rw [sign_of_cycleType, cycleType_of_card_le_mem_cycleType_add_two (by decide) ng]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : 4 ∈ cycleType g
n2 : 4 ≠ 2
n2' : 2 < 4
n5 : 4 ≤ 5
con : normalClosure {{ val := g, property := gA }} ≠ ⊤
⊢ card (Fin 5) < 4 + 2
[PROOFSTEP]
decide
[GOAL]
case neg.intro.intro.refine_2.«4»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : 4 ∈ cycleType g
n2 : 4 ≠ 2
n2' : 2 < 4
n5 : 4 ≤ 5
con : normalClosure {{ val := g, property := gA }} ≠ ⊤
⊢ (-1) ^ (Multiset.sum {4} + ↑Multiset.card {4}) ≠ 1
[PROOFSTEP]
dsimp only
[GOAL]
case neg.intro.intro.refine_2.«4»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : 4 ∈ cycleType g
n2 : 4 ≠ 2
n2' : 2 < 4
n5 : 4 ≤ 5
con : normalClosure {{ val := g, property := gA }} ≠ ⊤
⊢ (-1) ^ (Multiset.sum {4} + ↑Multiset.card {4}) ≠ 1
[PROOFSTEP]
decide
[GOAL]
case neg.intro.intro.refine_2.«5»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : 5 ∈ cycleType g
n2 : 5 ≠ 2
n2' : 2 < 5
n5 : 5 ≤ 5
⊢ normalClosure {{ val := g, property := gA }} = ⊤
[PROOFSTEP]
refine' (isConj_iff_cycleType_eq.2 _).normalClosure_eq_top_of normalClosure_finRotate_five
[GOAL]
case neg.intro.intro.refine_2.«5»
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : 5 ∈ cycleType g
n2 : 5 ≠ 2
n2' : 2 < 5
n5 : 5 ≤ 5
⊢ cycleType (finRotate 5) = cycleType g
[PROOFSTEP]
rw [cycleType_of_card_le_mem_cycleType_add_two (by decide) ng, cycleType_finRotate]
[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup { x // x ∈ alternatingGroup (Fin 5) }
Hn : Normal H
g : Perm (Fin 5)
gA : g ∈ alternatingGroup (Fin 5)
gH : {{ val := g, property := gA }} ⊆ ↑H
g1 : { val := g, property := gA } ≠ 1
n : ℕ
ng : 5 ∈ cycleType g
n2 : 5 ≠ 2
n2' : 2 < 5
n5 : 5 ≤ 5
⊢ card (Fin 5) < 5 + 2
[PROOFSTEP]
decide
