-- Mathlib/GroupTheory/SpecificGroups/Alternating.lean
theorem normalClosure_finRotate_five : normalClosure ({⟨finRotate 5,
    finRotate_bit1_mem_alternatingGroup (n := 2)⟩} : Set (alternatingGroup (Fin 5))) = ⊤ :=
  eq_top_iff.2
    (by
      have h3 :
        IsThreeCycle (Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹) :=
        card_support_eq_three_iff.1 (by decide)
      rw [← h3.alternating_normalClosure (by rw [card_fin])]
      refine normalClosure_le_normal ?_
      rw [Set.singleton_subset_iff, SetLike.mem_coe]
      have h :
        (⟨finRotate 5, finRotate_bit1_mem_alternatingGroup (n := 2)⟩ : alternatingGroup (Fin 5)) ∈
          normalClosure _ :=
        SetLike.mem_coe.1 (subset_normalClosure (Set.mem_singleton _))
      -- Porting note: added `:` to help the elaborator
      exact (mul_mem (Subgroup.normalClosure_normal.conj_mem _ h
        ⟨Fin.cycleRange 2, Fin.isThreeCycle_cycleRange_two.mem_alternatingGroup⟩) (inv_mem h) :))

Proof state:
h3 : (Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹).IsThreeCycle
⊢ normalClosure {⟨Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹, ⋯⟩} ≤
    normalClosure {⟨finRotate 5, ⋯⟩}

Tactic:
refine normalClosure_le_normal ?_

Result:
h3 : (Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹).IsThreeCycle
⊢ {⟨Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹, ⋯⟩} ⊆ ↑(normalClosure {⟨finRotate 5, ⋯⟩})

Proof state:
h3 : (Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹).IsThreeCycle
⊢ ⟨Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹, ⋯⟩ ∈ normalClosure {⟨finRotate 5, ⋯⟩}

Tactic:
have h :
  (⟨finRotate 5, finRotate_bit1_mem_alternatingGroup (n := 2)⟩ : alternatingGroup (Fin 5)) ∈
    normalClosure _ :=
  SetLike.mem_coe.1 (subset_normalClosure (Set.mem_singleton _))

Result:
h3 : (Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹).IsThreeCycle
h : ⟨finRotate 5, ⋯⟩ ∈ normalClosure {⟨finRotate 5, ⋯⟩}
⊢ ⟨Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹, ⋯⟩ ∈ normalClosure {⟨finRotate 5, ⋯⟩}

Proof state:
⊢ (Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹).support.card = 3

Tactic:
decide

Result:
no goals

Proof state:
h3 : (Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹).IsThreeCycle
⊢ {⟨Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹, ⋯⟩} ⊆ ↑(normalClosure {⟨finRotate 5, ⋯⟩})

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

Result:
h3 : (Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹).IsThreeCycle
⊢ ⟨Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹, ⋯⟩ ∈ normalClosure {⟨finRotate 5, ⋯⟩}

Proof state:
⊢ ⊤ ≤ normalClosure {⟨finRotate 5, ⋯⟩}

Tactic:
have h3 :
  IsThreeCycle (Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹) :=
  card_support_eq_three_iff.1 (by decide)

Result:
h3 : (Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹).IsThreeCycle
⊢ ⊤ ≤ normalClosure {⟨finRotate 5, ⋯⟩}

Proof state:
h3 : (Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹).IsThreeCycle
⊢ ⊤ ≤ normalClosure {⟨finRotate 5, ⋯⟩}

Tactic:
rw [← h3.alternating_normalClosure (by rw [card_fin])]

Result:
h3 : (Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹).IsThreeCycle
⊢ normalClosure {⟨Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹, ⋯⟩} ≤
    normalClosure {⟨finRotate 5, ⋯⟩}

Proof state:
h3 : (Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹).IsThreeCycle
h : ⟨finRotate 5, ⋯⟩ ∈ normalClosure {⟨finRotate 5, ⋯⟩}
⊢ ⟨Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹, ⋯⟩ ∈ normalClosure {⟨finRotate 5, ⋯⟩}

Tactic:
exact (mul_mem (Subgroup.normalClosure_normal.conj_mem _ h
  ⟨Fin.cycleRange 2, Fin.isThreeCycle_cycleRange_two.mem_alternatingGroup⟩) (inv_mem h) :)

Result:
no goals

Proof state:
h3 : (Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹).IsThreeCycle
⊢ 5 ≤ card (Fin 5)

Tactic:
rw [card_fin]

Result:
no goals