awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
hc : c.IsCycle
hgc : Commute g c
hgc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support
a : α
ha : a ∈ c.support
h :
  ∀ (i : ℤ) (hi : Eq (α := α) ((c ^ i : (a : α) → α) a : α) ((g : (a : α) → α) a : α)),
    Membership.mem (γ := Subgroup (Perm ↥c.support)) (Subgroup.zpowers c.subtypePermOfSupport)
      (g.subtypePerm (p := Membership.mem c.support) hgc')
⊢ Membership.mem (γ := Subgroup (Perm ↥c.support)) (Subgroup.zpowers c.subtypePermOfSupport)
    (g.subtypePerm (p := Membership.mem c.support) hgc')

Tactic:
obtain ⟨i, hi⟩ := hc.sameCycle (mem_support.mp ha) (mem_support.mp ((hgc' a).mpr ha))

Premises used: Iff.mpr, Equiv.Perm.IsCycle.sameCycle, Equiv.Perm.mem_support, Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
hc : c.IsCycle
hgc : Commute g c
hgc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support
a : α
ha : a ∈ c.support
i : ℤ
hi : Eq (α := α) ((c ^ i : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
h :
  (fun (x : ℤ) ↦ HPow.hPow (α := Perm ↥c.support) c.subtypePermOfSupport x) i =
    g.subtypePerm (p := Membership.mem c.support) hgc'
⊢ Membership.mem (γ := Subgroup (Perm ↥c.support)) (Subgroup.zpowers c.subtypePermOfSupport)
    (g.subtypePerm (p := Membership.mem c.support) hgc')

Tactic:
use i
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
hc : c.IsCycle
hgc : Commute g c
hgc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support
a : α
ha : a ∈ c.support
i : ℤ
hi : Eq (α := α) ((c ^ i : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
h :
  ∀ (x : α) (hx : x ∈ c.support),
    Eq.{u_2 + 1} (α := α)
      (↑(((fun (x : ℤ) ↦ HPow.hPow (α := Perm ↥c.support) c.subtypePermOfSupport x) i : (a : ↥c.support) → ↥c.support)
            (Subtype.mk (p := fun (x : α) ↦ x ∈ c.support) x hx)) :
        α)
      (↑((g.subtypePerm (p := Membership.mem c.support) hgc' : (a : ↥c.support) → ↥c.support)
            (Subtype.mk (p := fun (x : α) ↦ x ∈ c.support) x hx)) :
        α)
⊢ (fun (x : ℤ) ↦ HPow.hPow (α := Perm ↥c.support) c.subtypePermOfSupport x) i =
    g.subtypePerm (p := Membership.mem c.support) hgc'

Tactic:
ext ⟨x, hx⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
hc : c.IsCycle
hgc : Commute g c
hgc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support
a : α
ha : a ∈ c.support
i : ℤ
hi : Eq (α := α) ((c ^ i : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
x : α
hx : x ∈ c.support
h :
  Eq (α := α)
    ((↑((HPow.hPow (α := Perm ↥c.support) (c.subtypePerm (p := Membership.mem c.support) ⋯) i :
              (a : ↥c.support) → ↥c.support)
            (Subtype.mk (p := fun (x : α) ↦ x ∈ c.support) x hx)) :
        α) :
      α)
    ((g : (a : α) → α) x : α)
⊢ Eq.{u_2 + 1} (α := α)
    (↑(((fun (x : ℤ) ↦ HPow.hPow (α := Perm ↥c.support) c.subtypePermOfSupport x) i : (a : ↥c.support) → ↥c.support)
          (Subtype.mk (p := fun (x : α) ↦ x ∈ c.support) x hx)) :
      α)
    (↑((g.subtypePerm (p := Membership.mem c.support) hgc' : (a : ↥c.support) → ↥c.support)
          (Subtype.mk (p := fun (x : α) ↦ x ∈ c.support) x hx)) :
      α)

Tactic:
simp only [subtypePermOfSupport, Subtype.coe_mk, subtypePerm_apply]

Premises used: Subtype.coe_mk, Equiv.Perm.subtypePermOfSupport, Equiv.Perm.subtypePerm_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
hc : c.IsCycle
hgc : Commute g c
hgc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support
a : α
ha : a ∈ c.support
i : ℤ
hi : Eq (α := α) ((c ^ i : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
x : α
hx : x ∈ c.support
h : Eq (α := α) ((c ^ i : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
⊢ Eq (α := α)
    ((↑((HPow.hPow (α := Perm ↥c.support) (c.subtypePerm (p := Membership.mem c.support) ⋯) i :
              (a : ↥c.support) → ↥c.support)
            (Subtype.mk (p := fun (x : α) ↦ x ∈ c.support) x hx)) :
        α) :
      α)
    ((g : (a : α) → α) x : α)

Tactic:
rw [subtypePerm_apply_zpow_of_mem]

Premises used: Equiv.Perm.subtypePerm_apply_zpow_of_mem
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
hc : c.IsCycle
hgc : Commute g c
hgc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support
a : α
ha : a ∈ c.support
i : ℤ
hi : Eq (α := α) ((c ^ i : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
x : α
hx : x ∈ c.support
h :
  ∀ (j : ℤ) (hx : Membership.mem (α := α) c.support ((c ^ j : (a : α) → α) a : α)),
    Eq (α := α) ((c ^ i : (a : α) → α) ((c ^ j : (a : α) → α) a : α) : α)
      ((g : (a : α) → α) ((c ^ j : (a : α) → α) a : α) : α)
⊢ Eq (α := α) ((c ^ i : (a : α) → α) x : α) ((g : (a : α) → α) x : α)

Tactic:
obtain ⟨j, rfl⟩ := hc.sameCycle (mem_support.mp ha) (mem_support.mp hx)

Premises used: Equiv.Perm.IsCycle.sameCycle, Equiv.Perm.mem_support, Iff.mp, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
hc : c.IsCycle
hgc : Commute g c
hgc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support
a : α
ha : a ∈ c.support
i : ℤ
hi : Eq (α := α) ((c ^ i : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
j : ℤ
hx : Membership.mem (α := α) c.support ((c ^ j : (a : α) → α) a : α)
h : Eq (α := α) ((c ^ i * c ^ j : (a : α) → α) a : α) ((c ^ j * g : (a : α) → α) a : α)
⊢ Eq (α := α) ((c ^ i : (a : α) → α) ((c ^ j : (a : α) → α) a : α) : α)
    ((g : (a : α) → α) ((c ^ j : (a : α) → α) a : α) : α)

Tactic:
simp only [← mul_apply, Commute.eq (Commute.zpow_right hgc j)]

Premises used: Commute.zpow_right, Equiv.Perm.mul_apply, Commute.eq
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
hc : c.IsCycle
hgc : Commute g c
hgc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support
a : α
ha : a ∈ c.support
i : ℤ
hi : Eq (α := α) ((c ^ i : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
j : ℤ
hx : Membership.mem (α := α) c.support ((c ^ j : (a : α) → α) a : α)
h : Eq (α := α) ((c ^ j * c ^ i : (a : α) → α) a : α) ((c ^ j * g : (a : α) → α) a : α)
⊢ Eq (α := α) ((c ^ i * c ^ j : (a : α) → α) a : α) ((c ^ j * g : (a : α) → α) a : α)

Tactic:
rw [← zpow_add, add_comm i j, zpow_add]

Premises used: zpow_add, add_comm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
hc : c.IsCycle
hgc : Commute g c
hgc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support
a : α
ha : a ∈ c.support
i : ℤ
hi : Eq (α := α) ((c ^ i : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
j : ℤ
hx : Membership.mem (α := α) c.support ((c ^ j : (a : α) → α) a : α)
h : Eq (α := α) ((c ^ i : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
⊢ Eq (α := α) ((c ^ j * c ^ i : (a : α) → α) a : α) ((c ^ j * g : (a : α) → α) a : α)

Tactic:
simp only [mul_apply, EmbeddingLike.apply_eq_iff_eq]

Premises used: EmbeddingLike.apply_eq_iff_eq, Equiv.Perm.mul_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
hc : c.IsCycle
hgc : Commute g c
hgc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support
a : α
ha : a ∈ c.support
i : ℤ
hi : Eq (α := α) ((c ^ i : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
j : ℤ
hx : Membership.mem (α := α) c.support ((c ^ j : (a : α) → α) a : α)
⊢ Eq (α := α) ((c ^ i : (a : α) → α) a : α) ((g : (a : α) → α) a : α)

Tactic:
hi
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
hc : c.IsCycle
hgc : Commute g c
hgc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support
a : α
ha : a ∈ c.support
i : ℤ
hi : Eq (α := α) ((c ^ i : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
j : ℤ
hx : Membership.mem (α := α) c.support ((c ^ j : (a : α) → α) a : α)
⊢ Eq (α := α) ((c ^ i : (a : α) → α) a : α) ((g : (a : α) → α) a : α)

Tactic:
exact hi
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support
i : ℤ
hi :
  (fun (x : ℤ) ↦ HPow.hPow (α := Perm ↥c.support) c.subtypePermOfSupport x) i =
    g.subtypePerm (p := Membership.mem c.support) hc'
mpr : ∀ (x : α), Eq (α := α) ((g * c : (a : α) → α) x : α) ((c * g : (a : α) → α) x : α)
⊢ Commute g c

Tactic:
ext x
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support
i : ℤ
hi :
  (fun (x : ℤ) ↦ HPow.hPow (α := Perm ↥c.support) c.subtypePermOfSupport x) i =
    g.subtypePerm (p := Membership.mem c.support) hc'
x : α
mpr : Eq (α := α) ((g : (a : α) → α) ((c : (a : α) → α) x : α) : α) ((c : (a : α) → α) ((g : (a : α) → α) x : α) : α)
⊢ Eq (α := α) ((g * c : (a : α) → α) x : α) ((c * g : (a : α) → α) x : α)

Tactic:
simp only [coe_mul, Function.comp_apply]

Premises used: Equiv.Perm.coe_mul, Function.comp_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support
i : ℤ
hi :
  (fun (x : ℤ) ↦ HPow.hPow (α := Perm ↥c.support) c.subtypePermOfSupport x) i =
    g.subtypePerm (p := Membership.mem c.support) hc'
x : α
pos :
  ∀ (hx : x ∈ c.support),
    Eq (α := α) ((g : (a : α) → α) ((c : (a : α) → α) x : α) : α) ((c : (a : α) → α) ((g : (a : α) → α) x : α) : α)
neg :
  ∀ (hx : x ∉ c.support),
    Eq (α := α) ((g : (a : α) → α) ((c : (a : α) → α) x : α) : α) ((c : (a : α) → α) ((g : (a : α) → α) x : α) : α)
⊢ Eq (α := α) ((g : (a : α) → α) ((c : (a : α) → α) x : α) : α) ((c : (a : α) → α) ((g : (a : α) → α) x : α) : α)

Tactic:
by_cases hx : x ∈ c.support

Premises used: Equiv.Perm.support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support
i : ℤ
hi :
  (fun (x : ℤ) ↦ HPow.hPow (α := Perm ↥c.support) c.subtypePermOfSupport x) i =
    g.subtypePerm (p := Membership.mem c.support) hc'
x : α
hx : x ∈ c.support
hi' : ∀ x ∈ c.support, Eq (α := α) ((g : (a : α) → α) x : α) ((c ^ i : (a : α) → α) x : α)
rw :
  Eq (α := α) ((c ^ i : (a : α) → α) ((c : (a : α) → α) x : α) : α)
    ((c : (a : α) → α) ((c ^ i : (a : α) → α) x : α) : α)
⊢ Eq (α := α) ((g : (a : α) → α) ((c : (a : α) → α) x : α) : α) ((c : (a : α) → α) ((g : (a : α) → α) x : α) : α)

Tactic:
rw [hi' x hx, hi' (c x) (apply_mem_support.mpr hx)]

Premises used: Iff.mpr, Equiv.Perm.apply_mem_support, DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support
i : ℤ
hi :
  (fun (x : ℤ) ↦ HPow.hPow (α := Perm ↥c.support) c.subtypePermOfSupport x) i =
    g.subtypePerm (p := Membership.mem c.support) hc'
x : α
hx : x ∈ c.support
hi' : ∀ x ∈ c.support, Eq (α := α) ((g : (a : α) → α) x : α) ((c ^ i : (a : α) → α) x : α)
⊢ Eq (α := α) ((c ^ i : (a : α) → α) ((c : (a : α) → α) x : α) : α)
    ((c : (a : α) → α) ((c ^ i : (a : α) → α) x : α) : α)

Tactic:
simp only [← mul_apply, ← zpow_add_one, ← zpow_one_add, add_comm]

Premises used: zpow_add_one, zpow_one_add, add_comm, Equiv.Perm.mul_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support
i : ℤ
hi :
  (fun (x : ℤ) ↦ HPow.hPow (α := Perm ↥c.support) c.subtypePermOfSupport x) i =
    g.subtypePerm (p := Membership.mem c.support) hc'
x : α
hx : x ∈ c.support
pos : ∀ x ∈ c.support, Eq (α := α) ((g : (a : α) → α) x : α) ((c ^ i : (a : α) → α) x : α)
⊢ Eq (α := α) ((g : (a : α) → α) ((c : (a : α) → α) x : α) : α) ((c : (a : α) → α) ((g : (a : α) → α) x : α) : α)

Tactic:
suffices hi' : ∀ x ∈ c.support, g x = (c ^ i) x by
        rw [hi' x hx, hi' (c x) (apply_mem_support.mpr hx)]
        simp only [← mul_apply, ← zpow_add_one, ← zpow_one_add, add_comm]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support
i : ℤ
hi :
  (fun (x : ℤ) ↦ HPow.hPow (α := Perm ↥c.support) c.subtypePermOfSupport x) i =
    g.subtypePerm (p := Membership.mem c.support) hc'
x_1 : α
hx_1 : x_1 ∈ c.support
x : α
hx : x ∈ c.support
⊢ Eq (α := ↥c.support)
    (((fun (x : ℤ) ↦ HPow.hPow (α := Perm ↥c.support) c.subtypePermOfSupport x) i : (a : ↥c.support) → ↥c.support)
        (Subtype.mk (p := fun (x : α) ↦ x ∈ c.support) x hx) :
      ↥c.support)
    ((g.subtypePerm (p := Membership.mem c.support) hc' : (a : ↥c.support) → ↥c.support)
        (Subtype.mk (p := fun (x : α) ↦ x ∈ c.support) x hx) :
      ↥c.support)

Tactic:
have hix := Perm.congr_fun hi ⟨x, hx⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support
i : ℤ
hi :
  (fun (x : ℤ) ↦ HPow.hPow (α := Perm ↥c.support) c.subtypePermOfSupport x) i =
    g.subtypePerm (p := Membership.mem c.support) hc'
x_1 : α
hx_1 : x_1 ∈ c.support
x : α
hx : x ∈ c.support
hix :
  Eq (α := ↥c.support)
    (((fun (x : ℤ) ↦ HPow.hPow (α := Perm ↥c.support) c.subtypePermOfSupport x) i : (a : ↥c.support) → ↥c.support)
        (Subtype.mk (p := fun (x : α) ↦ x ∈ c.support) x hx) :
      ↥c.support)
    ((g.subtypePerm (p := Membership.mem c.support) hc' : (a : ↥c.support) → ↥c.support)
        (Subtype.mk (p := fun (x : α) ↦ x ∈ c.support) x hx) :
      ↥c.support)
⊢ Eq (α := α) ((c ^ i : (a : α) → α) x : α) ((g : (a : α) → α) x : α)

Tactic:
simp only [← Subtype.coe_inj, subtypePermOfSupport, subtypePerm_apply,
        subtypePerm_apply_zpow_of_mem] at hix

Premises used: Equiv.Perm.subtypePermOfSupport, Subtype.coe_inj, Equiv.Perm.subtypePerm_apply_zpow_of_mem, Equiv.Perm.subtypePerm_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support
i : ℤ
hi :
  (fun (x : ℤ) ↦ HPow.hPow (α := Perm ↥c.support) c.subtypePermOfSupport x) i =
    g.subtypePerm (p := Membership.mem c.support) hc'
x_1 : α
hx_1 : x_1 ∈ c.support
x : α
hx : x ∈ c.support
hix : Eq (α := α) ((c ^ i : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
⊢ Eq (α := α) ((g : (a : α) → α) x : α) ((c ^ i : (a : α) → α) x : α)

Tactic:
hix.symm

Premises used: Eq.symm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support
i : ℤ
hi :
  (fun (x : ℤ) ↦ HPow.hPow (α := Perm ↥c.support) c.subtypePermOfSupport x) i =
    g.subtypePerm (p := Membership.mem c.support) hc'
x_1 : α
hx_1 : x_1 ∈ c.support
x : α
hx : x ∈ c.support
hix : Eq (α := α) ((c ^ i : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
⊢ Eq (α := α) ((g : (a : α) → α) x : α) ((c ^ i : (a : α) → α) x : α)

Tactic:
exact hix.symm

Premises used: Eq.symm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support
i : ℤ
hi :
  (fun (x : ℤ) ↦ HPow.hPow (α := Perm ↥c.support) c.subtypePermOfSupport x) i =
    g.subtypePerm (p := Membership.mem c.support) hc'
x : α
hx : x ∉ c.support
neg : ((g : (a : α) → α) x : α) ∉ c.support
⊢ Eq (α := α) ((g : (a : α) → α) ((c : (a : α) → α) x : α) : α) ((c : (a : α) → α) ((g : (a : α) → α) x : α) : α)

Tactic:
rw [notMem_support.mp hx, eq_comm, ← notMem_support]

Premises used: Equiv.Perm.notMem_support, eq_comm, Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support
i : ℤ
hi :
  (fun (x : ℤ) ↦ HPow.hPow (α := Perm ↥c.support) c.subtypePermOfSupport x) i =
    g.subtypePerm (p := Membership.mem c.support) hc'
x : α
hx : x ∉ c.support
neg : ∀ (hx : Membership.mem (α := α) c.support ((g : (a : α) → α) x : α)), x ∈ c.support
⊢ ((g : (a : α) → α) x : α) ∉ c.support

Tactic:
contrapose hx
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support
i : ℤ
hi :
  (fun (x : ℤ) ↦ HPow.hPow (α := Perm ↥c.support) c.subtypePermOfSupport x) i =
    g.subtypePerm (p := Membership.mem c.support) hc'
x : α
hx : Membership.mem (α := α) c.support ((g : (a : α) → α) x : α)
⊢ x ∈ c.support

Tactic:
(hc' x).mp hx

Premises used: Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support
i : ℤ
hi :
  (fun (x : ℤ) ↦ HPow.hPow (α := Perm ↥c.support) c.subtypePermOfSupport x) i =
    g.subtypePerm (p := Membership.mem c.support) hc'
x : α
hx : Membership.mem (α := α) c.support ((g : (a : α) → α) x : α)
⊢ x ∈ c.support

Tactic:
exact (hc' x).mp hx

Premises used: Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
hc : c.IsCycle
simp_rw :
  (∃ (h : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support) (k : ℤ),
      HPow.hPow (α := Perm ↥c.support) c.subtypePermOfSupport k = g.subtypePerm (p := Membership.mem c.support) ⋯) ↔
    ∃ (h : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support) (k : ℤ),
      c ^ k =
        (ofSubtype (p := fun (x : α) ↦ x ∈ c.support) : (a : Perm ↥c.support) → Perm α)
          (g.subtypePerm (p := Membership.mem c.support) ⋯)
⊢ Commute g c ↔
    ∃ (hc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support),
      Membership.mem (α := Perm α) (γ := Subgroup (Perm α)) (Subgroup.zpowers c)
        ((ofSubtype (p := fun (x : α) ↦ x ∈ c.support) : (a : Perm ↥c.support) → Perm α)
            (g.subtypePerm (p := Membership.mem c.support) hc') :
          Perm α)

Tactic:
simp_rw [hc.commute_iff', Subgroup.mem_zpowers_iff]

Premises used: Equiv.Perm.IsCycle.commute_iff', Subgroup.mem_zpowers_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
hc : c.IsCycle
⊢ (∃ (h : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support) (k : ℤ),
      HPow.hPow (α := Perm ↥c.support) c.subtypePermOfSupport k = g.subtypePerm (p := Membership.mem c.support) ⋯) ↔
    ∃ (h : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support) (k : ℤ),
      c ^ k =
        (ofSubtype (p := fun (x : α) ↦ x ∈ c.support) : (a : Perm ↥c.support) → Perm α)
          (g.subtypePerm (p := Membership.mem c.support) ⋯)

Tactic:
exists_congr fun hc' => exists_congr fun k => ?_

Premises used: exists_congr
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
hc : c.IsCycle
refine :
  ∀ (hc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support) (k : ℤ),
    HPow.hPow (α := Perm ↥c.support) c.subtypePermOfSupport k = g.subtypePerm (p := Membership.mem c.support) ⋯ ↔
      c ^ k =
        (ofSubtype (p := fun (x : α) ↦ x ∈ c.support) : (a : Perm ↥c.support) → Perm α)
          (g.subtypePerm (p := Membership.mem c.support) ⋯)
⊢ (∃ (h : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support) (k : ℤ),
      HPow.hPow (α := Perm ↥c.support) c.subtypePermOfSupport k = g.subtypePerm (p := Membership.mem c.support) ⋯) ↔
    ∃ (h : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support) (k : ℤ),
      c ^ k =
        (ofSubtype (p := fun (x : α) ↦ x ∈ c.support) : (a : Perm ↥c.support) → Perm α)
          (g.subtypePerm (p := Membership.mem c.support) ⋯)

Tactic:
refine exists_congr fun hc' => exists_congr fun k => ?_

Premises used: exists_congr
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support
k : ℤ
rw :
  (c ^ k).subtypePerm (p := Membership.mem c.support) ⋯ = g.subtypePerm (p := Membership.mem c.support) ⋯ ↔
    c ^ k =
      (ofSubtype (p := fun (x : α) ↦ x ∈ c.support) : (a : Perm ↥c.support) → Perm α)
        (g.subtypePerm (p := Membership.mem c.support) ⋯)
⊢ HPow.hPow (α := Perm ↥c.support) c.subtypePermOfSupport k = g.subtypePerm (p := Membership.mem c.support) ⋯ ↔
    c ^ k =
      (ofSubtype (p := fun (x : α) ↦ x ∈ c.support) : (a : Perm ↥c.support) → Perm α)
        (g.subtypePerm (p := Membership.mem c.support) ⋯)

Tactic:
rw [subtypePermOfSupport, subtypePerm_zpow c k]

Premises used: Equiv.Perm.subtypePermOfSupport, Equiv.Perm.subtypePerm_zpow
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support
k : ℤ
simp :
  (∀ (a : α) (b : a ∈ c.support), Eq (α := α) ((c ^ k : (a : α) → α) a : α) ((g : (a : α) → α) a : α)) ↔
    ∀ (x : α),
      Eq (α := α) ((c ^ k : (a : α) → α) x : α)
        ((((ofSubtype (p := fun (x : α) ↦ x ∈ c.support) : (a : Perm ↥c.support) → Perm α)
                  (g.subtypePerm (p := Membership.mem c.support) ⋯) :
                Perm α) :
              (a : α) → α)
            x :
          α)
⊢ (c ^ k).subtypePerm (p := Membership.mem c.support) ⋯ = g.subtypePerm (p := Membership.mem c.support) ⋯ ↔
    c ^ k =
      (ofSubtype (p := fun (x : α) ↦ x ∈ c.support) : (a : Perm ↥c.support) → Perm α)
        (g.subtypePerm (p := Membership.mem c.support) ⋯)

Tactic:
simp only [Perm.ext_iff, subtypePerm_apply, Subtype.mk.injEq, Subtype.forall]

Premises used: Subtype.forall, Equiv.Perm.ext_iff, Subtype.mk.injEq, Equiv.Perm.subtypePerm_apply