awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f g : Perm α
s : Set α
h : f.IsCycleOn s
x : α
hx : Membership.mem (γ := Set α) ((⇑(Equiv.symm g) : (a : α) → α) ⁻¹' s) x
y : α
hy : Membership.mem (γ := Set α) ((⇑(Equiv.symm g) : (a : α) → α) ⁻¹' s) y
h₁ : x = (g : (a : α) → α) ((Equiv.symm g : (a : α) → α) x : α)
h₂ : y = (g : (a : α) → α) ((Equiv.symm g : (a : α) → α) y : α)
⊢ (g * f * g⁻¹).SameCycle x y

Tactic:
convert! Equiv.Perm.SameCycle.conj (h.2 hx hy) (g := g)

Premises used: And.right, Equiv.Perm.SameCycle.conj
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f g : Perm α
s : Set α
h : f.IsCycleOn s
x : α
hx : Membership.mem (γ := Set α) ((⇑(Equiv.symm g) : (a : α) → α) ⁻¹' s) x
y : α
hy : Membership.mem (γ := Set α) ((⇑(Equiv.symm g) : (a : α) → α) ⁻¹' s) y
⊢ x = (g : (a : α) → α) ((Equiv.symm g : (a : α) → α) x : α)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f g : Perm α
s : Set α
h : f.IsCycleOn s
x : α
hx : Membership.mem (γ := Set α) ((⇑(Equiv.symm g) : (a : α) → α) ⁻¹' s) x
y : α
hy : Membership.mem (γ := Set α) ((⇑(Equiv.symm g) : (a : α) → α) ⁻¹' s) y
⊢ y = (g : (a : α) → α) ((Equiv.symm g : (a : α) → α) y : α)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
a b : α
inst : DecidableEq α
hab : a ≠ b
⊢ Membership.mem (γ := Set α) {a, b} a

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
a b : α
inst : DecidableEq α
hab : a ≠ b
⊢ Membership.mem (γ := Set α) {a, b} b

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
a b : α
inst : DecidableEq α
hab : a ≠ b
x : α
hx : Membership.mem (γ := Set α) {a, b} x
y : α
hy : Membership.mem (γ := Set α) {a, b} y
rw : ∀ (hx : x = a ∨ x = b) (y : α) (hy : y = a ∨ y = b), (swap a b).SameCycle x y
⊢ (swap a b).SameCycle x y

Tactic:
rw [Set.mem_insert_iff, Set.mem_singleton_iff] at hx hy

Premises used: Set.mem_singleton_iff, Set.mem_insert_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
a b : α
inst : DecidableEq α
hab : a ≠ b
x : α
hx : x = a ∨ x = b
y : α
hy : y = a ∨ y = b
inl : ∀ (hab : x ≠ b) (hy : y = x ∨ y = b), (swap x b).SameCycle x y
inr : ∀ (hab : a ≠ x) (hy : y = a ∨ y = x), (swap a x).SameCycle x y
⊢ (swap a b).SameCycle x y

Tactic:
obtain rfl | rfl := hx

Premises used: rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
b : α
inst : DecidableEq α
x y : α
hab : x ≠ b
hy : y = x ∨ y = b
inl : ∀ (hab : y ≠ b), (swap y b).SameCycle y y
inl₁ : ∀ (hab : x ≠ y), (swap x y).SameCycle x y
⊢ (swap x b).SameCycle x y

Tactic:
obtain rfl | rfl := hy

Premises used: rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
a : α
inst : DecidableEq α
x y : α
hab : a ≠ x
hy : y = a ∨ y = x
inr : ∀ (hab : y ≠ x), (swap y x).SameCycle x y
inr₁ : ∀ (hab : a ≠ y), (swap a y).SameCycle y y
⊢ (swap a x).SameCycle x y

Tactic:
obtain rfl | rfl := hy

Premises used: rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
b : α
inst : DecidableEq α
y : α
hab : y ≠ b
rw : (1 : (a : α) → α) y = y
rw₁ : id y = y
rw₂ rw₃ : y = y
⊢ (HPow.hPow (β := ℤ) (swap y b) 0 : (a : α) → α) y = y

Tactic:
rw [zpow_zero, coe_one, id]

Premises used: zpow_zero, id, Equiv.Perm.coe_one
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
b : α
inst : DecidableEq α
y : α
hab : y ≠ b
⊢ (swap y b).SameCycle y y

Tactic:
exact ⟨0, by rw [zpow_zero, coe_one, id]⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : DecidableEq α
x y : α
hab : x ≠ y
rw : (swap x y : (a : α) → α) x = y
rw₁ rw₂ : y = y
⊢ (HPow.hPow (β := ℤ) (swap x y) 1 : (a : α) → α) x = y

Tactic:
rw [zpow_one, swap_apply_left]

Premises used: zpow_one, Equiv.swap_apply_left
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : DecidableEq α
x y : α
hab : x ≠ y
⊢ (swap x y).SameCycle x y

Tactic:
exact ⟨1, by rw [zpow_one, swap_apply_left]⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : DecidableEq α
x y : α
hab : y ≠ x
rw : (swap y x : (a : α) → α) x = y
rw₁ rw₂ : y = y
⊢ (HPow.hPow (β := ℤ) (swap y x) 1 : (a : α) → α) x = y

Tactic:
rw [zpow_one, swap_apply_right]

Premises used: zpow_one, Equiv.swap_apply_right
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : DecidableEq α
x y : α
hab : y ≠ x
⊢ (swap y x).SameCycle x y

Tactic:
exact ⟨1, by rw [zpow_one, swap_apply_right]⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
a : α
inst : DecidableEq α
y : α
hab : a ≠ y
rw : (1 : (a : α) → α) y = y
rw₁ : id y = y
rw₂ rw₃ : y = y
⊢ (HPow.hPow (β := ℤ) (swap a y) 0 : (a : α) → α) y = y

Tactic:
rw [zpow_zero, coe_one, id]

Premises used: zpow_zero, id, Equiv.Perm.coe_one
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
a : α
inst : DecidableEq α
y : α
hab : a ≠ y
⊢ (swap a y).SameCycle y y

Tactic:
exact ⟨0, by rw [zpow_zero, coe_one, id]⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Set α
a : α
hf : f.IsCycleOn s
hs : s.Nontrivial
ha : a ∈ s
obtain : ∀ (b : α) (hb : b ∈ s) (hba : b ≠ a), (f : (a : α) → α) a ≠ a
⊢ (f : (a : α) → α) a ≠ a

Tactic:
obtain ⟨b, hb, hba⟩ := hs.exists_ne a

Premises used: Set.Nontrivial.exists_ne
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Set α
a : α
hf : f.IsCycleOn s
hs : s.Nontrivial
ha : a ∈ s
b : α
hb : b ∈ s
hba : b ≠ a
obtain :
  ∀ (n : ℤ) (hb : Membership.mem (α := α) s ((f ^ n : (a : α) → α) a : α)) (hba : (f ^ n : (a : α) → α) a ≠ a),
    (f : (a : α) → α) a ≠ a
⊢ (f : (a : α) → α) a ≠ a

Tactic:
obtain ⟨n, rfl⟩ := hf.2 ha hb

Premises used: And.right, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Set α
a : α
hf : f.IsCycleOn s
hs : s.Nontrivial
ha : a ∈ s
n : ℤ
hb : Membership.mem (α := α) s ((f ^ n : (a : α) → α) a : α)
hba : (f ^ n : (a : α) → α) a ≠ a
⊢ (f : (a : α) → α) a ≠ a

Tactic:
fun h => hba (IsFixedPt.perm_zpow h n)

Premises used: Function.IsFixedPt.perm_zpow, Not
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Set α
a : α
hf : f.IsCycleOn s
hs : s.Nontrivial
ha : a ∈ s
n : ℤ
hb : Membership.mem (α := α) s ((f ^ n : (a : α) → α) a : α)
hba : (f ^ n : (a : α) → α) a ≠ a
⊢ (f : (a : α) → α) a ≠ a

Tactic:
exact fun h => hba (IsFixedPt.perm_zpow h n)

Premises used: Function.IsFixedPt.perm_zpow
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
hf : f.IsCycle
⊢ f.IsCycleOn {x : α | (f : (a : α) → α) x ≠ x}

Tactic:
⟨f.bijOn fun _ => f.apply_eq_iff_eq.not, fun _ ha _ => hf.sameCycle ha⟩

Premises used: Equiv.Perm.IsCycle.sameCycle, Iff.not, Equiv.bijOn, And.intro, Equiv.apply_eq_iff_eq, Equiv.Perm.IsCycleOn
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
⊢ f.IsCycle ↔ ∃ (s : Set α), s.Nontrivial ∧ f.IsCycleOn s ∧ ∀ ⦃x : α⦄, ¬IsFixedPt (⇑f : (a : α) → α) x → x ∈ s

Tactic:
⟨fun hf => ⟨{ x | f x ≠ x }, ?_, hf.isCycleOn, fun _ => id⟩, ?_⟩

Premises used: setOf, id, Ne, And.intro, Iff.intro, Equiv.Perm.IsCycle.isCycleOn, Exists.intro, DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
refine_1 : ∀ (hf : f.IsCycle), Set.Nontrivial.{u_2} (α := α) {x : α | (f : (a : α) → α) x ≠ x}
refine_2 :
  (∃ (s : Set α), s.Nontrivial ∧ f.IsCycleOn s ∧ ∀ ⦃x : α⦄, ¬IsFixedPt (⇑f : (a : α) → α) x → x ∈ s) → f.IsCycle
⊢ f.IsCycle ↔ ∃ (s : Set α), s.Nontrivial ∧ f.IsCycleOn s ∧ ∀ ⦃x : α⦄, ¬IsFixedPt (⇑f : (a : α) → α) x → x ∈ s

Tactic:
refine ⟨fun hf => ⟨{ x | f x ≠ x }, ?_, hf.isCycleOn, fun _ => id⟩, ?_⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
hf : f.IsCycle
refine_1 :
  ∀ (a : α) (ha : (f : (a : α) → α) a ≠ a ∧ ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle a y),
    Set.Nontrivial.{u_2} (α := α) {x : α | (f : (a : α) → α) x ≠ x}
⊢ Set.Nontrivial.{u_2} (α := α) {x : α | (f : (a : α) → α) x ≠ x}

Tactic:
obtain ⟨a, ha⟩ := hf
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
a : α
ha : (f : (a : α) → α) a ≠ a ∧ ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle a y
⊢ Set.Nontrivial.{u_2} (α := α) {x : α | (f : (a : α) → α) x ≠ x}

Tactic:
⟨f a, f.injective.ne ha.1, a, ha.1, ha.1⟩

Premises used: Function.Injective.ne, And.left, And.intro, Exists.intro, Equiv.injective, Set.Nontrivial, DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
a : α
ha : (f : (a : α) → α) a ≠ a ∧ ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle a y
⊢ Set.Nontrivial.{u_2} (α := α) {x : α | (f : (a : α) → α) x ≠ x}

Tactic:
exact ⟨f a, f.injective.ne ha.1, a, ha.1, ha.1⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Set α
hs : s.Nontrivial
hf : f.IsCycleOn s
hsf : ∀ ⦃x : α⦄, ¬IsFixedPt (⇑f : (a : α) → α) x → x ∈ s
refine_2 : ∀ (a : α) (ha : a ∈ s), f.IsCycle
⊢ f.IsCycle

Tactic:
obtain ⟨a, ha⟩ := hs.nonempty

Premises used: Set.Nontrivial.nonempty
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Set α
hs : s.Nontrivial
hf : f.IsCycleOn s
hsf : ∀ ⦃x : α⦄, ¬IsFixedPt (⇑f : (a : α) → α) x → x ∈ s
a : α
ha : a ∈ s
⊢ f.IsCycle

Tactic:
⟨a, hf.apply_ne hs ha, fun b hb => hf.2 ha <| hsf hb⟩

Premises used: Equiv.Perm.IsCycleOn.apply_ne, And.right, Equiv.Perm.IsCycle, And.intro, Exists.intro
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Set α
hs : s.Nontrivial
hf : f.IsCycleOn s
hsf : ∀ ⦃x : α⦄, ¬IsFixedPt (⇑f : (a : α) → α) x → x ∈ s
a : α
ha : a ∈ s
⊢ f.IsCycle

Tactic:
exact ⟨a, hf.apply_ne hs ha, fun b hb => hf.2 ha <| hsf hb⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Set α
x : α
hf : f.IsCycleOn s
hx : Membership.mem (α := α) s ((f : (a : α) → α) x : α)
⊢ x ∈ s

Tactic:
simpa using hf.1.perm_inv.1 hx

Premises used: Set.BijOn.perm_inv, And.left
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Nontrivial
obtain : ∀ (a : α) (ha : a ∈ s), IsCycle (α := { x : α // x ∈ s }) (f.subtypePerm (p := Membership.mem s) ⋯)
⊢ IsCycle (α := { x : α // x ∈ s }) (f.subtypePerm (p := Membership.mem s) ⋯)

Tactic:
obtain ⟨a, ha⟩ := hs.nonempty

Premises used: Set.Nontrivial.nonempty
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Nontrivial
a : α
ha : a ∈ s
⊢ IsCycle (α := { x : α // x ∈ s }) (f.subtypePerm (p := Membership.mem s) ⋯)

Tactic:
⟨⟨a, ha⟩, ne_of_apply_ne ((↑) : s → α) (hf.apply_ne hs ha), fun b _ =>
      (hf.2 (⟨a, ha⟩ : s).2 b.2).subtypePerm⟩

Premises used: Equiv.Perm.IsCycleOn.apply_ne, ne_of_apply_ne, Subtype.mk, And.right, Equiv.Perm.IsCycle, And.intro, Equiv.Perm.SameCycle.subtypePerm, Exists.intro, Subtype.val, Subtype.property
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Nontrivial
a : α
ha : a ∈ s
⊢ IsCycle (α := { x : α // x ∈ s }) (f.subtypePerm (p := Membership.mem s) ⋯)

Tactic:
exact
    ⟨⟨a, ha⟩, ne_of_apply_ne ((↑) : s → α) (hf.apply_ne hs ha), fun b _ =>
      (hf.2 (⟨a, ha⟩ : s).2 b.2).subtypePerm⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
inl :
  ∀ (hs : s.Subsingleton), IsCycleOn (α := { x : α // x ∈ s }) (f.subtypePerm (p := Membership.mem s) ⋯) _root_.Set.univ
inr :
  ∀ (hs : s.Nontrivial), IsCycleOn (α := { x : α // x ∈ s }) (f.subtypePerm (p := Membership.mem s) ⋯) _root_.Set.univ
⊢ IsCycleOn (α := { x : α // x ∈ s }) (f.subtypePerm (p := Membership.mem s) ⋯) _root_.Set.univ

Tactic:
obtain hs | hs := s.subsingleton_or_nontrivial

Premises used: Set.subsingleton_or_nontrivial
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Subsingleton
⊢ Subsingleton.{u_2 + 1} (↑s : Type u_2)

Tactic:
haveI := hs.coe_sort
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Subsingleton
this : Subsingleton.{u_2 + 1} (↑s : Type u_2)
⊢ IsCycleOn (α := { x : α // x ∈ s }) (f.subtypePerm (p := Membership.mem s) ⋯) _root_.Set.univ

Tactic:
isCycleOn_of_subsingleton _ _

Premises used: Equiv.Perm.isCycleOn_of_subsingleton
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Subsingleton
this : Subsingleton.{u_2 + 1} (↑s : Type u_2)
⊢ IsCycleOn (α := { x : α // x ∈ s }) (f.subtypePerm (p := Membership.mem s) ⋯) _root_.Set.univ

Tactic:
exact isCycleOn_of_subsingleton _ _

Premises used: Equiv.Perm.isCycleOn_of_subsingleton
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Nontrivial
⊢ IsCycleOn (α := { x : α // x ∈ s }) (f.subtypePerm (p := Membership.mem s) ⋯)
    {x : { x : α // x ∈ s } |
      (f.subtypePerm (p := Membership.mem s) ⋯ : (a : { x : α // x ∈ s }) → { x : α // x ∈ s }) x ≠ x}

Tactic:
(hf.isCycle_subtypePerm hs).isCycleOn

Premises used: Equiv.Perm.IsCycleOn.isCycle_subtypePerm, Equiv.Perm.IsCycle.isCycleOn
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Nontrivial
h :
  Eq.{u_2 + 1} (α := Set { x : α // x ∈ s }) _root_.Set.univ
    {x : { x : α // x ∈ s } |
      (f.subtypePerm (p := Membership.mem s) ⋯ : (a : { x : α // x ∈ s }) → { x : α // x ∈ s }) x ≠ x}
⊢ IsCycleOn (α := { x : α // x ∈ s }) (f.subtypePerm (p := Membership.mem s) ⋯) _root_.Set.univ

Tactic:
convert! (hf.isCycle_subtypePerm hs).isCycleOn

Premises used: Equiv.Perm.IsCycleOn.isCycle_subtypePerm, Equiv.Perm.IsCycle.isCycleOn
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Nontrivial
h :
  ∀ (x : { x : α // x ∈ s }),
    Membership.mem (γ := Set { x : α // x ∈ s })
      {x : { x : α // x ∈ s } |
        (f.subtypePerm (p := Membership.mem s) ⋯ : (a : { x : α // x ∈ s }) → { x : α // x ∈ s }) x ≠ x}
      x
⊢ Eq.{u_2 + 1} (α := Set { x : α // x ∈ s }) _root_.Set.univ
    {x : { x : α // x ∈ s } |
      (f.subtypePerm (p := Membership.mem s) ⋯ : (a : { x : α // x ∈ s }) → { x : α // x ∈ s }) x ≠ x}

Tactic:
rw [eq_comm, Set.eq_univ_iff_forall]

Premises used: Set.eq_univ_iff_forall, eq_comm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Nontrivial
⊢ ∀ (x : { x : α // x ∈ s }),
    Membership.mem (γ := Set { x : α // x ∈ s })
      {x : { x : α // x ∈ s } |
        (f.subtypePerm (p := Membership.mem s) ⋯ : (a : { x : α // x ∈ s }) → { x : α // x ∈ s }) x ≠ x}
      x

Tactic:
fun x => ne_of_apply_ne ((↑) : s → α) (hf.apply_ne hs x.2)

Premises used: Set.Mem, setOf, Equiv.Perm.IsCycleOn.apply_ne, ne_of_apply_ne, Subtype.val, Not, Subtype.property
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Nontrivial
⊢ ∀ (x : { x : α // x ∈ s }),
    Membership.mem (γ := Set { x : α // x ∈ s })
      {x : { x : α // x ∈ s } |
        (f.subtypePerm (p := Membership.mem s) ⋯ : (a : { x : α // x ∈ s }) → { x : α // x ∈ s }) x ≠ x}
      x

Tactic:
exact fun x => ne_of_apply_ne ((↑) : s → α) (hf.apply_ne hs x.2)

Premises used: ne_of_apply_ne, Subtype.val
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
ha : a ∈ s
n : ℕ
inl :
  ∀ (hf : f.IsCycleOn (↑{a} : Set α)) (ha : Membership.mem (γ := Finset α) {a} a),
    (f ^ n : (a : α) → α) a = a ↔ card (α := α) {a} ∣ n
inr : ∀ (hs : s.Nontrivial), (f ^ n : (a : α) → α) a = a ↔ #s ∣ n
⊢ (f ^ n : (a : α) → α) a = a ↔ #s ∣ n

Tactic:
obtain rfl | hs := Finset.eq_singleton_or_nontrivial ha

Premises used: Finset.eq_singleton_or_nontrivial, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
a : α
n : ℕ
hf : f.IsCycleOn (↑{a} : Set α)
ha : Membership.mem (γ := Finset α) {a} a
⊢ (f : (a : α) → α) a = a

Tactic:
rw [coe_singleton, isCycleOn_singleton] at hf

Premises used: Finset.coe_singleton, Equiv.Perm.isCycleOn_singleton
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
a : α
n : ℕ
hf : f.IsCycleOn (↑{a} : Set α)
ha : Membership.mem (γ := Finset α) {a} a
hf₁ : (f : (a : α) → α) a = a
⊢ Membership.mem (γ := Finset α) {a} a

Tactic:
rw [coe_singleton, isCycleOn_singleton] at hf

Premises used: Finset.coe_singleton, Equiv.Perm.isCycleOn_singleton
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
a : α
n : ℕ
hf : (f : (a : α) → α) a = a
ha : Membership.mem (γ := Finset α) {a} a
⊢ (f ^ n : (a : α) → α) a = a ↔ card (α := α) {a} ∣ n

Tactic:
simpa using IsFixedPt.iterate hf n

Premises used: Function.IsFixedPt.iterate
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
ha : a ∈ s
n : ℕ
hs : s.Nontrivial
⊢ ∀ (x : ↥s), ¬(f : (a : α) → α) (↑x : α) = (↑x : α)

Tactic:
have h (x : s) : ¬f x = x := hf.apply_ne hs x.2
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
ha : a ∈ s
n : ℕ
hs : s.Nontrivial
h : ∀ (x : ↥s), ¬(f : (a : α) → α) (↑x : α) = (↑x : α)
⊢ orderOf (G := Perm { x : α // x ∈ (↑s : Set α) }) (f.subtypePerm (p := Membership.mem (↑s : Set α)) ⋯) =
    card (α := { x : α // x ∈ (↑s : Set α) }) (support (f.subtypePerm (p := Membership.mem (↑s : Set α)) ⋯))

Tactic:
have := (hf.isCycle_subtypePerm hs).orderOf
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
ha : a ∈ s
n : ℕ
hs : s.Nontrivial
h : ∀ (x : ↥s), ¬(f : (a : α) → α) (↑x : α) = (↑x : α)
this :
  orderOf (G := Perm { x : α // x ∈ (↑s : Set α) }) (f.subtypePerm (p := Membership.mem (↑s : Set α)) ⋯) =
    card (α := { x : α // x ∈ (↑s : Set α) }) (support (f.subtypePerm (p := Membership.mem (↑s : Set α)) ⋯))
⊢ orderOf (G := Perm ↥s) (f.subtypePerm (p := Membership.mem (↑s : Set α)) ⋯) = #s

Tactic:
simp only [coe_sort_coe, support_subtypePerm, ne_eq, h, not_false_eq_true, univ_eq_attach,
      mem_attach, imp_self, implies_true, filter_true_of_mem, card_attach] at this

Premises used: Finset.coe_sort_coe, Finset.mem_attach, ne_eq, Finset.filter_true_of_mem, Finset.card_attach, Finset.univ_eq_attach, imp_self, implies_true, not_false_eq_true, Equiv.Perm.support_subtypePerm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
ha : a ∈ s
n : ℕ
hs : s.Nontrivial
h : ∀ (x : ↥s), ¬(f : (a : α) → α) (↑x : α) = (↑x : α)
this : orderOf (G := Perm ↥s) (f.subtypePerm (p := Membership.mem (↑s : Set α)) ⋯) = #s
inr :
  (f ^ n : (a : α) → α) a = a ↔
    (HPow.hPow (α := Perm { x : α // x ∈ (↑s : Set α) }) (f.subtypePerm (p := Membership.mem (↑s : Set α)) ⋯) n :
          (a : { x : α // x ∈ (↑s : Set α) }) → { x : α // x ∈ (↑s : Set α) })
        (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha) =
      Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha
⊢ (f ^ n : (a : α) → α) a = a ↔ #s ∣ n

Tactic:
rw [← this, orderOf_dvd_iff_pow_eq_one,
      (hf.isCycle_subtypePerm hs).pow_eq_one_iff'
        (ne_of_apply_ne ((↑) : s → α) <| hf.apply_ne hs (⟨a, ha⟩ : s).2)]

Premises used: Equiv.Perm.IsCycleOn.isCycle_subtypePerm, Equiv.Perm.IsCycle.pow_eq_one_iff', Equiv.Perm.IsCycleOn.apply_ne, ne_of_apply_ne, Subtype.mk, Subtype.val, orderOf_dvd_iff_pow_eq_one, Subtype.property
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
ha : a ∈ s
n : ℕ
hs : s.Nontrivial
h : ∀ (x : ↥s), ¬(f : (a : α) → α) (↑x : α) = (↑x : α)
this : orderOf (G := Perm ↥s) (f.subtypePerm (p := Membership.mem (↑s : Set α)) ⋯) = #s
⊢ (f ^ n : (a : α) → α) a = a ↔
    (HPow.hPow (α := Perm { x : α // x ∈ (↑s : Set α) }) (f.subtypePerm (p := Membership.mem (↑s : Set α)) ⋯) n :
          (a : { x : α // x ∈ (↑s : Set α) }) → { x : α // x ∈ (↑s : Set α) })
        (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha) =
      Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha

Tactic:
simp [-SetLike.coe_sort_coe]

Premises used: SetLike.coe_sort_coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
ha : a ∈ s
n : ℕ
hs : s.Nontrivial
inr inr₁ inr₂ : ∀ (h : ∀ (x : ↥s), ¬(f : (a : α) → α) (↑x : α) = (↑x : α)), (f ^ n : (a : α) → α) a = a ↔ #s ∣ n
inr₃ :
  ∀ (h : ∀ (x : ↥s), ¬(f : (a : α) → α) (↑x : α) = (↑x : α))
    (this :
      orderOf (G := Perm { x : α // x ∈ (↑s : Set α) }) (f.subtypePerm (p := Membership.mem (↑s : Set α)) ⋯) =
        card (α := { x : α // x ∈ (↑s : Set α) }) (support (f.subtypePerm (p := Membership.mem (↑s : Set α)) ⋯))),
    (f ^ n : (a : α) → α) a = a ↔ #s ∣ n
inr₄ :
  ∀ (h : ∀ (x : ↥s), ¬(f : (a : α) → α) (↑x : α) = (↑x : α))
    (this : orderOf (G := Perm ↥s) (f.subtypePerm (p := Membership.mem (↑s : Set α)) ⋯) = #s),
    (f ^ n : (a : α) → α) a = a ↔ #s ∣ n
inr₅ :
  ∀ (h : ∀ (x : ↥s), ¬(f : (a : α) → α) (↑x : α) = (↑x : α))
    (this : orderOf (G := Perm ↥s) (f.subtypePerm (p := Membership.mem (↑s : Set α)) ⋯) = #s),
    (f ^ n : (a : α) → α) a = a ↔
      (HPow.hPow (α := Perm { x : α // x ∈ (↑s : Set α) }) (f.subtypePerm (p := Membership.mem (↑s : Set α)) ⋯) n :
            (a : { x : α // x ∈ (↑s : Set α) }) → { x : α // x ∈ (↑s : Set α) })
          (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha) =
        Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha
⊢ (f ^ n : (a : α) → α) a = a ↔ #s ∣ n

Tactic:
classical
    have h (x : s) : ¬f x = x := hf.apply_ne hs x.2
    have := (hf.isCycle_subtypePerm hs).orderOf
    simp only [coe_sort_coe, support_subtypePerm, ne_eq, h, not_false_eq_true, univ_eq_attach,
      mem_attach, imp_self, implies_true, filter_true_of_mem, card_attach] at this
    rw [← this, orderOf_dvd_iff_pow_eq_one,
      (hf.isCycle_subtypePerm hs).pow_eq_one_iff'
        (ne_of_apply_ne ((↑) : s → α) <| hf.apply_ne hs (⟨a, ha⟩ : s).2)]
    simp [-SetLike.coe_sort_coe]

Premises used: Finset.coe_sort_coe, Equiv.Perm.IsCycleOn.isCycle_subtypePerm, SetLike.coe_sort_coe, Equiv.Perm.IsCycle.pow_eq_one_iff', Equiv.Perm.IsCycleOn.apply_ne, Finset.mem_attach, ne_eq, ne_of_apply_ne, Finset.filter_true_of_mem, Subtype.mk, Finset.card_attach, Finset.univ_eq_attach, imp_self, implies_true, not_false_eq_true, Subtype.val, orderOf_dvd_iff_pow_eq_one, Equiv.Perm.support_subtypePerm, Subtype.property
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
ha : a ∈ s
n : ℕ
rw : (f⁻¹ ^ (n + 1) : (a : α) → α) a = a ↔ (↑(#s) : ℤ) ∣ Int.negSucc n
⊢ (f ^ Int.negSucc n : (a : α) → α) a = a ↔ (↑(#s) : ℤ) ∣ Int.negSucc n

Tactic:
rw [zpow_negSucc, ← inv_pow]

Premises used: zpow_negSucc, inv_pow
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
ha : a ∈ s
n : ℕ
⊢ (f⁻¹ ^ (n + 1) : (a : α) → α) a = a ↔ (↑(#s) : ℤ) ∣ Int.negSucc n

Tactic:
(hf.inv.pow_apply_eq ha).trans (dvd_neg.trans Int.natCast_dvd_natCast).symm

Premises used: Equiv.Perm.IsCycleOn.inv, dvd_neg, Iff.trans, Iff.symm, Equiv.Perm.IsCycleOn.pow_apply_eq, Int.natCast_dvd_natCast
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
ha : a ∈ s
n : ℕ
⊢ (f⁻¹ ^ (n + 1) : (a : α) → α) a = a ↔ (↑(#s) : ℤ) ∣ Int.negSucc n

Tactic:
exact (hf.inv.pow_apply_eq ha).trans (dvd_neg.trans Int.natCast_dvd_natCast).symm

Premises used: Equiv.Perm.IsCycleOn.inv, dvd_neg, Iff.trans, Iff.symm, Equiv.Perm.IsCycleOn.pow_apply_eq, Int.natCast_dvd_natCast
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn (↑s : Set α)
ha : a ∈ s
m n : ℕ
rw :
  Eq (α := α) ((f ^ m : (a : α) → α) a : α) ((f ^ n : (a : α) → α) a : α) ↔
    (f ^ HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ) : (a : α) → α) a = a
⊢ Eq (α := α) ((f ^ m : (a : α) → α) a : α) ((f ^ n : (a : α) → α) a : α) ↔ m ≡ n [MOD #s]

Tactic:
rw [Nat.modEq_iff_dvd, ← hf.zpow_apply_eq ha]

Premises used: Nat.modEq_iff_dvd, Equiv.Perm.IsCycleOn.zpow_apply_eq