awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
s : Cycle α
h : s.Nodup
hn : s.Nontrivial
h₁ :
  ∀ (a : List α) (h : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a))
    (hn : Nontrivial (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a)),
    (formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a) h).IsCycle
⊢ (s.formPerm h).IsCycle

Tactic:
induction s using Quot.inductionOn
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
a : List α
h : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a)
hn : Nontrivial (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a)
⊢ (formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a) h).IsCycle

Tactic:
List.isCycle_formPerm h (length_nontrivial hn)

Premises used: Cycle.length_nontrivial, List.formPerm, Cycle.formPerm, List.prod, List.isCycle_formPerm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
a : List α
h : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a)
hn : Nontrivial (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a)
⊢ (formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a) h).IsCycle

Tactic:
exact List.isCycle_formPerm h (length_nontrivial hn)

Premises used: Cycle.length_nontrivial, List.isCycle_formPerm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s : Cycle α
h : s.Nodup
hn : s.Nontrivial
mk :
  ∀ (s : List α) (h : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s))
    (hn : Nontrivial (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)),
    (formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s) h).support =
      toFinset (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
⊢ (s.formPerm h).support = s.toFinset

Tactic:
obtain ⟨s⟩ := s
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s_1 : Cycle α
s : List α
h : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
hn : Nontrivial (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
⊢ (formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s) h).support =
    toFinset (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)

Tactic:
support_formPerm_of_nodup s h ?_

Premises used: Cycle.toMultiset, Quotient.liftOn', Cycle.toFinset, List.toFinset, List.support_formPerm_of_nodup, List.formPerm, Multiset.ofList, Cycle.formPerm, List.prod
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s_1 : Cycle α
s : List α
h : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
hn : Nontrivial (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
mk : ∀ (x : α), s ≠ [x]
⊢ (formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s) h).support =
    toFinset (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)

Tactic:
refine support_formPerm_of_nodup s h ?_

Premises used: List.support_formPerm_of_nodup
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s : Cycle α
x : α
h : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [x])
hn : Nontrivial (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [x])
⊢ False

Tactic:
simpa [Nat.succ_le_succ_iff] using length_nontrivial hn

Premises used: Cycle.length_nontrivial, Nat.succ_le_succ_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
s : Cycle α
h : s.Nodup
x : α
hx : x ∉ s
h₁ :
  ∀ (a : List α) (h : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a))
    (hx : x ∉ Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a),
    (formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a) h : (a : α) → α) x = x
⊢ (s.formPerm h : (a : α) → α) x = x

Tactic:
induction s using Quot.inductionOn
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
x : α
a : List α
h : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a)
hx : x ∉ Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a
⊢ (formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a) h : (a : α) → α) x = x

Tactic:
simpa using List.formPerm_apply_of_notMem hx

Premises used: List.formPerm_apply_of_notMem
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
s : Cycle α
h : s.Nodup
x : α
hx : x ∈ s
h₁ :
  ∀ (a : List α) (h : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a))
    (hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a) x),
    (formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a) h : (a : α) → α) x =
      next (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a) h x hx
⊢ (s.formPerm h : (a : α) → α) x = s.next h x hx

Tactic:
induction s using Quot.inductionOn
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
x : α
a : List α
h : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a)
hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a) x
⊢ x ∈ a

Tactic:
simp_all
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
x : α
a : List α
h : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a)
hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a) x
⊢ (formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a) h : (a : α) → α) x =
    next (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a) h x hx

Tactic:
simpa using List.formPerm_apply_mem_eq_next h _ (by simp_all)

Premises used: List.formPerm_apply_mem_eq_next
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
s : Cycle α
h : s.Nodup
h₁ :
  ∀ (a : List α) (h : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a)),
    (reverse (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a)).formPerm ⋯ =
      (formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a) h)⁻¹
⊢ s.reverse.formPerm ⋯ = (s.formPerm h)⁻¹

Tactic:
induction s using Quot.inductionOn
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : DecidableEq α
a : List α
h : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a)
⊢ (reverse (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a)).formPerm ⋯ =
    (formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a) h)⁻¹

Tactic:
simpa using formPerm_reverse _

Premises used: Cycle.formPerm_reverse
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_2
inst : DecidableEq α
s s' : Cycle α
hs : s.Nodup
hs' : s'.Nodup
h :
  ∀ (a₁ a₂ : List α) {hs : Nodup (Quotient.mk'' a₁)} {hs' : Nodup (Quotient.mk'' a₂)},
    formPerm (Quotient.mk'' a₁) hs = formPerm (Quotient.mk'' a₂) hs' ↔
      Eq (α := Cycle α) (Quotient.mk'' a₁) (Quotient.mk'' a₂) ∨
        length (Quotient.mk'' a₁) ≤ 1 ∧ length (Quotient.mk'' a₂) ≤ 1
⊢ s.formPerm hs = s'.formPerm hs' ↔ s = s' ∨ s.length ≤ 1 ∧ s'.length ≤ 1

Tactic:
induction s, s' using Quotient.inductionOn₂'
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_2
inst : DecidableEq α
a₁ a₂ : List α
hs : Nodup (Quotient.mk'' a₁)
hs' : Nodup (Quotient.mk'' a₂)
⊢ formPerm (Quotient.mk'' a₁) hs = formPerm (Quotient.mk'' a₂) hs' ↔
    Eq (α := Cycle α) (Quotient.mk'' a₁) (Quotient.mk'' a₂) ∨
      length (Quotient.mk'' a₁) ≤ 1 ∧ length (Quotient.mk'' a₂) ≤ 1

Tactic:
simpa using formPerm_eq_formPerm_iff hs hs'
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x : α
⊢ toList 1 x = []

Tactic:
simp [toList, cycleOf_one]

Premises used: Equiv.Perm.toList, Equiv.Perm.cycleOf_one
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
⊢ p.toList x = [] ↔ x ∉ p.support

Tactic:
simp [toList]

Premises used: Equiv.Perm.toList
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
⊢ (p.toList x).length = (p.cycleOf x).support.card

Tactic:
simp [toList]

Premises used: Equiv.Perm.toList
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x y : α
H : p.toList x = [y]
⊢ False

Tactic:
simpa [card_support_ne_one] using congr_arg length H

Premises used: Equiv.Perm.card_support_ne_one, congr_arg, List.length
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
⊢ 2 ≤ (p.toList x).length ↔ x ∈ p.support

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
h : x ∈ p.support
⊢ 0 < (p.toList x).length

Tactic:
zero_lt_two.trans_le (two_le_length_toList_iff_mem_support.mpr h)

Premises used: Iff.mpr, LT.lt.trans_le, Equiv.Perm.two_le_length_toList_iff_mem_support, zero_lt_two
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
n : ℕ
hn : n < (p.toList x).length
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) n hn = (p ^ n : (a : α) → α) x

Tactic:
simp [toList, pull_end]

Premises used: Equiv.Perm.toList
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
h : x ∈ p.support
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) 0 ⋯ = x

Tactic:
simp [toList]

Premises used: Equiv.Perm.toList
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x y : α
simp : (∃ m < (p.cycleOf x).support.card, (p ^ m : (a : α) → α) x = y) ↔ p.SameCycle x y ∧ x ∈ p.support
⊢ y ∈ p.toList x ↔ p.SameCycle x y ∧ x ∈ p.support

Tactic:
simp only [toList, mem_iterate, iterate_eq_pow, eq_comm (a := y)]

Premises used: Equiv.Perm.toList, Equiv.Perm.iterate_eq_pow, eq_comm, List.mem_iterate
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x y : α
mp : (∃ m < (p.cycleOf x).support.card, (p ^ m : (a : α) → α) x = y) → p.SameCycle x y ∧ x ∈ p.support
mpr : p.SameCycle x y ∧ x ∈ p.support → ∃ m < (p.cycleOf x).support.card, (p ^ m : (a : α) → α) x = y
⊢ (∃ m < (p.cycleOf x).support.card, (p ^ m : (a : α) → α) x = y) ↔ p.SameCycle x y ∧ x ∈ p.support

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
n : ℕ
hx : n < (p.cycleOf x).support.card
⊢ p.SameCycle x ((p ^ n : (a : α) → α) x) ∧ x ∈ p.support

Tactic:
⟨⟨n, rfl⟩, ?_⟩

Premises used: Nat.cast, And.intro, Exists.intro, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
n : ℕ
hx : n < (p.cycleOf x).support.card
mp : x ∈ p.support
⊢ p.SameCycle x ((p ^ n : (a : α) → α) x) ∧ x ∈ p.support

Tactic:
refine ⟨⟨n, rfl⟩, ?_⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
n : ℕ
hx : n < (p.cycleOf x).support.card
mp : ∀ (hx : x ∉ p.support), (p.cycleOf x).support.card ≤ n
⊢ x ∈ p.support

Tactic:
contrapose! hx
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
n : ℕ
hx : x ∉ p.support
⊢ (p.cycleOf x).support = ∅

Tactic:
rw [← support_cycleOf_eq_nil_iff] at hx

Premises used: Equiv.Perm.support_cycleOf_eq_nil_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
n : ℕ
hx : (p.cycleOf x).support = ∅
⊢ (p.cycleOf x).support.card ≤ n

Tactic:
simp [hx]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x y : α
h : p.SameCycle x y
hx : x ∈ p.support
⊢ ∃ m < (p.cycleOf x).support.card, (p ^ m : (a : α) → α) x = y

Tactic:
simpa using h.exists_pow_eq_of_mem_support hx

Premises used: Equiv.Perm.SameCycle.exists_pow_eq_of_mem_support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
pos : ∀ (hx : (p : (a : α) → α) x = x), (p.toList x).Nodup
neg : ∀ (hx : ¬(p : (a : α) → α) x = x), (p.toList x).Nodup
⊢ (p.toList x).Nodup

Tactic:
by_cases hx : p x = x

Premises used: DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : (p : (a : α) → α) x = x
⊢ p.toList x = []

Tactic:
rw [← notMem_support, ← toList_eq_nil_iff] at hx

Premises used: Equiv.Perm.notMem_support, Equiv.Perm.toList_eq_nil_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : p.toList x = []
⊢ (p.toList x).Nodup

Tactic:
simp [hx]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : ¬(p : (a : α) → α) x = x
⊢ (p.cycleOf x).IsCycle

Tactic:
have hc : IsCycle (cycleOf p x) := isCycle_cycleOf p hx
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : ¬(p : (a : α) → α) x = x
hc : (p.cycleOf x).IsCycle
neg :
  Function.Injective.{1, u_1 + 1} (β := α) fun (i : Fin (p.toList x).length) ↦
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) (↑i : ℕ) ⋯
⊢ (p.toList x).Nodup

Tactic:
rw [nodup_iff_injective_getElem]

Premises used: List.nodup_iff_injective_getElem
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : ¬(p : (a : α) → α) x = x
hc : (p.cycleOf x).IsCycle
n : ℕ
hn : n < (p.toList x).length
neg :
  ∀ (m : ℕ) (hm : m < (p.toList x).length),
    Eq.{u_1 + 1} (α := α)
        ((fun (i : Fin (p.toList x).length) ↦
            getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) (↑i : ℕ) ⋯)
          ⟨n, hn⟩)
        ((fun (i : Fin (p.toList x).length) ↦
            getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) (↑i : ℕ) ⋯)
          ⟨m, hm⟩) →
      (⟨n, hn⟩ : Fin (p.toList x).length) = ⟨m, hm⟩
⊢ ∀ ⦃a₂ : Fin (p.toList x).length⦄,
    Eq.{u_1 + 1} (α := α)
        ((fun (i : Fin (p.toList x).length) ↦
            getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) (↑i : ℕ) ⋯)
          ⟨n, hn⟩)
        ((fun (i : Fin (p.toList x).length) ↦
            getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) (↑i : ℕ) ⋯)
          a₂) →
      (⟨n, hn⟩ : Fin (p.toList x).length) = a₂

Tactic:
⟨m, hm⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : ¬(p : (a : α) → α) x = x
hc : (p.cycleOf x).IsCycle
n : ℕ
hn : n < (p.toList x).length
m : ℕ
hm : m < (p.toList x).length
neg :
  ∀ (hn_1 : n < orderOf (p.cycleOf x)) (m : ℕ) (hm : m < (p.toList x).length) (hm_1 : m < orderOf (p.cycleOf x)),
    Eq.{u_1 + 1} (α := α)
        ((fun (i : Fin (p.toList x).length) ↦
            getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) (↑i : ℕ) ⋯)
          ⟨n, hn⟩)
        ((fun (i : Fin (p.toList x).length) ↦
            getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) (↑i : ℕ) ⋯)
          ⟨m, hm⟩) →
      (⟨n, hn⟩ : Fin (p.toList x).length) = ⟨m, hm⟩
⊢ Eq.{u_1 + 1} (α := α)
      ((fun (i : Fin (p.toList x).length) ↦
          getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) (↑i : ℕ) ⋯)
        ⟨n, hn⟩)
      ((fun (i : Fin (p.toList x).length) ↦
          getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) (↑i : ℕ) ⋯)
        ⟨m, hm⟩) →
    (⟨n, hn⟩ : Fin (p.toList x).length) = ⟨m, hm⟩

Tactic:
rw [length_toList, ← hc.orderOf] at hm hn

Premises used: Equiv.Perm.IsCycle.orderOf, Equiv.Perm.length_toList
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : ¬(p : (a : α) → α) x = x
hc : (p.cycleOf x).IsCycle
n : ℕ
hn_1 : n < (p.toList x).length
hn : n < orderOf (p.cycleOf x)
m : ℕ
hm_1 : m < (p.toList x).length
hm : m < orderOf (p.cycleOf x)
neg :
  ∀ (hx : x ∈ (p.cycleOf x).support) (hc : (p.cycleOf x).IsCycle) (n : ℕ) (hn : n < (p.toList x).length)
    (hn_2 : n < orderOf (p.cycleOf x)) (m : ℕ) (hm : m < (p.toList x).length) (hm_2 : m < orderOf (p.cycleOf x)),
    Eq.{u_1 + 1} (α := α)
        ((fun (i : Fin (p.toList x).length) ↦
            getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) (↑i : ℕ) ⋯)
          ⟨n, hn⟩)
        ((fun (i : Fin (p.toList x).length) ↦
            getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) (↑i : ℕ) ⋯)
          ⟨m, hm⟩) →
      (⟨n, hn⟩ : Fin (p.toList x).length) = ⟨m, hm⟩
⊢ Eq.{u_1 + 1} (α := α)
      ((fun (i : Fin (p.toList x).length) ↦
          getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) (↑i : ℕ) ⋯)
        ⟨n, hn_1⟩)
      ((fun (i : Fin (p.toList x).length) ↦
          getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) (↑i : ℕ) ⋯)
        ⟨m, hm_1⟩) →
    (⟨n, hn_1⟩ : Fin (p.toList x).length) = ⟨m, hm_1⟩

Tactic:
rw [← cycleOf_apply_self, ← Ne, ← mem_support] at hx

Premises used: Equiv.Perm.mem_support, Ne, Equiv.Perm.cycleOf_apply_self
-- 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 < (p.toList x).length
hn : n < orderOf (p.cycleOf x)
m : ℕ
hm_1 : m < (p.toList x).length
hm : m < orderOf (p.cycleOf x)
neg :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) n ⋯ =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) m ⋯ →
    n = m
⊢ Eq.{u_1 + 1} (α := α)
      ((fun (i : Fin (p.toList x).length) ↦
          getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) (↑i : ℕ) ⋯)
        ⟨n, hn_1⟩)
      ((fun (i : Fin (p.toList x).length) ↦
          getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) (↑i : ℕ) ⋯)
        ⟨m, hm_1⟩) →
    (⟨n, hn_1⟩ : Fin (p.toList x).length) = ⟨m, hm_1⟩

Tactic:
simp only [Fin.mk.injEq]

Premises used: Fin.mk.injEq
-- 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 < (p.toList x).length
hn : n < orderOf (p.cycleOf x)
m : ℕ
hm_1 : m < (p.toList x).length
hm : m < orderOf (p.cycleOf x)
neg : Eq (α := α) ((p.cycleOf x ^ n : (a : α) → α) x : α) ((p.cycleOf x ^ m : (a : α) → α) x : α) → n = m
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) n ⋯ =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) m ⋯ →
    n = m

Tactic:
rw [getElem_toList, getElem_toList, ← cycleOf_pow_apply_self p x n, ←
    cycleOf_pow_apply_self p x m]

Premises used: Equiv.Perm.cycleOf_pow_apply_self, Equiv.Perm.getElem_toList
-- 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 < (p.toList x).length
hn : n < orderOf (p.cycleOf x)
m : ℕ
hm_1 : m < (p.toList x).length
hm : m < orderOf (p.cycleOf x)
neg :
  ∀ (hn : 0 < (p.toList x).length) (hn : 0 < orderOf (p.cycleOf x)),
    Eq (α := α) ((HPow.hPow (β := ℕ) (p.cycleOf x) 0 : (a : α) → α) x : α) ((p.cycleOf x ^ m : (a : α) → α) x : α) →
      0 = m
neg₁ :
  ∀ (n : ℕ) (hn : n + 1 < (p.toList x).length) (hn : n + 1 < orderOf (p.cycleOf x)),
    Eq (α := α) ((p.cycleOf x ^ (n + 1) : (a : α) → α) x : α) ((p.cycleOf x ^ m : (a : α) → α) x : α) → n + 1 = m
⊢ Eq (α := α) ((p.cycleOf x ^ n : (a : α) → α) x : α) ((p.cycleOf x ^ m : (a : α) → α) x : α) → n = m

Tactic:
rcases n with - | n
-- 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
m : ℕ
hm_1 : m < (p.toList x).length
hm : m < orderOf (p.cycleOf x)
hn_1 : 0 < (p.toList x).length
hn : 0 < orderOf (p.cycleOf x)
neg :
  ∀ (hm : 0 < (p.toList x).length) (hm : 0 < orderOf (p.cycleOf x)),
    Eq (α := α) ((HPow.hPow (β := ℕ) (p.cycleOf x) 0 : (a : α) → α) x : α)
        ((HPow.hPow (β := ℕ) (p.cycleOf x) 0 : (a : α) → α) x : α) →
      Eq (α := ℕ) 0 0
neg₁ :
  ∀ (m : ℕ) (hm : 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
⊢ Eq (α := α) ((HPow.hPow (β := ℕ) (p.cycleOf x) 0 : (a : α) → α) x : α) ((p.cycleOf x ^ m : (a : α) → α) x : α) → 0 = m

Tactic:
rcases m with - | m
-- 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
m : ℕ
hm_1 : m < (p.toList x).length
hm : m < orderOf (p.cycleOf x)
n : ℕ
hn_1 : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
neg :
  ∀ (hm : 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
neg₁ :
  ∀ (m : ℕ) (hm : m + 1 < (p.toList x).length) (hm : m + 1 < orderOf (p.cycleOf x)),
    Eq (α := α) ((p.cycleOf x ^ (n + 1) : (a : α) → α) x : α) ((p.cycleOf x ^ (m + 1) : (a : α) → α) x : α) →
      n + 1 = m + 1
⊢ Eq (α := α) ((p.cycleOf x ^ (n + 1) : (a : α) → α) x : α) ((p.cycleOf x ^ m : (a : α) → α) x : α) → n + 1 = m

Tactic:
rcases m with - | m
-- 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)
hm_1 : 0 < (p.toList x).length
hm : 0 < orderOf (p.cycleOf x)
⊢ Eq (α := α) ((HPow.hPow (β := ℕ) (p.cycleOf x) 0 : (a : α) → α) x : α)
      ((HPow.hPow (β := ℕ) (p.cycleOf x) 0 : (a : α) → α) x : α) →
    Eq (α := ℕ) 0 0

Tactic:
simp
-- 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)
⊢ (p ^ m.succ : (a : α) → α) x ≠ 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 : α
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
⊢ m + 1 < (p.toList x).length

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