awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
hn_1 : 0 < (p.toList x).length
hn : 0 < orderOf (p.cycleOf x)
m : ℕ
hm_1 : m + 1 < (p.toList x).length
hm : m + 1 < orderOf (p.cycleOf x)
hx₁ : (p ^ m.succ : (a : α) → α) x ≠ x
hm₁ : m + 1 < (p.toList x).length
⊢ m + 1 < orderOf (p.cycleOf x)

Tactic:
rw [← hc.support_pow_of_pos_of_lt_orderOf m.zero_lt_succ hm, mem_support,
      cycleOf_pow_apply_self] at hx

Premises used: Nat.zero_lt_succ, Equiv.Perm.mem_support, Equiv.Perm.cycleOf_pow_apply_self, Equiv.Perm.IsCycle.support_pow_of_pos_of_lt_orderOf
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hc : (p.cycleOf x).IsCycle
hn_1 : 0 < (p.toList x).length
hn : 0 < orderOf (p.cycleOf x)
m : ℕ
hx : (p ^ m.succ : (a : α) → α) x ≠ x
hm_1 : m + 1 < (p.toList x).length
hm : m + 1 < orderOf (p.cycleOf x)
⊢ Eq (α := α) ((HPow.hPow (β := ℕ) (p.cycleOf x) 0 : (a : α) → α) x : α) ((p.cycleOf x ^ (m + 1) : (a : α) → α) x : α) →
    0 = m + 1

Tactic:
simp [hx.symm]

Premises used: Ne.symm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn_1 : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
hm_1 : 0 < (p.toList x).length
hm : 0 < orderOf (p.cycleOf x)
⊢ (p ^ n.succ : (a : α) → α) x ≠ x

Tactic:
rw [← hc.support_pow_of_pos_of_lt_orderOf n.zero_lt_succ hn, mem_support,
      cycleOf_pow_apply_self] at hx

Premises used: Nat.zero_lt_succ, Equiv.Perm.mem_support, Equiv.Perm.cycleOf_pow_apply_self, Equiv.Perm.IsCycle.support_pow_of_pos_of_lt_orderOf
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn_1 : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
hm_1 : 0 < (p.toList x).length
hm : 0 < orderOf (p.cycleOf x)
hx₁ : (p ^ n.succ : (a : α) → α) x ≠ x
⊢ n + 1 < (p.toList x).length

Tactic:
rw [← hc.support_pow_of_pos_of_lt_orderOf n.zero_lt_succ hn, mem_support,
      cycleOf_pow_apply_self] at hx

Premises used: Nat.zero_lt_succ, Equiv.Perm.mem_support, Equiv.Perm.cycleOf_pow_apply_self, Equiv.Perm.IsCycle.support_pow_of_pos_of_lt_orderOf
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn_1 : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
hm_1 : 0 < (p.toList x).length
hm : 0 < orderOf (p.cycleOf x)
hx₁ : (p ^ n.succ : (a : α) → α) x ≠ x
hn₁ : n + 1 < (p.toList x).length
⊢ n + 1 < orderOf (p.cycleOf x)

Tactic:
rw [← hc.support_pow_of_pos_of_lt_orderOf n.zero_lt_succ hn, mem_support,
      cycleOf_pow_apply_self] at hx

Premises used: Nat.zero_lt_succ, Equiv.Perm.mem_support, Equiv.Perm.cycleOf_pow_apply_self, Equiv.Perm.IsCycle.support_pow_of_pos_of_lt_orderOf
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn_1 : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
hm_1 : 0 < (p.toList x).length
hm : 0 < orderOf (p.cycleOf x)
hx₁ : (p ^ n.succ : (a : α) → α) x ≠ x
hn₁ : n + 1 < (p.toList x).length
hn₂ : n + 1 < orderOf (p.cycleOf x)
⊢ 0 < (p.toList x).length

Tactic:
rw [← hc.support_pow_of_pos_of_lt_orderOf n.zero_lt_succ hn, mem_support,
      cycleOf_pow_apply_self] at hx

Premises used: Nat.zero_lt_succ, Equiv.Perm.mem_support, Equiv.Perm.cycleOf_pow_apply_self, Equiv.Perm.IsCycle.support_pow_of_pos_of_lt_orderOf
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn_1 : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
hm_1 : 0 < (p.toList x).length
hm : 0 < orderOf (p.cycleOf x)
hx₁ : (p ^ n.succ : (a : α) → α) x ≠ x
hn₁ : n + 1 < (p.toList x).length
hn₂ : n + 1 < orderOf (p.cycleOf x)
hm₁ : 0 < (p.toList x).length
⊢ 0 < orderOf (p.cycleOf x)

Tactic:
rw [← hc.support_pow_of_pos_of_lt_orderOf n.zero_lt_succ hn, mem_support,
      cycleOf_pow_apply_self] at hx

Premises used: Nat.zero_lt_succ, Equiv.Perm.mem_support, Equiv.Perm.cycleOf_pow_apply_self, Equiv.Perm.IsCycle.support_pow_of_pos_of_lt_orderOf
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hc : (p.cycleOf x).IsCycle
n : ℕ
hx : (p ^ n.succ : (a : α) → α) x ≠ x
hn_1 : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
hm_1 : 0 < (p.toList x).length
hm : 0 < orderOf (p.cycleOf x)
⊢ Eq (α := α) ((p.cycleOf x ^ (n + 1) : (a : α) → α) x : α) ((HPow.hPow (β := ℕ) (p.cycleOf x) 0 : (a : α) → α) x : α) →
    n + 1 = 0

Tactic:
simp [hx]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn_1 : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
m : ℕ
hm_1 : m + 1 < (p.toList x).length
hm : m + 1 < orderOf (p.cycleOf x)
h : Eq (α := α) ((p.cycleOf x ^ (n + 1) : (a : α) → α) x : α) ((p.cycleOf x ^ (m + 1) : (a : α) → α) x : α)
⊢ ¬orderOf (p.cycleOf x) ∣ n.succ

Tactic:
have hn' : ¬orderOf (p.cycleOf x) ∣ n.succ := Nat.not_dvd_of_pos_of_lt n.zero_lt_succ hn
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn_1 : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
m : ℕ
hm_1 : m + 1 < (p.toList x).length
hm : m + 1 < orderOf (p.cycleOf x)
h : Eq (α := α) ((p.cycleOf x ^ (n + 1) : (a : α) → α) x : α) ((p.cycleOf x ^ (m + 1) : (a : α) → α) x : α)
hn' : ¬orderOf (p.cycleOf x) ∣ n.succ
⊢ ¬orderOf (p.cycleOf x) ∣ m.succ

Tactic:
have hm' : ¬orderOf (p.cycleOf x) ∣ m.succ := Nat.not_dvd_of_pos_of_lt m.zero_lt_succ hm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn_1 : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
m : ℕ
hm_1 : m + 1 < (p.toList x).length
hm : m + 1 < orderOf (p.cycleOf x)
h : Eq (α := α) ((p.cycleOf x ^ (n + 1) : (a : α) → α) x : α) ((p.cycleOf x ^ (m + 1) : (a : α) → α) x : α)
hn' : ¬orderOf (p.cycleOf x) ∣ n.succ
hm' : ¬orderOf (p.cycleOf x) ∣ m.succ
⊢ (p.cycleOf x ^ n.succ).support = (p.cycleOf x).support

Tactic:
rw [← hc.support_pow_eq_iff] at hn' hm'

Premises used: Equiv.Perm.IsCycle.support_pow_eq_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn_1 : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
m : ℕ
hm_1 : m + 1 < (p.toList x).length
hm : m + 1 < orderOf (p.cycleOf x)
h : Eq (α := α) ((p.cycleOf x ^ (n + 1) : (a : α) → α) x : α) ((p.cycleOf x ^ (m + 1) : (a : α) → α) x : α)
hn' : ¬orderOf (p.cycleOf x) ∣ n.succ
hm' : ¬orderOf (p.cycleOf x) ∣ m.succ
hn'₁ : (p.cycleOf x ^ n.succ).support = (p.cycleOf x).support
⊢ (p.cycleOf x ^ m.succ).support = (p.cycleOf x).support

Tactic:
rw [← hc.support_pow_eq_iff] at hn' hm'

Premises used: Equiv.Perm.IsCycle.support_pow_eq_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn_1 : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
m : ℕ
hm_1 : m + 1 < (p.toList x).length
hm : m + 1 < orderOf (p.cycleOf x)
h : Eq (α := α) ((p.cycleOf x ^ (n + 1) : (a : α) → α) x : α) ((p.cycleOf x ^ (m + 1) : (a : α) → α) x : α)
hn' : (p.cycleOf x ^ n.succ).support = (p.cycleOf x).support
hm' : (p.cycleOf x ^ m.succ).support = (p.cycleOf x).support
neg : p.cycleOf x ^ (n + 1) = p.cycleOf x ^ (m + 1)
⊢ n + 1 = m + 1

Tactic:
rw [← Nat.mod_eq_of_lt hn, ← Nat.mod_eq_of_lt hm, ← pow_inj_mod]

Premises used: Nat.mod_eq_of_lt, pow_inj_mod
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn_1 : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
m : ℕ
hm_1 : m + 1 < (p.toList x).length
hm : m + 1 < orderOf (p.cycleOf x)
h : Eq (α := α) ((p.cycleOf x ^ (n + 1) : (a : α) → α) x : α) ((p.cycleOf x ^ (m + 1) : (a : α) → α) x : α)
hn' : (p.cycleOf x ^ n.succ).support = (p.cycleOf x).support
hm' : (p.cycleOf x ^ m.succ).support = (p.cycleOf x).support
⊢ p.cycleOf x ^ (n + 1) = p.cycleOf x ^ (m + 1)

Tactic:
support_congr ?_ ?_

Premises used: Equiv.Perm.support_congr
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn_1 : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
m : ℕ
hm_1 : m + 1 < (p.toList x).length
hm : m + 1 < orderOf (p.cycleOf x)
h : Eq (α := α) ((p.cycleOf x ^ (n + 1) : (a : α) → α) x : α) ((p.cycleOf x ^ (m + 1) : (a : α) → α) x : α)
hn' : (p.cycleOf x ^ n.succ).support = (p.cycleOf x).support
hm' : (p.cycleOf x ^ m.succ).support = (p.cycleOf x).support
neg : (p.cycleOf x ^ (n + 1)).support ⊆ (p.cycleOf x ^ (m + 1)).support
neg₁ :
  ∀ x_1 ∈ (p.cycleOf x ^ (m + 1)).support,
    Eq (α := α) ((p.cycleOf x ^ (n + 1) : (a : α) → α) x_1 : α) ((p.cycleOf x ^ (m + 1) : (a : α) → α) x_1 : α)
⊢ p.cycleOf x ^ (n + 1) = p.cycleOf x ^ (m + 1)

Tactic:
refine support_congr ?_ ?_

Premises used: Equiv.Perm.support_congr
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn_1 : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
m : ℕ
hm_1 : m + 1 < (p.toList x).length
hm : m + 1 < orderOf (p.cycleOf x)
h : Eq (α := α) ((p.cycleOf x ^ (n + 1) : (a : α) → α) x : α) ((p.cycleOf x ^ (m + 1) : (a : α) → α) x : α)
hn' : (p.cycleOf x ^ n.succ).support = (p.cycleOf x).support
hm' : (p.cycleOf x ^ m.succ).support = (p.cycleOf x).support
neg : (p.cycleOf x ^ (n + 1)).support ⊆ (p.cycleOf x).support
neg₁ neg₂ : (p.cycleOf x).support ⊆ (p.cycleOf x).support
⊢ (p.cycleOf x ^ (n + 1)).support ⊆ (p.cycleOf x ^ (m + 1)).support

Tactic:
rw [hm', hn']
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn_1 : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
m : ℕ
hm_1 : m + 1 < (p.toList x).length
hm : m + 1 < orderOf (p.cycleOf x)
h : Eq (α := α) ((p.cycleOf x ^ (n + 1) : (a : α) → α) x : α) ((p.cycleOf x ^ (m + 1) : (a : α) → α) x : α)
hn' : (p.cycleOf x ^ n.succ).support = (p.cycleOf x).support
hm' : (p.cycleOf x ^ m.succ).support = (p.cycleOf x).support
neg :
  ∀ x_1 ∈ (p.cycleOf x).support,
    Eq (α := α) ((p.cycleOf x ^ (n + 1) : (a : α) → α) x_1 : α) ((p.cycleOf x ^ (m + 1) : (a : α) → α) x_1 : α)
⊢ ∀ x_1 ∈ (p.cycleOf x ^ (m + 1)).support,
    Eq (α := α) ((p.cycleOf x ^ (n + 1) : (a : α) → α) x_1 : α) ((p.cycleOf x ^ (m + 1) : (a : α) → α) x_1 : α)

Tactic:
rw [hm']
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn_1 : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
m : ℕ
hm_1 : m + 1 < (p.toList x).length
hm : m + 1 < orderOf (p.cycleOf x)
h : Eq (α := α) ((p.cycleOf x ^ (n + 1) : (a : α) → α) x : α) ((p.cycleOf x ^ (m + 1) : (a : α) → α) x : α)
hn' : (p.cycleOf x ^ n.succ).support = (p.cycleOf x).support
hm' : (p.cycleOf x ^ m.succ).support = (p.cycleOf x).support
y : α
hy : y ∈ (p.cycleOf x).support
neg :
  ∀ (k : ℕ) (hy : Membership.mem (α := α) (p.cycleOf x).support ((p.cycleOf x ^ k : (a : α) → α) x : α)),
    Eq (α := α) ((p.cycleOf x ^ (n + 1) : (a : α) → α) ((p.cycleOf x ^ k : (a : α) → α) x : α) : α)
      ((p.cycleOf x ^ (m + 1) : (a : α) → α) ((p.cycleOf x ^ k : (a : α) → α) x : α) : α)
⊢ Eq (α := α) ((p.cycleOf x ^ (n + 1) : (a : α) → α) y : α) ((p.cycleOf x ^ (m + 1) : (a : α) → α) y : α)

Tactic:
obtain ⟨k, rfl⟩ := hc.exists_pow_eq (mem_support.mp hx) (mem_support.mp hy)

Premises used: Equiv.Perm.IsCycle.exists_pow_eq, Equiv.Perm.mem_support, Iff.mp, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn_1 : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
m : ℕ
hm_1 : m + 1 < (p.toList x).length
hm : m + 1 < orderOf (p.cycleOf x)
h : Eq (α := α) ((p.cycleOf x ^ (n + 1) : (a : α) → α) x : α) ((p.cycleOf x ^ (m + 1) : (a : α) → α) x : α)
hn' : (p.cycleOf x ^ n.succ).support = (p.cycleOf x).support
hm' : (p.cycleOf x ^ m.succ).support = (p.cycleOf x).support
k : ℕ
hy : Membership.mem (α := α) (p.cycleOf x).support ((p.cycleOf x ^ k : (a : α) → α) x : α)
neg :
  Eq (α := α) ((p.cycleOf x ^ (n + 1) * p.cycleOf x ^ k : (a : α) → α) x : α)
    ((p.cycleOf x ^ (m + 1) : (a : α) → α) ((p.cycleOf x ^ k : (a : α) → α) x : α) : α)
neg₁ :
  Eq (α := α) ((p.cycleOf x ^ k * p.cycleOf x ^ (n + 1) : (a : α) → α) x : α)
    ((p.cycleOf x ^ (m + 1) : (a : α) → α) ((p.cycleOf x ^ k : (a : α) → α) x : α) : α)
neg₂ :
  Eq (α := α) ((p.cycleOf x ^ k : (a : α) → α) ((p.cycleOf x ^ (n + 1) : (a : α) → α) x : α) : α)
    ((p.cycleOf x ^ (m + 1) : (a : α) → α) ((p.cycleOf x ^ k : (a : α) → α) x : α) : α)
neg₃ :
  Eq (α := α) ((p.cycleOf x ^ k : (a : α) → α) ((p.cycleOf x ^ (m + 1) : (a : α) → α) x : α) : α)
    ((p.cycleOf x ^ (m + 1) : (a : α) → α) ((p.cycleOf x ^ k : (a : α) → α) x : α) : α)
neg₄ :
  Eq (α := α) ((p.cycleOf x ^ k * p.cycleOf x ^ (m + 1) : (a : α) → α) x : α)
    ((p.cycleOf x ^ (m + 1) : (a : α) → α) ((p.cycleOf x ^ k : (a : α) → α) x : α) : α)
neg₅ :
  Eq (α := α) ((p.cycleOf x ^ k * p.cycleOf x ^ (m + 1) : (a : α) → α) x : α)
    ((p.cycleOf x ^ (m + 1) * p.cycleOf x ^ k : (a : α) → α) x : α)
neg₆ neg₇ :
  Eq (α := α) ((p.cycleOf x ^ (m + 1) * p.cycleOf x ^ k : (a : α) → α) x : α)
    ((p.cycleOf x ^ (m + 1) * p.cycleOf x ^ k : (a : α) → α) x : α)
⊢ Eq (α := α) ((p.cycleOf x ^ (n + 1) : (a : α) → α) ((p.cycleOf x ^ k : (a : α) → α) x : α) : α)
    ((p.cycleOf x ^ (m + 1) : (a : α) → α) ((p.cycleOf x ^ k : (a : α) → α) x : α) : α)

Tactic:
rw [← mul_apply, (Commute.pow_pow_self _ _ _).eq, mul_apply, h, ← mul_apply, ← mul_apply,
      (Commute.pow_pow_self _ _ _).eq]

Premises used: Commute.pow_pow_self, Equiv.Perm.mul_apply, Commute.eq
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x y : α
hy : y ∈ p.toList x
⊢ p.SameCycle x y ∧ x ∈ p.support

Tactic:
rw [mem_toList_iff] at hy

Premises used: Equiv.Perm.mem_toList_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x y : α
hy_1 : y ∈ p.toList x
hy : p.SameCycle x y ∧ x ∈ p.support
obtain :
  ∀ (k : ℕ) (hk : k < (p.cycleOf x).support.card) (hk' : (p ^ k : (a : α) → α) x = y),
    (p.toList x).next y hy_1 = (p : (a : α) → α) y
⊢ (p.toList x).next y hy_1 = (p : (a : α) → α) y

Tactic:
obtain ⟨k, hk, hk'⟩ := hy.left.exists_pow_eq_of_mem_support hy.right

Premises used: Equiv.Perm.SameCycle.exists_pow_eq_of_mem_support, And.right, And.left
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x y : α
hy_1 : y ∈ p.toList x
hy : p.SameCycle x y ∧ x ∈ p.support
k : ℕ
hk : k < (p.cycleOf x).support.card
hk' : (p ^ k : (a : α) → α) x = y
⊢ k < (p.toList x).length

Tactic:
simpa using hk
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x y : α
hy_1 : y ∈ p.toList x
hy : p.SameCycle x y ∧ x ∈ p.support
k : ℕ
hk : k < (p.cycleOf x).support.card
hk' : (p ^ k : (a : α) → α) x = y
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) k ⋯ = y

Tactic:
rw [← getElem_toList p x k (by simpa using hk)] at hk'

Premises used: Equiv.Perm.getElem_toList
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x y : α
hy_1 : y ∈ p.toList x
hy : p.SameCycle x y ∧ x ∈ p.support
k : ℕ
hk : k < (p.cycleOf x).support.card
hk' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) k ⋯ = y
simp_rw :
  (p.toList x).next (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) k ⋯) ⋯ =
    (p : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) k ⋯)
⊢ (p.toList x).next y hy_1 = (p : (a : α) → α) y

Tactic:
simp_rw [← hk']
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x y : α
hy_1 : y ∈ p.toList x
hy : p.SameCycle x y ∧ x ∈ p.support
k : ℕ
hk : k < (p.cycleOf x).support.card
hk' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) k ⋯ = y
rw : Eq (α := α) ((p ^ ((k + 1) % (p.toList x).length) : (a : α) → α) x : α) ((p ^ (k + 1) : (a : α) → α) x : α)
⊢ (p.toList x).next (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) k ⋯) ⋯ =
    (p : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) k ⋯)

Tactic:
rw [next_getElem _ (nodup_toList _ _), getElem_toList, getElem_toList, ← mul_apply, ← pow_succ']

Premises used: Equiv.Perm.getElem_toList, List.next_getElem, Equiv.Perm.mul_apply, Equiv.Perm.nodup_toList, pow_succ'
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x y : α
hy_1 : y ∈ p.toList x
hy : p.SameCycle x y ∧ x ∈ p.support
k : ℕ
hk : k < (p.cycleOf x).support.card
hk' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) k ⋯ = y
simp_rw :
  Eq (α := α) ((p ^ ((k + 1) % (p.cycleOf x).support.card) : (a : α) → α) x : α) ((p ^ (k + 1) : (a : α) → α) x : α)
⊢ Eq (α := α) ((p ^ ((k + 1) % (p.toList x).length) : (a : α) → α) x : α) ((p ^ (k + 1) : (a : α) → α) x : α)

Tactic:
simp_rw [length_toList]

Premises used: Equiv.Perm.length_toList
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x y : α
hy_1 : y ∈ p.toList x
hy : p.SameCycle x y ∧ x ∈ p.support
k : ℕ
hk : k < (p.cycleOf x).support.card
hk' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) k ⋯ = y
rw : (p.cycleOf x).IsCycle
⊢ Eq (α := α) ((p ^ ((k + 1) % (p.cycleOf x).support.card) : (a : α) → α) x : α) ((p ^ (k + 1) : (a : α) → α) x : α)

Tactic:
rw [← pow_mod_orderOf_cycleOf_apply p (k + 1), IsCycle.orderOf]

Premises used: Equiv.Perm.IsCycle.orderOf, HAdd.hAdd, Equiv.Perm.pow_mod_orderOf_cycleOf_apply, OfNat.ofNat
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x y : α
hy_1 : y ∈ p.toList x
hy : p.SameCycle x y ∧ x ∈ p.support
k : ℕ
hk : k < (p.cycleOf x).support.card
hk' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) k ⋯ = y
⊢ (p.cycleOf x).IsCycle

Tactic:
isCycle_cycleOf _ (mem_support.mp hy.right)

Premises used: Equiv.Perm.isCycle_cycleOf, Equiv.Perm.mem_support, And.right, Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x y : α
hy_1 : y ∈ p.toList x
hy : p.SameCycle x y ∧ x ∈ p.support
k : ℕ
hk : k < (p.cycleOf x).support.card
hk' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) k ⋯ = y
⊢ (p.cycleOf x).IsCycle

Tactic:
exact isCycle_cycleOf _ (mem_support.mp hy.right)

Premises used: Equiv.Perm.isCycle_cycleOf, Equiv.Perm.mem_support, And.right, Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
k : ℕ
hl : (p.toList ((p ^ k : (a : α) → α) x)).length = ((p.toList x).rotate k).length
h :
  ∀ (i : ℕ) (h₁ : i < (p.toList ((p ^ k : (a : α) → α) x)).length) (h₂ : i < ((p.toList x).rotate k).length),
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList ((p ^ k : (a : α) → α) x)) i h₁ =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ((p.toList x).rotate k) i h₂
⊢ p.toList ((p ^ k : (a : α) → α) x) = (p.toList x).rotate k

Tactic:
apply ext_getElem

Premises used: List.ext_getElem
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
k : ℕ
⊢ (p.toList ((p ^ k : (a : α) → α) x)).length = ((p.toList x).rotate k).length

Tactic:
simp only [length_toList, cycleOf_self_apply_pow, length_rotate]

Premises used: List.length_rotate, Equiv.Perm.cycleOf_self_apply_pow, Equiv.Perm.length_toList
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
k n : ℕ
hn : n < (p.toList ((p ^ k : (a : α) → α) x)).length
hn' : n < ((p.toList x).rotate k).length
h :
  (p ^ n : (a : α) → α) ((p ^ k : (a : α) → α) x : α) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ((p.toList x).rotate k) n hn'
h₁ :
  (p ^ n : (a : α) → α) ((p ^ k : (a : α) → α) x : α) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) ((n + k) % (p.toList x).length) ⋯
h₂ :
  Eq (α := α) ((p ^ n : (a : α) → α) ((p ^ k : (a : α) → α) x : α) : α)
    ((p ^ ((n + k) % (p.toList x).length) : (a : α) → α) x : α)
h₃ :
  Eq (α := α) ((p ^ n : (a : α) → α) ((p ^ k : (a : α) → α) x : α) : α)
    ((p ^ ((n + k) % (p.cycleOf x).support.card) : (a : α) → α) x : α)
h₄ : Eq (α := α) ((p ^ n : (a : α) → α) ((p ^ k : (a : α) → α) x : α) : α) ((p ^ (n + k) : (a : α) → α) x : α)
h₅ : Eq (α := α) ((p ^ n : (a : α) → α) ((p ^ k : (a : α) → α) x : α) : α) ((p ^ n * p ^ k : (a : α) → α) x : α)
h₆ h₇ :
  Eq (α := α) ((p ^ n : (a : α) → α) ((p ^ k : (a : α) → α) x : α) : α)
    ((p ^ n : (a : α) → α) ((p ^ k : (a : α) → α) x : α) : α)
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList ((p ^ k : (a : α) → α) x)) n hn =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) ((p.toList x).rotate k) n hn'

Tactic:
rw [getElem_toList, getElem_rotate, getElem_toList, length_toList,
      pow_mod_card_support_cycleOf_self_apply, pow_add, mul_apply]

Premises used: pow_add, List.getElem_rotate, Equiv.Perm.getElem_toList, Equiv.Perm.pow_mod_card_support_cycleOf_self_apply, Equiv.Perm.mul_apply, Equiv.Perm.length_toList
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x y : α
h : f.SameCycle x y
pos : ∀ (hx : x ∈ f.support), f.toList x ~r f.toList y
neg : ∀ (hx : x ∉ f.support), f.toList x ~r f.toList y
⊢ f.toList x ~r f.toList y

Tactic:
by_cases hx : x ∈ f.support

Premises used: Equiv.Perm.support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x y : α
h : f.SameCycle x y
hx : x ∈ f.support
pos : 0 < (f.cycleOf x).support.card → ∀ (hy : (HPow.hPow (β := ℕ) f 0 : (a : α) → α) x = y), f.toList x ~r f.toList y
pos₁ :
  ∀ (k : ℕ), k + 1 < (f.cycleOf x).support.card → ∀ (hy : (f ^ (k + 1) : (a : α) → α) x = y), f.toList x ~r f.toList y
⊢ f.toList x ~r f.toList y

Tactic:
obtain ⟨_ | k, _, hy⟩ := h.exists_pow_eq_of_mem_support hx

Premises used: Equiv.Perm.SameCycle.exists_pow_eq_of_mem_support