awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
pos pos₁ : Eq (α := α) ((σ ^ m : (a : α) → α) y : α) ((σ ^ n : (a : α) → α) y : α)
⊢ 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:
simp_rw [zpow_apply_eq_self_of_apply_eq_self hy]

Premises used: Equiv.Perm.zpow_apply_eq_self_of_apply_eq_self
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y : α
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) ⋯))
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σ) :
        α)
neg :
  Eq (α := α)
    ((σ ^ i : (a : α) → α)
        ((σ ^ m : (a : α) → α)
            (Classical.choose (p := fun (x : α) ↦
              (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) :
          α) :
      α)
    ((σ ^ i : (a : α) → α)
        ((σ ^ n : (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σ) :
          α) :
      α)

Tactic:
rw [Subtype.coe_mk, Subtype.coe_mk, zpow_apply_comm σ m i, zpow_apply_comm σ n i]

Premises used: Subtype.coe_mk, Equiv.Perm.zpow_apply_comm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y : α
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) ⋯))
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 (α := α)
    ((σ ^ i : (a : α) → α)
        ((σ ^ m : (a : α) → α)
            (Classical.choose (p := fun (x : α) ↦
              (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) :
          α) :
      α)
    ((σ ^ i : (a : α) → α)
        ((σ ^ n : (a : α) → α)
            (Classical.choose (p := fun (x : α) ↦
              (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) :
          α) :
      α)

Tactic:
congr_arg _ (Subtype.ext_iff.mp h)

Premises used: Subtype.ext_iff, congr_arg, Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y : α
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) ⋯))
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 (α := α)
    ((σ ^ i : (a : α) → α)
        ((σ ^ m : (a : α) → α)
            (Classical.choose (p := fun (x : α) ↦
              (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) :
          α) :
      α)
    ((σ ^ i : (a : α) → α)
        ((σ ^ n : (a : α) → α)
            (Classical.choose (p := fun (x : α) ↦
              (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) :
          α) :
      α)

Tactic:
exact congr_arg _ (Subtype.ext_iff.mp h)

Premises used: Subtype.ext_iff, congr_arg, Iff.mp
-- 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
y : α
hy : y ∈ σ.support
⊢ (σ : (a : α) → α) y ≠ y

Tactic:
rw [mem_support] at hy

Premises used: Equiv.Perm.mem_support
-- 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
y : α
hy_1 : y ∈ σ.support
hy : (σ : (a : α) → α) y ≠ y
right :
  ∀ (n : ℤ)
    (hy :
      Membership.mem (α := α) σ.support
        ((σ ^ n : (a : α) → α)
            (Classical.choose (p := fun (x : α) ↦
              (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) :
          α))
    (hy_2 :
      Ne (α := α)
        ((σ : (a : α) → α)
            ((σ ^ n : (a : α) → α)
                (Classical.choose (p := fun (x : α) ↦
                  (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) :
              α) :
          α)
        ((σ ^ n : (a : α) → α)
            (Classical.choose (p := fun (x : α) ↦
              (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) :
          α)),
    ∃ (a : ↥(Subgroup.zpowers σ)),
      Eq (α := ↥σ.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))
            a :
          ↥σ.support)
        (Subtype.mk (p := fun (x : α) ↦ x ∈ σ.support)
            ((σ ^ n : (a : α) → α)
              (Classical.choose (p := fun (x : α) ↦
                (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ))
            hy :
          ↥σ.support)
⊢ ∃ (a : ↥(Subgroup.zpowers σ)),
    (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))
        a =
      Subtype.mk (p := fun (x : α) ↦ x ∈ σ.support) y hy_1

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

Premises used: Classical.choose_spec, And.right, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y : α
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
hσ : σ.IsCycle
n : ℤ
hy_1 :
  Membership.mem (α := α) σ.support
    ((σ ^ n : (a : α) → α)
        (Classical.choose (p := fun (x : α) ↦
          (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) :
      α)
hy :
  Ne (α := α)
    ((σ : (a : α) → α)
        ((σ ^ n : (a : α) → α)
            (Classical.choose (p := fun (x : α) ↦
              (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) :
          α) :
      α)
    ((σ ^ n : (a : α) → α)
        (Classical.choose (p := fun (x : α) ↦
          (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) :
      α)
⊢ ∃ (a : ↥(Subgroup.zpowers σ)),
    Eq (α := ↥σ.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))
          a :
        ↥σ.support)
      (Subtype.mk (p := fun (x : α) ↦ x ∈ σ.support)
          ((σ ^ n : (a : α) → α)
            (Classical.choose (p := fun (x : α) ↦
              (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ))
          hy_1 :
        ↥σ.support)

Tactic:
⟨⟨σ ^ n, n, rfl⟩, rfl⟩

Premises used: Subtype.mk, HPow.hPow, Exists.intro, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y : α
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
hσ : σ.IsCycle
n : ℤ
hy_1 :
  Membership.mem (α := α) σ.support
    ((σ ^ n : (a : α) → α)
        (Classical.choose (p := fun (x : α) ↦
          (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) :
      α)
hy :
  Ne (α := α)
    ((σ : (a : α) → α)
        ((σ ^ n : (a : α) → α)
            (Classical.choose (p := fun (x : α) ↦
              (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) :
          α) :
      α)
    ((σ ^ n : (a : α) → α)
        (Classical.choose (p := fun (x : α) ↦
          (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) :
      α)
⊢ ∃ (a : ↥(Subgroup.zpowers σ)),
    Eq (α := ↥σ.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))
          a :
        ↥σ.support)
      (Subtype.mk (p := fun (x : α) ↦ x ∈ σ.support)
          ((σ ^ n : (a : α) → α)
            (Classical.choose (p := fun (x : α) ↦
              (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ))
          hy_1 :
        ↥σ.support)

Tactic:
exact ⟨⟨σ ^ n, n, rfl⟩, rfl⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
hσ : σ.IsCycle
n : ℕ
⊢ Eq (α := ↥σ.support)
    ((hσ.zpowersEquivSupport : (a : ↥(Subgroup.zpowers σ)) → ↥σ.support)
        (Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x) (σ ^ n)
          ⋯) :
      ↥σ.support)
    (Subtype.mk (p := fun (x : α) ↦ x ∈ σ.support)
        ((σ ^ n : (a : α) → α)
          (Classical.choose (p := fun (x : α) ↦
            (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ))
        ⋯ :
      ↥σ.support)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
hσ : σ.IsCycle
n : ℕ
⊢ Eq (α := ↥(Subgroup.zpowers σ))
    ((Equiv.symm hσ.zpowersEquivSupport : (a : ↥σ.support) → ↥(Subgroup.zpowers σ))
        (Subtype.mk (p := fun (x : α) ↦ x ∈ σ.support)
          ((σ ^ n : (a : α) → α)
            (Classical.choose (p := fun (x : α) ↦
              (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ))
          ⋯) :
      ↥(Subgroup.zpowers σ))
    (Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x) (σ ^ n) ⋯ :
      ↥(Subgroup.zpowers σ))

Tactic:
(Equiv.symm_apply_eq _).2 hσ.zpowersEquivSupport_apply

Premises used: Iff.mpr, Equiv.symm_apply_eq, Equiv.Perm.IsCycle.zpowersEquivSupport_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
rw : Fintype.card.{u_2} ↥(Subgroup.zpowers f) = Fintype.card.{u_2} ↥f.support
⊢ orderOf f = #f.support

Tactic:
rw [← Fintype.card_zpowers, ← Fintype.card_coe]

Premises used: Fintype.card_zpowers, Fintype.card_coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
⊢ Fintype.card.{u_2} ↥(Subgroup.zpowers f) = Fintype.card.{u_2} ↥f.support

Tactic:
Fintype.card_congr (IsCycle.zpowersEquivSupport hf)

Premises used: Fintype.card_congr, Equiv.Perm.IsCycle.zpowersEquivSupport
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
⊢ Fintype.card.{u_2} ↥(Subgroup.zpowers f) = Fintype.card.{u_2} ↥f.support

Tactic:
convert! Fintype.card_congr (IsCycle.zpowersEquivSupport hf)

Premises used: Fintype.card_congr, Equiv.Perm.IsCycle.zpowersEquivSupport
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_4
inst : DecidableEq α
b x : α
f : Perm α
⊢ (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b →
    (HPow.hPow (β := ℕ) f 0 : (a : α) → α) ((f : (a : α) → α) x : α) = b →
      ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b

Tactic:
fun _ h => ⟨0, h⟩

Premises used: Exists.intro, OfNat.ofNat
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_4
inst : DecidableEq α
⊢ ∀ {b x : α} {f : Perm α},
    (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b →
      (HPow.hPow (β := ℕ) f 0 : (a : α) → α) ((f : (a : α) → α) x : α) = b →
        ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b

Tactic:
exact fun _ h => ⟨0, h⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
hn :
  ∀ {b x : α} {f : Perm α},
    (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b →
      (f ^ n : (a : α) → α) ((f : (a : α) → α) x : α) = b →
        ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
b x : α
f : Perm α
hb : (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b
h : (f ^ (n + 1) : (a : α) → α) ((f : (a : α) → α) x : α) = b
succ :
  ∀ (hfbx : (f : (a : α) → α) x = b),
    ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
succ₁ :
  ∀ (hfbx : (f : (a : α) → α) x ≠ b),
    ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
⊢ ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b

Tactic:
obtain hfbx | hfbx := eq_or_ne (f x) b

Premises used: eq_or_ne, DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
hn :
  ∀ {b x : α} {f : Perm α},
    (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b →
      (f ^ n : (a : α) → α) ((f : (a : α) → α) x : α) = b →
        ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
b x : α
f : Perm α
hb : (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b
h : (f ^ (n + 1) : (a : α) → α) ((f : (a : α) → α) x : α) = b
hfbx : (f : (a : α) → α) x = b
⊢ ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b

Tactic:
⟨0, hfbx⟩

Premises used: Exists.intro, OfNat.ofNat
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
hn :
  ∀ {b x : α} {f : Perm α},
    (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b →
      (f ^ n : (a : α) → α) ((f : (a : α) → α) x : α) = b →
        ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
b x : α
f : Perm α
hb : (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b
h : (f ^ (n + 1) : (a : α) → α) ((f : (a : α) → α) x : α) = b
hfbx : (f : (a : α) → α) x = b
⊢ ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b

Tactic:
exact ⟨0, hfbx⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
hn :
  ∀ {b x : α} {f : Perm α},
    (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b →
      (f ^ n : (a : α) → α) ((f : (a : α) → α) x : α) = b →
        ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
b x : α
f : Perm α
hb : (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b
h : (f ^ (n + 1) : (a : α) → α) ((f : (a : α) → α) x : α) = b
hfbx : (f : (a : α) → α) x ≠ b
⊢ (f : (a : α) → α) b ≠ b ∧ b ≠ x

Tactic:
have : f b ≠ b ∧ b ≠ x := ne_and_ne_of_swap_mul_apply_ne_self hb
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
hn :
  ∀ {b x : α} {f : Perm α},
    (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b →
      (f ^ n : (a : α) → α) ((f : (a : α) → α) x : α) = b →
        ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
b x : α
f : Perm α
hb : (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b
h : (f ^ (n + 1) : (a : α) → α) ((f : (a : α) → α) x : α) = b
hfbx : (f : (a : α) → α) x ≠ b
this : (f : (a : α) → α) b ≠ b ∧ b ≠ x
⊢ Ne (α := α) ((swap x ((f : (a : α) → α) x) * f : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) : α)
    ((Equiv.symm f : (a : α) → α) b : α)

Tactic:
simpa [swap_apply_of_ne_of_ne this.2 hfbx.symm, eq_symm_apply, f.injective.eq_iff]
        using this.1

Premises used: Function.Injective.eq_iff, Ne.symm, Equiv.swap_apply_of_ne_of_ne, And.right, And.left, Equiv.injective, Equiv.eq_symm_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
hn :
  ∀ {b x : α} {f : Perm α},
    (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b →
      (f ^ n : (a : α) → α) ((f : (a : α) → α) x : α) = b →
        ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
b x : α
f : Perm α
hb : (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b
h : (f ^ (n + 1) : (a : α) → α) ((f : (a : α) → α) x : α) = b
hfbx : (f : (a : α) → α) x ≠ b
this : (f : (a : α) → α) b ≠ b ∧ b ≠ x
⊢ Ne (α := α) ((swap x ((f : (a : α) → α) x) * f : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) : α)
    ((Equiv.symm f : (a : α) → α) b : α)

Tactic:
have hb' : (swap x (f x) * f) (f.symm b) ≠ f.symm b := by
      simpa [swap_apply_of_ne_of_ne this.2 hfbx.symm, eq_symm_apply, f.injective.eq_iff]
        using this.1