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 : α
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 : α)
⊢ 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) : (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 : α)
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 : α)
⊢ 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 * p ^ k : (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 : α)
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 : α)
⊢ 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 : (a : α) → α) ((p ^ k : (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 α
f : Perm α
x y : α
h : f.SameCycle x y
⊢ f.toList x ~r f.toList y
have pos : ∀ (hx : x ∈ f.support), f.toList x ~r f.toList y
Tactic: by_cases hx : x ∈ f.support
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
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
⊢ f.toList x ~r f.toList y
have neg : ∀ (hx : x ∉ f.support), f.toList x ~r f.toList y
Tactic: by_cases hx : x ∈ f.support
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x y : α
h : f.SameCycle x y
hx : x ∈ f.support
⊢ f.toList x ~r f.toList y
have pos : 0 < (f.cycleOf x).support.card → ∀ (hy : (HPow.hPow (β := ℕ) f 0 : (a : α) → α) x = y), f.toList x ~r f.toList y
Tactic: obtain ⟨_ | k, _, hy⟩ := h.exists_pow_eq_of_mem_support hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
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
⊢ f.toList x ~r f.toList y
have pos₁ : ∀ (k : ℕ), k + 1 < (f.cycleOf x).support.card → ∀ (hy : (f ^ (k + 1) : (a : α) → α) x = y), f.toList x ~r f.toList y
Tactic: obtain ⟨_ | k, _, hy⟩ := h.exists_pow_eq_of_mem_support hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x y : α
h : f.SameCycle x y
hx : x ∈ f.support
left : 0 < (f.cycleOf x).support.card
hy : (HPow.hPow (β := ℕ) f 0 : (a : α) → α) x = y
⊢ f.toList x ~r f.toList y
have hy₁ : x = y
Tactic: simp only [coe_one, id, pow_zero] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x y : α
h : f.SameCycle x y
hx : x ∈ f.support
k : ℕ
left : k + 1 < (f.cycleOf x).support.card
hy : (f ^ (k + 1) : (a : α) → α) x = y
⊢ f.toList x ~r f.toList y
have h₁ : (f.toList x).rotate k.succ = f.toList y
Tactic: use k.succ
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x y : α
h : f.SameCycle x y
hx : x ∈ f.support
k : ℕ
left : k + 1 < (f.cycleOf x).support.card
hy : (f ^ (k + 1) : (a : α) → α) x = y
⊢ (f.toList x).rotate k.succ = f.toList y
have h₁ : f.toList ((f ^ k.succ : (a : α) → α) x) = f.toList y
Tactic: rw [← toList_pow_apply_eq_rotate, hy]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x y : α
h : f.SameCycle x y
hx : x ∈ f.support
k : ℕ
left : k + 1 < (f.cycleOf x).support.card
hy : (f ^ (k + 1) : (a : α) → α) x = y
h₁ : f.toList ((f ^ k.succ : (a : α) → α) x) = f.toList y
⊢ (f.toList x).rotate k.succ = f.toList y
have h₂ : f.toList y = f.toList y
Tactic: rw [← toList_pow_apply_eq_rotate, hy]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x y : α
h : f.SameCycle x y
hx : x ∉ f.support
⊢ f.toList x ~r f.toList y
have neg : y ∉ f.support
Tactic: rw [toList_eq_nil_iff.mpr hx, isRotated_nil_iff', eq_comm, toList_eq_nil_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
n : ℕ
⊢ Membership.mem (α := α) (p.toList x) ((p ^ n : (a : α) → α) x : α) ↔ x ∈ p.support
have rw : x ∈ p.support → p.SameCycle x ((p ^ n : (a : α) → α) x)
Tactic: rw [mem_toList_iff, and_iff_right_iff_imp]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
n : ℕ
⊢ x ∈ p.support → p.SameCycle x ((p ^ n : (a : α) → α) x)
have refine : x ∈ p.support → p.SameCycle ((p ^ n : (a : α) → α) x) x
Tactic: refine fun _ => SameCycle.symm ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
n : ℕ
h : x ∈ p.support
⊢ p.SameCycle ((p ^ n : (a : α) → α) x) x
have rw : p.SameCycle x x
Tactic: rw [sameCycle_pow_left]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
⊢ l.formPerm.toList (l.get (⟨0, ⋯⟩ : Fin l.length)) = l
have hc : l.formPerm.IsCycle
Tactic: have hc : l.formPerm.IsCycle := List.isCycle_formPerm hn hl
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
hc : l.formPerm.IsCycle
⊢ l.formPerm.support = l.toFinset
have refine : ∀ (x : α), l ≠ [x]
Tactic: refine support_formPerm_of_nodup _ hn ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
hc : l.formPerm.IsCycle
⊢ l.formPerm.toList (l.get (⟨0, ⋯⟩ : Fin l.length)) = l
have hs : l.formPerm.support = l.toFinset
Tactic: have hs : l.formPerm.support = l.toFinset := by
    refine support_formPerm_of_nodup _ hn ?_
    rintro _ rfl
    simp at hl
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
hc : l.formPerm.IsCycle
hs : l.formPerm.support = l.toFinset
⊢ l.formPerm.toList (l.get (⟨0, ⋯⟩ : Fin l.length)) = l
have rw : iterate (⇑l.formPerm : (a : α) → α) (l.get (⟨0, sorry⟩ : Fin l.length)) l.length = l
Tactic: rw [toList, hc.cycleOf_eq (mem_support.mp _), hs, card_toFinset, dedup_eq_self.mpr hn]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
hc : l.formPerm.IsCycle
hs : l.formPerm.support = l.toFinset
rw : iterate (⇑l.formPerm : (a : α) → α) (l.get (⟨0, ⋯⟩ : Fin l.length)) l.length = l
⊢ l.formPerm.toList (l.get (⟨0, ⋯⟩ : Fin l.length)) = l
have rw₁ : l.get (⟨0, sorry⟩ : Fin l.length) ∈ l.formPerm.support
Tactic: rw [toList, hc.cycleOf_eq (mem_support.mp _), hs, card_toFinset, dedup_eq_self.mpr hn]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
hc : l.formPerm.IsCycle
hs : l.formPerm.support = l.toFinset
⊢ iterate (⇑l.formPerm : (a : α) → α) (l.get (⟨0, ⋯⟩ : Fin l.length)) l.length = l
have refine : ∀ (k : ℕ) (hk : k < (iterate (⇑l.formPerm : (a : α) → α) (l.get (⟨0, sorry⟩ : Fin l.length)) l.length).length)
  (hk' : k < l.length),
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length)
      (iterate (⇑l.formPerm : (a : α) → α) (l.get (⟨0, sorry⟩ : Fin l.length)) l.length) k hk =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk'
Tactic: refine ext_getElem (by simp) fun k hk hk' => ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
x : α
hx : x ∈ l
⊢ l.formPerm.toList x ~r l
have obtain : ∀ (k : Fin l.length) (hx : l.get k ∈ l), l.formPerm.toList (l.get k) ~r l
Tactic: obtain ⟨k, hk, rfl⟩ := get_of_mem hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
k : Fin l.length
hx : l.get k ∈ l
⊢ l.formPerm.toList (l.get k) ~r l
have hr : l ~r l.rotate (↑k : ℕ)
Tactic: have hr : l ~r l.rotate k := ⟨k, rfl⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
k : Fin l.length
hx : l.get k ∈ l
hr : l ~r l.rotate (↑k : ℕ)
⊢ l.formPerm.toList (l.get k) ~r l
have rw : (l.rotate (↑k : ℕ)).formPerm.toList (l.get k) ~r l
Tactic: rw [formPerm_eq_of_isRotated hn hr]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
k : Fin l.length
hx : l.get k ∈ l
hr : l ~r l.rotate (↑k : ℕ)
⊢ (l.rotate (↑k : ℕ)).formPerm.toList (l.get k) ~r l
have rw : (l.rotate (↑k : ℕ)).formPerm.toList
    ((l.rotate (↑k : ℕ)).get
      (⟨(l.length - (↑k : ℕ) % l.length + (↑k : ℕ)) % l.length, sorry⟩ : Fin (l.rotate (↑k : ℕ)).length)) ~r
  l
Tactic: rw [get_eq_get_rotate l k k]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
k : Fin l.length
hx : l.get k ∈ l
hr : l ~r l.rotate (↑k : ℕ)
⊢ (l.rotate (↑k : ℕ)).formPerm.toList
      ((l.rotate (↑k : ℕ)).get
        (⟨(l.length - (↑k : ℕ) % l.length + (↑k : ℕ)) % l.length, ⋯⟩ : Fin (l.rotate (↑k : ℕ)).length)) ~r
    l
have simp : (l.rotate (↑k : ℕ)).formPerm.toList ((l.rotate (↑k : ℕ)).get (⟨0, sorry⟩ : Fin (l.rotate (↑k : ℕ)).length)) ~r l
Tactic: simp only [Nat.mod_eq_of_lt k.2, tsub_add_cancel_of_le (le_of_lt k.2), Nat.mod_self]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
k : Fin l.length
hx : l.get k ∈ l
hr : l ~r l.rotate (↑k : ℕ)
⊢ (l.rotate (↑k : ℕ)).formPerm.toList ((l.rotate (↑k : ℕ)).get (⟨0, ⋯⟩ : Fin (l.rotate (↑k : ℕ)).length)) ~r l
have rw : l.rotate (↑k : ℕ) ~r l
Tactic: rw [toList_formPerm_nontrivial]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
k : Fin l.length
hx : l.get k ∈ l
hr : l ~r l.rotate (↑k : ℕ)
rw : l.rotate (↑k : ℕ) ~r l
⊢ (l.rotate (↑k : ℕ)).formPerm.toList ((l.rotate (↑k : ℕ)).get (⟨0, ⋯⟩ : Fin (l.rotate (↑k : ℕ)).length)) ~r l
have hl₁ : 2 ≤ (l.rotate (↑k : ℕ)).length
Tactic: rw [toList_formPerm_nontrivial]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
k : Fin l.length
hx : l.get k ∈ l
hr : l ~r l.rotate (↑k : ℕ)
rw : l.rotate (↑k : ℕ) ~r l
hl₁ : 2 ≤ (l.rotate (↑k : ℕ)).length
⊢ (l.rotate (↑k : ℕ)).formPerm.toList ((l.rotate (↑k : ℕ)).get (⟨0, ⋯⟩ : Fin (l.rotate (↑k : ℕ)).length)) ~r l
have hn₁ : (l.rotate (↑k : ℕ)).Nodup
Tactic: rw [toList_formPerm_nontrivial]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x : α
⊢ (f.toList x).formPerm = f.cycleOf x
have pos : ∀ (hx : (f : (a : α) → α) x = x), (f.toList x).formPerm = f.cycleOf x
Tactic: by_cases hx : f x = x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x : α
pos : ∀ (hx : (f : (a : α) → α) x = x), (f.toList x).formPerm = f.cycleOf x
⊢ (f.toList x).formPerm = f.cycleOf x
have neg : ∀ (hx : ¬(f : (a : α) → α) x = x), (f.toList x).formPerm = f.cycleOf x
Tactic: by_cases hx : f x = x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x : α
hx : (f : (a : α) → α) x = x
⊢ (f.toList x).formPerm = f.cycleOf x
have pos : (f.toList x).formPerm = 1
Tactic: rw [(cycleOf_eq_one_iff f).mpr hx, toList_eq_nil_iff.mpr (notMem_support.mpr hx),
      formPerm_nil]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x : α
hx : (f : (a : α) → α) x = x
pos : (f.toList x).formPerm = 1
⊢ (f.toList x).formPerm = f.cycleOf x
have pos₁ : Eq.{u_1 + 1} (α := Perm α) (formPerm []) 1
Tactic: rw [(cycleOf_eq_one_iff f).mpr hx, toList_eq_nil_iff.mpr (notMem_support.mpr hx),
      formPerm_nil]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x : α
hx : (f : (a : α) → α) x = x
pos : (f.toList x).formPerm = 1
pos₁ : Eq.{u_1 + 1} (α := Perm α) (formPerm []) 1
⊢ (f.toList x).formPerm = f.cycleOf x
have pos₂ : Eq.{u_1 + 1} (α := Perm α) 1 1
Tactic: rw [(cycleOf_eq_one_iff f).mpr hx, toList_eq_nil_iff.mpr (notMem_support.mpr hx),
      formPerm_nil]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x : α
hx : ¬(f : (a : α) → α) x = x
⊢ (f.toList x).formPerm = f.cycleOf x
have neg : ∀ (y : α), Eq (α := α) (((f.toList x).formPerm : (a : α) → α) y : α) ((f.cycleOf x : (a : α) → α) y : α)
Tactic: ext y
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x : α
hx : ¬(f : (a : α) → α) x = x
y : α
⊢ Eq (α := α) (((f.toList x).formPerm : (a : α) → α) y : α) ((f.cycleOf x : (a : α) → α) y : α)
have pos : ∀ (hy : f.SameCycle x y), Eq (α := α) (((f.toList x).formPerm : (a : α) → α) y : α) ((f.cycleOf x : (a : α) → α) y : α)
Tactic: by_cases hy : SameCycle f x y
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x : α
hx : ¬(f : (a : α) → α) x = x
y : α
pos :
  ∀ (hy : f.SameCycle x y),
    Eq (α := α) (((f.toList x).formPerm : (a : α) → α) y : α) ((f.cycleOf x : (a : α) → α) y : α)
⊢ Eq (α := α) (((f.toList x).formPerm : (a : α) → α) y : α) ((f.cycleOf x : (a : α) → α) y : α)
have neg : ∀ (hy : ¬f.SameCycle x y), Eq (α := α) (((f.toList x).formPerm : (a : α) → α) y : α) ((f.cycleOf x : (a : α) → α) y : α)
Tactic: by_cases hy : SameCycle f x y
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x : α
hx : ¬(f : (a : α) → α) x = x
y : α
hy : f.SameCycle x y
⊢ Eq (α := α) (((f.toList x).formPerm : (a : α) → α) y : α) ((f.cycleOf x : (a : α) → α) y : α)
have pos : ∀ k < (f.cycleOf x).support.card,
  ∀ (hy : f.SameCycle x ((f ^ k : (a : α) → α) x)),
    Eq (α := α) (((f.toList x).formPerm : (a : α) → α) ((f ^ k : (a : α) → α) x : α) : α)
      ((f.cycleOf x : (a : α) → α) ((f ^ k : (a : α) → α) x : α) : α)
Tactic: obtain ⟨k, _, rfl⟩ := hy.exists_pow_eq_of_mem_support (mem_support.mpr hx)
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x : α
hx : ¬(f : (a : α) → α) x = x
k : ℕ
left : k < (f.cycleOf x).support.card
hy : f.SameCycle x ((f ^ k : (a : α) → α) x)
⊢ Eq (α := α) (((f.toList x).formPerm : (a : α) → α) ((f ^ k : (a : α) → α) x : α) : α)
    ((f.cycleOf x : (a : α) → α) ((f ^ k : (a : α) → α) x : α) : α)
have pos : Membership.mem (α := α) (f.toList x) ((f ^ k : (a : α) → α) x : α)
Tactic: rw [cycleOf_apply_apply_pow_self, List.formPerm_apply_mem_eq_next (nodup_toList f x),
      next_toList_eq_apply, pow_succ', mul_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x : α
hx : ¬(f : (a : α) → α) x = x
k : ℕ
left : k < (f.cycleOf x).support.card
hy : f.SameCycle x ((f ^ k : (a : α) → α) x)
⊢ Membership.mem (α := α) (f.toList x) ((f ^ k : (a : α) → α) x : α)
have pos : f.SameCycle x ((f ^ k : (a : α) → α) x) ∧ x ∈ f.support
Tactic: rw [mem_toList_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x : α
hx : ¬(f : (a : α) → α) x = x
y : α
hy : ¬f.SameCycle x y
⊢ Eq (α := α) (((f.toList x).formPerm : (a : α) → α) y : α) ((f.cycleOf x : (a : α) → α) y : α)
have neg : y ∉ f.toList x
Tactic: rw [cycleOf_apply_of_not_sameCycle hy, formPerm_apply_of_notMem]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x_1 : α
f : Perm α
hf : f.IsCycle
x y : α
m : Multiset α
s : Cycle α
⊢ (if (f : (a : α) → α) x = x then if (f : (a : α) → α) y = y then s else (↑(f.toList y) : Cycle α)
    else (↑(f.toList x) : Cycle α)) ≍
    if (f : (a : α) → α) y = y then if (f : (a : α) → α) x = x then s else (↑(f.toList x) : Cycle α)
    else (↑(f.toList y) : Cycle α)
have refine : (if (f : (a : α) → α) x = x then if (f : (a : α) → α) y = y then s else (↑(f.toList y) : Cycle α)
  else (↑(f.toList x) : Cycle α)) =
  if (f : (a : α) → α) y = y then if (f : (a : α) → α) x = x then s else (↑(f.toList x) : Cycle α)
  else (↑(f.toList y) : Cycle α)
Tactic: refine heq_of_eq ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x_1 : α
f : Perm α
hf : f.IsCycle
x y : α
m : Multiset α
s : Cycle α
⊢ (if (f : (a : α) → α) x = x then if (f : (a : α) → α) y = y then s else (↑(f.toList y) : Cycle α)
    else (↑(f.toList x) : Cycle α)) =
    if (f : (a : α) → α) y = y then if (f : (a : α) → α) x = x then s else (↑(f.toList x) : Cycle α)
    else (↑(f.toList y) : Cycle α)
have pos : ∀ (hx : (f : (a : α) → α) x = x) (hy : (f : (a : α) → α) y = y), s = s
Tactic: split_ifs with hx hy hy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x_1 : α
f : Perm α
hf : f.IsCycle
x y : α
m : Multiset α
s : Cycle α
pos : ∀ (hx : (f : (a : α) → α) x = x) (hy : (f : (a : α) → α) y = y), s = s
⊢ (if (f : (a : α) → α) x = x then if (f : (a : α) → α) y = y then s else (↑(f.toList y) : Cycle α)
    else (↑(f.toList x) : Cycle α)) =
    if (f : (a : α) → α) y = y then if (f : (a : α) → α) x = x then s else (↑(f.toList x) : Cycle α)
    else (↑(f.toList y) : Cycle α)
have neg : ∀ (hx : (f : (a : α) → α) x = x) (hy : ¬(f : (a : α) → α) y = y), (↑(f.toList y) : Cycle α) = (↑(f.toList y) : Cycle α)
Tactic: split_ifs with hx hy hy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x_1 : α
f : Perm α
hf : f.IsCycle
x y : α
m : Multiset α
s : Cycle α
pos : ∀ (hx : (f : (a : α) → α) x = x) (hy : (f : (a : α) → α) y = y), s = s
neg :
  ∀ (hx : (f : (a : α) → α) x = x) (hy : ¬(f : (a : α) → α) y = y),
    (↑(f.toList y) : Cycle α) = (↑(f.toList y) : Cycle α)
⊢ (if (f : (a : α) → α) x = x then if (f : (a : α) → α) y = y then s else (↑(f.toList y) : Cycle α)
    else (↑(f.toList x) : Cycle α)) =
    if (f : (a : α) → α) y = y then if (f : (a : α) → α) x = x then s else (↑(f.toList x) : Cycle α)
    else (↑(f.toList y) : Cycle α)
have pos₁ : ∀ (hx : ¬(f : (a : α) → α) x = x) (hy : (f : (a : α) → α) y = y), (↑(f.toList x) : Cycle α) = (↑(f.toList x) : Cycle α)
Tactic: split_ifs with hx hy hy