awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
f_1 g : Perm α
x_1 y_1 : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x y : α
hxy : f.SameCycle x y
hx : x ∉ f.support
⊢ Nonempty α

Tactic:
haveI : Nonempty α := ⟨x⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
f_1 g : Perm α
x_1 y_1 : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x y : α
hxy : f.SameCycle x y
hx : x ∉ f.support
this : Nonempty α
⊢ (f : (a : α) → α) x = x

Tactic:
rw [notMem_support] at hx

Premises used: Equiv.Perm.notMem_support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
f_1 g : Perm α
x_1 y_1 : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x y : α
hxy : f.SameCycle x y
hx : x ∉ f.support
this : Nonempty α
hx₁ : (f : (a : α) → α) x = x
⊢ Nonempty α

Tactic:
rw [notMem_support] at hx

Premises used: Equiv.Perm.notMem_support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
f_1 g : Perm α
x_1 y_1 : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x y : α
hxy : f.SameCycle x y
hx : (f : (a : α) → α) x = x
this : Nonempty α
⊢ ∃ m < Fintype.card α, (f ^ m : (a : α) → α) x = y

Tactic:
⟨0, Fintype.card_pos, hxy.eq_of_left hx⟩

Premises used: And.intro, Exists.intro, Equiv.Perm.SameCycle.eq_of_left, OfNat.ofNat, Fintype.card_pos
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
f_1 g : Perm α
x_1 y_1 : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x y : α
hxy : f.SameCycle x y
hx : (f : (a : α) → α) x = x
this : Nonempty α
⊢ ∃ m < Fintype.card α, (f ^ m : (a : α) → α) x = y

Tactic:
exact ⟨0, Fintype.card_pos, hxy.eq_of_left hx⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
f_1 g : Perm α
x_1 y_1 : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x y : α
hxy : f.SameCycle x y
hx : x ∉ f.support
case case₁ case₂ : ∀ (this : Nonempty α), ∃ m < Fintype.card α, (f ^ m : (a : α) → α) x = y
case₃ : ∀ (hx : (f : (a : α) → α) x = x) (this : Nonempty α), ∃ m < Fintype.card α, (f ^ m : (a : α) → α) x = y
⊢ ∃ m < Fintype.card α, (f ^ m : (a : α) → α) x = y

Tactic:
case neg =>
        haveI : Nonempty α := ⟨x⟩
        rw [notMem_support] at hx
        exact ⟨0, Fintype.card_pos, hxy.eq_of_left hx⟩

Premises used: Equiv.Perm.notMem_support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
x : α
inst : DecidableEq α
inst_1 : Fintype α
h : (f : (a : α) → α) x ≠ x
⊢ 2 ≤ #(f.cycleOf x).support

Tactic:
simpa using (isCycle_cycleOf _ h).two_le_card_support

Premises used: Equiv.Perm.isCycle_cycleOf, Equiv.Perm.IsCycle.two_le_card_support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
x : α
inst : DecidableEq α
inst_1 : Fintype α
refine : ∀ (h : 2 ≤ #(f.cycleOf x).support), (f : (a : α) → α) x ≠ x
⊢ 2 ≤ #(f.cycleOf x).support ↔ (f : (a : α) → α) x ≠ x

Tactic:
refine ⟨fun h => ?_, fun h => by simpa using (isCycle_cycleOf _ h).two_le_card_support⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
x : α
inst : DecidableEq α
inst_1 : Fintype α
h : 2 ≤ #(f.cycleOf x).support
contrapose! : ∀ (h : (f : (a : α) → α) x = x), #(f.cycleOf x).support < 2
⊢ (f : (a : α) → α) x ≠ x

Tactic:
contrapose! h
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
x : α
inst : DecidableEq α
inst_1 : Fintype α
h : (f : (a : α) → α) x = x
⊢ f.cycleOf x = 1

Tactic:
rw [← cycleOf_eq_one_iff] at h

Premises used: Equiv.Perm.cycleOf_eq_one_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
x : α
inst : DecidableEq α
inst_1 : Fintype α
h : f.cycleOf x = 1
⊢ #(f.cycleOf x).support < 2

Tactic:
simp [h]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
x : α
inst : DecidableEq α
inst_1 : Fintype α
rw : Nat.succ 0 ≤ #(f.cycleOf x).support ↔ 2 ≤ #(f.cycleOf x).support
⊢ (f.cycleOf x).support.Nonempty ↔ (f : (a : α) → α) x ≠ x

Tactic:
rw [← two_le_card_support_cycleOf_iff, ← card_pos, ← Nat.succ_le_iff]

Premises used: Equiv.Perm.two_le_card_support_cycleOf_iff, Finset.card_pos, Nat.succ_le_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
x : α
inst : DecidableEq α
inst_1 : Fintype α
⊢ Nat.succ 0 ≤ #(f.cycleOf x).support ↔ 2 ≤ #(f.cycleOf x).support

Tactic:
⟨fun h => Or.resolve_left h.eq_or_lt (card_support_ne_one _).symm, zero_lt_two.trans_le⟩

Premises used: LE.le.eq_or_lt, Equiv.Perm.card_support_ne_one, Or.resolve_left, Ne.symm, LT.lt.trans_le, Iff.intro, zero_lt_two, Equiv.Perm.cycleOf
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
x : α
inst : DecidableEq α
inst_1 : Fintype α
⊢ Nat.succ 0 ≤ #(f.cycleOf x).support ↔ 2 ≤ #(f.cycleOf x).support

Tactic:
exact ⟨fun h => Or.resolve_left h.eq_or_lt (card_support_ne_one _).symm, zero_lt_two.trans_le⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
x y : α
inst : DecidableEq α
inst_1 : Fintype α
⊢ y ∈ (f.cycleOf x).support ↔ f.SameCycle x y ∧ x ∈ f.support

Tactic:
mem_support_cycleOf_iff_aux

Premises used: _private.0.Equiv.Perm.mem_support_cycleOf_iff_aux
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
x y : α
hx : (f : (a : α) → α) x ≠ x
inst : DecidableEq α
inst_1 : Fintype α
⊢ y ∈ (f.cycleOf x).support ↔ f.SameCycle x y

Tactic:
mem_support_cycleOf_iff'_aux hx

Premises used: _private.0.Equiv.Perm.mem_support_cycleOf_iff'_aux
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
x y : α
hx : x ∈ g.support
hy : y ∈ g.support
⊢ g.SameCycle x y ↔ g.cycleOf x = g.cycleOf y

Tactic:
⟨SameCycle.cycleOf_eq, fun h ↦ ?_⟩

Premises used: Equiv.Perm.SameCycle.cycleOf_eq, Iff.intro
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
x y : α
hx : x ∈ g.support
hy : y ∈ g.support
refine : ∀ (h : g.cycleOf x = g.cycleOf y), g.SameCycle x y
⊢ g.SameCycle x y ↔ g.cycleOf x = g.cycleOf y

Tactic:
refine ⟨SameCycle.cycleOf_eq, fun h ↦ ?_⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
x y : α
hx : x ∈ g.support
hy : y ∈ g.support
h : g.cycleOf x = g.cycleOf y
rw : y ∈ (g.cycleOf x).support
rw₁ : y ∈ (g.cycleOf y).support
rw₂ rw₃ : g.SameCycle y y
⊢ g.SameCycle x y

Tactic:
rw [← mem_support_cycleOf_iff' (mem_support.mp hx), h,
    mem_support_cycleOf_iff' (mem_support.mp hy)]

Premises used: Equiv.Perm.mem_support, Equiv.Perm.mem_support_cycleOf_iff', Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
x : α
inst : DecidableEq α
inst_1 : Fintype α
⊢ (f.cycleOf x).support = ∅ ↔ x ∉ f.support

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x : α
⊢ f.IsCycleOn (↑(f.cycleOf x).support : Set α)

Tactic:
isCycleOn_support_cycleOf_aux f x

Premises used: _private.0.Equiv.Perm.isCycleOn_support_cycleOf_aux
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
x y : α
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
h : f.SameCycle x y
hx : x ∈ f.support
⊢ ∃ i < #(f.cycleOf x).support, (f ^ i : (a : α) → α) x = y

Tactic:
h.exists_pow_eq_of_mem_support_aux hx

Premises used: _private.0.Equiv.Perm.SameCycle.exists_pow_eq_of_mem_support_aux
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x y : α
hy : y ∈ (f.cycleOf x).support
⊢ (if f.SameCycle x y then (f : (a : α) → α) y else y) ≠ y

Tactic:
rw [mem_support, cycleOf_apply] at hy

Premises used: Equiv.Perm.mem_support, Equiv.Perm.cycleOf_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x y : α
hy : (if f.SameCycle x y then (f : (a : α) → α) y else y) ≠ y
pos : f.SameCycle x y → ∀ (hy : (f : (a : α) → α) y ≠ y), y ∈ f.support
neg : ¬f.SameCycle x y → ∀ (hy : y ≠ y), y ∈ f.support
⊢ y ∈ f.support

Tactic:
split_ifs at hy
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x y : α
h : f.SameCycle x y
hy : (f : (a : α) → α) y ≠ y
⊢ y ∈ f.support

Tactic:
mem_support.mpr hy

Premises used: Iff.mpr, Equiv.Perm.mem_support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x y : α
h : f.SameCycle x y
hy : (f : (a : α) → α) y ≠ y
⊢ y ∈ f.support

Tactic:
exact mem_support.mpr hy

Premises used: Iff.mpr, Equiv.Perm.mem_support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x y : α
h : ¬f.SameCycle x y
hy : y ≠ y
⊢ y ∈ f.support

Tactic:
absurd rfl hy

Premises used: absurd, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x y : α
h : ¬f.SameCycle x y
hy : y ≠ y
⊢ y ∈ f.support

Tactic:
exact absurd rfl hy

Premises used: absurd, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
x y : α
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
h : f.SameCycle x y
⊢ x ∈ f.support ↔ y ∈ f.support

Tactic:
⟨fun hx => support_cycleOf_le f x (mem_support_cycleOf_iff.mpr ⟨h, hx⟩), fun hy =>
    support_cycleOf_le f y (mem_support_cycleOf_iff.mpr ⟨h.symm, hy⟩)⟩

Premises used: Iff.mpr, Equiv.Perm.support_cycleOf_le, Equiv.Perm.SameCycle.symm, Equiv.Perm.mem_support_cycleOf_iff, And.intro, Iff.intro
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
n : ℕ
x : α
pos :
  ∀ (hx : (f : (a : α) → α) x = x),
    Eq (α := α) ((f ^ (n % #(f.cycleOf x).support) : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α)
neg :
  ∀ (hx : ¬(f : (a : α) → α) x = x),
    Eq (α := α) ((f ^ (n % #(f.cycleOf x).support) : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α)
⊢ Eq (α := α) ((f ^ (n % #(f.cycleOf x).support) : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α)

Tactic:
by_cases hx : f x = x

Premises used: DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
n : ℕ
x : α
hx : (f : (a : α) → α) x = x
pos : x = (f ^ n : (a : α) → α) x
pos₁ pos₂ : x = x
⊢ Eq (α := α) ((f ^ (n % #(f.cycleOf x).support) : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α)

Tactic:
rw [pow_apply_eq_self_of_apply_eq_self hx, pow_apply_eq_self_of_apply_eq_self hx]

Premises used: Equiv.Perm.pow_apply_eq_self_of_apply_eq_self
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
n : ℕ
x : α
hx : ¬(f : (a : α) → α) x = x
neg : Eq (α := α) ((f.cycleOf x ^ (n % #(f.cycleOf x).support) : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α)
neg₁ :
  Eq (α := α) ((f.cycleOf x ^ (n % #(f.cycleOf x).support) : (a : α) → α) x : α) ((f.cycleOf x ^ n : (a : α) → α) x : α)
neg₂ :
  Eq (α := α) ((f.cycleOf x ^ (n % orderOf (f.cycleOf x)) : (a : α) → α) x : α) ((f.cycleOf x ^ n : (a : α) → α) x : α)
neg₃ neg₄ : Eq (α := α) ((f.cycleOf x ^ n : (a : α) → α) x : α) ((f.cycleOf x ^ n : (a : α) → α) x : α)
⊢ Eq (α := α) ((f ^ (n % #(f.cycleOf x).support) : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α)

Tactic:
rw [← cycleOf_pow_apply_self, ← cycleOf_pow_apply_self f, ← (isCycle_cycleOf f hx).orderOf,
      pow_mod_orderOf]

Premises used: Equiv.Perm.isCycle_cycleOf, pow_mod_orderOf, Equiv.Perm.cycleOf_pow_apply_self, Equiv.Perm.IsCycle.orderOf
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : f.SameCycle x y
pos : ∀ (hx : x ∈ f.support), ∃ (i : ℕ), 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i : (a : α) → α) x = y
neg : ∀ (hx : x ∉ f.support), ∃ (i : ℕ), 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i : (a : α) → α) x = y
⊢ ∃ (i : ℕ), 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i : (a : α) → α) x = y

Tactic:
by_cases hx : x ∈ f.support

Premises used: Equiv.Perm.support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
pos :
  ∀ (k : ℕ) (hk : k < #(f.cycleOf x).support) (hk' : (f ^ k : (a : α) → α) x = y),
    ∃ (i : ℕ), 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i : (a : α) → α) x = y
⊢ ∃ (i : ℕ), 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i : (a : α) → α) x = y

Tactic:
obtain ⟨k, hk, hk'⟩ := h.exists_pow_eq_of_mem_support hx

Premises used: Equiv.Perm.SameCycle.exists_pow_eq_of_mem_support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
k : ℕ
hk : k < #(f.cycleOf x).support
hk' : (f ^ k : (a : α) → α) x = y
pos :
  ∀ (hk : 0 < #(f.cycleOf x).support) (hk' : (HPow.hPow (β := ℕ) f 0 : (a : α) → α) x = y),
    ∃ (i : ℕ), 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i : (a : α) → α) x = y
pos₁ :
  ∀ (k : ℕ) (hk : k + 1 < #(f.cycleOf x).support) (hk' : (f ^ (k + 1) : (a : α) → α) x = y),
    ∃ (i : ℕ), 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i : (a : α) → α) x = y
⊢ ∃ (i : ℕ), 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i : (a : α) → α) x = y

Tactic:
rcases k with - | k
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
hk : 0 < #(f.cycleOf x).support
hk' : (HPow.hPow (β := ℕ) f 0 : (a : α) → α) x = y
⊢ ∃ (i : ℕ), 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i : (a : α) → α) x = y

Tactic:
⟨#(f.cycleOf x).support, hk, self_le_add_right _ _, ?_⟩

Premises used: Equiv.Perm.support, self_le_add_right, And.intro, Exists.intro, Finset.card, Equiv.Perm.cycleOf
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
hk : 0 < #(f.cycleOf x).support
hk' : (HPow.hPow (β := ℕ) f 0 : (a : α) → α) x = y
pos : (f ^ #(f.cycleOf x).support : (a : α) → α) x = y
⊢ ∃ (i : ℕ), 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i : (a : α) → α) x = y

Tactic:
refine ⟨#(f.cycleOf x).support, hk, self_le_add_right _ _, ?_⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
hk : 0 < #(f.cycleOf x).support
hk' : (HPow.hPow (β := ℕ) f 0 : (a : α) → α) x = y
⊢ x = y

Tactic:
simp only [pow_zero, coe_one, id_eq] at hk'

Premises used: Equiv.Perm.coe_one, pow_zero, id_eq
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
hk : 0 < #(f.cycleOf x).support
hk' : x = y
pos : ∀ (h : f.SameCycle x x), (f ^ #(f.cycleOf x).support : (a : α) → α) x = x
⊢ (f ^ #(f.cycleOf x).support : (a : α) → α) x = y

Tactic:
subst hk'
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
x : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
hx : x ∈ f.support
hk : 0 < #(f.cycleOf x).support
h : f.SameCycle x x
pos : (f ^ orderOf (f.cycleOf x) : (a : α) → α) x = x
pos₁ : (f.cycleOf x ^ orderOf (f.cycleOf x) : (a : α) → α) x = x
pos₂ : (1 : (a : α) → α) x = x
pos₃ pos₄ : x = x
⊢ (f ^ #(f.cycleOf x).support : (a : α) → α) x = x

Tactic:
rw [← (isCycle_cycleOf _ <| mem_support.1 hx).orderOf, ← cycleOf_pow_apply_self,
        pow_orderOf_eq_one, one_apply]

Premises used: Equiv.Perm.isCycle_cycleOf, Equiv.Perm.mem_support, Equiv.Perm.cycleOf_pow_apply_self, Equiv.Perm.IsCycle.orderOf, pow_orderOf_eq_one, Equiv.Perm.one_apply, Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
k : ℕ
hk : k + 1 < #(f.cycleOf x).support
hk' : (f ^ (k + 1) : (a : α) → α) x = y
⊢ 0 < k + 1

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
k : ℕ
hk : k + 1 < #(f.cycleOf x).support
hk' : (f ^ (k + 1) : (a : α) → α) x = y
⊢ ∃ (i : ℕ), 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i : (a : α) → α) x = y

Tactic:
exact ⟨k + 1, by simp, Nat.le_succ_of_le hk.le, hk'⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∉ f.support
⊢ 1 ≤ #(f.cycleOf x).support + 1

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∉ f.support
neg : (HPow.hPow (β := ℕ) f 1 : (a : α) → α) x = y
⊢ ∃ (i : ℕ), 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i : (a : α) → α) x = y

Tactic:
refine ⟨1, zero_lt_one, by simp, ?_⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∉ f.support
neg : ∀ (k : ℤ), Eq (α := α) ((HPow.hPow (β := ℕ) f 1 : (a : α) → α) x : α) ((f ^ k : (a : α) → α) x : α)
⊢ (HPow.hPow (β := ℕ) f 1 : (a : α) → α) x = y

Tactic:
obtain ⟨k, rfl⟩ := h

Premises used: Equiv.Perm.SameCycle.rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
x : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
hx : x ∉ f.support
k : ℤ
neg :
  ∀ (hx : (f : (a : α) → α) x = x) (k : ℤ),
    Eq (α := α) ((HPow.hPow (β := ℕ) f 1 : (a : α) → α) x : α) ((f ^ k : (a : α) → α) x : α)
⊢ Eq (α := α) ((HPow.hPow (β := ℕ) f 1 : (a : α) → α) x : α) ((f ^ k : (a : α) → α) x : α)

Tactic:
rw [notMem_support] at hx

Premises used: Equiv.Perm.notMem_support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
x : α
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
hx : (f : (a : α) → α) x = x
k : ℤ
neg : x = (f ^ k : (a : α) → α) x
neg₁ neg₂ : x = x
⊢ Eq (α := α) ((HPow.hPow (β := ℕ) f 1 : (a : α) → α) x : α) ((f ^ k : (a : α) → α) x : α)

Tactic:
rw [pow_apply_eq_self_of_apply_eq_self hx, zpow_apply_eq_self_of_apply_eq_self hx]

Premises used: Equiv.Perm.zpow_apply_eq_self_of_apply_eq_self, Equiv.Perm.pow_apply_eq_self_of_apply_eq_self
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
m n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
rw :
  Eq (α := α) ((g ^ m : (a : α) → α) x : α) ((g ^ n : (a : α) → α) x : α) ↔
    (m - n) % (↑(#(g.cycleOf x).support) : ℤ) = 0
⊢ Eq (α := α) ((g ^ m : (a : α) → α) x : α) ((g ^ n : (a : α) → α) x : α) ↔
    m % (↑(#(g.cycleOf x).support) : ℤ) = n % (↑(#(g.cycleOf x).support) : ℤ)

Tactic:
rw [Int.emod_eq_emod_iff_emod_sub_eq_zero]

Premises used: Int.emod_eq_emod_iff_emod_sub_eq_zero
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
m n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
rw : Eq (α := α) ((g ^ n * g ^ (m - n) : (a : α) → α) x : α) ((g ^ n : (a : α) → α) x : α)
| Eq (α := α) ((g ^ m : (a : α) → α) x : α) ((g ^ n : (a : α) → α) x : α)

Tactic:
rw [← Int.sub_add_cancel m n, Int.add_comm, zpow_add]

Premises used: zpow_add, Int.add_comm, Int.sub_add_cancel
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
m n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
conv_lhs :
  Eq (α := α) ((g ^ n * g ^ (m - n) : (a : α) → α) x : α) ((g ^ n : (a : α) → α) x : α) ↔
    (m - n) % (↑(#(g.cycleOf x).support) : ℤ) = 0
⊢ Eq (α := α) ((g ^ m : (a : α) → α) x : α) ((g ^ n : (a : α) → α) x : α) ↔
    (m - n) % (↑(#(g.cycleOf x).support) : ℤ) = 0

Tactic:
conv_lhs => rw [← Int.sub_add_cancel m n, Int.add_comm, zpow_add]

Premises used: zpow_add, Int.add_comm, Int.sub_add_cancel
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
m n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
simp : (g ^ (m - n) : (a : α) → α) x = x ↔ (m - n) % (↑(#(g.cycleOf x).support) : ℤ) = 0
⊢ Eq (α := α) ((g ^ n * g ^ (m - n) : (a : α) → α) x : α) ((g ^ n : (a : α) → α) x : α) ↔
    (m - n) % (↑(#(g.cycleOf x).support) : ℤ) = 0

Tactic:
simp only [coe_mul, Function.comp_apply, EmbeddingLike.apply_eq_iff_eq]

Premises used: Equiv.Perm.coe_mul, EmbeddingLike.apply_eq_iff_eq, Function.comp_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
m n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
rw : (g ^ (m - n) : (a : α) → α) x = x ↔ (↑(#(g.cycleOf x).support) : ℤ) ∣ m - n
⊢ (g ^ (m - n) : (a : α) → α) x = x ↔ (m - n) % (↑(#(g.cycleOf x).support) : ℤ) = 0

Tactic:
rw [← Int.dvd_iff_emod_eq_zero]

Premises used: Int.dvd_iff_emod_eq_zero
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
m n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
rw : (m - n) % (↑(#(g.cycleOf x).support) : ℤ) = 0 ↔ (↑(#(g.cycleOf x).support) : ℤ) ∣ m - n
hg : (g.cycleOf x).IsCycle
hx₁ : (g.cycleOf x : (a : α) → α) x ≠ x
⊢ (g ^ (m - n) : (a : α) → α) x = x ↔ (↑(#(g.cycleOf x).support) : ℤ) ∣ m - n

Tactic:
rw [← cycleOf_zpow_apply_self g x, cycle_zpow_mem_support_iff]

Premises used: Equiv.Perm.cycle_zpow_mem_support_iff, Equiv.Perm.cycleOf_zpow_apply_self
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
m n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
rw rw₁ : (↑(#(g.cycleOf x).support) : ℤ) ∣ m - n ↔ (↑(#(g.cycleOf x).support) : ℤ) ∣ m - n
⊢ (m - n) % (↑(#(g.cycleOf x).support) : ℤ) = 0 ↔ (↑(#(g.cycleOf x).support) : ℤ) ∣ m - n

Tactic:
rw [← Int.dvd_iff_emod_eq_zero]

Premises used: Int.dvd_iff_emod_eq_zero
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
m n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
⊢ (g.cycleOf x).IsCycle

Tactic:
isCycle_cycleOf g hx

Premises used: Equiv.Perm.isCycle_cycleOf
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
m n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
⊢ (g.cycleOf x).IsCycle

Tactic:
exact isCycle_cycleOf g hx

Premises used: Equiv.Perm.isCycle_cycleOf
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
m n : ℤ
x : α
hx hx₁ : (g : (a : α) → α) x ≠ x
⊢ (g.cycleOf x : (a : α) → α) x ≠ x

Tactic:
simp only [cycleOf_apply_self]

Premises used: Equiv.Perm.cycleOf_apply_self
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
m n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
⊢ (g : (a : α) → α) x ≠ x

Tactic:
hx
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
m n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
⊢ (g : (a : α) → α) x ≠ x

Tactic:
exact hx
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
hg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → Membership.mem (γ := List α) [] x
simp : ∀ (hg : ∀ {x : α}, (g : (a : α) → α) x = x), 1 = g
⊢ List.prod [] = g ∧
    (∀ (g' : Perm α), Membership.mem (γ := List (Perm α)) [] g' → g'.IsCycle) ∧
      List.Pairwise.{u_2} (α := Perm α) Disjoint []

Tactic:
simp only [imp_false, List.Pairwise.nil, List.not_mem_nil, forall_const, and_true,
          forall_prop_of_false, Classical.not_not, not_false_iff, List.prod_nil] at *

Premises used: and_true, Classical.not_not, imp_false, forall_prop_of_false, List.Pairwise.nil, List.prod_nil, forall_const, not_false_iff, List.not_mem_nil