α : 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 α) }}
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ card α
f : Perm α
hf : IsThreeCycle f
⊢ ⊤ ≤ normalClosure {{ val := f, property := (_ : f ∈ alternatingGroup α) }}
have hi : Function.Injective (alternatingGroup α).subtype := Subtype.coe_injective
α : 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 α) }})
α : 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 α) }}
refine' eq_top_iff.1 (map_injective hi (le_antisymm (map_mono le_top) _))
α : 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 α) }})
α : 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 α) }})
rw [← MonoidHom.range_eq_map, subtype_range, normalClosure, MonoidHom.map_closure]
α : 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 α) }}
α : 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 α) }})
refine' (le_of_eq closure_three_cycles_eq_alternating.symm).trans (closure_mono _)
α : 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 α) }}
α : 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 α) }}
intro g h
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 α) }}
α : 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 α) }}
obtain ⟨c, rfl⟩ := isConj_iff.1 (isConj_iff_cycleType_eq.2 (hf.trans h.symm))
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 α) }}
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 α) }}
refine' ⟨⟨c * f * c⁻¹, h.mem_alternatingGroup⟩, _, rfl⟩
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 α) }
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 α) }}
rw [Group.mem_conjugatesOfSet_iff]
no goals
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 α) }
exact ⟨⟨f, hf.mem_alternatingGroup⟩, Set.mem_singleton _, isThreeCycle_isConj h5 hf h⟩