awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x y : α
h : f.SameCycle x y
⊢ f.SameCycle x y

Tactic:
h
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x y : α
h : f.SameCycle x y
⊢ f.SameCycle x y

Tactic:
exact h
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x y : α
h neg : ¬f.SameCycle x y
⊢ (((ofSubtype (p := fun (x_1 : α) ↦ f.SameCycle x x_1) : (a : Perm { x_1 : α // f.SameCycle x x_1 }) → Perm α)
            (f.subtypePerm (p := f.SameCycle x) ⋯) :
          Perm α) :
        (a : α) → α)
      y =
    y

Tactic:
apply ofSubtype_apply_of_not_mem

Premises used: Equiv.Perm.ofSubtype_apply_of_not_mem
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x y : α
h : ¬f.SameCycle x y
⊢ ¬f.SameCycle x y

Tactic:
h
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x y : α
h : ¬f.SameCycle x y
⊢ ¬f.SameCycle x y

Tactic:
exact h
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x y : α
rw :
  y =
    if f.SameCycle x (if f⁻¹.SameCycle x y then (f⁻¹ : (a : α) → α) y else y) then
      (f : (a : α) → α) (if f⁻¹.SameCycle x y then (f⁻¹ : (a : α) → α) y else y : α)
    else if f⁻¹.SameCycle x y then (f⁻¹ : (a : α) → α) y else y
⊢ Eq (α := α) (((f.cycleOf x)⁻¹ : (a : α) → α) y : α) ((f⁻¹.cycleOf x : (a : α) → α) y : α)

Tactic:
rw [inv_eq_iff_eq, cycleOf_apply, cycleOf_apply]

Premises used: Equiv.Perm.inv_eq_iff_eq, Equiv.Perm.cycleOf_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x y : α
pos : f⁻¹.SameCycle x y → f.SameCycle x ((f⁻¹ : (a : α) → α) y) → y = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) y : α)
neg : f⁻¹.SameCycle x y → ¬f.SameCycle x ((f⁻¹ : (a : α) → α) y) → y = (f⁻¹ : (a : α) → α) y
pos₁ : ¬f⁻¹.SameCycle x y → f.SameCycle x y → y = (f : (a : α) → α) y
neg₁ : ¬f⁻¹.SameCycle x y → ¬f.SameCycle x y → y = y
⊢ y =
    if f.SameCycle x (if f⁻¹.SameCycle x y then (f⁻¹ : (a : α) → α) y else y) then
      (f : (a : α) → α) (if f⁻¹.SameCycle x y then (f⁻¹ : (a : α) → α) y else y : α)
    else if f⁻¹.SameCycle x y then (f⁻¹ : (a : α) → α) y else y

Tactic:
split_ifs
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x y : α
h : f⁻¹.SameCycle x y
h_1 : f.SameCycle x ((f⁻¹ : (a : α) → α) y)
⊢ y = (f : (a : α) → α) ((f⁻¹ : (a : α) → α) y : α)

Tactic:
simp_all [sameCycle_inv, sameCycle_symm_apply_right]

Premises used: Equiv.Perm.sameCycle_symm_apply_right, Equiv.Perm.sameCycle_inv
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x y : α
h : f⁻¹.SameCycle x y
h_1 : ¬f.SameCycle x ((f⁻¹ : (a : α) → α) y)
⊢ y = (f⁻¹ : (a : α) → α) y

Tactic:
simp_all [sameCycle_inv, sameCycle_symm_apply_right]

Premises used: Equiv.Perm.sameCycle_symm_apply_right, Equiv.Perm.sameCycle_inv
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x y : α
h : ¬f⁻¹.SameCycle x y
h_1 : f.SameCycle x y
⊢ y = (f : (a : α) → α) y

Tactic:
simp_all [sameCycle_inv, sameCycle_symm_apply_right]

Premises used: Equiv.Perm.sameCycle_symm_apply_right, Equiv.Perm.sameCycle_inv
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x y : α
h : ¬f⁻¹.SameCycle x y
h_1 : ¬f.SameCycle x y
⊢ y = y

Tactic:
simp_all [sameCycle_inv, sameCycle_symm_apply_right]

Premises used: Equiv.Perm.sameCycle_symm_apply_right, Equiv.Perm.sameCycle_inv
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x : α
⊢ Eq (α := α) ((HPow.hPow (β := ℕ) (f.cycleOf x) 0 : (a : α) → α) x : α) ((HPow.hPow (β := ℕ) f 0 : (a : α) → α) x : α)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x : α
n : ℕ
hn : Eq (α := α) ((f.cycleOf x ^ n : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α)
succ : f.SameCycle x ((f ^ n : (a : α) → α) x)
⊢ Eq (α := α) ((f.cycleOf x ^ (n + 1) : (a : α) → α) x : α) ((f ^ (n + 1) : (a : α) → α) x : α)

Tactic:
rw [pow_succ', mul_apply, cycleOf_apply, hn, if_pos, pow_succ', mul_apply]

Premises used: if_pos, Equiv.Perm.cycleOf_apply, Equiv.Perm.mul_apply, pow_succ'
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x : α
n : ℕ
hn : Eq (α := α) ((f.cycleOf x ^ n : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α)
⊢ f.SameCycle x ((f ^ n : (a : α) → α) x)

Tactic:
⟨n, rfl⟩

Premises used: Equiv.Perm.SameCycle, Nat.cast, Exists.intro, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x : α
n : ℕ
hn : Eq (α := α) ((f.cycleOf x ^ n : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α)
⊢ f.SameCycle x ((f ^ n : (a : α) → α) x)

Tactic:
exact ⟨n, rfl⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x : α
n : ℕ
zero :
  Eq (α := α) ((HPow.hPow (β := ℕ) (f.cycleOf x) 0 : (a : α) → α) x : α) ((HPow.hPow (β := ℕ) f 0 : (a : α) → α) x : α)
succ :
  ∀ (n : ℕ) (hn : Eq (α := α) ((f.cycleOf x ^ n : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α)),
    Eq (α := α) ((f.cycleOf x ^ (n + 1) : (a : α) → α) x : α) ((f ^ (n + 1) : (a : α) → α) x : α)
⊢ Eq (α := α) ((f.cycleOf x ^ n : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α)

Tactic:
induction n with
  | zero => rfl
  | succ n hn =>
    rw [pow_succ', mul_apply, cycleOf_apply, hn, if_pos, pow_succ', mul_apply]
    exact ⟨n, rfl⟩

Premises used: if_pos, Equiv.Perm.cycleOf_apply, Equiv.Perm.mul_apply, pow_succ'
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x : α
z : ℕ
⊢ Eq (α := α) ((f.cycleOf x ^ Int.ofNat z : (a : α) → α) x : α) ((f ^ Int.ofNat z : (a : α) → α) x : α)

Tactic:
cycleOf_pow_apply_self f x z

Premises used: Equiv.Perm.cycleOf_pow_apply_self
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x : α
z : ℕ
⊢ Eq (α := α) ((f.cycleOf x ^ Int.ofNat z : (a : α) → α) x : α) ((f ^ Int.ofNat z : (a : α) → α) x : α)

Tactic:
exact cycleOf_pow_apply_self f x z

Premises used: Equiv.Perm.cycleOf_pow_apply_self
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x : α
z : ℕ
negSucc : Eq (α := α) (((f.cycleOf x ^ (z + 1))⁻¹ : (a : α) → α) x : α) ((f ^ Int.negSucc z : (a : α) → α) x : α)
negSucc₁ : Eq (α := α) (((f.cycleOf x)⁻¹ ^ (z + 1) : (a : α) → α) x : α) ((f ^ Int.negSucc z : (a : α) → α) x : α)
negSucc₂ : Eq (α := α) ((f⁻¹.cycleOf x ^ (z + 1) : (a : α) → α) x : α) ((f ^ Int.negSucc z : (a : α) → α) x : α)
negSucc₃ : Eq (α := α) ((f⁻¹.cycleOf x ^ (z + 1) : (a : α) → α) x : α) (((f ^ (z + 1))⁻¹ : (a : α) → α) x : α)
negSucc₄ : Eq (α := α) ((f⁻¹.cycleOf x ^ (z + 1) : (a : α) → α) x : α) ((f⁻¹ ^ (z + 1) : (a : α) → α) x : α)
negSucc₅ negSucc₆ : Eq (α := α) ((f⁻¹ ^ (z + 1) : (a : α) → α) x : α) ((f⁻¹ ^ (z + 1) : (a : α) → α) x : α)
⊢ Eq (α := α) ((f.cycleOf x ^ Int.negSucc z : (a : α) → α) x : α) ((f ^ Int.negSucc z : (a : α) → α) x : α)

Tactic:
rw [zpow_negSucc, ← inv_pow, cycleOf_inv, zpow_negSucc, ← inv_pow, cycleOf_pow_apply_self]

Premises used: Equiv.Perm.cycleOf_inv, zpow_negSucc, Equiv.Perm.cycleOf_pow_apply_self, inv_pow
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x : α
z : ℤ
ofNat : ∀ (z : ℕ), Eq (α := α) ((f.cycleOf x ^ Int.ofNat z : (a : α) → α) x : α) ((f ^ Int.ofNat z : (a : α) → α) x : α)
negSucc :
  ∀ (z : ℕ), Eq (α := α) ((f.cycleOf x ^ Int.negSucc z : (a : α) → α) x : α) ((f ^ Int.negSucc z : (a : α) → α) x : α)
⊢ Eq (α := α) ((f.cycleOf x ^ z : (a : α) → α) x : α) ((f ^ z : (a : α) → α) x : α)

Tactic:
cases z with
  | ofNat z => exact cycleOf_pow_apply_self f x z
  | negSucc z =>
    rw [zpow_negSucc, ← inv_pow, cycleOf_inv, zpow_negSucc, ← inv_pow, cycleOf_pow_apply_self]

Premises used: Equiv.Perm.cycleOf_inv, zpow_negSucc, Equiv.Perm.cycleOf_pow_apply_self, inv_pow
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
x y : α
inst : DecidableRel f.SameCycle
⊢ f.SameCycle x y → Eq (α := α) ((f.cycleOf x : (a : α) → α) y : α) ((f : (a : α) → α) y : α)

Tactic:
ofSubtype_apply_of_mem _

Premises used: Equiv.Perm.ofSubtype_apply_of_mem
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
x y : α
inst : DecidableRel f.SameCycle
⊢ ¬f.SameCycle x y → (f.cycleOf x : (a : α) → α) y = y

Tactic:
ofSubtype_apply_of_not_mem _

Premises used: Equiv.Perm.ofSubtype_apply_of_not_mem
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
x y : α
inst : DecidableRel f.SameCycle
h : f.SameCycle x y
H : ∀ (z : α), Eq (α := α) ((f.cycleOf x : (a : α) → α) z : α) ((f.cycleOf y : (a : α) → α) z : α)
⊢ f.cycleOf x = f.cycleOf y

Tactic:
ext z
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
x y : α
inst : DecidableRel f.SameCycle
h : f.SameCycle x y
z : α
H : Eq (α := α) (if f.SameCycle x z then (f : (a : α) → α) z else z : α) ((f.cycleOf y : (a : α) → α) z : α)
⊢ Eq (α := α) ((f.cycleOf x : (a : α) → α) z : α) ((f.cycleOf y : (a : α) → α) z : α)

Tactic:
rw [Equiv.Perm.cycleOf_apply]

Premises used: Equiv.Perm.cycleOf_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
x y : α
inst : DecidableRel f.SameCycle
h : f.SameCycle x y
z : α
pos : ∀ (hz : f.SameCycle x z), Eq (α := α) ((f : (a : α) → α) z : α) ((f.cycleOf y : (a : α) → α) z : α)
neg : ∀ (hz : ¬f.SameCycle x z), z = (f.cycleOf y : (a : α) → α) z
⊢ Eq (α := α) (if f.SameCycle x z then (f : (a : α) → α) z else z : α) ((f.cycleOf y : (a : α) → α) z : α)

Tactic:
split_ifs with hz
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
x y : α
inst : DecidableRel f.SameCycle
h : f.SameCycle x y
z : α
hz : f.SameCycle x z
⊢ Eq (α := α) ((f : (a : α) → α) z : α) ((f.cycleOf y : (a : α) → α) z : α)

Tactic:
(h.symm.trans hz).cycleOf_apply.symm

Premises used: Equiv.Perm.SameCycle.symm, Equiv.Perm.SameCycle.trans, Equiv.Perm.SameCycle.cycleOf_apply, Eq.symm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
x y : α
inst : DecidableRel f.SameCycle
h : f.SameCycle x y
z : α
hz : f.SameCycle x z
⊢ Eq (α := α) ((f : (a : α) → α) z : α) ((f.cycleOf y : (a : α) → α) z : α)

Tactic:
exact (h.symm.trans hz).cycleOf_apply.symm

Premises used: Equiv.Perm.SameCycle.symm, Equiv.Perm.SameCycle.trans, Equiv.Perm.SameCycle.cycleOf_apply, Eq.symm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
x y : α
inst : DecidableRel f.SameCycle
h : f.SameCycle x y
z : α
hz : ¬f.SameCycle x z
⊢ z = (f.cycleOf y : (a : α) → α) z

Tactic:
(cycleOf_apply_of_not_sameCycle (mt h.trans hz)).symm

Premises used: mt, Equiv.Perm.SameCycle.trans, Equiv.Perm.cycleOf_apply_of_not_sameCycle, Eq.symm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
x y : α
inst : DecidableRel f.SameCycle
h : f.SameCycle x y
z : α
hz : ¬f.SameCycle x z
⊢ z = (f.cycleOf y : (a : α) → α) z

Tactic:
exact (cycleOf_apply_of_not_sameCycle (mt h.trans hz)).symm

Premises used: mt, Equiv.Perm.SameCycle.trans, Equiv.Perm.cycleOf_apply_of_not_sameCycle, Eq.symm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x : α
k : ℤ
rw : Eq (α := α) ((f : (a : α) → α) ((f ^ k : (a : α) → α) x : α) : α) ((f ^ (k + 1) : (a : α) → α) x : α)
rw₁ : f.SameCycle x ((f ^ k : (a : α) → α) x)
⊢ Eq (α := α) ((f.cycleOf x : (a : α) → α) ((f ^ k : (a : α) → α) x : α) : α) ((f ^ (k + 1) : (a : α) → α) x : α)

Tactic:
rw [SameCycle.cycleOf_apply]

Premises used: Equiv.Perm.SameCycle.cycleOf_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x : α
k : ℤ
rw : Eq (α := α) ((f : (a : α) → α) ((f ^ k : (a : α) → α) x : α) : α) ((f ^ (1 + k) : (a : α) → α) x : α)
rw₁ :
  Eq (α := α) ((f : (a : α) → α) ((f ^ k : (a : α) → α) x : α) : α)
    ((HPow.hPow (β := ℤ) f 1 * f ^ k : (a : α) → α) x : α)
rw₂ : Eq (α := α) ((f : (a : α) → α) ((f ^ k : (a : α) → α) x : α) : α) ((f * f ^ k : (a : α) → α) x : α)
rw₃ rw₄ :
  Eq (α := α) ((f : (a : α) → α) ((f ^ k : (a : α) → α) x : α) : α)
    ((f : (a : α) → α) ((f ^ k : (a : α) → α) x : α) : α)
⊢ Eq (α := α) ((f : (a : α) → α) ((f ^ k : (a : α) → α) x : α) : α) ((f ^ (k + 1) : (a : α) → α) x : α)

Tactic:
rw [add_comm, zpow_add, zpow_one, mul_apply]

Premises used: zpow_add, zpow_one, add_comm, Equiv.Perm.mul_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x : α
k : ℤ
⊢ f.SameCycle x ((f ^ k : (a : α) → α) x)

Tactic:
⟨k, rfl⟩

Premises used: Equiv.Perm.SameCycle, Exists.intro, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x : α
k : ℤ
⊢ f.SameCycle x ((f ^ k : (a : α) → α) x)

Tactic:
exact ⟨k, rfl⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x : α
k : ℕ
⊢ Eq (α := α) ((f.cycleOf x : (a : α) → α) ((HPow.hPow (β := ℤ) f (↑k : ℤ) : (a : α) → α) x : α) : α)
    ((f ^ HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 : (a : α) → α) x : α)

Tactic:
cycleOf_apply_apply_zpow_self f x k

Premises used: Equiv.Perm.cycleOf_apply_apply_zpow_self, Nat.cast
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x : α
k : ℕ
⊢ Eq (α := α) ((f.cycleOf x : (a : α) → α) ((f ^ k : (a : α) → α) x : α) : α) ((f ^ (k + 1) : (a : α) → α) x : α)

Tactic:
convert! cycleOf_apply_apply_zpow_self f x k using 1

Premises used: Equiv.Perm.cycleOf_apply_apply_zpow_self, Nat.cast
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x : α
⊢ Eq (α := α) ((f.cycleOf x : (a : α) → α) ((HPow.hPow (β := ℕ) f 1 : (a : α) → α) x : α) : α)
    ((f ^ HAdd.hAdd (α := ℕ) 1 1 : (a : α) → α) x : α)

Tactic:
cycleOf_apply_apply_pow_self f x 1

Premises used: Equiv.Perm.cycleOf_apply_apply_pow_self, OfNat.ofNat
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x : α
⊢ Eq (α := α) ((f.cycleOf x : (a : α) → α) ((f : (a : α) → α) x : α) : α)
    ((f : (a : α) → α) ((f : (a : α) → α) x : α) : α)

Tactic:
convert! cycleOf_apply_apply_pow_self f x 1 using 1

Premises used: Equiv.Perm.cycleOf_apply_apply_pow_self, OfNat.ofNat
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x : α
⊢ Eq (α := α) ((f.cycleOf x : (a : α) → α) x : α) ((f : (a : α) → α) x : α)

Tactic:
SameCycle.rfl.cycleOf_apply

Premises used: Equiv.Perm.SameCycle.rfl, Equiv.Perm.SameCycle.cycleOf_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
x : α
inst : DecidableRel f.SameCycle
hf : f.IsCycle
hx : (f : (a : α) → α) x ≠ x
y : α
h : f.SameCycle x y
rw rw₁ : Eq (α := α) ((f : (a : α) → α) y : α) ((f : (a : α) → α) y : α)
⊢ Eq (α := α) ((f.cycleOf x : (a : α) → α) y : α) ((f : (a : α) → α) y : α)

Tactic:
rw [h.cycleOf_apply]

Premises used: Equiv.Perm.SameCycle.cycleOf_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
x : α
inst : DecidableRel f.SameCycle
hf : f.IsCycle
hx : (f : (a : α) → α) x ≠ x
y : α
h : ¬f.SameCycle x y
rw : y = (f : (a : α) → α) y
rw₁ rw₂ : y = y
⊢ Eq (α := α) ((f.cycleOf x : (a : α) → α) y : α) ((f : (a : α) → α) y : α)

Tactic:
rw [cycleOf_apply_of_not_sameCycle h,
        Classical.not_not.1 (mt ((isCycle_iff_sameCycle hx).1 hf).2 h)]

Premises used: Iff.mpr, Classical.not_not, mt, Equiv.Perm.cycleOf_apply_of_not_sameCycle, Equiv.Perm.isCycle_iff_sameCycle, Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
x : α
f : Perm α
inst : DecidableRel f.SameCycle
simp_rw : (∀ (x_1 : α), (if f.SameCycle x x_1 then (f : (a : α) → α) x_1 else x_1) = x_1) ↔ (f : (a : α) → α) x = x
⊢ f.cycleOf x = 1 ↔ (f : (a : α) → α) x = x

Tactic:
simp_rw [Perm.ext_iff, cycleOf_apply, one_apply]

Premises used: Equiv.Perm.ext_iff, Equiv.Perm.cycleOf_apply, Equiv.Perm.one_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
x : α
f : Perm α
inst : DecidableRel f.SameCycle
⊢ (∀ (x_1 : α), (if f.SameCycle x x_1 then (f : (a : α) → α) x_1 else x_1) = x_1) ↔ (f : (a : α) → α) x = x

Tactic:
⟨fun h => (if_pos (SameCycle.refl f x)).symm.trans (h x), fun h y => ?_⟩

Premises used: if_pos, Equiv.Perm.SameCycle.refl, Iff.intro, Eq.symm, Eq.trans
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
x : α
f : Perm α
inst : DecidableRel f.SameCycle
refine : ∀ (h : (f : (a : α) → α) x = x) (y : α), (if f.SameCycle x y then (f : (a : α) → α) y else y) = y
⊢ (∀ (x_1 : α), (if f.SameCycle x x_1 then (f : (a : α) → α) x_1 else x_1) = x_1) ↔ (f : (a : α) → α) x = x

Tactic:
refine ⟨fun h => (if_pos (SameCycle.refl f x)).symm.trans (h x), fun h y => ?_⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
x : α
f : Perm α
inst : DecidableRel f.SameCycle
h : (f : (a : α) → α) x = x
y : α
pos : ∀ (hy : (f : (a : α) → α) y = y), (if f.SameCycle x y then (f : (a : α) → α) y else y) = y
neg : ∀ (hy : ¬(f : (a : α) → α) y = y), (if f.SameCycle x y then (f : (a : α) → α) y else y) = y
⊢ (if f.SameCycle x y then (f : (a : α) → α) y else y) = y

Tactic:
by_cases hy : f y = y

Premises used: DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
x : α
f : Perm α
inst : DecidableRel f.SameCycle
h : (f : (a : α) → α) x = x
y : α
hy : (f : (a : α) → α) y = y
pos : (if f.SameCycle x y then y else y) = y
pos₁ pos₂ : y = y
⊢ (if f.SameCycle x y then (f : (a : α) → α) y else y) = y

Tactic:
rw [hy, ite_self]

Premises used: ite_self
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
x : α
f : Perm α
inst : DecidableRel f.SameCycle
h : (f : (a : α) → α) x = x
y : α
hy : ¬(f : (a : α) → α) y = y
inl : (f : (a : α) → α) x = x → (f : (a : α) → α) y = y → False
inr : ¬(f : (a : α) → α) x = x → ¬(f : (a : α) → α) y = y → False
⊢ ¬((f : (a : α) → α) x = x ↔ (f : (a : α) → α) y = y)

Tactic:
tauto
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
x : α
f : Perm α
inst : DecidableRel f.SameCycle
h : (f : (a : α) → α) x = x
y : α
hy : ¬(f : (a : α) → α) y = y
⊢ (if f.SameCycle x y then (f : (a : α) → α) y else y) = y

Tactic:
exact if_neg (mt SameCycle.apply_eq_self_iff (by tauto))

Premises used: mt, Equiv.Perm.SameCycle.apply_eq_self_iff, if_neg
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x : α
⊢ f.cycleOf ((f : (a : α) → α) x) = f.cycleOf x

Tactic:
(sameCycle_apply_right.2 SameCycle.rfl).symm.cycleOf_eq

Premises used: Iff.mpr, Equiv.Perm.SameCycle.rfl, Equiv.Perm.SameCycle.symm, Equiv.Perm.sameCycle_apply_right, Equiv.Perm.SameCycle.cycleOf_eq
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
n : ℕ
x : α
⊢ f.cycleOf ((f ^ n : (a : α) → α) x) = f.cycleOf x

Tactic:
SameCycle.rfl.pow_left.cycleOf_eq

Premises used: Equiv.Perm.SameCycle.rfl, Equiv.Perm.SameCycle.cycleOf_eq, Equiv.Perm.SameCycle.pow_left
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
n : ℤ
x : α
⊢ f.cycleOf ((f ^ n : (a : α) → α) x) = f.cycleOf x

Tactic:
SameCycle.rfl.zpow_left.cycleOf_eq

Premises used: Equiv.Perm.SameCycle.rfl, Equiv.Perm.SameCycle.cycleOf_eq, Equiv.Perm.SameCycle.zpow_left
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
x : α
inst : DecidableRel f.SameCycle
inst_1 : DecidableEq α
hf : f.IsCycle
pos : ∀ (hx : (f : (a : α) → α) x = x), f.cycleOf x = if (f : (a : α) → α) x = x then 1 else f
neg : ∀ (hx : ¬(f : (a : α) → α) x = x), f.cycleOf x = if (f : (a : α) → α) x = x then 1 else f
⊢ f.cycleOf x = if (f : (a : α) → α) x = x then 1 else f

Tactic:
by_cases hx : f x = x

Premises used: DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
x : α
inst : DecidableRel f.SameCycle
inst_1 : DecidableEq α
hf : f.IsCycle
hx : (f : (a : α) → α) x = x
pos : f.cycleOf x = 1
pos₁ pos₂ pos₃ pos₄ : (f : (a : α) → α) x = x
⊢ f.cycleOf x = if (f : (a : α) → α) x = x then 1 else f

Tactic:
rwa [if_pos hx, cycleOf_eq_one_iff]

Premises used: Equiv.Perm.cycleOf_eq_one_iff, if_pos
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
f : Perm α
x : α
inst : DecidableRel f.SameCycle
inst_1 : DecidableEq α
hf : f.IsCycle
hx : ¬(f : (a : α) → α) x = x
neg : f.cycleOf x = f
neg₁ : f = f
neg₂ : (f : (a : α) → α) x ≠ x
neg₃ : f = f
neg₄ neg₅ neg₆ : (f : (a : α) → α) x ≠ x
⊢ f.cycleOf x = if (f : (a : α) → α) x = x then 1 else f

Tactic:
rwa [if_neg hx, hf.cycleOf_eq]

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

Tactic:
(cycleOf_eq_one_iff 1).mpr rfl

Premises used: Iff.mpr, Equiv.Perm.cycleOf_eq_one_iff, OfNat.ofNat, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
x : α
f : Perm α
inst : DecidableRel f.SameCycle
hx rwa rwa₁ rwa₂ rwa₃ : (f : (a : α) → α) x ≠ x
⊢ (f.cycleOf x : (a : α) → α) x ≠ x

Tactic:
rwa [SameCycle.rfl.cycleOf_apply]

Premises used: Equiv.Perm.SameCycle.rfl, Equiv.Perm.SameCycle.cycleOf_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
x : α
f : Perm α
inst : DecidableRel f.SameCycle
hx : (f : (a : α) → α) x ≠ x
this : (f.cycleOf x : (a : α) → α) x ≠ x
y : α
h : (f.cycleOf x : (a : α) → α) y ≠ y
hxy : f.SameCycle x y
i : ℤ
hi rw : (f ^ i : (a : α) → α) x = y
rw₁ rw₂ : y = y
⊢ (f.cycleOf x ^ i : (a : α) → α) x = y

Tactic:
rw [cycleOf_zpow_apply_self, hi]

Premises used: Equiv.Perm.cycleOf_zpow_apply_self
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
x : α
f : Perm α
inst : DecidableRel f.SameCycle
hx : (f : (a : α) → α) x ≠ x
this : (f.cycleOf x : (a : α) → α) x ≠ x
y : α
h : (f.cycleOf x : (a : α) → α) y ≠ y
hxy : ¬f.SameCycle x y
⊢ y ≠ y

Tactic:
rw [cycleOf_apply_of_not_sameCycle hxy] at h

Premises used: Equiv.Perm.cycleOf_apply_of_not_sameCycle
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
x : α
f : Perm α
inst : DecidableRel f.SameCycle
hx : (f : (a : α) → α) x ≠ x
this : (f.cycleOf x : (a : α) → α) x ≠ x
y : α
h : (f.cycleOf x : (a : α) → α) y ≠ y
hxy : ¬f.SameCycle x y
h₁ : y ≠ y
⊢ ¬f.SameCycle x y

Tactic:
rw [cycleOf_apply_of_not_sameCycle hxy] at h

Premises used: Equiv.Perm.cycleOf_apply_of_not_sameCycle
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
x : α
f : Perm α
inst : DecidableRel f.SameCycle
hx : (f : (a : α) → α) x ≠ x
this : (f.cycleOf x : (a : α) → α) x ≠ x
y : α
h : y ≠ y
hxy : ¬f.SameCycle x y
⊢ (f.cycleOf x).SameCycle x y

Tactic:
(h rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Factors
Goal:
α : Type u_2
x : α
f : Perm α
inst : DecidableRel f.SameCycle
hx : (f : (a : α) → α) x ≠ x
this : (f.cycleOf x : (a : α) → α) x ≠ x
y : α
h : y ≠ y
hxy : ¬f.SameCycle x y
⊢ (f.cycleOf x).SameCycle x y

Tactic:
exact (h rfl).elim

Premises used: False.elim, rfl