-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
hσ : σ.IsCycle
hτ : τ.IsCycle
h : #σ.support = #τ.support
x : α
hx : x ∈ (↑σ.support : Set α)
obtain :
  ∀ (n : ℕ)
    (hx :
      Membership.mem (α := α) (↑σ.support : Set α)
        ((σ ^ n : (a : α) → α)
            (Classical.choose (p := fun (x : α) ↦
              (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) :
          α)),
    Eq (α := α)
      ((↑((hτ.zpowersEquivSupport : (a : ↥(Subgroup.zpowers τ)) → { x : α // x ∈ (↑τ.support : Set α) })
              (((zpowersEquivZPowers ⋯ : ↥(Subgroup.zpowers σ) ≃ ↥(Subgroup.zpowers τ)) :
                  (a : ↥(Subgroup.zpowers σ)) → ↥(Subgroup.zpowers τ))
                ((Equiv.symm hσ.zpowersEquivSupport :
                    (a : { x : α // x ∈ (↑σ.support : Set α) }) → ↥(Subgroup.zpowers σ))
                  (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α))
                    ((σ : (a : α) → α)
                      ((σ ^ n : (a : α) → α)
                          (Classical.choose (p := fun (x : α) ↦
                            (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) :
                        α))
                    ⋯)))) :
          α) :
        α)
      ((τ : (a : α) → α)
          (↑((hτ.zpowersEquivSupport : (a : ↥(Subgroup.zpowers τ)) → { x : α // x ∈ (↑τ.support : Set α) })
                (((zpowersEquivZPowers ⋯ : ↥(Subgroup.zpowers σ) ≃ ↥(Subgroup.zpowers τ)) :
                    (a : ↥(Subgroup.zpowers σ)) → ↥(Subgroup.zpowers τ))
                  ((Equiv.symm hσ.zpowersEquivSupport :
                      (a : { x : α // x ∈ (↑σ.support : Set α) }) → ↥(Subgroup.zpowers σ))
                    (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α))
                      ((σ ^ n : (a : α) → α)
                        (Classical.choose (p := fun (x : α) ↦
                          (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ))
                      hx)))) :
            α) :
        α)
⊢ Eq (α := α)
    ((↑((hτ.zpowersEquivSupport : (a : ↥(Subgroup.zpowers τ)) → { x : α // x ∈ (↑τ.support : Set α) })
            (((zpowersEquivZPowers ⋯ : ↥(Subgroup.zpowers σ) ≃ ↥(Subgroup.zpowers τ)) :
                (a : ↥(Subgroup.zpowers σ)) → ↥(Subgroup.zpowers τ))
              ((Equiv.symm hσ.zpowersEquivSupport : (a : { x : α // x ∈ (↑σ.support : Set α) }) → ↥(Subgroup.zpowers σ))
                (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) ((σ : (a : α) → α) x) ⋯)))) :
        α) :
      α)
    ((τ : (a : α) → α)
        (↑((hτ.zpowersEquivSupport : (a : ↥(Subgroup.zpowers τ)) → { x : α // x ∈ (↑τ.support : Set α) })
              (((zpowersEquivZPowers ⋯ : ↥(Subgroup.zpowers σ) ≃ ↥(Subgroup.zpowers τ)) :
                  (a : ↥(Subgroup.zpowers σ)) → ↥(Subgroup.zpowers τ))
                ((Equiv.symm hσ.zpowersEquivSupport :
                    (a : { x : α // x ∈ (↑σ.support : Set α) }) → ↥(Subgroup.zpowers σ))
                  (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) x hx)))) :
          α) :
      α)

Tactic:
obtain ⟨n, rfl⟩ := hσ.exists_pow_eq (Classical.choose_spec hσ).1 (mem_support.1 hx)

Premises used: Equiv.Perm.IsCycle.exists_pow_eq, Equiv.Perm.mem_support, Classical.choose_spec, And.left, Iff.mp, rfl