-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
hσ : σ.IsCycle
hτ : τ.IsCycle
h : #σ.support = #τ.support
x : α
hx : x ∈ (↑σ.support : Set α)
⊢ 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)))) :
          α) :
      α)
have 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 sorry : ↥(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σ) :
                      α))
                  sorry)))) :
        α) :
      α)
    ((τ : (a : α) → α)
        (↑((hτ.zpowersEquivSupport : (a : ↥(Subgroup.zpowers τ)) → { x : α // x ∈ (↑τ.support : Set α) })
              (((zpowersEquivZPowers sorry : ↥(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)))) :
          α) :
      α)
Tactic: obtain ⟨n, rfl⟩ := hσ.exists_pow_eq (Classical.choose_spec hσ).1 (mem_support.1 hx)
Cleared hypotheses: x, hx