awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
n : ℕ
x : α
rw : Eq (α := α) ((f.cycleOf x ^ (n % orderOf (f.cycleOf x)) : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α)
rw₁ :
  Eq (α := α) ((f.cycleOf x ^ (n % orderOf (f.cycleOf x)) : (a : α) → α) x : α) ((f.cycleOf x ^ n : (a : α) → α) x : α)
rw₂ rw₃ : Eq (α := α) ((f.cycleOf x ^ n : (a : α) → α) x : α) ((f.cycleOf x ^ n : (a : α) → α) x : α)
⊢ Eq (α := α) ((f ^ (n % orderOf (f.cycleOf x)) : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α)

Tactic:
rw [← cycleOf_pow_apply_self f, ← cycleOf_pow_apply_self f, pow_mod_orderOf]

Premises used: pow_mod_orderOf, Equiv.Perm.cycleOf_pow_apply_self
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f g : Perm α
inst : DecidableRel f.SameCycle
inst_1 : DecidableRel (f * g).SameCycle
h : Commute f g
x : α
hx : (g : (a : α) → α) x = x
H : ∀ (y : α), Eq (α := α) (((f * g).cycleOf x : (a : α) → α) y : α) ((f.cycleOf x : (a : α) → α) y : α)
⊢ (f * g).cycleOf x = f.cycleOf x

Tactic:
ext y
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f g : Perm α
inst : DecidableRel f.SameCycle
inst_1 : DecidableRel (f * g).SameCycle
h : Commute f g
x : α
hx : (g : (a : α) → α) x = x
y : α
pos :
  ∀ (hxy : (f * g).SameCycle x y),
    Eq (α := α) (((f * g).cycleOf x : (a : α) → α) y : α) ((f.cycleOf x : (a : α) → α) y : α)
neg :
  ∀ (hxy : ¬(f * g).SameCycle x y),
    Eq (α := α) (((f * g).cycleOf x : (a : α) → α) y : α) ((f.cycleOf x : (a : α) → α) y : α)
⊢ Eq (α := α) (((f * g).cycleOf x : (a : α) → α) y : α) ((f.cycleOf x : (a : α) → α) y : α)

Tactic:
by_cases hxy : (f * g).SameCycle x y

Premises used: HMul.hMul, Equiv.Perm.SameCycle
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f g : Perm α
inst : DecidableRel f.SameCycle
inst_1 : DecidableRel (f * g).SameCycle
h : Commute f g
x : α
hx : (g : (a : α) → α) x = x
y : α
hxy : (f * g).SameCycle x y
pos :
  ∀ (z : ℤ),
    Eq (α := α) (((f * g).cycleOf x : (a : α) → α) (((f * g) ^ z : (a : α) → α) x : α) : α)
      ((f.cycleOf x : (a : α) → α) (((f * g) ^ z : (a : α) → α) x : α) : α)
⊢ Eq (α := α) (((f * g).cycleOf x : (a : α) → α) y : α) ((f.cycleOf x : (a : α) → α) y : α)

Tactic:
obtain ⟨z, rfl⟩ := hxy

Premises used: rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f g : Perm α
inst : DecidableRel f.SameCycle
inst_1 : DecidableRel (f * g).SameCycle
h : Commute f g
x : α
hx : (g : (a : α) → α) x = x
z : ℤ
pos :
  Eq (α := α) (((f * g) ^ (z + 1) : (a : α) → α) x : α)
    ((f.cycleOf x : (a : α) → α) (((f * g) ^ z : (a : α) → α) x : α) : α)
⊢ Eq (α := α) (((f * g).cycleOf x : (a : α) → α) (((f * g) ^ z : (a : α) → α) x : α) : α)
    ((f.cycleOf x : (a : α) → α) (((f * g) ^ z : (a : α) → α) x : α) : α)

Tactic:
rw [cycleOf_apply_apply_zpow_self]

Premises used: Equiv.Perm.cycleOf_apply_apply_zpow_self
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f g : Perm α
inst : DecidableRel f.SameCycle
inst_1 : DecidableRel (f * g).SameCycle
h : Commute f g
x : α
hx : (g : (a : α) → α) x = x
z : ℤ
⊢ Eq (α := α) (((f * g) ^ (z + 1) : (a : α) → α) x : α)
    ((f.cycleOf x : (a : α) → α) (((f * g) ^ z : (a : α) → α) x : α) : α)

Tactic:
simp [h.mul_zpow, zpow_apply_eq_self_of_apply_eq_self hx]

Premises used: Equiv.Perm.zpow_apply_eq_self_of_apply_eq_self, Commute.mul_zpow
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f g : Perm α
inst : DecidableRel f.SameCycle
inst_1 : DecidableRel (f * g).SameCycle
h : Commute f g
x : α
hx : (g : (a : α) → α) x = x
y : α
hxy : ¬(f * g).SameCycle x y
neg : ¬f.SameCycle x y
⊢ Eq (α := α) (((f * g).cycleOf x : (a : α) → α) y : α) ((f.cycleOf x : (a : α) → α) y : α)

Tactic:
rw [cycleOf_apply_of_not_sameCycle hxy, cycleOf_apply_of_not_sameCycle]

Premises used: Equiv.Perm.cycleOf_apply_of_not_sameCycle
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f g : Perm α
inst : DecidableRel f.SameCycle
inst_1 : DecidableRel (f * g).SameCycle
h : Commute f g
x : α
hx : (g : (a : α) → α) x = x
y : α
hxy : ¬(f * g).SameCycle x y
neg : ∀ (hxy : f.SameCycle x y), (f * g).SameCycle x y
⊢ ¬f.SameCycle x y

Tactic:
contrapose hxy
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f g : Perm α
inst : DecidableRel f.SameCycle
inst_1 : DecidableRel (f * g).SameCycle
h : Commute f g
x : α
hx : (g : (a : α) → α) x = x
y : α
hxy : f.SameCycle x y
neg : ∀ (z : ℤ), (f * g).SameCycle x ((f ^ z : (a : α) → α) x)
⊢ (f * g).SameCycle x y

Tactic:
obtain ⟨z, rfl⟩ := hxy

Premises used: rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f g : Perm α
inst : DecidableRel f.SameCycle
inst_1 : DecidableRel (f * g).SameCycle
h : Commute f g
x : α
hx : (g : (a : α) → α) x = x
z : ℤ
⊢ (f * g).SameCycle x ((f ^ z : (a : α) → α) x)

Tactic:
⟨z, ?_⟩

Premises used: Equiv.Perm.SameCycle, Exists.intro
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f g : Perm α
inst : DecidableRel f.SameCycle
inst_1 : DecidableRel (f * g).SameCycle
h : Commute f g
x : α
hx : (g : (a : α) → α) x = x
z : ℤ
neg : Eq (α := α) (((f * g) ^ z : (a : α) → α) x : α) ((f ^ z : (a : α) → α) x : α)
⊢ (f * g).SameCycle x ((f ^ z : (a : α) → α) x)

Tactic:
refine ⟨z, ?_⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f g : Perm α
inst : DecidableRel f.SameCycle
inst_1 : DecidableRel (f * g).SameCycle
h : Commute f g
x : α
hx : (g : (a : α) → α) x = x
z : ℤ
⊢ Eq (α := α) (((f * g) ^ z : (a : α) → α) x : α) ((f ^ z : (a : α) → α) x : α)

Tactic:
simp [h.mul_zpow, zpow_apply_eq_self_of_apply_eq_self hx]

Premises used: Equiv.Perm.zpow_apply_eq_self_of_apply_eq_self, Commute.mul_zpow
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f g : Perm α
inst : DecidableRel f.SameCycle
inst_1 : DecidableRel g.SameCycle
inst_2 : DecidableRel (f * g).SameCycle
h : f.Disjoint g
x : α
inl : ∀ (hfx : (f : (a : α) → α) x = x), (f * g).cycleOf x = f.cycleOf x * g.cycleOf x
inr : ∀ (hgx : (g : (a : α) → α) x = x), (f * g).cycleOf x = f.cycleOf x * g.cycleOf x
⊢ (f * g).cycleOf x = f.cycleOf x * g.cycleOf x

Tactic:
rcases (disjoint_iff_eq_or_eq.mp h) x with hfx | hgx

Premises used: Iff.mp, Equiv.Perm.disjoint_iff_eq_or_eq
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f g : Perm α
inst : DecidableRel f.SameCycle
inst_1 : DecidableRel g.SameCycle
inst_2 : DecidableRel (f * g).SameCycle
h : f.Disjoint g
x : α
hfx : (f : (a : α) → α) x = x
⊢ (f * g).cycleOf x = f.cycleOf x * g.cycleOf x

Tactic:
simp [h.commute.eq, cycleOf_mul_of_apply_right_eq_self h.symm.commute, hfx]

Premises used: Equiv.Perm.Disjoint.symm, Equiv.Perm.Disjoint.commute, Equiv.Perm.cycleOf_mul_of_apply_right_eq_self, Commute.eq
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f g : Perm α
inst : DecidableRel f.SameCycle
inst_1 : DecidableRel g.SameCycle
inst_2 : DecidableRel (f * g).SameCycle
h : f.Disjoint g
x : α
hgx : (g : (a : α) → α) x = x
⊢ (f * g).cycleOf x = f.cycleOf x * g.cycleOf x

Tactic:
simp [cycleOf_mul_of_apply_right_eq_self h.commute, hgx]

Premises used: Equiv.Perm.Disjoint.commute, Equiv.Perm.cycleOf_mul_of_apply_right_eq_self
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f g : Perm α
inst : DecidableRel f.SameCycle
inst_1 : DecidableRel g.SameCycle
inst_2 : DecidableRel (f * g).SameCycle
h : f.Disjoint g
x : α
inl : ∀ (hfx : (f : (a : α) → α) x = x), (f * g).cycleOf x = f.cycleOf x * g.cycleOf x
inr inr₁ : ∀ (hgx : (g : (a : α) → α) x = x), (f * g).cycleOf x = f.cycleOf x * g.cycleOf x
⊢ (f * g).cycleOf x = f.cycleOf x * g.cycleOf x

Tactic:
classical
  rcases (disjoint_iff_eq_or_eq.mp h) x with hfx | hgx
  · simp [h.commute.eq, cycleOf_mul_of_apply_right_eq_self h.symm.commute, hfx]
  · simp [cycleOf_mul_of_apply_right_eq_self h.commute, hgx]

Premises used: Equiv.Perm.Disjoint.commute, Iff.mp, Equiv.Perm.cycleOf_mul_of_apply_right_eq_self, Commute.eq, Equiv.Perm.disjoint_iff_eq_or_eq
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
x y : α
inst : DecidableRel f.SameCycle
inst_1 : DecidableEq α
inst_2 : Fintype α
pos : ∀ (hx : (f : (a : α) → α) x = x), y ∈ (f.cycleOf x).support ↔ f.SameCycle x y ∧ x ∈ f.support
neg : ∀ (hx : ¬(f : (a : α) → α) x = x), y ∈ (f.cycleOf x).support ↔ f.SameCycle x y ∧ x ∈ f.support
⊢ y ∈ (f.cycleOf x).support ↔ f.SameCycle x y ∧ x ∈ f.support

Tactic:
by_cases hx : f x = x

Premises used: DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
x y : α
inst : DecidableRel f.SameCycle
inst_1 : DecidableEq α
inst_2 : Fintype α
hx : (f : (a : α) → α) x = x
pos : Membership.mem (γ := Finset α) (support 1) y ↔ f.SameCycle x y ∧ x ∈ f.support
⊢ y ∈ (f.cycleOf x).support ↔ f.SameCycle x y ∧ x ∈ f.support

Tactic:
rw [(cycleOf_eq_one_iff _).mpr hx]

Premises used: Iff.mpr, Equiv.Perm.cycleOf_eq_one_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
x y : α
inst : DecidableRel f.SameCycle
inst_1 : DecidableEq α
inst_2 : Fintype α
hx : (f : (a : α) → α) x = x
⊢ Membership.mem (γ := Finset α) (support 1) y ↔ f.SameCycle x y ∧ x ∈ f.support

Tactic:
simp [hx]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
x y : α
inst : DecidableRel f.SameCycle
inst_1 : DecidableEq α
inst_2 : Fintype α
hx : ¬(f : (a : α) → α) x = x
neg : (if f.SameCycle x y then (f : (a : α) → α) y else y) ≠ y ↔ f.SameCycle x y ∧ x ∈ f.support
⊢ y ∈ (f.cycleOf x).support ↔ f.SameCycle x y ∧ x ∈ f.support

Tactic:
rw [mem_support, cycleOf_apply]

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

Tactic:
split_ifs with hy
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
x y : α
inst : DecidableRel f.SameCycle
inst_1 : DecidableEq α
inst_2 : Fintype α
hx : ¬(f : (a : α) → α) x = x
hy : f.SameCycle x y
pos : ¬(f : (a : α) → α) y = y ↔ True
⊢ (f : (a : α) → α) y ≠ y ↔ f.SameCycle x y ∧ x ∈ f.support

Tactic:
simp only [hx, hy, Ne, not_false_iff, and_self_iff, mem_support]

Premises used: Equiv.Perm.mem_support, Ne, and_self_iff, not_false_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
x y : α
inst : DecidableRel f.SameCycle
inst_1 : DecidableEq α
inst_2 : Fintype α
hx : ¬(f : (a : α) → α) x = x
hy : f.SameCycle x y
pos : ∀ (k : ℤ), ¬Eq (α := α) ((f : (a : α) → α) ((f ^ k : (a : α) → α) x : α) : α) ((f ^ k : (a : α) → α) x : α) ↔ True
⊢ ¬(f : (a : α) → α) y = y ↔ True

Tactic:
rcases hy with ⟨k, rfl⟩

Premises used: rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
x : α
inst : DecidableRel f.SameCycle
inst_1 : DecidableEq α
inst_2 : Fintype α
hx : ¬(f : (a : α) → α) x = x
k : ℤ
pos : ¬((f ^ k : (a : α) → α) x : α) ∉ f.support ↔ True
⊢ ¬Eq (α := α) ((f : (a : α) → α) ((f ^ k : (a : α) → α) x : α) : α) ((f ^ k : (a : α) → α) x : α) ↔ True

Tactic:
rw [← notMem_support]

Premises used: Equiv.Perm.notMem_support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
x : α
inst : DecidableRel f.SameCycle
inst_1 : DecidableEq α
inst_2 : Fintype α
hx : ¬(f : (a : α) → α) x = x
k : ℤ
⊢ ¬((f ^ k : (a : α) → α) x : α) ∉ f.support ↔ True

Tactic:
simpa using hx
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
x y : α
inst : DecidableRel f.SameCycle
inst_1 : DecidableEq α
inst_2 : Fintype α
hx : ¬(f : (a : α) → α) x = x
hy : ¬f.SameCycle x y
⊢ y ≠ y ↔ f.SameCycle x y ∧ x ∈ f.support

Tactic:
simpa [hx] using hy
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
x y : α
hx : (f : (a : α) → α) x ≠ x
inst : DecidableRel f.SameCycle
inst_1 : DecidableEq α
inst_2 : Fintype α
rw : f.SameCycle x y ∧ x ∈ f.support ↔ f.SameCycle x y
rw₁ rw₂ : f.SameCycle x y ↔ f.SameCycle x y
⊢ y ∈ (f.cycleOf x).support ↔ f.SameCycle x y

Tactic:
rw [mem_support_cycleOf_iff_aux, and_iff_left (mem_support.2 hx)]

Premises used: Iff.mpr, Equiv.Perm.mem_support, and_iff_left, _private.0.Equiv.Perm.mem_support_cycleOf_iff_aux
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
x : α
f : Perm α
inst : DecidableRel f.SameCycle
⊢ (f.cycleOf x).IsCycle ↔ (f : (a : α) → α) x ≠ x

Tactic:
⟨fun hx => ?_, f.isCycle_cycleOf⟩

Premises used: Equiv.Perm.isCycle_cycleOf, Iff.intro
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
x : α
f : Perm α
inst : DecidableRel f.SameCycle
refine : ∀ (hx : (f.cycleOf x).IsCycle), (f : (a : α) → α) x ≠ x
⊢ (f.cycleOf x).IsCycle ↔ (f : (a : α) → α) x ≠ x

Tactic:
refine ⟨fun hx => ?_, f.isCycle_cycleOf⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
x : α
f : Perm α
inst : DecidableRel f.SameCycle
hx : (f.cycleOf x).IsCycle
rw : ¬f.cycleOf x = 1
⊢ (f : (a : α) → α) x ≠ x

Tactic:
rw [Ne, ← cycleOf_eq_one_iff f]

Premises used: Equiv.Perm.cycleOf_eq_one_iff, Ne
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
x : α
f : Perm α
inst : DecidableRel f.SameCycle
hx : (f.cycleOf x).IsCycle
⊢ ¬f.cycleOf x = 1

Tactic:
hx.ne_one

Premises used: Equiv.Perm.IsCycle.ne_one
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
x : α
f : Perm α
inst : DecidableRel f.SameCycle
hx : (f.cycleOf x).IsCycle
⊢ ¬f.cycleOf x = 1

Tactic:
exact hx.ne_one

Premises used: Equiv.Perm.IsCycle.ne_one
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
inst_2 : DecidableRel f.SameCycle
x : α
⊢ ∀ (a : α),
    Membership.mem (α := α) (↑(f.cycleOf x).support : Set α) ((f : (a : α) → α) a : α) ↔
      a ∈ (↑(f.cycleOf x).support : Set α)

Tactic:
fun _ ↦
        ⟨fun h ↦ mem_support_cycleOf_iff_aux.2 ?_, fun h ↦ mem_support_cycleOf_iff_aux.2 ?_⟩

Premises used: Iff.mpr, _private.0.Equiv.Perm.mem_support_cycleOf_iff_aux, Iff.intro
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
inst_2 : DecidableRel f.SameCycle
x : α
refine_1 :
  ∀ (x_1 : α) (h : Membership.mem (α := α) (↑(f.cycleOf x).support : Set α) ((f : (a : α) → α) x_1 : α)),
    f.SameCycle x x_1 ∧ x ∈ f.support
refine_2 :
  ∀ (x_1 : α) (h : x_1 ∈ (↑(f.cycleOf x).support : Set α)), f.SameCycle x ((f : (a : α) → α) x_1) ∧ x ∈ f.support
⊢ ∀ (a : α),
    Membership.mem (α := α) (↑(f.cycleOf x).support : Set α) ((f : (a : α) → α) a : α) ↔
      a ∈ (↑(f.cycleOf x).support : Set α)

Tactic:
refine fun _ ↦
        ⟨fun h ↦ mem_support_cycleOf_iff_aux.2 ?_, fun h ↦ mem_support_cycleOf_iff_aux.2 ?_⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
inst_2 : DecidableRel f.SameCycle
x x_1 : α
h : Membership.mem (α := α) (↑(f.cycleOf x).support : Set α) ((f : (a : α) → α) x_1 : α)
⊢ f.SameCycle x x_1 ∧ x ∈ f.support

Tactic:
⟨sameCycle_apply_right.1 (mem_support_cycleOf_iff_aux.1 h).1,
      (mem_support_cycleOf_iff_aux.1 h).2⟩

Premises used: Equiv.Perm.sameCycle_apply_right, And.right, And.left, _private.0.Equiv.Perm.mem_support_cycleOf_iff_aux, And.intro, Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
inst_2 : DecidableRel f.SameCycle
x x_1 : α
h : Membership.mem (α := α) (↑(f.cycleOf x).support : Set α) ((f : (a : α) → α) x_1 : α)
⊢ f.SameCycle x x_1 ∧ x ∈ f.support

Tactic:
exact ⟨sameCycle_apply_right.1 (mem_support_cycleOf_iff_aux.1 h).1,
      (mem_support_cycleOf_iff_aux.1 h).2⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
inst_2 : DecidableRel f.SameCycle
x x_1 : α
h : x_1 ∈ (↑(f.cycleOf x).support : Set α)
⊢ f.SameCycle x ((f : (a : α) → α) x_1) ∧ x ∈ f.support

Tactic:
⟨sameCycle_apply_right.2 (mem_support_cycleOf_iff_aux.1 h).1,
      (mem_support_cycleOf_iff_aux.1 h).2⟩

Premises used: Iff.mpr, Equiv.Perm.sameCycle_apply_right, And.right, And.left, _private.0.Equiv.Perm.mem_support_cycleOf_iff_aux, And.intro, Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
inst_2 : DecidableRel f.SameCycle
x x_1 : α
h : x_1 ∈ (↑(f.cycleOf x).support : Set α)
⊢ f.SameCycle x ((f : (a : α) → α) x_1) ∧ x ∈ f.support

Tactic:
exact ⟨sameCycle_apply_right.2 (mem_support_cycleOf_iff_aux.1 h).1,
      (mem_support_cycleOf_iff_aux.1 h).2⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
inst_2 : DecidableRel f.SameCycle
x a : α
ha : a ∈ (↑(f.cycleOf x).support : Set α)
b : α
hb : b ∈ (↑(f.cycleOf x).support : Set α)
rw : ∀ (ha : f.SameCycle x a ∧ x ∈ f.support) (b : α) (hb : f.SameCycle x b ∧ x ∈ f.support), f.SameCycle a b
⊢ f.SameCycle a b

Tactic:
rw [mem_coe, mem_support_cycleOf_iff_aux] at ha hb

Premises used: _private.0.Equiv.Perm.mem_support_cycleOf_iff_aux, Finset.mem_coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
inst_2 : DecidableRel f.SameCycle
x a : α
ha : f.SameCycle x a ∧ x ∈ f.support
b : α
hb : f.SameCycle x b ∧ x ∈ f.support
⊢ f.SameCycle a b

Tactic:
ha.1.symm.trans hb.1

Premises used: Equiv.Perm.SameCycle.symm, Equiv.Perm.SameCycle.trans, And.left
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
inst_2 : DecidableRel f.SameCycle
x a : α
ha : f.SameCycle x a ∧ x ∈ f.support
b : α
hb : f.SameCycle x b ∧ x ∈ f.support
⊢ f.SameCycle a b

Tactic:
exact ha.1.symm.trans hb.1

Premises used: Equiv.Perm.SameCycle.symm, Equiv.Perm.SameCycle.trans, And.left
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
x y : α
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel f.SameCycle
h : f.SameCycle x y
hx : x ∈ f.support
⊢ (f : (a : α) → α) x ≠ x

Tactic:
rw [mem_support] at hx

Premises used: Equiv.Perm.mem_support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
x y : α
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel f.SameCycle
h : f.SameCycle x y
hx : (f : (a : α) → α) x ≠ x
rw rw₁ : f.SameCycle x x
⊢ x ∈ (f.cycleOf x).support

Tactic:
rw [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
x y : α
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel f.SameCycle
h : f.SameCycle x y
hx : (f : (a : α) → α) x ≠ x
rwa rwa₁ rwa₂ rwa₃ : f.SameCycle x y
⊢ y ∈ (f.cycleOf x).support

Tactic:
rwa [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
x y : α
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel f.SameCycle
h : f.SameCycle x y
hx : (f : (a : α) → α) x ≠ x
⊢ ∃ i < #(f.cycleOf x).support, (f ^ i : (a : α) → α) x = y

Tactic:
exact Equiv.Perm.IsCycleOn.exists_pow_eq (b := y) (f.isCycleOn_support_cycleOf_aux x)
    (by rw [mem_support_cycleOf_iff'_aux hx]) (by rwa [mem_support_cycleOf_iff'_aux hx])

Premises used: Equiv.Perm.IsCycleOn.exists_pow_eq, _private.0.Equiv.Perm.isCycleOn_support_cycleOf_aux
-- 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 : α
simp : (∃ m < Fintype.card α, (f ^ m : (a : α) → α) x = y) ↔ f.SameCycle x y
⊢ y ∈ List.iterate (⇑f : (a : α) → α) x (Fintype.card α) ↔ f.SameCycle x y

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

Premises used: Equiv.Perm.iterate_eq_pow, eq_comm, List.mem_iterate
-- 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 : α
mp : (∃ m < Fintype.card α, (f ^ m : (a : α) → α) x = y) → f.SameCycle x y
mpr : f.SameCycle x y → ∃ m < Fintype.card α, (f ^ m : (a : α) → α) x = y
⊢ (∃ m < Fintype.card α, (f ^ m : (a : α) → α) x = y) ↔ f.SameCycle x y

Tactic:
constructor
-- 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 : α
n : ℕ
left : n < Fintype.card α
hn : (f ^ n : (a : α) → α) x = y
⊢ f.SameCycle x y

Tactic:
⟨n, hn⟩

Premises used: Equiv.Perm.SameCycle, Nat.cast, Exists.intro
-- 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 : α
n : ℕ
left : n < Fintype.card α
hn : (f ^ n : (a : α) → α) x = y
⊢ f.SameCycle x y

Tactic:
exact ⟨n, hn⟩
-- 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
by_cases : ∀ (hx : x ∈ f.support), ∃ m < Fintype.card α, (f ^ m : (a : α) → α) x = y
by_cases₁ : ∀ (hx : x ∉ f.support), ∃ m < Fintype.card α, (f ^ m : (a : α) → α) x = y
⊢ ∃ m < Fintype.card α, (f ^ m : (a : α) → α) x = y

Tactic:
by_cases hx : x ∈ f.support

Premises used: Equiv.Perm.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
_inst : (f : Perm α) → DecidableRel f.SameCycle := fun (f : Perm α) ↦ Classical.decRel f.SameCycle
rcases :
  ∀ (i : ℕ) (hixy : i < #(f.cycleOf x).support) (hi : (f ^ i : (a : α) → α) x = y),
    ∃ m < Fintype.card α, (f ^ m : (a : α) → α) x = y
⊢ ∃ m < Fintype.card α, (f ^ m : (a : α) → α) x = y

Tactic:
rcases hxy.exists_pow_eq_of_mem_support_aux hx with ⟨i, hixy, hi⟩

Premises used: _private.0.Equiv.Perm.SameCycle.exists_pow_eq_of_mem_support_aux
-- 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
_inst : (f : Perm α) → DecidableRel f.SameCycle := fun (f : Perm α) ↦ Classical.decRel f.SameCycle
i : ℕ
hixy : i < #(f.cycleOf x).support
hi : (f ^ i : (a : α) → α) x = y
⊢ ∃ m < Fintype.card α, (f ^ m : (a : α) → α) x = y

Tactic:
⟨i, lt_of_lt_of_le hixy (card_le_univ _), hi⟩

Premises used: Finset.card_le_univ, And.intro, Exists.intro, lt_of_lt_of_le
-- 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
_inst : (f : Perm α) → DecidableRel f.SameCycle := fun (f : Perm α) ↦ Classical.decRel f.SameCycle
i : ℕ
hixy : i < #(f.cycleOf x).support
hi : (f ^ i : (a : α) → α) x = y
⊢ ∃ m < Fintype.card α, (f ^ m : (a : α) → α) x = y

Tactic:
refine ⟨i, lt_of_lt_of_le hixy (card_le_univ _), hi⟩
-- 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
⊢ ∃ m < Fintype.card α, (f ^ m : (a : α) → α) x = y

Tactic:
case pos =>
        -- we can't invoke the aux lemmas above without obtaining the decidable instance we are
        -- already building; but now we've left the data, so we can do this non-constructively
        -- without sacrificing computability.
        let _inst (f : Perm α) : DecidableRel (SameCycle f) := Classical.decRel _
        rcases hxy.exists_pow_eq_of_mem_support_aux hx with ⟨i, hixy, hi⟩
        refine ⟨i, lt_of_lt_of_le hixy (card_le_univ _), hi⟩

Premises used: _private.0.Equiv.Perm.SameCycle.exists_pow_eq_of_mem_support_aux