awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
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)).support ⊆ (p.cycleOf x ^ (m + 1)).support
have neg : (p.cycleOf x ^ (n + 1)).support ⊆ (p.cycleOf x).support
Tactic: rw [hm', hn']
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
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
⊢ (p.cycleOf x ^ (n + 1)).support ⊆ (p.cycleOf x ^ (m + 1)).support
have neg₁ : (p.cycleOf x).support ⊆ (p.cycleOf x).support
Tactic: rw [hm', hn']
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
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
⊢ ∀ 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 : α)
have neg : ∀ x_1 ∈ (p.cycleOf x).support,
  Eq (α := α) ((p.cycleOf x ^ (n + 1) : (a : α) → α) x_1 : α) ((p.cycleOf x ^ (m + 1) : (a : α) → α) x_1 : α)
Tactic: rw [hm']
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
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
⊢ Eq (α := α) ((p.cycleOf x ^ (n + 1) : (a : α) → α) y : α) ((p.cycleOf x ^ (m + 1) : (a : α) → α) y : α)
have 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 : α) : α)
Tactic: obtain ⟨k, rfl⟩ := hc.exists_pow_eq (mem_support.mp hx) (mem_support.mp hy)
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
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 : α)
⊢ 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 : α) : α)
have 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 : α) : α)
Tactic: rw [← mul_apply, (Commute.pow_pow_self _ _ _).eq, mul_apply, h, ← mul_apply, ← mul_apply,
      (Commute.pow_pow_self _ _ _).eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
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 : α) : α)
⊢ 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 : α) : α)
have 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 : α) : α)
Tactic: rw [← mul_apply, (Commute.pow_pow_self _ _ _).eq, mul_apply, h, ← mul_apply, ← mul_apply,
      (Commute.pow_pow_self _ _ _).eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
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 : α) : α)
⊢ 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 : α) : α)
have 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 : α) : α)
Tactic: rw [← mul_apply, (Commute.pow_pow_self _ _ _).eq, mul_apply, h, ← mul_apply, ← mul_apply,
      (Commute.pow_pow_self _ _ _).eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
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 : α) : α)
⊢ 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 : α) : α)
have 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 : α) : α)
Tactic: rw [← mul_apply, (Commute.pow_pow_self _ _ _).eq, mul_apply, h, ← mul_apply, ← mul_apply,
      (Commute.pow_pow_self _ _ _).eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
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 : α) : α)
⊢ 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 : α) : α)
have 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 : α) : α)
Tactic: rw [← mul_apply, (Commute.pow_pow_self _ _ _).eq, mul_apply, h, ← mul_apply, ← mul_apply,
      (Commute.pow_pow_self _ _ _).eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
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 : α) : α)
⊢ 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 : α) : α)
have neg₅ : Eq (α := α) ((p.cycleOf x ^ k * p.cycleOf x ^ (m + 1) : (a : α) → α) x : α)
  ((p.cycleOf x ^ (m + 1) * 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]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
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 : α)
⊢ 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 : α) : α)
have neg₆ : Eq (α := α) ((p.cycleOf x ^ (m + 1) * p.cycleOf x ^ k : (a : α) → α) x : α)
  ((p.cycleOf x ^ (m + 1) * 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]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x y : α
hy : y ∈ p.toList x
⊢ (p.toList x).next y hy = (p : (a : α) → α) y
have hy₁ : p.SameCycle x y ∧ x ∈ p.support
Tactic: rw [mem_toList_iff] at hy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
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
⊢ (p.toList x).next y hy_1 = (p : (a : α) → α) y
have 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
Tactic: obtain ⟨k, hk, hk'⟩ := hy.left.exists_pow_eq_of_mem_support hy.right
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (hypothesis)
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
⊢ (p.toList x).next y hy_1 = (p : (a : α) → α) y
have hk'₁ : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) k sorry = y
Tactic: rw [← getElem_toList p x k (by simpa using hk)] at hk'
Cleared hypotheses: hk'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
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.toList x).next y hy_1 = (p : (a : α) → α) y
have simp_rw : (p.toList x).next (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) k sorry) sorry =
  (p : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) k sorry)
Tactic: simp_rw [← hk']
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
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.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 ⋯)
have rw : Eq (α := α) ((p ^ ((k + 1) % (p.toList x).length) : (a : α) → α) x : α) ((p ^ (k + 1) : (a : α) → α) x : α)
Tactic: rw [next_getElem _ (nodup_toList _ _), getElem_toList, getElem_toList, ← mul_apply, ← pow_succ']
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
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
⊢ Eq (α := α) ((p ^ ((k + 1) % (p.toList x).length) : (a : α) → α) x : α) ((p ^ (k + 1) : (a : α) → α) x : α)
have simp_rw : Eq (α := α) ((p ^ ((k + 1) % (p.cycleOf x).support.card) : (a : α) → α) x : α) ((p ^ (k + 1) : (a : α) → α) x : α)
Tactic: simp_rw [length_toList]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
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
⊢ Eq (α := α) ((p ^ ((k + 1) % (p.cycleOf x).support.card) : (a : α) → α) x : α) ((p ^ (k + 1) : (a : α) → α) x : α)
have rw : (p.cycleOf x).IsCycle
Tactic: rw [← pow_mod_orderOf_cycleOf_apply p (k + 1), IsCycle.orderOf]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
k : ℕ
⊢ p.toList ((p ^ k : (a : α) → α) x) = (p.toList x).rotate k
have hl : (p.toList ((p ^ k : (a : α) → α) x)).length = ((p.toList x).rotate k).length
Tactic: apply ext_getElem
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
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
⊢ p.toList ((p ^ k : (a : α) → α) x) = (p.toList x).rotate k
have 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₂
Tactic: apply ext_getElem
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
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
⊢ 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'
have h : (p ^ n : (a : α) → α) ((p ^ k : (a : α) → α) x : α) =
  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]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
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'
⊢ 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'
have 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) sorry
Tactic: rw [getElem_toList, getElem_rotate, getElem_toList, length_toList,
      pow_mod_card_support_cycleOf_self_apply, pow_add, mul_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
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) ⋯
⊢ 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'
have h₂ : Eq (α := α) ((p ^ n : (a : α) → α) ((p ^ k : (a : α) → α) x : α) : α)
  ((p ^ ((n + k) % (p.toList x).length) : (a : α) → α) x : α)
Tactic: rw [getElem_toList, getElem_rotate, getElem_toList, length_toList,
      pow_mod_card_support_cycleOf_self_apply, pow_add, mul_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
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 : α)
⊢ 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'
have h₃ : Eq (α := α) ((p ^ n : (a : α) → α) ((p ^ k : (a : α) → α) x : α) : α)
  ((p ^ ((n + k) % (p.cycleOf x).support.card) : (a : α) → α) x : α)
Tactic: rw [getElem_toList, getElem_rotate, getElem_toList, length_toList,
      pow_mod_card_support_cycleOf_self_apply, pow_add, mul_apply]