-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y_1 : α
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
hσ : σ.IsCycle
m n : ℤ
h :
  Eq.{u_2 + 1} (α := ↥σ.support)
    ((fun (τ : (↑(↑(Subgroup.zpowers σ) : Set (Perm α)) : Type u_2)) ↦
        (Subtype.mk (p := fun (x : α) ↦ x ∈ σ.support)
            (((↑τ : Perm α) : (a : α) → α)
              (Classical.choose (p := fun (x : α) ↦
                (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ))
            ⋯ :
          ↥σ.support))
      (Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
        ((fun (x : ℤ) ↦ σ ^ x) m) ⋯))
    ((fun (τ : (↑(↑(Subgroup.zpowers σ) : Set (Perm α)) : Type u_2)) ↦
        (Subtype.mk (p := fun (x : α) ↦ x ∈ σ.support)
            (((↑τ : Perm α) : (a : α) → α)
              (Classical.choose (p := fun (x : α) ↦
                (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ))
            ⋯ :
          ↥σ.support))
      (Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
        ((fun (x : ℤ) ↦ σ ^ x) n) ⋯))
y : α
hy : ¬(σ : (a : α) → α) y = y
neg :
  ∀ (i : ℤ)
    (hy :
      ¬Eq (α := α)
          ((σ : (a : α) → α)
              ((σ ^ i : (a : α) → α)
                  (Classical.choose (p := fun (x : α) ↦
                    (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) :
                α) :
            α)
          ((σ ^ i : (a : α) → α)
              (Classical.choose (p := fun (x : α) ↦
                (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) :
            α)),
    Eq (α := α)
      (((↑(Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
                  ((fun (x : ℤ) ↦ σ ^ x) m) ⋯) :
              Perm α) :
            (a : α) → α)
          ((σ ^ i : (a : α) → α)
              (Classical.choose (p := fun (x : α) ↦
                (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) :
            α) :
        α)
      (((↑(Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
                  ((fun (x : ℤ) ↦ σ ^ x) n) ⋯) :
              Perm α) :
            (a : α) → α)
          ((σ ^ i : (a : α) → α)
              (Classical.choose (p := fun (x : α) ↦
                (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) :
            α) :
        α)
⊢ Eq (α := α)
    (((↑(Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
                ((fun (x : ℤ) ↦ σ ^ x) m) ⋯) :
            Perm α) :
          (a : α) → α)
        y :
      α)
    (((↑(Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
                ((fun (x : ℤ) ↦ σ ^ x) n) ⋯) :
            Perm α) :
          (a : α) → α)
        y :
      α)

Tactic:
obtain ⟨i, rfl⟩ := (Classical.choose_spec hσ).2 hy

Premises used: Classical.choose_spec, And.right, rfl