awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
left : 0 < (f.cycleOf x).support.card
hy : (HPow.hPow (β := ℕ) f 0 : (a : α) → α) x = y
⊢ x = y

Tactic:
simp only [coe_one, id, pow_zero] at hy

Premises used: id, Equiv.Perm.coe_one, pow_zero
-- 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
left : 0 < (f.cycleOf x).support.card
hy : x = y
⊢ f.toList x ~r f.toList y

Tactic:
simp [hy, IsRotated.refl]

Premises used: List.IsRotated.refl
-- 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
k : ℕ
left : k + 1 < (f.cycleOf x).support.card
hy : (f ^ (k + 1) : (a : α) → α) x = y
h₁ : (f.toList x).rotate k.succ = f.toList y
⊢ f.toList x ~r f.toList y

Tactic:
use k.succ

Premises used: Nat.succ
-- 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
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
h₂ h₃ : f.toList y = f.toList y
⊢ (f.toList x).rotate k.succ = f.toList y

Tactic:
rw [← toList_pow_apply_eq_rotate, hy]

Premises used: Equiv.Perm.toList_pow_apply_eq_rotate
-- 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
neg : y ∉ f.support
⊢ f.toList x ~r f.toList y

Tactic:
rw [toList_eq_nil_iff.mpr hx, isRotated_nil_iff', eq_comm, toList_eq_nil_iff]

Premises used: Iff.mpr, List.isRotated_nil_iff', Equiv.Perm.toList_eq_nil_iff, eq_comm
-- 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 neg neg₁ neg₂ neg₃ : x ∉ f.support
⊢ y ∉ f.support

Tactic:
rwa [← h.mem_support_iff]

Premises used: Equiv.Perm.SameCycle.mem_support_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
n : ℕ
rw : x ∈ p.support → p.SameCycle x ((p ^ n : (a : α) → α) x)
⊢ Membership.mem (α := α) (p.toList x) ((p ^ n : (a : α) → α) x : α) ↔ x ∈ p.support

Tactic:
rw [mem_toList_iff, and_iff_right_iff_imp]

Premises used: Equiv.Perm.mem_toList_iff, and_iff_right_iff_imp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
n : ℕ
⊢ x ∈ p.support → p.SameCycle x ((p ^ n : (a : α) → α) x)

Tactic:
fun _ => SameCycle.symm ?_

Premises used: Equiv.Perm.SameCycle.symm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
n : ℕ
refine : x ∈ p.support → p.SameCycle ((p ^ n : (a : α) → α) x) x
⊢ x ∈ p.support → p.SameCycle x ((p ^ n : (a : α) → α) x)

Tactic:
refine fun _ => SameCycle.symm ?_

Premises used: Equiv.Perm.SameCycle.symm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
n : ℕ
h : x ∈ p.support
rw rw₁ : p.SameCycle x x
⊢ p.SameCycle ((p ^ n : (a : α) → α) x) x

Tactic:
rw [sameCycle_pow_left]

Premises used: Equiv.Perm.sameCycle_pow_left
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x : α
⊢ toList (formPerm []) x = []

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x y : α
⊢ [x].formPerm.toList y = []

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
⊢ l.formPerm.IsCycle

Tactic:
have hc : l.formPerm.IsCycle := List.isCycle_formPerm hn hl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
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

Tactic:
support_formPerm_of_nodup _ hn ?_

Premises used: List.support_formPerm_of_nodup
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
hc : l.formPerm.IsCycle
refine : ∀ (x : α), l ≠ [x]
⊢ l.formPerm.support = l.toFinset

Tactic:
refine support_formPerm_of_nodup _ hn ?_

Premises used: List.support_formPerm_of_nodup
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x : α
hl : 2 ≤ [x].length
hn : [x].Nodup
hc : [x].formPerm.IsCycle
⊢ False

Tactic:
simp at hl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
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

Tactic:
have hs : l.formPerm.support = l.toFinset := by
    refine support_formPerm_of_nodup _ hn ?_
    rintro _ rfl
    simp at hl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
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
rw₁ : l.get (⟨0, ⋯⟩ : Fin l.length) ∈ l.formPerm.support
⊢ l.formPerm.toList (l.get (⟨0, ⋯⟩ : Fin l.length)) = l

Tactic:
rw [toList, hc.cycleOf_eq (mem_support.mp _), hs, card_toFinset, dedup_eq_self.mpr hn]

Premises used: Iff.mpr, Equiv.Perm.toList, List.dedup_eq_self, Equiv.Perm.mem_support, List.card_toFinset, Equiv.Perm.IsCycle.cycleOf_eq, Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
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).length = l.length

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
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
refine :
  ∀ (k : ℕ) (hk : k < (iterate (⇑l.formPerm : (a : α) → α) (l.get (⟨0, ⋯⟩ : 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, ⋯⟩ : Fin l.length)) l.length) k hk =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk'
⊢ iterate (⇑l.formPerm : (a : α) → α) (l.get (⟨0, ⋯⟩ : Fin l.length)) l.length = l

Tactic:
refine ext_getElem (by simp) fun k hk hk' => ?_

Premises used: List.ext_getElem
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
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
k : ℕ
hk : k < (iterate (⇑l.formPerm : (a : α) → α) (l.get (⟨0, ⋯⟩ : 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, ⋯⟩ : Fin l.length)) l.length) k hk =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk'

Tactic:
simp only [get_eq_getElem, getElem_iterate, iterate_eq_pow, formPerm_pow_apply_getElem _ hn,
      zero_add, Nat.mod_eq_of_lt hk']

Premises used: Equiv.Perm.iterate_eq_pow, List.get_eq_getElem, Nat.mod_eq_of_lt, zero_add, List.formPerm_pow_apply_getElem, List.getElem_iterate
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
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.get (⟨0, ⋯⟩ : Fin l.length) ∈ l.formPerm.support

Tactic:
simp [hs]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
x : α
hx : x ∈ l
obtain : ∀ (k : Fin l.length) (hx : l.get k ∈ l), l.formPerm.toList (l.get k) ~r l
⊢ l.formPerm.toList x ~r l

Tactic:
obtain ⟨k, hk, rfl⟩ := get_of_mem hx

Premises used: List.get_of_mem, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
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 ~r l.rotate (↑k : ℕ)

Tactic:
have hr : l ~r l.rotate k := ⟨k, rfl⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
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 : ℕ)).formPerm.toList (l.get k) ~r l
⊢ l.formPerm.toList (l.get k) ~r l

Tactic:
rw [formPerm_eq_of_isRotated hn hr]

Premises used: List.formPerm_eq_of_isRotated
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
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 : ℕ)).formPerm.toList
      ((l.rotate (↑k : ℕ)).get
        (⟨(l.length - (↑k : ℕ) % l.length + (↑k : ℕ)) % l.length, ⋯⟩ : Fin (l.rotate (↑k : ℕ)).length)) ~r
    l
⊢ (l.rotate (↑k : ℕ)).formPerm.toList (l.get k) ~r l

Tactic:
rw [get_eq_get_rotate l k k]

Premises used: List.get_eq_get_rotate, Fin.val
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
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 : ℕ)
simp : (l.rotate (↑k : ℕ)).formPerm.toList ((l.rotate (↑k : ℕ)).get (⟨0, ⋯⟩ : Fin (l.rotate (↑k : ℕ)).length)) ~r l
⊢ (l.rotate (↑k : ℕ)).formPerm.toList
      ((l.rotate (↑k : ℕ)).get
        (⟨(l.length - (↑k : ℕ) % l.length + (↑k : ℕ)) % l.length, ⋯⟩ : 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]

Premises used: Nat.mod_self, le_of_lt, Fin.isLt, tsub_add_cancel_of_le, Nat.mod_eq_of_lt
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
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
hn₁ : (l.rotate (↑k : ℕ)).Nodup
⊢ (l.rotate (↑k : ℕ)).formPerm.toList ((l.rotate (↑k : ℕ)).get (⟨0, ⋯⟩ : Fin (l.rotate (↑k : ℕ)).length)) ~r l

Tactic:
rw [toList_formPerm_nontrivial]

Premises used: Equiv.Perm.toList_formPerm_nontrivial
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
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 : ℕ) ~r l

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
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 : ℕ)
⊢ 2 ≤ (l.rotate (↑k : ℕ)).length

Tactic:
simpa using hl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
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 : ℕ)).Nodup

Tactic:
simpa using hn
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
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
neg : ∀ (hx : ¬(f : (a : α) → α) x = x), (f.toList x).formPerm = f.cycleOf x
⊢ (f.toList x).formPerm = f.cycleOf x

Tactic:
by_cases hx : f x = x

Premises used: DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
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
pos₂ pos₃ : Eq.{u_1 + 1} (α := Perm α) 1 1
⊢ (f.toList x).formPerm = f.cycleOf x

Tactic:
rw [(cycleOf_eq_one_iff f).mpr hx, toList_eq_nil_iff.mpr (notMem_support.mpr hx),
      formPerm_nil]

Premises used: Iff.mpr, Equiv.Perm.notMem_support, Equiv.Perm.cycleOf_eq_one_iff, Equiv.Perm.toList_eq_nil_iff, List.formPerm_nil
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x : α
hx : ¬(f : (a : α) → α) x = x
neg : ∀ (y : α), Eq (α := α) (((f.toList x).formPerm : (a : α) → α) y : α) ((f.cycleOf x : (a : α) → α) y : α)
⊢ (f.toList x).formPerm = f.cycleOf x

Tactic:
ext y
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
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 : α)
neg :
  ∀ (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 : α)

Tactic:
by_cases hy : SameCycle f x y

Premises used: Equiv.Perm.SameCycle
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x : α
hx : ¬(f : (a : α) → α) x = x
y : α
hy : f.SameCycle x y
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 : α) : α)
⊢ Eq (α := α) (((f.toList x).formPerm : (a : α) → α) y : α) ((f.cycleOf x : (a : α) → α) y : α)

Tactic:
obtain ⟨k, _, rfl⟩ := hy.exists_pow_eq_of_mem_support (mem_support.mpr hx)

Premises used: Equiv.Perm.SameCycle.exists_pow_eq_of_mem_support, Iff.mpr, Equiv.Perm.mem_support, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
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)
pos : Membership.mem (α := α) (f.toList x) ((f ^ k : (a : α) → α) x : α)
⊢ Eq (α := α) (((f.toList x).formPerm : (a : α) → α) ((f ^ k : (a : α) → α) x : α) : α)
    ((f.cycleOf x : (a : α) → α) ((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]

Premises used: Equiv.Perm.next_toList_eq_apply, Equiv.Perm.cycleOf_apply_apply_pow_self, Equiv.Perm.mul_apply, List.formPerm_apply_mem_eq_next, Equiv.Perm.nodup_toList, pow_succ'
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
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)
pos : f.SameCycle x ((f ^ k : (a : α) → α) x) ∧ x ∈ f.support
⊢ Membership.mem (α := α) (f.toList x) ((f ^ k : (a : α) → α) x : α)

Tactic:
rw [mem_toList_iff]

Premises used: Equiv.Perm.mem_toList_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
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)
⊢ f.SameCycle x ((f ^ k : (a : α) → α) x) ∧ x ∈ f.support

Tactic:
⟨⟨k, rfl⟩, mem_support.mpr hx⟩

Premises used: Iff.mpr, Equiv.Perm.mem_support, Nat.cast, And.intro, Exists.intro, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
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)
⊢ f.SameCycle x ((f ^ k : (a : α) → α) x) ∧ x ∈ f.support

Tactic:
exact ⟨⟨k, rfl⟩, mem_support.mpr hx⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x : α
hx : ¬(f : (a : α) → α) x = x
y : α
hy : ¬f.SameCycle x y
neg : y ∉ f.toList x
⊢ Eq (α := α) (((f.toList x).formPerm : (a : α) → α) y : α) ((f.cycleOf x : (a : α) → α) y : α)

Tactic:
rw [cycleOf_apply_of_not_sameCycle hy, formPerm_apply_of_notMem]

Premises used: Equiv.Perm.cycleOf_apply_of_not_sameCycle, List.formPerm_apply_of_notMem
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
x : α
hx : ¬(f : (a : α) → α) x = x
y : α
hy : ¬f.SameCycle x y
⊢ y ∉ f.toList x

Tactic:
simp [mem_toList_iff, 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_1 : α
f : Perm α
hf : f.IsCycle
x y : α
_ :
  ∀ (m : Multiset α) (b : Cycle α),
    (if (f : (a : α) → α) x = x then if (f : (a : α) → α) y = y then b else (↑(f.toList y) : Cycle α)
      else (↑(f.toList x) : Cycle α)) ≍
      if (f : (a : α) → α) y = y then if (f : (a : α) → α) x = x then b else (↑(f.toList x) : Cycle α)
      else (↑(f.toList y) : Cycle α)
⊢ ∀ (m : Multiset α) (b : Cycle α),
    (if (f : (a : α) → α) x = x then if (f : (a : α) → α) y = y then b else (↑(f.toList y) : Cycle α)
      else (↑(f.toList x) : Cycle α)) ≍
      if (f : (a : α) → α) y = y then if (f : (a : α) → α) x = x then b else (↑(f.toList x) : Cycle α)
      else (↑(f.toList y) : Cycle α)

Tactic:
_
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
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 α)

Tactic:
heq_of_eq ?_

Premises used: heq_of_eq
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x_1 : α
f : Perm α
hf : f.IsCycle
x y : α
m : Multiset α
s : Cycle α
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 α)
⊢ (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 ?_

Premises used: heq_of_eq
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
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 α)
pos₁ :
  ∀ (hx : ¬(f : (a : α) → α) x = x) (hy : (f : (a : α) → α) y = y),
    (↑(f.toList x) : Cycle α) = (↑(f.toList x) : Cycle α)
neg₁ :
  ∀ (hx : ¬(f : (a : α) → α) x = x) (hy : ¬(f : (a : α) → α) y = y),
    (↑(f.toList x) : 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 α)

Tactic:
split_ifs with hx hy hy
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x_1 : α
f : Perm α
hf : f.IsCycle
x y : α
m : Multiset α
s : Cycle α
hx : (f : (a : α) → α) x = x
hy : (f : (a : α) → α) y = y
⊢ s = s

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x_1 : α
f : Perm α
hf : f.IsCycle
x y : α
m : Multiset α
s : Cycle α
hx : (f : (a : α) → α) x = x
hy : (f : (a : α) → α) y = y
⊢ s = s

Tactic:
try rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x_1 : α
f : Perm α
hf : f.IsCycle
x y : α
m : Multiset α
s : Cycle α
hx : (f : (a : α) → α) x = x
hy : ¬(f : (a : α) → α) y = y
⊢ (↑(f.toList y) : Cycle α) = (↑(f.toList y) : Cycle α)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x_1 : α
f : Perm α
hf : f.IsCycle
x y : α
m : Multiset α
s : Cycle α
hx : (f : (a : α) → α) x = x
hy : ¬(f : (a : α) → α) y = y
⊢ (↑(f.toList y) : Cycle α) = (↑(f.toList y) : Cycle α)

Tactic:
try rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x_1 : α
f : Perm α
hf : f.IsCycle
x y : α
m : Multiset α
s : Cycle α
hx : ¬(f : (a : α) → α) x = x
hy : (f : (a : α) → α) y = y
⊢ (↑(f.toList x) : Cycle α) = (↑(f.toList x) : Cycle α)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x_1 : α
f : Perm α
hf : f.IsCycle
x y : α
m : Multiset α
s : Cycle α
hx : ¬(f : (a : α) → α) x = x
hy : (f : (a : α) → α) y = y
⊢ (↑(f.toList x) : Cycle α) = (↑(f.toList x) : Cycle α)

Tactic:
try rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x_1 : α
f : Perm α
hf : f.IsCycle
x y : α
m : Multiset α
s : Cycle α
hx : ¬(f : (a : α) → α) x = x
hy : ¬(f : (a : α) → α) y = y
⊢ f.SameCycle x y

Tactic:
have hc : SameCycle f x y := IsCycle.sameCycle hf hx hy
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x_1 : α
f : Perm α
hf : f.IsCycle
x y : α
m : Multiset α
s : Cycle α
hx : ¬(f : (a : α) → α) x = x
hy : ¬(f : (a : α) → α) y = y
hc : f.SameCycle x y
⊢ (↑(f.toList x) : Cycle α) = (↑(f.toList y) : Cycle α)

Tactic:
Quotient.sound' hc.toList_isRotated

Premises used: Quotient.sound', Equiv.Perm.SameCycle.toList_isRotated, Cycle.ofList, Cycle
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x_1 : α
f : Perm α
hf : f.IsCycle
x y : α
m : Multiset α
s : Cycle α
hx : ¬(f : (a : α) → α) x = x
hy : ¬(f : (a : α) → α) y = y
hc : f.SameCycle x y
⊢ (↑(f.toList x) : Cycle α) = (↑(f.toList y) : Cycle α)

Tactic:
exact Quotient.sound' hc.toList_isRotated

Premises used: Quotient.sound'
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hx : (f : (a : α) → α) x ≠ x
⊢ Finset.val Finset.univ = x ::ₘ Multiset.erase (Finset.val Finset.univ) x

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hx : (f : (a : α) → α) x ≠ x
⊢ Finset.val Finset.univ = x ::ₘ Multiset.erase (Finset.val Finset.univ) x

Tactic:
have key : (Finset.univ : Finset α).val = x ::ₘ Finset.univ.val.erase x := by simp