awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
hx' : Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
intro :
  ∀
    (this :
      ∀ {a b : ℕ} (hx' : Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)) (hab : a ≤ b),
        f ^ a = f ^ b)
    (hab : ¬a ≤ b), f ^ a = f ^ b
wlog :
  ∀ {a b : ℕ} (hx' : Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)) (hab : a ≤ b),
    f ^ a = f ^ b
⊢ f ^ a = f ^ b

Tactic:
wlog hab : a ≤ b generalizing a b
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
hx' : Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
this :
  ∀ {a b : ℕ} (hx' : Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)) (hab : a ≤ b),
    f ^ a = f ^ b
hab : ¬a ≤ b
⊢ f ^ a = f ^ b

Tactic:
(this hx'.symm (le_of_not_ge hab)).symm

Premises used: le_of_not_ge, Eq.symm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
hx' : Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
this :
  ∀ {a b : ℕ} (hx' : Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)) (hab : a ≤ b),
    f ^ a = f ^ b
hab : ¬a ≤ b
⊢ f ^ a = f ^ b

Tactic:
exact (this hx'.symm (le_of_not_ge hab)).symm

Premises used: le_of_not_ge, Eq.symm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
a b : ℕ
hx' : Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
hab : a ≤ b
this : f ^ (b - a) = 1
⊢ f ^ b = f ^ a

Tactic:
rw [pow_sub _ hab, mul_inv_eq_one] at this

Premises used: pow_sub, mul_inv_eq_one
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
a b : ℕ
hx' : Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
hab : a ≤ b
this : f ^ b = f ^ a
rw rw₁ : f ^ a = f ^ a
⊢ f ^ a = f ^ b

Tactic:
rw [this]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
a b : ℕ
hx' : Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
hab : a ≤ b
suffices : f ^ (b - a) = 1
⊢ f ^ a = f ^ b

Tactic:
suffices f ^ (b - a) = 1 by
        rw [pow_sub _ hab, mul_inv_eq_one] at this
        rw [this]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
a b : ℕ
hx' : Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
hab : a ≤ b
rw : ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ (b - a) : (a : β) → β) x = x
⊢ f ^ (b - a) = 1

Tactic:
rw [hf.pow_eq_one_iff]

Premises used: Equiv.Perm.IsCycle.pow_eq_one_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
a b : ℕ
hx' : Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
hab : a ≤ b
pos :
  ∀ (hfa : Membership.mem (α := β) f.support ((f ^ a : (a : β) → β) x : β)),
    ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ (b - a) : (a : β) → β) x = x
neg :
  ∀ (hfa : ((f ^ a : (a : β) → β) x : β) ∉ f.support),
    ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ (b - a) : (a : β) → β) x = x
⊢ ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ (b - a) : (a : β) → β) x = x

Tactic:
by_cases hfa : (f ^ a) x ∈ f.support

Premises used: Equiv.Perm.support, HPow.hPow, DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
a b : ℕ
hx' : Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
hab : a ≤ b
hfa : Membership.mem (α := β) f.support ((f ^ a : (a : β) → β) x : β)
⊢ ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ (b - a) : (a : β) → β) x = x

Tactic:
⟨(f ^ a) x, mem_support.mp hfa, ?_⟩

Premises used: Equiv.Perm.mem_support, HPow.hPow, And.intro, Exists.intro, Iff.mp, DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
a b : ℕ
hx' : Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
hab : a ≤ b
hfa : Membership.mem (α := β) f.support ((f ^ a : (a : β) → β) x : β)
pos : Eq (α := β) ((f ^ (b - a) : (a : β) → β) ((f ^ a : (a : β) → β) x : β) : β) ((f ^ a : (a : β) → β) x : β)
⊢ ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ (b - a) : (a : β) → β) x = x

Tactic:
refine ⟨(f ^ a) x, mem_support.mp hfa, ?_⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
a b : ℕ
hx' : Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
hab : a ≤ b
hfa : Membership.mem (α := β) f.support ((f ^ a : (a : β) → β) x : β)
⊢ Eq (α := β) ((f ^ (b - a) : (a : β) → β) ((f ^ a : (a : β) → β) x : β) : β) ((f ^ a : (a : β) → β) x : β)

Tactic:
simp [pow_sub _ hab, ← hx']

Premises used: pow_sub
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
a b : ℕ
hx' : Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
hab : a ≤ b
hfa : ((f ^ a : (a : β) → β) x : β) ∉ f.support
⊢ Eq (α := β) ((HPow.hPow (β := ℤ) f 1 : (a : β) → β) ((HPow.hPow (β := ℤ) f (↑a : ℤ) : (a : β) → β) x : β) : β)
    ((HPow.hPow (β := ℤ) f (↑a : ℤ) : (a : β) → β) ((HPow.hPow (β := ℤ) f 1 : (a : β) → β) x : β) : β)

Tactic:
have h := @Equiv.Perm.zpow_apply_comm _ f 1 a x
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
a b : ℕ
hx' : Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
hab : a ≤ b
hfa : ((f ^ a : (a : β) → β) x : β) ∉ f.support
h :
  Eq (α := β) ((HPow.hPow (β := ℤ) f 1 : (a : β) → β) ((HPow.hPow (β := ℤ) f (↑a : ℤ) : (a : β) → β) x : β) : β)
    ((HPow.hPow (β := ℤ) f (↑a : ℤ) : (a : β) → β) ((HPow.hPow (β := ℤ) f 1 : (a : β) → β) x : β) : β)
⊢ Eq (α := β) ((f : (a : β) → β) ((f ^ a : (a : β) → β) x : β) : β)
    ((f ^ a : (a : β) → β) ((f : (a : β) → β) x : β) : β)

Tactic:
simp only [zpow_one, zpow_natCast] at h

Premises used: zpow_natCast, zpow_one
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
a b : ℕ
hx' : Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
hab : a ≤ b
hfa : ((f ^ a : (a : β) → β) x : β) ∉ f.support
h :
  Eq (α := β) ((f : (a : β) → β) ((f ^ a : (a : β) → β) x : β) : β)
    ((f ^ a : (a : β) → β) ((f : (a : β) → β) x : β) : β)
⊢ (f : (a : β) → β) x = x

Tactic:
rw [notMem_support, h, Function.Injective.eq_iff (f ^ a).injective] at hfa

Premises used: Equiv.Perm.notMem_support, Function.Injective.eq_iff, HPow.hPow, Equiv.injective
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
a b : ℕ
hx' : Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
hab : a ≤ b
hfa : ((f ^ a : (a : β) → β) x : β) ∉ f.support
h :
  Eq (α := β) ((f : (a : β) → β) ((f ^ a : (a : β) → β) x : β) : β)
    ((f ^ a : (a : β) → β) ((f : (a : β) → β) x : β) : β)
hfa₁ : (f : (a : β) → β) x = x
⊢ Eq (α := β) ((f : (a : β) → β) ((f ^ a : (a : β) → β) x : β) : β)
    ((f ^ a : (a : β) → β) ((f : (a : β) → β) x : β) : β)

Tactic:
rw [notMem_support, h, Function.Injective.eq_iff (f ^ a).injective] at hfa

Premises used: Equiv.Perm.notMem_support, Function.Injective.eq_iff, HPow.hPow, Equiv.injective
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
a b : ℕ
hx' : Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
hab : a ≤ b
hfa : (f : (a : β) → β) x = x
h :
  Eq (α := β) ((f : (a : β) → β) ((f ^ a : (a : β) → β) x : β) : β)
    ((f ^ a : (a : β) → β) ((f : (a : β) → β) x : β) : β)
⊢ ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ (b - a) : (a : β) → β) x = x

Tactic:
contradiction
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
intro :
  ∀ (val : Fintype β),
    f ^ a = f ^ b ↔
      ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
intro₁ :
  ∀ (val : Fintype β),
    f ^ a = f ^ b →
      ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
intro₂ intro₃ :
  ∀ (val : Fintype β),
    (∃ (x : β), (f : (a : β) → β) x ≠ x ∧ Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)) →
      f ^ a = f ^ b
⊢ f ^ a = f ^ b ↔
    ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)

Tactic:
classical
    cases nonempty_fintype β
    constructor
    · intro h
      obtain ⟨x, hx, -⟩ := id hf
      exact ⟨x, hx, by simp [h]⟩
    · rintro ⟨x, hx, hx'⟩
      wlog hab : a ≤ b generalizing a b
      · exact (this hx'.symm (le_of_not_ge hab)).symm
      suffices f ^ (b - a) = 1 by
        rw [pow_sub _ hab, mul_inv_eq_one] at this
        rw [this]
      rw [hf.pow_eq_one_iff]
      by_cases hfa : (f ^ a) x ∈ f.support
      · refine ⟨(f ^ a) x, mem_support.mp hfa, ?_⟩
        simp [pow_sub _ hab, ← hx']
      · have h := @Equiv.Perm.zpow_apply_comm _ f 1 a x
        simp only [zpow_one, zpow_natCast] at h
        rw [notMem_support, h, Function.Injective.eq_iff (f ^ a).injective] at hfa
        contradiction

Premises used: zpow_natCast, Equiv.Perm.notMem_support, Function.Injective.eq_iff, Equiv.Perm.IsCycle.pow_eq_one_iff, zpow_one, id, nonempty_fintype, HPow.hPow, Equiv.injective
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
intro : ∀ (val : Fintype β), (f ^ n).IsCycle
⊢ (f ^ n).IsCycle

Tactic:
cases nonempty_fintype β

Premises used: nonempty_fintype
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val : Fintype β
⊢ n.Coprime (orderOf f)

Tactic:
Nat.Coprime.symm ?_

Premises used: Nat.Coprime.symm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val : Fintype β
refine : (orderOf f).Coprime n
⊢ n.Coprime (orderOf f)

Tactic:
refine Nat.Coprime.symm ?_

Premises used: Nat.Coprime.symm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val : Fintype β
rw : ¬orderOf f ∣ n
⊢ (orderOf f).Coprime n

Tactic:
rw [Nat.Prime.coprime_iff_not_dvd hf']

Premises used: Nat.Prime.coprime_iff_not_dvd
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val : Fintype β
⊢ ¬orderOf f ∣ n

Tactic:
Nat.not_dvd_of_pos_of_lt hn hn'

Premises used: Nat.not_dvd_of_pos_of_lt
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val : Fintype β
⊢ ¬orderOf f ∣ n

Tactic:
exact Nat.not_dvd_of_pos_of_lt hn hn'

Premises used: Nat.not_dvd_of_pos_of_lt
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val : Fintype β
⊢ n.Coprime (orderOf f)

Tactic:
have : n.Coprime (orderOf f) := by
      refine Nat.Coprime.symm ?_
      rw [Nat.Prime.coprime_iff_not_dvd hf']
      exact Nat.not_dvd_of_pos_of_lt hn hn'
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val : Fintype β
this : n.Coprime (orderOf f)
⊢ (f ^ n).IsCycle

Tactic:
(pow_iff hf).mpr this

Premises used: Iff.mpr, Equiv.Perm.IsCycle.pow_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val : Fintype β
this : n.Coprime (orderOf f)
⊢ (f ^ n).IsCycle

Tactic:
exact (pow_iff hf).mpr this

Premises used: Iff.mpr, Equiv.Perm.IsCycle.pow_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
intro : ∀ (val : Fintype β), (f ^ n).IsCycle
intro₁ : ∀ (val : Fintype β) (this : n.Coprime (orderOf f)), (f ^ n).IsCycle
⊢ (f ^ n).IsCycle

Tactic:
classical
    cases nonempty_fintype β
    have : n.Coprime (orderOf f) := by
      refine Nat.Coprime.symm ?_
      rw [Nat.Prime.coprime_iff_not_dvd hf']
      exact Nat.not_dvd_of_pos_of_lt hn hn'
    exact (pow_iff hf).mpr this

Premises used: nonempty_fintype
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
n : ℤ
h : (Equiv.addLeft 1 : (a : ℤ) → ℤ) n ≠ n
⊢ (HPow.hPow (α := Perm ℤ) (Equiv.addLeft 1) n : (a : ℤ) → ℤ) 0 = n

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
n : ℤ
h : (Equiv.addRight 1 : (a : ℤ) → ℤ) n ≠ n
⊢ (HPow.hPow (α := Perm ℤ) (Equiv.addRight 1) n : (a : ℤ) → ℤ) 0 = n

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
hσ : σ.IsCycle
hτ : τ.IsCycle
h : #σ.support = #τ.support
rw : #σ.support = orderOf τ
rw₁ : #τ.support = orderOf τ
rw₂ rw₃ : #τ.support = #τ.support
⊢ orderOf σ = orderOf τ

Tactic:
rw [hσ.orderOf, h, hτ.orderOf]

Premises used: Equiv.Perm.IsCycle.orderOf
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
hσ : σ.IsCycle
hτ : τ.IsCycle
h : #σ.support = #τ.support
by :
  ∀ (x : α) (hx : x ∈ (↑σ.support : Set α)),
    Eq (α := α)
      ((↑((Equiv.trans (Equiv.symm hσ.zpowersEquivSupport)
                  (Equiv.trans (zpowersEquivZPowers ⋯) hτ.zpowersEquivSupport) :
                (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
              (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) ((σ : (a : α) → α) x) ⋯)) :
          α) :
        α)
      ((τ : (a : α) → α)
          (↑((Equiv.trans (Equiv.symm hσ.zpowersEquivSupport)
                    (Equiv.trans (zpowersEquivZPowers ⋯) hτ.zpowersEquivSupport) :
                  (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
                (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) x hx)) :
            α) :
        α)
⊢ IsConj σ τ

Tactic:
refine
    isConj_of_support_equiv
      (hσ.zpowersEquivSupport.symm.trans <|
        (zpowersEquivZPowers <| by rw [hσ.orderOf, h, hτ.orderOf]).trans hτ.zpowersEquivSupport)
      ?_

Premises used: Equiv.trans, zpowersEquivZPowers, Equiv.Perm.IsCycle.zpowersEquivSupport, Equiv.Perm.isConj_of_support_equiv, Equiv.symm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
hσ : σ.IsCycle
hτ : τ.IsCycle
h : #σ.support = #τ.support
x : α
hx : x ∈ (↑σ.support : Set α)
simp :
  Eq (α := α)
    ((↑((hτ.zpowersEquivSupport : (a : ↥(Subgroup.zpowers τ)) → { x : α // x ∈ (↑τ.support : Set α) })
            (((zpowersEquivZPowers ⋯ : ↥(Subgroup.zpowers σ) ≃ ↥(Subgroup.zpowers τ)) :
                (a : ↥(Subgroup.zpowers σ)) → ↥(Subgroup.zpowers τ))
              ((Equiv.symm hσ.zpowersEquivSupport : (a : { x : α // x ∈ (↑σ.support : Set α) }) → ↥(Subgroup.zpowers σ))
                (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) ((σ : (a : α) → α) x) ⋯)))) :
        α) :
      α)
    ((τ : (a : α) → α)
        (↑((hτ.zpowersEquivSupport : (a : ↥(Subgroup.zpowers τ)) → { x : α // x ∈ (↑τ.support : Set α) })
              (((zpowersEquivZPowers ⋯ : ↥(Subgroup.zpowers σ) ≃ ↥(Subgroup.zpowers τ)) :
                  (a : ↥(Subgroup.zpowers σ)) → ↥(Subgroup.zpowers τ))
                ((Equiv.symm hσ.zpowersEquivSupport :
                    (a : { x : α // x ∈ (↑σ.support : Set α) }) → ↥(Subgroup.zpowers σ))
                  (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) x hx)))) :
          α) :
      α)
⊢ Eq (α := α)
    ((↑((Equiv.trans (Equiv.symm hσ.zpowersEquivSupport) (Equiv.trans (zpowersEquivZPowers ⋯) hτ.zpowersEquivSupport) :
              (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
            (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) ((σ : (a : α) → α) x) ⋯)) :
        α) :
      α)
    ((τ : (a : α) → α)
        (↑((Equiv.trans (Equiv.symm hσ.zpowersEquivSupport)
                  (Equiv.trans (zpowersEquivZPowers ⋯) hτ.zpowersEquivSupport) :
                (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
              (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) x hx)) :
          α) :
      α)

Tactic:
simp only [Equiv.trans_apply]

Premises used: Equiv.trans_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
hσ : σ.IsCycle
hτ : τ.IsCycle
h : #σ.support = #τ.support
n : ℕ
hx :
  Membership.mem (α := α) (↑σ.support : Set α)
    ((σ ^ n : (a : α) → α)
        (Classical.choose (p := fun (x : α) ↦
          (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) :
      α)
⊢ Eq (α := α)
    ((↑((hτ.zpowersEquivSupport : (a : ↥(Subgroup.zpowers τ)) → { x : α // x ∈ (↑τ.support : Set α) })
            (((zpowersEquivZPowers ⋯ : ↥(Subgroup.zpowers σ) ≃ ↥(Subgroup.zpowers τ)) :
                (a : ↥(Subgroup.zpowers σ)) → ↥(Subgroup.zpowers τ))
              ((Equiv.symm hσ.zpowersEquivSupport : (a : { x : α // x ∈ (↑σ.support : Set α) }) → ↥(Subgroup.zpowers σ))
                (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α))
                  ((σ : (a : α) → α)
                    ((σ ^ n : (a : α) → α)
                        (Classical.choose (p := fun (x : α) ↦
                          (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) :
                      α))
                  ⋯)))) :
        α) :
      α)
    ((τ : (a : α) → α)
        (↑((hτ.zpowersEquivSupport : (a : ↥(Subgroup.zpowers τ)) → { x : α // x ∈ (↑τ.support : Set α) })
              (((zpowersEquivZPowers ⋯ : ↥(Subgroup.zpowers σ) ≃ ↥(Subgroup.zpowers τ)) :
                  (a : ↥(Subgroup.zpowers σ)) → ↥(Subgroup.zpowers τ))
                ((Equiv.symm hσ.zpowersEquivSupport :
                    (a : { x : α // x ∈ (↑σ.support : Set α) }) → ↥(Subgroup.zpowers σ))
                  (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α))
                    ((σ ^ n : (a : α) → α)
                      (Classical.choose (p := fun (x : α) ↦
                        (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ))
                    hx)))) :
          α) :
      α)

Tactic:
simp [← Perm.mul_apply, ← pow_succ']

Premises used: Equiv.Perm.mul_apply, pow_succ'
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
hσ : σ.IsCycle
hτ : τ.IsCycle
h : IsConj σ τ
obtain : ∀ (π : Perm α) (hτ : (π * σ * π⁻¹).IsCycle) (h : IsConj σ (π * σ * π⁻¹)), #σ.support = #(π * σ * π⁻¹).support
⊢ #σ.support = #τ.support

Tactic:
obtain ⟨π, rfl⟩ := (_root_.isConj_iff).1 h

Premises used: isConj_iff, Iff.mp, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
π : Perm α
hτ : (π * σ * π⁻¹).IsCycle
h : IsConj σ (π * σ * π⁻¹)
⊢ #σ.support = #(π * σ * π⁻¹).support

Tactic:
card_support_conj.symm

Premises used: Equiv.Perm.card_support_conj, Eq.symm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
π : Perm α
hτ : (π * σ * π⁻¹).IsCycle
h : IsConj σ (π * σ * π⁻¹)
⊢ #σ.support = #(π * σ * π⁻¹).support

Tactic:
exact card_support_conj.symm

Premises used: Equiv.Perm.card_support_conj, Eq.symm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
⊢ f.IsCycleOn ∅

Tactic:
simp [IsCycleOn]

Premises used: Equiv.Perm.IsCycleOn
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
s : Set α
⊢ IsCycleOn 1 s ↔ s.Subsingleton

Tactic:
simp [IsCycleOn, Set.bijOn_id, Set.Subsingleton]

Premises used: Set.Subsingleton, Set.bijOn_id, Equiv.Perm.IsCycleOn
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
a : α
⊢ f.IsCycleOn {a} ↔ (f : (a : α) → α) a = a

Tactic:
simp [IsCycleOn, SameCycle.rfl]

Premises used: Equiv.Perm.SameCycle.rfl, Equiv.Perm.IsCycleOn
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Subsingleton α
f : Perm α
s : Set α
⊢ f.IsCycleOn s

Tactic:
⟨s.bijOn_of_subsingleton _, fun x _ y _ => (Subsingleton.elim x y).sameCycle _⟩

Premises used: Eq.sameCycle, Set.bijOn_of_subsingleton, And.intro, Subsingleton.elim, Equiv.Perm.IsCycleOn
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Set α
simp :
  (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → f.SameCycle x y) →
    (Set.BijOn (⇑f⁻¹ : (a : α) → α) s s ↔ Set.BijOn (⇑f : (a : α) → α) s s)
⊢ f⁻¹.IsCycleOn s ↔ f.IsCycleOn s

Tactic:
simp only [IsCycleOn, sameCycle_inv, and_congr_left_iff]

Premises used: Equiv.Perm.sameCycle_inv, and_congr_left_iff, Equiv.Perm.IsCycleOn
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Set α
⊢ (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → f.SameCycle x y) →
    (Set.BijOn (⇑f⁻¹ : (a : α) → α) s s ↔ Set.BijOn (⇑f : (a : α) → α) s s)

Tactic:
fun _ ↦ ⟨fun h ↦ Set.BijOn.perm_inv h, fun h ↦ Set.BijOn.perm_inv h⟩

Premises used: Set.BijOn.perm_inv, Iff.intro
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
s : Set α
⊢ (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → f.SameCycle x y) →
    (Set.BijOn (⇑f⁻¹ : (a : α) → α) s s ↔ Set.BijOn (⇑f : (a : α) → α) s s)

Tactic:
exact fun _ ↦ ⟨fun h ↦ Set.BijOn.perm_inv h, fun h ↦ Set.BijOn.perm_inv h⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f g : Perm α
s : Set α
h : f.IsCycleOn s
x : α
hx : Membership.mem (γ := Set α) ((⇑g : (a : α) → α) '' s) x
y : α
hy : Membership.mem (γ := Set α) ((⇑g : (a : α) → α) '' s) y
rw :
  ∀ (hx : Membership.mem (γ := Set α) ((⇑(Equiv.symm g) : (a : α) → α) ⁻¹' s) x) (y : α)
    (hy : Membership.mem (γ := Set α) ((⇑(Equiv.symm g) : (a : α) → α) ⁻¹' s) y), (g * f * g⁻¹).SameCycle x y
⊢ (g * f * g⁻¹).SameCycle x y

Tactic:
rw [Equiv.image_eq_preimage_symm] at hx hy

Premises used: Equiv.image_eq_preimage_symm
-- 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
⊢ (g * f * g⁻¹).SameCycle ((g : (a : α) → α) ((Equiv.symm g : (a : α) → α) x : α))
    ((g : (a : α) → α) ((Equiv.symm g : (a : α) → α) y : α))

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

Premises used: And.right, Equiv.Perm.SameCycle.conj