-- Mathlib/GroupTheory/SpecificGroups/Alternating.lean
theorem IsThreeCycle.alternating_normalClosure (h5 : 5 ≤ Fintype.card α) {f : Perm α}
    (hf : IsThreeCycle f) :
    normalClosure ({⟨f, hf.mem_alternatingGroup⟩} : Set (alternatingGroup α)) = ⊤ :=
  eq_top_iff.2
    (by
      have hi : Function.Injective (alternatingGroup α).subtype := Subtype.coe_injective
      refine eq_top_iff.1 (map_injective hi (le_antisymm (map_mono le_top) ?_))
      rw [← MonoidHom.range_eq_map, range_subtype, normalClosure, MonoidHom.map_closure]
      refine (le_of_eq closure_three_cycles_eq_alternating.symm).trans (closure_mono ?_)
      intro g h
      obtain ⟨c, rfl⟩ := isConj_iff.1 (isConj_iff_cycleType_eq.2 (hf.trans h.symm))
      refine ⟨⟨c * f * c⁻¹, h.mem_alternatingGroup⟩, ?_, rfl⟩
      rw [Group.mem_conjugatesOfSet_iff]
      exact ⟨⟨f, hf.mem_alternatingGroup⟩, Set.mem_singleton _, isThreeCycle_isConj h5 hf h⟩)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ card α
f : Perm α
hf : f.IsThreeCycle
⊢ ⊤ ≤ normalClosure {⟨f, ⋯⟩}

Tactic:
have hi : Function.Injective (alternatingGroup α).subtype := Subtype.coe_injective

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ card α
f : Perm α
hf : f.IsThreeCycle
hi : Function.Injective ⇑(alternatingGroup α).subtype
⊢ ⊤ ≤ normalClosure {⟨f, ⋯⟩}

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ card α
f : Perm α
hf : f.IsThreeCycle
hi : Function.Injective ⇑(alternatingGroup α).subtype
g : Perm α
h : g ∈ {σ | σ.IsThreeCycle}
⊢ g ∈ ⇑(alternatingGroup α).subtype '' Group.conjugatesOfSet {⟨f, ⋯⟩}

Tactic:
obtain ⟨c, rfl⟩ := isConj_iff.1 (isConj_iff_cycleType_eq.2 (hf.trans h.symm))

Result:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ card α
f : Perm α
hf : f.IsThreeCycle
hi : Function.Injective ⇑(alternatingGroup α).subtype
c : Perm α
h : c * f * c⁻¹ ∈ {σ | σ.IsThreeCycle}
⊢ c * f * c⁻¹ ∈ ⇑(alternatingGroup α).subtype '' Group.conjugatesOfSet {⟨f, ⋯⟩}

Proof state:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ card α
f : Perm α
hf : f.IsThreeCycle
hi : Function.Injective ⇑(alternatingGroup α).subtype
c : Perm α
h : c * f * c⁻¹ ∈ {σ | σ.IsThreeCycle}
⊢ ∃ a ∈ {⟨f, ⋯⟩}, IsConj a ⟨c * f * c⁻¹, ⋯⟩

Tactic:
exact ⟨⟨f, hf.mem_alternatingGroup⟩, Set.mem_singleton _, isThreeCycle_isConj h5 hf h⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ card α
f : Perm α
hf : f.IsThreeCycle
hi : Function.Injective ⇑(alternatingGroup α).subtype
⊢ alternatingGroup α ≤ closure (⇑(alternatingGroup α).subtype '' Group.conjugatesOfSet {⟨f, ⋯⟩})

Tactic:
refine (le_of_eq closure_three_cycles_eq_alternating.symm).trans (closure_mono ?_)

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ card α
f : Perm α
hf : f.IsThreeCycle
hi : Function.Injective ⇑(alternatingGroup α).subtype
⊢ {σ | σ.IsThreeCycle} ⊆ ⇑(alternatingGroup α).subtype '' Group.conjugatesOfSet {⟨f, ⋯⟩}

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ card α
f : Perm α
hf : f.IsThreeCycle
hi : Function.Injective ⇑(alternatingGroup α).subtype
⊢ ⊤ ≤ normalClosure {⟨f, ⋯⟩}

Tactic:
refine eq_top_iff.1 (map_injective hi (le_antisymm (map_mono le_top) ?_))

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ card α
f : Perm α
hf : f.IsThreeCycle
hi : Function.Injective ⇑(alternatingGroup α).subtype
⊢ map (alternatingGroup α).subtype ⊤ ≤ map (alternatingGroup α).subtype (normalClosure {⟨f, ⋯⟩})

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ card α
f : Perm α
hf : f.IsThreeCycle
hi : Function.Injective ⇑(alternatingGroup α).subtype
⊢ {σ | σ.IsThreeCycle} ⊆ ⇑(alternatingGroup α).subtype '' Group.conjugatesOfSet {⟨f, ⋯⟩}

Tactic:
intro g h

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ card α
f : Perm α
hf : f.IsThreeCycle
hi : Function.Injective ⇑(alternatingGroup α).subtype
g : Perm α
h : g ∈ {σ | σ.IsThreeCycle}
⊢ g ∈ ⇑(alternatingGroup α).subtype '' Group.conjugatesOfSet {⟨f, ⋯⟩}

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ card α
f : Perm α
hf : f.IsThreeCycle
hi : Function.Injective ⇑(alternatingGroup α).subtype
⊢ map (alternatingGroup α).subtype ⊤ ≤ map (alternatingGroup α).subtype (normalClosure {⟨f, ⋯⟩})

Tactic:
rw [← MonoidHom.range_eq_map, range_subtype, normalClosure, MonoidHom.map_closure]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ card α
f : Perm α
hf : f.IsThreeCycle
hi : Function.Injective ⇑(alternatingGroup α).subtype
⊢ alternatingGroup α ≤ closure (⇑(alternatingGroup α).subtype '' Group.conjugatesOfSet {⟨f, ⋯⟩})

Proof state:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ card α
f : Perm α
hf : f.IsThreeCycle
hi : Function.Injective ⇑(alternatingGroup α).subtype
c : Perm α
h : c * f * c⁻¹ ∈ {σ | σ.IsThreeCycle}
⊢ ⟨c * f * c⁻¹, ⋯⟩ ∈ Group.conjugatesOfSet {⟨f, ⋯⟩}

Tactic:
rw [Group.mem_conjugatesOfSet_iff]

Result:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ card α
f : Perm α
hf : f.IsThreeCycle
hi : Function.Injective ⇑(alternatingGroup α).subtype
c : Perm α
h : c * f * c⁻¹ ∈ {σ | σ.IsThreeCycle}
⊢ ∃ a ∈ {⟨f, ⋯⟩}, IsConj a ⟨c * f * c⁻¹, ⋯⟩

Proof state:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ card α
f : Perm α
hf : f.IsThreeCycle
hi : Function.Injective ⇑(alternatingGroup α).subtype
c : Perm α
h : c * f * c⁻¹ ∈ {σ | σ.IsThreeCycle}
⊢ c * f * c⁻¹ ∈ ⇑(alternatingGroup α).subtype '' Group.conjugatesOfSet {⟨f, ⋯⟩}

Tactic:
refine ⟨⟨c * f * c⁻¹, h.mem_alternatingGroup⟩, ?_, rfl⟩

Result:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ card α
f : Perm α
hf : f.IsThreeCycle
hi : Function.Injective ⇑(alternatingGroup α).subtype
c : Perm α
h : c * f * c⁻¹ ∈ {σ | σ.IsThreeCycle}
⊢ ⟨c * f * c⁻¹, ⋯⟩ ∈ Group.conjugatesOfSet {⟨f, ⋯⟩}