awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
key : Finset.val Finset.univ = x ::ₘ Multiset.erase (Finset.val Finset.univ) x
rw :
  (x ::ₘ Multiset.erase (Finset.val Finset.univ) x).recOn (C := fun (x : Multiset α) ↦ Cycle α)
      (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [])
      (fun (x : α) (x_1 : Multiset α) (l : Cycle α) ↦ if (f : (a : α) → α) x = x then l else (↑(f.toList x) : Cycle α))
      ⋯ =
    (↑(f.toList x) : Cycle α)
⊢ f.toCycle hf = (↑(f.toList x) : Cycle α)

Tactic:
rw [toCycle, key]

Premises used: Equiv.Perm.toCycle
-- 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
key : Finset.val Finset.univ = x ::ₘ Multiset.erase (Finset.val Finset.univ) x
⊢ (x ::ₘ Multiset.erase (Finset.val Finset.univ) x).recOn (C := fun (x : Multiset α) ↦ Cycle α)
      (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [])
      (fun (x : α) (x_1 : Multiset α) (l : Cycle α) ↦ if (f : (a : α) → α) x = x then l else (↑(f.toList x) : Cycle α))
      ⋯ =
    (↑(f.toList x) : Cycle α)

Tactic:
simp [hx]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
hf : f.IsCycle
⊢ ∃ (x : α), f.toCycle hf = (↑(f.toList x) : Cycle α)

Tactic:
Exists.casesOn hf (fun x h => ⟨x, Perm.toCycle_eq_toList f hf x h.1⟩)

Premises used: Exists.casesOn
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
hf : f.IsCycle
obtain : ∀ (x : α) (hx : (f : (a : α) → α) x ≠ x), (f.toCycle hf).Nodup
⊢ (f.toCycle hf).Nodup

Tactic:
obtain ⟨x, hx, -⟩ := id hf

Premises used: id
-- 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
⊢ (f.toCycle hf).Nodup

Tactic:
simpa [toCycle_eq_toList f hf x hx] using nodup_toList _ _

Premises used: Equiv.Perm.toCycle_eq_toList, Equiv.Perm.nodup_toList
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
hf : f.IsCycle
obtain : ∀ (x : α) (hx : (f : (a : α) → α) x ≠ x), (f.toCycle hf).Nontrivial
⊢ (f.toCycle hf).Nontrivial

Tactic:
obtain ⟨x, hx, -⟩ := id hf

Premises used: id
-- 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
⊢ (f.toCycle hf).Nontrivial

Tactic:
simp [toCycle_eq_toList f hf x hx, hx, Cycle.nontrivial_coe_nodup_iff (nodup_toList _ _)]

Premises used: Equiv.Perm.toCycle_eq_toList, Cycle.nontrivial_coe_nodup_iff, Equiv.Perm.nodup_toList
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
mp : x ∈ f.toCycle hf → (f : (a : α) → α) x ≠ x
mpr : (f : (a : α) → α) x ≠ x → x ∈ f.toCycle hf
⊢ x ∈ f.toCycle hf ↔ (f : (a : α) → α) x ≠ x

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
mp : ∀ (l : α) (hl : f.toCycle hf = (↑(f.toList l) : Cycle α)), x ∈ f.toCycle hf → (f : (a : α) → α) x ≠ x
⊢ x ∈ f.toCycle hf → (f : (a : α) → α) x ≠ x

Tactic:
have ⟨l, hl⟩ := exists_toCycle_toList f hf
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
l : α
hl : f.toCycle hf = (↑(f.toList l) : Cycle α)
mp : x ∈ f.toList l → ¬(f : (a : α) → α) x = x
⊢ x ∈ f.toCycle hf → (f : (a : α) → α) x ≠ x

Tactic:
simp only [hl, Cycle.mem_coe_iff, ne_eq]

Premises used: Cycle.mem_coe_iff, ne_eq
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
l : α
hl : f.toCycle hf = (↑(f.toList l) : Cycle α)
h : x ∈ f.toList l
⊢ f.SameCycle l x

Tactic:
have ⟨h1, h2⟩ := mem_toList_iff.mp h
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
l : α
hl : f.toCycle hf = (↑(f.toList l) : Cycle α)
h : x ∈ f.toList l
h1 : f.SameCycle l x
⊢ l ∈ f.support

Tactic:
have ⟨h1, h2⟩ := mem_toList_iff.mp h
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
l : α
hl : f.toCycle hf = (↑(f.toList l) : Cycle α)
h : x ∈ f.toList l
h1 : f.SameCycle l x
h2 : l ∈ f.support
⊢ ¬(f : (a : α) → α) x = x

Tactic:
((isCycle_iff_sameCycle (mem_support.mp h2)).mp (y := x) hf).mp h1

Premises used: Equiv.Perm.mem_support, Equiv.Perm.isCycle_iff_sameCycle, Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
l : α
hl : f.toCycle hf = (↑(f.toList l) : Cycle α)
h : x ∈ f.toList l
h1 : f.SameCycle l x
h2 : l ∈ f.support
⊢ ¬(f : (a : α) → α) x = x

Tactic:
exact ((isCycle_iff_sameCycle (mem_support.mp h2)).mp (y := x) hf).mp h1

Premises used: Equiv.Perm.mem_support, Equiv.Perm.isCycle_iff_sameCycle, Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
h : (f : (a : α) → α) x ≠ x
mpr : ∃ m < (f.cycleOf x).support.card, x = (f ^ m : (a : α) → α) x
⊢ x ∈ f.toCycle hf

Tactic:
simp only [toCycle_eq_toList f hf x h, Cycle.mem_coe_iff, toList, mem_iterate, iterate_eq_pow]

Premises used: Cycle.mem_coe_iff, Equiv.Perm.toList, Equiv.Perm.iterate_eq_pow, Equiv.Perm.toCycle_eq_toList, List.mem_iterate
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
h : (f : (a : α) → α) x ≠ x
h₁ : 0 < (f.cycleOf x).support.card ∧ x = (HPow.hPow (β := ℕ) f 0 : (a : α) → α) x
⊢ ∃ m < (f.cycleOf x).support.card, x = (f ^ m : (a : α) → α) x

Tactic:
use 0
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
h : (f : (a : α) → α) x ≠ x
⊢ 0 < (f.cycleOf x).support.card

Tactic:
simpa
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
h : (f : (a : α) → α) x ≠ x
⊢ x = (HPow.hPow (β := ℕ) f 0 : (a : α) → α) x

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
h : (f : (a : α) → α) x ≠ x
⊢ 0 < (f.cycleOf x).support.card ∧ x = (HPow.hPow (β := ℕ) f 0 : (a : α) → α) x

Tactic:
exact ⟨by simpa, by simp⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
hx : x ∈ f.toCycle hf
have : ∀ (l : α) (hl : f.toCycle hf = (↑(f.toList l) : Cycle α)), (f.toCycle hf).next ⋯ x hx = (f : (a : α) → α) x
⊢ (f.toCycle hf).next ⋯ x hx = (f : (a : α) → α) x

Tactic:
have ⟨l, hl⟩ := exists_toCycle_toList f hf
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
hx : x ∈ f.toCycle hf
l : α
hl : f.toCycle hf = (↑(f.toList l) : Cycle α)
simp : ∀ (hx_1 : x ∈ f.toList l), (↑(f.toList l) : Cycle α).next ⋯ x ⋯ = (f : (a : α) → α) x
⊢ (f.toCycle hf).next ⋯ x hx = (f : (a : α) → α) x

Tactic:
simp only [hl, Cycle.mem_coe_iff] at ⊢ hx

Premises used: Cycle.mem_coe_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
hx_1 : x ∈ f.toCycle hf
l : α
hl : f.toCycle hf = (↑(f.toList l) : Cycle α)
hx : x ∈ f.toList l
⊢ (↑(f.toList l) : Cycle α).next ⋯ x ⋯ = (f : (a : α) → α) x

Tactic:
Equiv.Perm.next_toList_eq_apply f l x hx

Premises used: Equiv.Perm.next_toList_eq_apply, Cycle.ofList, List.next, Cycle.next
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
hx_1 : x ∈ f.toCycle hf
l : α
hl : f.toCycle hf = (↑(f.toList l) : Cycle α)
hx : x ∈ f.toList l
⊢ (↑(f.toList l) : Cycle α).next ⋯ x ⋯ = (f : (a : α) → α) x

Tactic:
exact Equiv.Perm.next_toList_eq_apply f l x hx

Premises used: Equiv.Perm.next_toList_eq_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
f : { f : Perm α // f.IsCycle }
obtain :
  ∀ (x : α) (hx : ((↑f : Perm α) : (a : α) → α) x ≠ x),
    (fun (s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }) ↦
          Subtype.mk (p := fun (f : Perm α) ↦ f.IsCycle) ((↑s : Cycle α).formPerm ⋯) ⋯)
        ((fun (f : { f : Perm α // f.IsCycle }) ↦
            (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial) ((↑f : Perm α).toCycle ⋯) ⋯ :
              { s : Cycle α // s.Nodup ∧ s.Nontrivial }))
          f) =
      f
⊢ (fun (s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }) ↦
        Subtype.mk (p := fun (f : Perm α) ↦ f.IsCycle) ((↑s : Cycle α).formPerm ⋯) ⋯)
      ((fun (f : { f : Perm α // f.IsCycle }) ↦
          (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial) ((↑f : Perm α).toCycle ⋯) ⋯ :
            { s : Cycle α // s.Nodup ∧ s.Nontrivial }))
        f) =
    f

Tactic:
obtain ⟨x, hx, -⟩ := id f.prop

Premises used: id, Subtype.prop
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x_1 : α
f : { f : Perm α // f.IsCycle }
x : α
hx : ((↑f : Perm α) : (a : α) → α) x ≠ x
⊢ (fun (s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }) ↦
        Subtype.mk (p := fun (f : Perm α) ↦ f.IsCycle) ((↑s : Cycle α).formPerm ⋯) ⋯)
      ((fun (f : { f : Perm α // f.IsCycle }) ↦
          (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial) ((↑f : Perm α).toCycle ⋯) ⋯ :
            { s : Cycle α // s.Nodup ∧ s.Nontrivial }))
        f) =
    f

Tactic:
simpa [toCycle_eq_toList (f : Perm α) f.prop x hx, formPerm_toList, Subtype.ext_iff] using
      f.prop.cycleOf_eq hx

Premises used: Equiv.Perm.IsCycle.cycleOf_eq, Equiv.Perm.formPerm_toList, Subtype.ext_iff, Equiv.Perm.toCycle_eq_toList, Subtype.prop, Subtype.val
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }
mk :
  ∀ (val : Cycle α) (s : List α) (hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s))
    (ht : Cycle.Nontrivial (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)),
    Eq (α := { s : Cycle α // s.Nodup ∧ s.Nontrivial })
      ((fun (f : { f : Perm α // f.IsCycle }) ↦
          (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial) ((↑f : Perm α).toCycle ⋯) ⋯ :
            { s : Cycle α // s.Nodup ∧ s.Nontrivial }))
        ((fun (s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }) ↦
            Subtype.mk (p := fun (f : Perm α) ↦ f.IsCycle) ((↑s : Cycle α).formPerm ⋯) ⋯)
          (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial)
            (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s) ⋯)))
      (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial)
        (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s) ⋯)
⊢ (fun (f : { f : Perm α // f.IsCycle }) ↦
        (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial) ((↑f : Perm α).toCycle ⋯) ⋯ :
          { s : Cycle α // s.Nodup ∧ s.Nontrivial }))
      ((fun (s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }) ↦
          Subtype.mk (p := fun (f : Perm α) ↦ f.IsCycle) ((↑s : Cycle α).formPerm ⋯) ⋯)
        s) =
    s

Tactic:
rcases s with ⟨⟨s⟩, hn, ht⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
val : Cycle α
s : List α
hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
ht : Cycle.Nontrivial (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
mk :
  ∀ (x : α) (hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s) x),
    Eq (α := { s : Cycle α // s.Nodup ∧ s.Nontrivial })
      ((fun (f : { f : Perm α // f.IsCycle }) ↦
          (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial) ((↑f : Perm α).toCycle ⋯) ⋯ :
            { s : Cycle α // s.Nodup ∧ s.Nontrivial }))
        ((fun (s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }) ↦
            Subtype.mk (p := fun (f : Perm α) ↦ f.IsCycle) ((↑s : Cycle α).formPerm ⋯) ⋯)
          (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial)
            (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s) ⋯)))
      (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial)
        (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s) ⋯)
⊢ Eq (α := { s : Cycle α // s.Nodup ∧ s.Nontrivial })
    ((fun (f : { f : Perm α // f.IsCycle }) ↦
        (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial) ((↑f : Perm α).toCycle ⋯) ⋯ :
          { s : Cycle α // s.Nodup ∧ s.Nontrivial }))
      ((fun (s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }) ↦
          Subtype.mk (p := fun (f : Perm α) ↦ f.IsCycle) ((↑s : Cycle α).formPerm ⋯) ⋯)
        (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial)
          (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s) ⋯)))
    (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial)
      (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s) ⋯)

Tactic:
obtain ⟨x, -, -, hx, -⟩ := id ht

Premises used: id
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x_1 : α
val : Cycle α
s : List α
hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
ht : Cycle.Nontrivial (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
x : α
hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s) x
⊢ 2 ≤ s.length

Tactic:
simpa using Cycle.length_nontrivial ht

Premises used: Cycle.length_nontrivial
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x_1 : α
val : Cycle α
s : List α
hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
ht : Cycle.Nontrivial (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
x : α
hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s) x
⊢ 2 ≤ s.length

Tactic:
have hl : 2 ≤ s.length := by simpa using Cycle.length_nontrivial ht
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x_1 : α
val : Cycle α
s : List α
hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
ht : Cycle.Nontrivial (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
x : α
hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s) x
hl : 2 ≤ s.length
mk :
  ∀ (hn_1 : s.Nodup) (hx : x ∈ s),
    Eq (α := { s : Cycle α // s.Nodup ∧ s.Nontrivial })
      (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial) (s.formPerm.toCycle ⋯) ⋯)
      (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial) (↑s : Cycle α) ⋯)
⊢ Eq (α := { s : Cycle α // s.Nodup ∧ s.Nontrivial })
    ((fun (f : { f : Perm α // f.IsCycle }) ↦
        (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial) ((↑f : Perm α).toCycle ⋯) ⋯ :
          { s : Cycle α // s.Nodup ∧ s.Nontrivial }))
      ((fun (s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }) ↦
          Subtype.mk (p := fun (f : Perm α) ↦ f.IsCycle) ((↑s : Cycle α).formPerm ⋯) ⋯)
        (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial)
          (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s) ⋯)))
    (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial)
      (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s) ⋯)

Tactic:
simp only [Cycle.mk_eq_coe, Cycle.nodup_coe_iff, Cycle.mem_coe_iff,
      Cycle.formPerm_coe] at hn hx ⊢

Premises used: Cycle.mem_coe_iff, Cycle.mk_eq_coe, Cycle.formPerm_coe, Cycle.nodup_coe_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x_1 : α
val : Cycle α
s : List α
hn_1 : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
ht : Cycle.Nontrivial (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
x : α
hl : 2 ≤ s.length
hn : s.Nodup
hx : x ∈ s
mk :
  (↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial) (s.formPerm.toCycle ⋯) ⋯) : Cycle α) =
    (↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial) (↑s : Cycle α) ⋯) : Cycle α)
⊢ Eq (α := { s : Cycle α // s.Nodup ∧ s.Nontrivial })
    (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial) (s.formPerm.toCycle ⋯) ⋯)
    (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial) (↑s : Cycle α) ⋯)

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x_1 : α
val : Cycle α
s : List α
hn_1 : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
ht : Cycle.Nontrivial (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
x : α
hl : 2 ≤ s.length
hn : s.Nodup
hx : x ∈ s
mk : s.formPerm.toCycle ⋯ = (↑s : Cycle α)
⊢ (↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial) (s.formPerm.toCycle ⋯) ⋯) : Cycle α) =
    (↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial) (↑s : Cycle α) ⋯) : Cycle α)

Tactic:
dsimp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x_1 : α
val : Cycle α
s : List α
hn_1 : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
ht : Cycle.Nontrivial (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
x : α
hl : 2 ≤ s.length
hn : s.Nodup
hx : x ∈ s
mk : (↑(s.formPerm.toList x) : Cycle α) = (↑s : Cycle α)
mk₁ : (s.formPerm : (a : α) → α) x ≠ x
⊢ s.formPerm.toCycle ⋯ = (↑s : Cycle α)

Tactic:
rw [toCycle_eq_toList _ _ x]

Premises used: Equiv.Perm.toCycle_eq_toList
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x_1 : α
val : Cycle α
s : List α
hn_1 : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
ht : Cycle.Nontrivial (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
x : α
hl : 2 ≤ s.length
hn : s.Nodup
hx : x ∈ s
⊢ (↑(s.formPerm.toList x) : Cycle α) = (↑s : Cycle α)

Tactic:
Quotient.sound' ?_

Premises used: Quotient.sound', Cycle.ofList, Cycle
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x_1 : α
val : Cycle α
s : List α
hn_1 : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
ht : Cycle.Nontrivial (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
x : α
hl : 2 ≤ s.length
hn : s.Nodup
hx : x ∈ s
mk : (IsRotated.setoid α : List α → List α → Prop) (s.formPerm.toList x) s
⊢ (↑(s.formPerm.toList x) : Cycle α) = (↑s : Cycle α)

Tactic:
refine Quotient.sound' ?_

Premises used: Quotient.sound'
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x_1 : α
val : Cycle α
s : List α
hn_1 : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
ht : Cycle.Nontrivial (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
x : α
hl : 2 ≤ s.length
hn : s.Nodup
hx : x ∈ s
⊢ (IsRotated.setoid α : List α → List α → Prop) (s.formPerm.toList x) s

Tactic:
toList_formPerm_isRotated_self _ hl hn _ hx

Premises used: Equiv.Perm.toList_formPerm_isRotated_self
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x_1 : α
val : Cycle α
s : List α
hn_1 : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
ht : Cycle.Nontrivial (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
x : α
hl : 2 ≤ s.length
hn : s.Nodup
hx : x ∈ s
⊢ (IsRotated.setoid α : List α → List α → Prop) (s.formPerm.toList x) s

Tactic:
exact toList_formPerm_isRotated_self _ hl hn _ hx

Premises used: Equiv.Perm.toList_formPerm_isRotated_self
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x_1 : α
val : Cycle α
s : List α
hn_1 : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
ht : Cycle.Nontrivial (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
x : α
hl : 2 ≤ s.length
hn : s.Nodup
hx : x ∈ s
mk : x ∈ s.toFinset
mk₁ : ∀ (x : α), s ≠ [x]
⊢ (s.formPerm : (a : α) → α) x ≠ x

Tactic:
rw [← mem_support, support_formPerm_of_nodup _ hn]

Premises used: Equiv.Perm.mem_support, List.support_formPerm_of_nodup
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x_1 : α
val : Cycle α
s : List α
hn_1 : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
ht : Cycle.Nontrivial (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
x : α
hl : 2 ≤ s.length
hn : s.Nodup
hx : x ∈ s
⊢ x ∈ s.toFinset

Tactic:
simpa using hx
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x_1 : α
val : Cycle α
x x_2 : α
hn_1 : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [x_2])
ht : Cycle.Nontrivial (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [x_2])
hl : 2 ≤ [x_2].length
hn : [x_2].Nodup
hx : x ∈ [x_2]
⊢ False

Tactic:
simp at hl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
f : Perm α
hf : f.IsCycle
intro : ∀ (val : Fintype α), ∃! s : Cycle α, ∃ (h : s.Nodup), s.formPerm h = f
⊢ ∃! s : Cycle α, ∃ (h : s.Nodup), s.formPerm h = f

Tactic:
cases nonempty_fintype α

Premises used: nonempty_fintype
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
f : Perm α
hf : f.IsCycle
val : Fintype α
intro :
  ∀ (x : α) (hx : (f : (a : α) → α) x ≠ x) (hy : ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle x y),
    ∃! s : Cycle α, ∃ (h : s.Nodup), s.formPerm h = f
⊢ ∃! s : Cycle α, ∃ (h : s.Nodup), s.formPerm h = f

Tactic:
obtain ⟨x, hx, hy⟩ := id hf

Premises used: id
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
f : Perm α
hf : f.IsCycle
val : Fintype α
x : α
hx : (f : (a : α) → α) x ≠ x
hy : ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle x y
⊢ ∃! s : Cycle α, ∃ (h : s.Nodup), s.formPerm h = f

Tactic:
⟨f.toList x, ⟨nodup_toList f x, ?_⟩, ?_⟩

Premises used: Equiv.Perm.toList, Cycle.ofList, ExistsUnique, And.intro, Exists.intro, Equiv.Perm.nodup_toList
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
f : Perm α
hf : f.IsCycle
val : Fintype α
x : α
hx : (f : (a : α) → α) x ≠ x
hy : ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle x y
intro : (↑(f.toList x) : Cycle α).formPerm ⋯ = f
intro₁ : ∀ (y : Cycle α), (fun (s : Cycle α) ↦ ∃ (h : s.Nodup), s.formPerm h = f) y → y = (↑(f.toList x) : Cycle α)
⊢ ∃! s : Cycle α, ∃ (h : s.Nodup), s.formPerm h = f

Tactic:
refine ⟨f.toList x, ⟨nodup_toList f x, ?_⟩, ?_⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Concrete
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
f : Perm α
hf : f.IsCycle
val : Fintype α
x : α
hx : (f : (a : α) → α) x ≠ x
hy : ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle x y
⊢ (↑(f.toList x) : Cycle α).formPerm ⋯ = f

Tactic:
simp [formPerm_toList, hf.cycleOf_eq hx]

Premises used: Equiv.Perm.IsCycle.cycleOf_eq, Equiv.Perm.formPerm_toList