awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.ConjAct
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Finite α
g : Perm α
s : Finset α
this : Fintype α
k : Perm α
h :
  (↑(HSMul.hSMul (α := ConjAct (Perm α))
              (((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) g)⁻¹ : ConjAct (Perm α)) k).support :
        Set α) ⊆
      {x : α | x ∈ s} ↔
    (↑k.support : Set α) ⊆ {x : α | x ∈ g • s}
⊢ k ∈
      HSMul.hSMul (α := ConjAct (Perm α)) (β := Subgroup (Perm α))
        ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) g : ConjAct (Perm α))
        (MonoidHom.range (G := Perm ↥s) (ofSubtype (p := fun (x : α) ↦ x ∈ s))) ↔
    Membership.mem (γ := Subgroup (Perm α))
      (MonoidHom.range (G := Perm ↥(g • s)) (ofSubtype (p := fun (x : α) ↦ x ∈ g • s))) k

Tactic:
simp_rw [Subgroup.mem_pointwise_smul_iff_inv_smul_mem, mem_range_ofSubtype_iff]

Premises used: Equiv.Perm.mem_range_ofSubtype_iff, Subgroup.mem_pointwise_smul_iff_inv_smul_mem
-- Module: Mathlib.GroupTheory.Perm.ConjAct
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Finite α
g : Perm α
s : Finset α
this : Fintype α
k : Perm α
⊢ (↑(HSMul.hSMul (α := ConjAct (Perm α))
              (((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) g)⁻¹ : ConjAct (Perm α)) k).support :
        Set α) ⊆
      {x : α | x ∈ s} ↔
    (↑k.support : Set α) ⊆ {x : α | x ∈ g • s}

Tactic:
simp [support_conj_eq_smul_support, Set.subset_smul_set_iff]

Premises used: Set.subset_smul_set_iff, Equiv.Perm.support_conj_eq_smul_support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x : α
⊢ f.SameCycle x x

Tactic:
⟨0, rfl⟩

Premises used: Equiv.Perm.SameCycle, Exists.intro, OfNat.ofNat, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x : α
⊢ f.SameCycle x x

Tactic:
SameCycle.refl _ _

Premises used: Equiv.Perm.SameCycle.refl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
x y : α
h : x = y
f : Perm α
rw rw₁ : f.SameCycle y y
⊢ f.SameCycle x y

Tactic:
rw [h]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x y : α
h : f.SameCycle x y
i : ℤ
hi : (f ^ i : (a : α) → α) x = y
⊢ (f ^ (-i) : (a : α) → α) y = x

Tactic:
simp [zpow_neg, ← hi]

Premises used: zpow_neg
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x y : α
⊢ f.SameCycle x y ↔ f.SameCycle y x

Tactic:
⟨SameCycle.symm, SameCycle.symm⟩

Premises used: Equiv.Perm.SameCycle.symm, Iff.intro
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x y z : α
h : f.SameCycle x y
h_1 : f.SameCycle y z
i : ℤ
hi : (f ^ i : (a : α) → α) x = y
j : ℤ
hj : (f ^ j : (a : α) → α) y = z
rw : (f ^ j * f ^ i : (a : α) → α) x = z
rw₁ : (f ^ j : (a : α) → α) ((f ^ i : (a : α) → α) x : α) = z
rw₂ : (f ^ j : (a : α) → α) y = z
rw₃ rw₄ : z = z
⊢ (f ^ (j + i) : (a : α) → α) x = z

Tactic:
rw [zpow_add, mul_apply, hi, hj]

Premises used: zpow_add, Equiv.Perm.mul_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
⊢ Equivalence f.SameCycle

Tactic:
⟨SameCycle.refl f, SameCycle.symm, SameCycle.trans⟩

Premises used: Equiv.Perm.SameCycle.symm, Equiv.Perm.SameCycle.trans, Equiv.Perm.SameCycle.refl, Equivalence.mk
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
x y : α
⊢ SameCycle 1 x y ↔ x = y

Tactic:
simp [SameCycle]

Premises used: Equiv.Perm.SameCycle
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x y : α
⊢ (∃ (b : ℤ), (HPow.hPow (β := ℤ) f⁻¹ ((Equiv.symm (Equiv.neg ℤ) : (a : ℤ) → ℤ) b : ℤ) : (a : α) → α) x = y) ↔
    f.SameCycle x y

Tactic:
simp [SameCycle]

Premises used: Equiv.Perm.SameCycle
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f g : Perm α
x y : α
i : ℤ
⊢ ((g * f * g⁻¹) ^ i : (a : α) → α) x = y ↔
    Eq (α := α) ((f ^ i : (a : α) → α) ((g⁻¹ : (a : α) → α) x : α) : α) ((g⁻¹ : (a : α) → α) y : α)

Tactic:
simp [conj_zpow, eq_symm_apply]

Premises used: conj_zpow, Equiv.eq_symm_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f g : Perm α
x y : α
⊢ f.SameCycle x y → (g * f * g⁻¹).SameCycle ((g : (a : α) → α) x) ((g : (a : α) → α) y)

Tactic:
simp [sameCycle_conj]

Premises used: Equiv.Perm.sameCycle_conj
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x y : α
h : f.SameCycle x y
i : ℤ
hi : (f ^ i : (a : α) → α) x = y
rw :
  (f : (a : α) → α) x = x ↔
    Eq (α := α) ((f : (a : α) → α) ((f ^ i : (a : α) → α) x : α) : α) ((f ^ i : (a : α) → α) x : α)
rw₁ : (f : (a : α) → α) x = x ↔ Eq (α := α) ((f * f ^ i : (a : α) → α) x : α) ((f ^ i : (a : α) → α) x : α)
rw₂ : (f : (a : α) → α) x = x ↔ Eq (α := α) ((f ^ (1 + i) : (a : α) → α) x : α) ((f ^ i : (a : α) → α) x : α)
rw₃ : (f : (a : α) → α) x = x ↔ Eq (α := α) ((f ^ (i + 1) : (a : α) → α) x : α) ((f ^ i : (a : α) → α) x : α)
rw₄ : (f : (a : α) → α) x = x ↔ Eq (α := α) ((f ^ i * f : (a : α) → α) x : α) ((f ^ i : (a : α) → α) x : α)
rw₅ :
  (f : (a : α) → α) x = x ↔
    Eq (α := α) ((f ^ i : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f ^ i : (a : α) → α) x : α)
rw₆ rw₇ : (f : (a : α) → α) x = x ↔ (f : (a : α) → α) x = x
⊢ (f : (a : α) → α) x = x ↔ (f : (a : α) → α) y = y

Tactic:
rw [← hi, ← mul_apply, ← zpow_one_add, add_comm, zpow_add_one, mul_apply,
    (f ^ i).injective.eq_iff]

Premises used: Function.Injective.eq_iff, zpow_add_one, zpow_one_add, add_comm, HPow.hPow, Equiv.Perm.mul_apply, Equiv.injective
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x y : α
h : f.SameCycle x y
hx : IsFixedPt (⇑f : (a : α) → α) x
⊢ x = y

Tactic:
let ⟨_, hn⟩ := h
  (hx.perm_zpow _).eq.symm.trans hn

Premises used: Function.IsFixedPt.perm_zpow, _private.0.Equiv.Perm.SameCycle.symm.match_1, Function.IsFixedPt.eq, Eq.symm, Eq, Eq.trans
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x y : α
h : f.SameCycle x y
hy : IsFixedPt (⇑f : (a : α) → α) y
⊢ x = y

Tactic:
h.eq_of_left <| h.apply_eq_self_iff.2 hy

Premises used: Iff.mpr, Equiv.Perm.SameCycle.apply_eq_self_iff, Equiv.Perm.SameCycle.eq_of_left
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x y : α
⊢ (∃ (b : ℤ),
      (HPow.hPow (β := ℤ) f ((Equiv.symm (Equiv.addRight 1) : (a : ℤ) → ℤ) b : ℤ) : (a : α) → α)
          ((f : (a : α) → α) x : α) =
        y) ↔
    f.SameCycle x y

Tactic:
simp [zpow_sub, SameCycle, Int.add_neg_one, Function.comp]

Premises used: Int.add_neg_one, Function.comp, Equiv.Perm.SameCycle, zpow_sub
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x y : α
rw : f.SameCycle ((f : (a : α) → α) y) x ↔ f.SameCycle x y
rw₁ : f.SameCycle y x ↔ f.SameCycle x y
rw₂ rw₃ : f.SameCycle x y ↔ f.SameCycle x y
⊢ f.SameCycle x ((f : (a : α) → α) y) ↔ f.SameCycle x y

Tactic:
rw [sameCycle_comm, sameCycle_apply_left, sameCycle_comm]

Premises used: Equiv.Perm.sameCycle_comm, Equiv.Perm.sameCycle_apply_left
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x y : α
rw : f.SameCycle ((f : (a : α) → α) ((Equiv.symm f : (a : α) → α) x : α)) y ↔ f.SameCycle x y
rw₁ rw₂ : f.SameCycle x y ↔ f.SameCycle x y
⊢ f.SameCycle ((Equiv.symm f : (a : α) → α) x) y ↔ f.SameCycle x y

Tactic:
rw [← sameCycle_apply_left, apply_symm_apply]

Premises used: Equiv.apply_symm_apply, Equiv.Perm.sameCycle_apply_left
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x y : α
rw : f.SameCycle x ((f : (a : α) → α) ((Equiv.symm f : (a : α) → α) y : α)) ↔ f.SameCycle x y
rw₁ rw₂ : f.SameCycle x y ↔ f.SameCycle x y
⊢ f.SameCycle x ((Equiv.symm f : (a : α) → α) y) ↔ f.SameCycle x y

Tactic:
rw [← sameCycle_apply_right, apply_symm_apply]

Premises used: Equiv.apply_symm_apply, Equiv.Perm.sameCycle_apply_right
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x y : α
n : ℤ
⊢ (∃ (b : ℤ),
      (HPow.hPow (β := ℤ) f ((Equiv.symm (Equiv.addRight n) : (a : ℤ) → ℤ) b : ℤ) : (a : α) → α)
          ((f ^ n : (a : α) → α) x : α) =
        y) ↔
    f.SameCycle x y

Tactic:
simp [SameCycle, zpow_add]

Premises used: zpow_add, Equiv.Perm.SameCycle
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x y : α
n : ℤ
rw : f.SameCycle ((f ^ n : (a : α) → α) y) x ↔ f.SameCycle x y
rw₁ : f.SameCycle y x ↔ f.SameCycle x y
rw₂ rw₃ : f.SameCycle x y ↔ f.SameCycle x y
⊢ f.SameCycle x ((f ^ n : (a : α) → α) y) ↔ f.SameCycle x y

Tactic:
rw [sameCycle_comm, sameCycle_zpow_left, sameCycle_comm]

Premises used: Equiv.Perm.sameCycle_comm, Equiv.Perm.sameCycle_zpow_left
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x y : α
n : ℕ
rw : f.SameCycle ((HPow.hPow (β := ℤ) f (↑n : ℤ) : (a : α) → α) x) y ↔ f.SameCycle x y
rw₁ rw₂ : f.SameCycle x y ↔ f.SameCycle x y
⊢ f.SameCycle ((f ^ n : (a : α) → α) x) y ↔ f.SameCycle x y

Tactic:
rw [← zpow_natCast, sameCycle_zpow_left]

Premises used: zpow_natCast, Equiv.Perm.sameCycle_zpow_left
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x y : α
n : ℕ
rw : f.SameCycle x ((HPow.hPow (β := ℤ) f (↑n : ℤ) : (a : α) → α) y) ↔ f.SameCycle x y
rw₁ rw₂ : f.SameCycle x y ↔ f.SameCycle x y
⊢ f.SameCycle x ((f ^ n : (a : α) → α) y) ↔ f.SameCycle x y

Tactic:
rw [← zpow_natCast, sameCycle_zpow_right]

Premises used: zpow_natCast, Equiv.Perm.sameCycle_zpow_right
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x y : α
n : ℕ
h_1 : (f ^ n).SameCycle x y
m : ℤ
h : ((f ^ n) ^ m : (a : α) → α) x = y
⊢ (f ^ ((↑n : ℤ) * m) : (a : α) → α) x = y

Tactic:
simp [zpow_mul, h]

Premises used: zpow_mul
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x y : α
n : ℤ
h_1 : (f ^ n).SameCycle x y
m : ℤ
h : ((f ^ n) ^ m : (a : α) → α) x = y
⊢ (f ^ (n * m) : (a : α) → α) x = y

Tactic:
simp [zpow_mul, h]

Premises used: zpow_mul
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
p : α → Prop
h : ∀ (x : α), p ((f : (a : α) → α) x) ↔ p x
x y : { x : α // p x }
n : ℤ
⊢ (f.subtypePerm (p := p) h ^ n : (a : { x : α // p x }) → { x : α // p x }) x = y ↔
    (f ^ n : (a : α) → α) (↑x : α) = (↑y : α)

Tactic:
simp [Subtype.ext_iff]

Premises used: Subtype.ext_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
β : Type u_3
g : Perm α
x y : α
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_2 + 1, max 1 (u_3 + 1)} α (Subtype p)
n : ℤ
rw :
  Eq (α := β) (((g ^ n).extendDomain (p := p) f : (a : β) → β) (↑((f : (a : α) → Subtype p) x) : β) : β)
      ((↑((f : (a : α) → Subtype p) y) : β) : β) ↔
    (g ^ n : (a : α) → α) x = y
rw₁ :
  Eq.{u_3 + 1} (α := β) (↑((f : (a : α) → Subtype p) ((g ^ n : (a : α) → α) x)) : β)
      (↑((f : (a : α) → Subtype p) y) : β) ↔
    (g ^ n : (a : α) → α) x = y
rw₂ :
  Eq.{max 1 (u_3 + 1)} (α := Subtype p) ((f : (a : α) → Subtype p) ((g ^ n : (a : α) → α) x) : Subtype p)
      ((f : (a : α) → Subtype p) y : Subtype p) ↔
    (g ^ n : (a : α) → α) x = y
rw₃ rw₄ : (g ^ n : (a : α) → α) x = y ↔ (g ^ n : (a : α) → α) x = y
⊢ Eq (α := β) ((g.extendDomain (p := p) f ^ n : (a : β) → β) (↑((f : (a : α) → Subtype p) x) : β) : β)
      ((↑((f : (a : α) → Subtype p) y) : β) : β) ↔
    (g ^ n : (a : α) → α) x = y

Tactic:
rw [← extendDomain_zpow, extendDomain_apply_image, Subtype.coe_inj, f.injective.eq_iff]

Premises used: Function.Injective.eq_iff, Subtype.coe_inj, Equiv.Perm.extendDomain_apply_image, Equiv.injective, Equiv.Perm.extendDomain_zpow
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x : α
inst : Finite α
k : ℤ
h :
  (k % (↑(orderOf f) : ℤ)).natAbs < orderOf f ∧
    Eq (α := α) ((f ^ (k % (↑(orderOf f) : ℤ)).natAbs : (a : α) → α) x : α) ((f ^ k : (a : α) → α) x : α)
⊢ ∃ i < orderOf f, Eq (α := α) ((f ^ i : (a : α) → α) x : α) ((f ^ k : (a : α) → α) x : α)

Tactic:
use (k % orderOf f).natAbs

Premises used: Nat.cast, orderOf, HMod.hMod, Int.natAbs
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x : α
inst : Finite α
k : ℤ
⊢ LT.lt (α := ℤ) 0 (↑(orderOf f) : ℤ)

Tactic:
have h₀ := Int.natCast_pos.mpr (orderOf_pos f)
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x : α
inst : Finite α
k : ℤ
h₀ : LT.lt (α := ℤ) 0 (↑(orderOf f) : ℤ)
⊢ 0 ≤ k % (↑(orderOf f) : ℤ)

Tactic:
have h₁ := Int.emod_nonneg k h₀.ne'
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x : α
inst : Finite α
k : ℤ
h₀ : LT.lt (α := ℤ) 0 (↑(orderOf f) : ℤ)
h₁ : 0 ≤ k % (↑(orderOf f) : ℤ)
h :
  (k % (↑(orderOf f) : ℤ)).natAbs < orderOf f ∧ Eq (α := α) ((f ^ k : (a : α) → α) x : α) ((f ^ k : (a : α) → α) x : α)
⊢ (k % (↑(orderOf f) : ℤ)).natAbs < orderOf f ∧
    Eq (α := α) ((f ^ (k % (↑(orderOf f) : ℤ)).natAbs : (a : α) → α) x : α) ((f ^ k : (a : α) → α) x : α)

Tactic:
rw [← zpow_natCast, Int.natAbs_of_nonneg h₁, zpow_mod_orderOf]

Premises used: zpow_natCast, zpow_mod_orderOf, Int.natAbs_of_nonneg
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x : α
inst : Finite α
k : ℤ
h₀ : LT.lt (α := ℤ) 0 (↑(orderOf f) : ℤ)
h₁ : 0 ≤ k % (↑(orderOf f) : ℤ)
⊢ Eq (α := α) ((f ^ k : (a : α) → α) x : α) ((f ^ k : (a : α) → α) x : α)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x : α
inst : Finite α
k : ℤ
h₀ : LT.lt (α := ℤ) 0 (↑(orderOf f) : ℤ)
h₁ : 0 ≤ k % (↑(orderOf f) : ℤ)
h : (k % (↑(orderOf f) : ℤ)).natAbs < orderOf f
⊢ (k % (↑(orderOf f) : ℤ)).natAbs < orderOf f ∧ Eq (α := α) ((f ^ k : (a : α) → α) x : α) ((f ^ k : (a : α) → α) x : α)

Tactic:
refine ⟨?_, by rfl⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x : α
inst : Finite α
k : ℤ
h₀ : LT.lt (α := ℤ) 0 (↑(orderOf f) : ℤ)
h₁ : 0 ≤ k % (↑(orderOf f) : ℤ)
h : k % (↑(orderOf f) : ℤ) < (↑(orderOf f) : ℤ)
⊢ (k % (↑(orderOf f) : ℤ)).natAbs < orderOf f

Tactic:
rw [← Int.ofNat_lt, Int.natAbs_of_nonneg h₁]

Premises used: Int.ofNat_lt, Int.natAbs_of_nonneg
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x : α
inst : Finite α
k : ℤ
h₀ : LT.lt (α := ℤ) 0 (↑(orderOf f) : ℤ)
h₁ : 0 ≤ k % (↑(orderOf f) : ℤ)
⊢ k % (↑(orderOf f) : ℤ) < (↑(orderOf f) : ℤ)

Tactic:
Int.emod_lt_of_pos _ h₀

Premises used: Int.emod_lt_of_pos
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x : α
inst : Finite α
k : ℤ
h₀ : LT.lt (α := ℤ) 0 (↑(orderOf f) : ℤ)
h₁ : 0 ≤ k % (↑(orderOf f) : ℤ)
⊢ k % (↑(orderOf f) : ℤ) < (↑(orderOf f) : ℤ)

Tactic:
exact Int.emod_lt_of_pos _ h₀

Premises used: Int.emod_lt_of_pos
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x y : α
inst : Finite α
h : f.SameCycle x y
zero :
  ∀ (hi : 0 < orderOf f) (h : f.SameCycle x ((HPow.hPow (β := ℕ) f 0 : (a : α) → α) x)),
    ∃ (i : ℕ),
      0 < i ∧ i ≤ orderOf f ∧ Eq (α := α) ((f ^ i : (a : α) → α) x : α) ((HPow.hPow (β := ℕ) f 0 : (a : α) → α) x : α)
succ :
  ∀ (i : ℕ) (hi : i + 1 < orderOf f) (h : f.SameCycle x ((f ^ (i + 1) : (a : α) → α) x)),
    ∃ (i_1 : ℕ),
      0 < i_1 ∧ i_1 ≤ orderOf f ∧ Eq (α := α) ((f ^ i_1 : (a : α) → α) x : α) ((f ^ (i + 1) : (a : α) → α) x : α)
⊢ ∃ (i : ℕ), 0 < i ∧ i ≤ orderOf f ∧ (f ^ i : (a : α) → α) x = y

Tactic:
obtain ⟨_ | i, hi, rfl⟩ := h.exists_pow_eq'

Premises used: Equiv.Perm.SameCycle.rfl, Equiv.Perm.SameCycle.exists_pow_eq'
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x : α
inst : Finite α
hi : 0 < orderOf f
h : f.SameCycle x ((HPow.hPow (β := ℕ) f 0 : (a : α) → α) x)
⊢ ∃ (i : ℕ),
    0 < i ∧ i ≤ orderOf f ∧ Eq (α := α) ((f ^ i : (a : α) → α) x : α) ((HPow.hPow (β := ℕ) f 0 : (a : α) → α) x : α)

Tactic:
⟨orderOf f, orderOf_pos f, le_rfl, ?_⟩

Premises used: le_rfl, orderOf, And.intro, Exists.intro, orderOf_pos
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x : α
inst : Finite α
hi : 0 < orderOf f
h : f.SameCycle x ((HPow.hPow (β := ℕ) f 0 : (a : α) → α) x)
zero : Eq (α := α) ((f ^ orderOf f : (a : α) → α) x : α) ((HPow.hPow (β := ℕ) f 0 : (a : α) → α) x : α)
⊢ ∃ (i : ℕ),
    0 < i ∧ i ≤ orderOf f ∧ Eq (α := α) ((f ^ i : (a : α) → α) x : α) ((HPow.hPow (β := ℕ) f 0 : (a : α) → α) x : α)

Tactic:
refine ⟨orderOf f, orderOf_pos f, le_rfl, ?_⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x : α
inst : Finite α
hi : 0 < orderOf f
h : f.SameCycle x ((HPow.hPow (β := ℕ) f 0 : (a : α) → α) x)
zero : Eq (α := α) ((1 : (a : α) → α) x : α) ((HPow.hPow (β := ℕ) f 0 : (a : α) → α) x : α)
zero₁ zero₂ : Eq (α := α) ((1 : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)
⊢ Eq (α := α) ((f ^ orderOf f : (a : α) → α) x : α) ((HPow.hPow (β := ℕ) f 0 : (a : α) → α) x : α)

Tactic:
rw [pow_orderOf_eq_one, pow_zero]

Premises used: pow_zero, pow_orderOf_eq_one
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x : α
inst : Finite α
i : ℕ
hi : i + 1 < orderOf f
h : f.SameCycle x ((f ^ (i + 1) : (a : α) → α) x)
⊢ Eq (α := α) ((f ^ i.succ : (a : α) → α) x : α) ((f ^ (i + 1) : (a : α) → α) x : α)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x : α
inst : Finite α
i : ℕ
hi : i + 1 < orderOf f
h : f.SameCycle x ((f ^ (i + 1) : (a : α) → α) x)
⊢ ∃ (i_1 : ℕ),
    0 < i_1 ∧ i_1 ≤ orderOf f ∧ Eq (α := α) ((f ^ i_1 : (a : α) → α) x : α) ((f ^ (i + 1) : (a : α) → α) x : α)

Tactic:
exact ⟨i.succ, i.zero_lt_succ, hi.le, by rfl⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x y : α
inst : Finite α
h : f.SameCycle x y
obtain :
  ∀ (i : ℕ) (hi : i < orderOf f) (hx : (f ^ i : (a : α) → α) x = y),
    ∃ (i : Fin (orderOf f)), (f ^ (↑i : ℕ) : (a : α) → α) x = y
⊢ ∃ (i : Fin (orderOf f)), (f ^ (↑i : ℕ) : (a : α) → α) x = y

Tactic:
obtain ⟨i, hi, hx⟩ := SameCycle.exists_pow_eq' h

Premises used: Equiv.Perm.SameCycle.exists_pow_eq'
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x y : α
inst : Finite α
h : f.SameCycle x y
i : ℕ
hi : i < orderOf f
hx : (f ^ i : (a : α) → α) x = y
⊢ ∃ (i : Fin (orderOf f)), (f ^ (↑i : ℕ) : (a : α) → α) x = y

Tactic:
⟨⟨i, hi⟩, hx⟩

Premises used: Fin.mk, Exists.intro
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x y : α
inst : Finite α
h : f.SameCycle x y
i : ℕ
hi : i < orderOf f
hx : (f ^ i : (a : α) → α) x = y
⊢ ∃ (i : Fin (orderOf f)), (f ^ (↑i : ℕ) : (a : α) → α) x = y

Tactic:
exact ⟨⟨i, hi⟩, hx⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x y : α
inst : Finite α
h : f.SameCycle x y
obtain : ∀ i < orderOf f, ∀ (hi : (f ^ i : (a : α) → α) x = y), ∃ (i : ℕ), (f ^ i : (a : α) → α) x = y
⊢ ∃ (i : ℕ), (f ^ i : (a : α) → α) x = y

Tactic:
obtain ⟨i, _, hi⟩ := h.exists_pow_eq'

Premises used: Equiv.Perm.SameCycle.exists_pow_eq'
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x y : α
inst : Finite α
h : f.SameCycle x y
i : ℕ
left : i < orderOf f
hi : (f ^ i : (a : α) → α) x = y
⊢ ∃ (i : ℕ), (f ^ i : (a : α) → α) x = y

Tactic:
⟨i, hi⟩

Premises used: Exists.intro
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x y : α
inst : Finite α
h : f.SameCycle x y
i : ℕ
left : i < orderOf f
hi : (f ^ i : (a : α) → α) x = y
⊢ ∃ (i : ℕ), (f ^ i : (a : α) → α) x = y

Tactic:
exact ⟨i, hi⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
h : f.IsCycle
hf : f = 1
⊢ False

Tactic:
simp [hf, IsCycle] at h

Premises used: Equiv.Perm.IsCycle
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
⊢ ¬IsCycle.{u_2} (α := α) 1

Tactic:
fun H => H.ne_one rfl

Premises used: Equiv.Perm.IsCycle.ne_one, Not, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x y : α
hf : f.IsCycle
hx : (f : (a : α) → α) x ≠ x
hy : (f : (a : α) → α) y ≠ y
g : α
hg : (f : (a : α) → α) g ≠ g ∧ ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle g y
a : ℤ
ha : (f ^ a : (a : α) → α) g = x
b : ℤ
hb : (f ^ b : (a : α) → α) g = y
rw : (f ^ (b - a) : (a : α) → α) ((f ^ a : (a : α) → α) g : α) = y
rw₁ : (f ^ (b - a) * f ^ a : (a : α) → α) g = y
rw₂ : (f ^ (b - a + a) : (a : α) → α) g = y
rw₃ : (f ^ b : (a : α) → α) g = y
rw₄ rw₅ : y = y
⊢ (f ^ (b - a) : (a : α) → α) x = y

Tactic:
rw [← ha, ← mul_apply, ← zpow_add, sub_add_cancel, hb]

Premises used: zpow_add, Equiv.Perm.mul_apply, sub_add_cancel
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
x y : α
⊢ f.IsCycle → (f : (a : α) → α) x ≠ x → (f : (a : α) → α) y ≠ y → ∃ (i : ℤ), (f ^ i : (a : α) → α) x = y

Tactic:
IsCycle.sameCycle

Premises used: Equiv.Perm.IsCycle.sameCycle, Equiv.Perm.SameCycle
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
hf : f.IsCycle
⊢ f⁻¹.IsCycle

Tactic:
hf.imp fun _ ⟨hx, h⟩ =>
    ⟨inv_eq_iff_eq.not.2 hx.symm, fun _ hy => (h <| inv_eq_iff_eq.not.2 hy.symm).inv⟩

Premises used: Exists.imp, Equiv.Perm.IsCycle
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
⊢ f⁻¹.IsCycle ↔ f.IsCycle

Tactic:
⟨fun h => h.inv, IsCycle.inv⟩

Premises used: Equiv.Perm.IsCycle.inv, Iff.intro
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f g : Perm α
x : α
hx : (f : (a : α) → α) x ≠ x
h : ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle x y
⊢ Ne (α := α) ((g * f * g⁻¹ : (a : α) → α) ((g : (a : α) → α) x : α) : α) ((g : (a : α) → α) x : α)

Tactic:
simp [coe_mul, hx]

Premises used: Equiv.Perm.coe_mul
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f g : Perm α
x : α
hx : (f : (a : α) → α) x ≠ x
h : ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle x y
refine : ∀ (y : α) (hy : (g * f * g⁻¹ : (a : α) → α) y ≠ y), (g * f * g⁻¹).SameCycle ((g : (a : α) → α) x) y
⊢ (g * f * g⁻¹).IsCycle

Tactic:
refine ⟨g x, by simp [coe_mul, hx], fun y hy => ?_⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f g : Perm α
x : α
hx : (f : (a : α) → α) x ≠ x
h : ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle x y
y : α
hy : (g * f * g⁻¹ : (a : α) → α) y ≠ y
⊢ (g * f * g⁻¹).SameCycle ((g : (a : α) → α) x) y

Tactic:
simpa using (h <| eq_inv_iff_eq.not.2 hy).conj (g := g)

Premises used: Iff.mpr, Iff.not, Equiv.Perm.SameCycle.conj, Equiv.Perm.eq_inv_iff_eq
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
β : Type u_3
g : Perm α
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_2 + 1, max 1 (u_3 + 1)} α (Subtype p)
a : α
ha : (g : (a : α) → α) a ≠ a
ha' : ∀ ⦃y : α⦄, (g : (a : α) → α) y ≠ y → g.SameCycle a y
⊢ (g.extendDomain (p := p) f).IsCycle

Tactic:
⟨f a, ?_, fun b hb => ?_⟩

Premises used: Equiv.Perm.IsCycle, And.intro, Exists.intro, Subtype.val, DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
β : Type u_3
g : Perm α
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_2 + 1, max 1 (u_3 + 1)} α (Subtype p)
a : α
ha : (g : (a : α) → α) a ≠ a
ha' : ∀ ⦃y : α⦄, (g : (a : α) → α) y ≠ y → g.SameCycle a y
refine_1 :
  Ne (α := β) ((g.extendDomain (p := p) f : (a : β) → β) (↑((f : (a : α) → Subtype p) a) : β) : β)
    ((↑((f : (a : α) → Subtype p) a) : β) : β)
refine_2 :
  ∀ (b : β) (hb : (g.extendDomain (p := p) f : (a : β) → β) b ≠ b),
    (g.extendDomain (p := p) f).SameCycle (↑((f : (a : α) → Subtype p) a) : β) b
⊢ (g.extendDomain (p := p) f).IsCycle

Tactic:
refine ⟨f a, ?_, fun b hb => ?_⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
β : Type u_3
g : Perm α
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_2 + 1, max 1 (u_3 + 1)} α (Subtype p)
a : α
ha : (g : (a : α) → α) a ≠ a
ha' : ∀ ⦃y : α⦄, (g : (a : α) → α) y ≠ y → g.SameCycle a y
refine_1 :
  Ne.{u_3 + 1} (α := β) (↑((f : (a : α) → Subtype p) ((g : (a : α) → α) a)) : β) (↑((f : (a : α) → Subtype p) a) : β)
⊢ Ne (α := β) ((g.extendDomain (p := p) f : (a : β) → β) (↑((f : (a : α) → Subtype p) a) : β) : β)
    ((↑((f : (a : α) → Subtype p) a) : β) : β)

Tactic:
rw [extendDomain_apply_image]

Premises used: Equiv.Perm.extendDomain_apply_image