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
hc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support
k : ℤ
h :
  ∀ (a : α),
    (∀ (b : a ∈ c.support), Eq (α := α) ((c ^ k : (a : α) → α) a : α) ((g : (a : α) → α) a : α)) ↔
      Eq (α := α) ((c ^ k : (a : α) → α) a : α)
        ((((ofSubtype (p := fun (x : α) ↦ x ∈ c.support) : (a : Perm ↥c.support) → Perm α)
                  (g.subtypePerm (p := Membership.mem c.support) ⋯) :
                Perm α) :
              (a : α) → α)
            a :
          α)
⊢ (∀ (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 :
          α)

Tactic:
apply forall_congr'

Premises used: forall_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 : ℤ
a : α
pos :
  ∀ (ha : a ∈ c.support),
    (∀ (b : a ∈ c.support), Eq (α := α) ((c ^ k : (a : α) → α) a : α) ((g : (a : α) → α) a : α)) ↔
      Eq (α := α) ((c ^ k : (a : α) → α) a : α)
        ((((ofSubtype (p := fun (x : α) ↦ x ∈ c.support) : (a : Perm ↥c.support) → Perm α)
                  (g.subtypePerm (p := Membership.mem c.support) ⋯) :
                Perm α) :
              (a : α) → α)
            a :
          α)
neg :
  ∀ (ha : a ∉ c.support),
    (∀ (b : a ∈ c.support), Eq (α := α) ((c ^ k : (a : α) → α) a : α) ((g : (a : α) → α) a : α)) ↔
      Eq (α := α) ((c ^ k : (a : α) → α) a : α)
        ((((ofSubtype (p := fun (x : α) ↦ x ∈ c.support) : (a : Perm ↥c.support) → Perm α)
                  (g.subtypePerm (p := Membership.mem c.support) ⋯) :
                Perm α) :
              (a : α) → α)
            a :
          α)
⊢ (∀ (b : a ∈ c.support), Eq (α := α) ((c ^ k : (a : α) → α) a : α) ((g : (a : α) → α) a : α)) ↔
    Eq (α := α) ((c ^ k : (a : α) → α) a : α)
      ((((ofSubtype (p := fun (x : α) ↦ x ∈ c.support) : (a : Perm ↥c.support) → Perm α)
                (g.subtypePerm (p := Membership.mem c.support) ⋯) :
              Perm α) :
            (a : α) → α)
          a :
        α)

Tactic:
by_cases ha : a ∈ 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
k : ℤ
a : α
ha : a ∈ c.support
pos :
  Eq (α := α) ((c ^ k : (a : α) → α) a : α) ((g : (a : α) → α) a : α) ↔
    Eq (α := α) ((c ^ k : (a : α) → α) a : α)
      ((((ofSubtype (p := fun (x : α) ↦ x ∈ c.support) : (a : Perm ↥c.support) → Perm α)
                (g.subtypePerm (p := Membership.mem c.support) ⋯) :
              Perm α) :
            (a : α) → α)
          a :
        α)
pos₁ pos₂ :
  Eq (α := α) ((c ^ k : (a : α) → α) a : α) ((g : (a : α) → α) a : α) ↔
    Eq (α := α) ((c ^ k : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
⊢ (∀ (b : a ∈ c.support), Eq (α := α) ((c ^ k : (a : α) → α) a : α) ((g : (a : α) → α) a : α)) ↔
    Eq (α := α) ((c ^ k : (a : α) → α) a : α)
      ((((ofSubtype (p := fun (x : α) ↦ x ∈ c.support) : (a : Perm ↥c.support) → Perm α)
                (g.subtypePerm (p := Membership.mem c.support) ⋯) :
              Perm α) :
            (a : α) → α)
          a :
        α)

Tactic:
rw [imp_iff_right ha, ofSubtype_subtypePerm_of_mem hc' ha]

Premises used: imp_iff_right, Equiv.Perm.ofSubtype_subtypePerm_of_mem
-- 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 : ℤ
a : α
ha : a ∉ c.support
neg : a ∉ (c ^ k).support
neg₁ : a ∉ c.support
⊢ (∀ (b : a ∈ c.support), Eq (α := α) ((c ^ k : (a : α) → α) a : α) ((g : (a : α) → α) a : α)) ↔
    Eq (α := α) ((c ^ k : (a : α) → α) a : α)
      ((((ofSubtype (p := fun (x : α) ↦ x ∈ c.support) : (a : Perm ↥c.support) → Perm α)
                (g.subtypePerm (p := Membership.mem c.support) ⋯) :
              Perm α) :
            (a : α) → α)
          a :
        α)

Tactic:
rw [iff_true_left (fun b ↦ (ha b).elim), ofSubtype_apply_of_not_mem, ← notMem_support]

Premises used: Equiv.Perm.notMem_support, False.elim, Equiv.Perm.ofSubtype_apply_of_not_mem, iff_true_left
-- 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 : ℤ
a : α
ha : a ∉ c.support
⊢ a ∉ (c ^ k).support

Tactic:
Finset.notMem_mono (support_zpow_le c k) ha

Premises used: Equiv.Perm.support_zpow_le, Finset.notMem_mono
-- 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 : ℤ
a : α
ha : a ∉ c.support
⊢ a ∉ (c ^ k).support

Tactic:
exact Finset.notMem_mono (support_zpow_le c k) ha

Premises used: Equiv.Perm.support_zpow_le, Finset.notMem_mono
-- 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 : ℤ
a : α
ha : a ∉ c.support
⊢ a ∉ c.support

Tactic:
ha
-- 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 : ℤ
a : α
ha : a ∉ c.support
⊢ a ∉ c.support

Tactic:
exact ha
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), Membership.mem (α := α) s ((g : (a : α) → α) x : α) ↔ x ∈ s
hc : c.support ⊆ s
n : ℤ
mp :
  c ^ n = (ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) →
    c.subtypePerm (p := Membership.mem s) ⋯ ^ n = g.subtypePerm (p := Membership.mem s) hg
mpr :
  c.subtypePerm (p := Membership.mem s) ⋯ ^ n = g.subtypePerm (p := Membership.mem s) hg →
    c ^ n = (ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg)
⊢ c ^ n = (ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) ↔
    c.subtypePerm (p := Membership.mem s) ⋯ ^ n = g.subtypePerm (p := Membership.mem s) hg

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), Membership.mem (α := α) s ((g : (a : α) → α) x : α) ↔ x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c ^ n = (ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg)
mp :
  ∀ (x : α) (hx : x ∈ s),
    Eq.{u_2 + 1} (α := α)
      (↑((c.subtypePerm (p := Membership.mem s) ⋯ ^ n : (a : ↥s) → ↥s) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)) :
        α)
      (↑((g.subtypePerm (p := Membership.mem s) hg : (a : ↥s) → ↥s) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)) : α)
⊢ c.subtypePerm (p := Membership.mem s) ⋯ ^ n = g.subtypePerm (p := Membership.mem s) hg

Tactic:
ext ⟨x, hx⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), Membership.mem (α := α) s ((g : (a : α) → α) x : α) ↔ x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c ^ n = (ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg)
x : α
hx : x ∈ s
⊢ Eq.{u_2 + 1} (α := α)
    (↑((c.subtypePerm (p := Membership.mem s) ⋯ ^ n : (a : ↥s) → ↥s) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)) : α)
    (↑((g.subtypePerm (p := Membership.mem s) hg : (a : ↥s) → ↥s) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)) : α)

Tactic:
simpa [Perm.congr_fun h _] using ofSubtype_subtypePerm_of_mem _ hx

Premises used: Equiv.Perm.ofSubtype_subtypePerm_of_mem, Equiv.Perm.congr_fun
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), Membership.mem (α := α) s ((g : (a : α) → α) x : α) ↔ x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c.subtypePerm (p := Membership.mem s) ⋯ ^ n = g.subtypePerm (p := Membership.mem s) hg
mpr :
  ∀ (x : α),
    Eq (α := α) ((c ^ n : (a : α) → α) x : α)
      ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) :
              Perm α) :
            (a : α) → α)
          x :
        α)
⊢ c ^ n = (ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg)

Tactic:
ext x
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), Membership.mem (α := α) s ((g : (a : α) → α) x : α) ↔ x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c.subtypePerm (p := Membership.mem s) ⋯ ^ n = g.subtypePerm (p := Membership.mem s) hg
x : α
mpr :
  Eq (α := α) ((c ^ n : (a : α) → α) x : α)
    ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (c.subtypePerm (p := Membership.mem s) ⋯ ^ n) :
            Perm α) :
          (a : α) → α)
        x :
      α)
⊢ Eq (α := α) ((c ^ n : (a : α) → α) x : α)
    ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) :
            Perm α) :
          (a : α) → α)
        x :
      α)

Tactic:
rw [← h]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), Membership.mem (α := α) s ((g : (a : α) → α) x : α) ↔ x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c.subtypePerm (p := Membership.mem s) ⋯ ^ n = g.subtypePerm (p := Membership.mem s) hg
x : α
pos :
  ∀ (hx : x ∈ s),
    Eq (α := α) ((c ^ n : (a : α) → α) x : α)
      ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (c.subtypePerm (p := Membership.mem s) ⋯ ^ n) :
              Perm α) :
            (a : α) → α)
          x :
        α)
neg :
  ∀ (hx : x ∉ s),
    Eq (α := α) ((c ^ n : (a : α) → α) x : α)
      ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (c.subtypePerm (p := Membership.mem s) ⋯ ^ n) :
              Perm α) :
            (a : α) → α)
          x :
        α)
⊢ Eq (α := α) ((c ^ n : (a : α) → α) x : α)
    ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (c.subtypePerm (p := Membership.mem s) ⋯ ^ n) :
            Perm α) :
          (a : α) → α)
        x :
      α)

Tactic:
by_cases hx : x ∈ s
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), Membership.mem (α := α) s ((g : (a : α) → α) x : α) ↔ x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c.subtypePerm (p := Membership.mem s) ⋯ ^ n = g.subtypePerm (p := Membership.mem s) hg
x : α
hx : x ∈ s
pos :
  Eq (α := α) ((c ^ n : (a : α) → α) x : α)
    ((↑((c.subtypePerm (p := Membership.mem s) ⋯ ^ n : (a : ↥s) → ↥s) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)) :
        α) :
      α)
pos₁ :
  Eq (α := α) ((c ^ n : (a : α) → α) x : α)
    ((↑(((c ^ n).subtypePerm (p := Membership.mem s) ⋯ : (a : ↥s) → ↥s) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)) :
        α) :
      α)
pos₂ pos₃ :
  Eq (α := α) ((c ^ n : (a : α) → α) x : α)
    ((↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s)
            ((c ^ n : (a : α) → α) (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx) : α)) ⋯) :
        α) :
      α)
⊢ Eq (α := α) ((c ^ n : (a : α) → α) x : α)
    ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (c.subtypePerm (p := Membership.mem s) ⋯ ^ n) :
            Perm α) :
          (a : α) → α)
        x :
      α)

Tactic:
rw [ofSubtype_apply_of_mem (subtypePerm c _ ^ n) hx,
        subtypePerm_zpow, subtypePerm_apply]

Premises used: Equiv.Perm.subtypePerm, Equiv.Perm.ofSubtype_apply_of_mem, HPow.hPow, Equiv.Perm.subtypePerm_zpow, Equiv.Perm.subtypePerm_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), Membership.mem (α := α) s ((g : (a : α) → α) x : α) ↔ x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c.subtypePerm (p := Membership.mem s) ⋯ ^ n = g.subtypePerm (p := Membership.mem s) hg
x : α
hx : x ∉ s
neg : x ∉ (c ^ n).support
⊢ Eq (α := α) ((c ^ n : (a : α) → α) x : α)
    ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (c.subtypePerm (p := Membership.mem s) ⋯ ^ n) :
            Perm α) :
          (a : α) → α)
        x :
      α)

Tactic:
rw [ofSubtype_apply_of_not_mem (subtypePerm c _ ^ n) hx,
        ← notMem_support]

Premises used: Equiv.Perm.notMem_support, Equiv.Perm.subtypePerm, HPow.hPow, Equiv.Perm.ofSubtype_apply_of_not_mem
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), Membership.mem (α := α) s ((g : (a : α) → α) x : α) ↔ x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c.subtypePerm (p := Membership.mem s) ⋯ ^ n = g.subtypePerm (p := Membership.mem s) hg
x : α
hx : x ∉ s
⊢ x ∉ (c ^ n).support

Tactic:
fun hx' ↦ hx (hc (support_zpow_le _ _ hx'))

Premises used: Equiv.Perm.support_zpow_le, Not
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), Membership.mem (α := α) s ((g : (a : α) → α) x : α) ↔ x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c.subtypePerm (p := Membership.mem s) ⋯ ^ n = g.subtypePerm (p := Membership.mem s) hg
x : α
hx : x ∉ s
⊢ x ∉ (c ^ n).support

Tactic:
exact fun hx' ↦ hx (hc (support_zpow_le _ _ hx'))

Premises used: Equiv.Perm.support_zpow_le
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
q : ℤ := n / (↑(#g.support) : ℤ)
set :
  let r := n % (↑(#g.support) : ℤ);
  (g ^ n : (a : α) → α) x = x ↔ r = 0
⊢ (g ^ n : (a : α) → α) x = x ↔ n % (↑(#g.support) : ℤ) = 0

Tactic:
set r := n % #g.support

Premises used: Equiv.Perm.support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
q : ℤ := n / (↑(#g.support) : ℤ)
r : ℤ := n % (↑(#g.support) : ℤ)
rw : n / (↑(#g.support) : ℤ) = q ∧ n % (↑(#g.support) : ℤ) = r
rw₁ : LT.lt (α := ℤ) 0 (↑(#g.support) : ℤ)
⊢ r + (↑(#g.support) : ℤ) * q = n ∧ 0 ≤ r ∧ r < (↑(#g.support) : ℤ)

Tactic:
rw [← Int.ediv_emod_unique _]

Premises used: Int.ediv_emod_unique
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
q : ℤ := n / (↑(#g.support) : ℤ)
r : ℤ := n % (↑(#g.support) : ℤ)
⊢ n / (↑(#g.support) : ℤ) = q ∧ n % (↑(#g.support) : ℤ) = r

Tactic:
⟨rfl, rfl⟩

Premises used: And.intro, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
q : ℤ := n / (↑(#g.support) : ℤ)
r : ℤ := n % (↑(#g.support) : ℤ)
⊢ n / (↑(#g.support) : ℤ) = q ∧ n % (↑(#g.support) : ℤ) = r

Tactic:
exact ⟨rfl, rfl⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
q : ℤ := n / (↑(#g.support) : ℤ)
r : ℤ := n % (↑(#g.support) : ℤ)
simp : 0 < #g.support
⊢ LT.lt (α := ℤ) 0 (↑(#g.support) : ℤ)

Tactic:
simp only [Int.natCast_pos]

Premises used: Int.natCast_pos
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
q : ℤ := n / (↑(#g.support) : ℤ)
r : ℤ := n % (↑(#g.support) : ℤ)
apply : LT.lt (α := ℕ) 0 2
⊢ 0 < #g.support

Tactic:
apply lt_of_lt_of_le _ (IsCycle.two_le_card_support hg)

Premises used: Equiv.Perm.IsCycle.two_le_card_support, lt_of_lt_of_le
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
q : ℤ := n / (↑(#g.support) : ℤ)
r : ℤ := n % (↑(#g.support) : ℤ)
⊢ LT.lt (α := ℕ) 0 2

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
q : ℤ := n / (↑(#g.support) : ℤ)
r : ℤ := n % (↑(#g.support) : ℤ)
⊢ r + (↑(#g.support) : ℤ) * q = n ∧ 0 ≤ r ∧ r < (↑(#g.support) : ℤ)

Tactic:
have div_euc : r + #g.support * q = n ∧ 0 ≤ r ∧ r < #g.support := by
    rw [← Int.ediv_emod_unique _]
    · exact ⟨rfl, rfl⟩
    simp only [Int.natCast_pos]
    apply lt_of_lt_of_le _ (IsCycle.two_le_card_support hg); simp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
q : ℤ := n / (↑(#g.support) : ℤ)
r : ℤ := n % (↑(#g.support) : ℤ)
div_euc : r + (↑(#g.support) : ℤ) * q = n ∧ 0 ≤ r ∧ r < (↑(#g.support) : ℤ)
⊢ r + (↑(orderOf g) : ℤ) * q = n ∧ 0 ≤ r ∧ r < (↑(orderOf g) : ℤ)

Tactic:
simp only [← hg.orderOf] at div_euc

Premises used: Equiv.Perm.IsCycle.orderOf
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
q : ℤ := n / (↑(#g.support) : ℤ)
r : ℤ := n % (↑(#g.support) : ℤ)
div_euc : r + (↑(orderOf g) : ℤ) * q = n ∧ 0 ≤ r ∧ r < (↑(orderOf g) : ℤ)
obtain : ∀ (m : ℕ) (hm : r = (↑m : ℤ)), (g ^ n : (a : α) → α) x = x ↔ r = 0
⊢ (g ^ n : (a : α) → α) x = x ↔ r = 0

Tactic:
obtain ⟨m, hm⟩ := Int.eq_ofNat_of_zero_le div_euc.2.1

Premises used: Int.eq_ofNat_of_zero_le, And.right, And.left
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
q : ℤ := n / (↑(#g.support) : ℤ)
r : ℤ := n % (↑(#g.support) : ℤ)
div_euc : r + (↑(orderOf g) : ℤ) * q = n ∧ 0 ≤ r ∧ r < (↑(orderOf g) : ℤ)
m : ℕ
hm : r = (↑m : ℤ)
⊢ (↑m : ℤ) + (↑(orderOf g) : ℤ) * q = n ∧ m < orderOf g

Tactic:
simp only [hm, Nat.cast_nonneg, Nat.cast_lt, true_and] at div_euc

Premises used: Nat.cast_nonneg, Nat.cast_lt, true_and
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
q : ℤ := n / (↑(#g.support) : ℤ)
r : ℤ := n % (↑(#g.support) : ℤ)
m : ℕ
hm : r = (↑m : ℤ)
div_euc : (↑m : ℤ) + (↑(orderOf g) : ℤ) * q = n ∧ m < orderOf g
rw : (HPow.hPow (β := ℤ) g (↑m : ℤ) * g ^ ((↑(orderOf g) : ℤ) * q) : (a : α) → α) x = x ↔ r = 0
⊢ (g ^ n : (a : α) → α) x = x ↔ r = 0

Tactic:
rw [← div_euc.1, zpow_add g]

Premises used: zpow_add, And.left
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
q : ℤ := n / (↑(#g.support) : ℤ)
r : ℤ := n % (↑(#g.support) : ℤ)
m : ℕ
hm : r = (↑m : ℤ)
div_euc : (↑m : ℤ) + (↑(orderOf g) : ℤ) * q = n ∧ m < orderOf g
simp : (g ^ m : (a : α) → α) x = x ↔ m = 0
⊢ (HPow.hPow (β := ℤ) g (↑m : ℤ) * g ^ ((↑(orderOf g) : ℤ) * q) : (a : α) → α) x = x ↔ r = 0

Tactic:
simp only [hm, Nat.cast_eq_zero, zpow_natCast, coe_mul, comp_apply, zpow_mul,
    pow_orderOf_eq_one, one_zpow, coe_one, id_eq]

Premises used: zpow_natCast, Equiv.Perm.coe_mul, zpow_mul, one_zpow, Equiv.Perm.coe_one, pow_orderOf_eq_one, Nat.cast_eq_zero, Function.comp_apply, id_eq
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
q : ℤ := n / (↑(#g.support) : ℤ)
r : ℤ := n % (↑(#g.support) : ℤ)
m : ℕ
hm : r = (↑m : ℤ)
div_euc : (↑m : ℤ) + (↑(orderOf g) : ℤ) * q = n ∧ m < orderOf g
mp : (g ^ m : (a : α) → α) x = x → g ^ m = 1
mpr : g ^ m = 1 → (g ^ m : (a : α) → α) x = x
⊢ (g ^ m : (a : α) → α) x = x ↔ g ^ m = 1

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
q : ℤ := n / (↑(#g.support) : ℤ)
r : ℤ := n % (↑(#g.support) : ℤ)
m : ℕ
hm : r = (↑m : ℤ)
div_euc : (↑m : ℤ) + (↑(orderOf g) : ℤ) * q = n ∧ m < orderOf g
hgm : (g ^ m : (a : α) → α) x = x
mp : ∃ (x : α), (g : (a : α) → α) x ≠ x ∧ (g ^ m : (a : α) → α) x = x
⊢ g ^ m = 1

Tactic:
simp only [IsCycle.pow_eq_one_iff hg]

Premises used: Equiv.Perm.IsCycle.pow_eq_one_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
q : ℤ := n / (↑(#g.support) : ℤ)
r : ℤ := n % (↑(#g.support) : ℤ)
m : ℕ
hm : r = (↑m : ℤ)
div_euc : (↑m : ℤ) + (↑(orderOf g) : ℤ) * q = n ∧ m < orderOf g
hgm : (g ^ m : (a : α) → α) x = x
w : α
h : (g : (a : α) → α) x ≠ x ∧ (g ^ m : (a : α) → α) x = x
⊢ ∃ (x : α), (g : (a : α) → α) x ≠ x ∧ (g ^ m : (a : α) → α) x = x

Tactic:
use x
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
q : ℤ := n / (↑(#g.support) : ℤ)
r : ℤ := n % (↑(#g.support) : ℤ)
m : ℕ
hm : r = (↑m : ℤ)
div_euc : (↑m : ℤ) + (↑(orderOf g) : ℤ) * q = n ∧ m < orderOf g
hgm : g ^ m = 1
⊢ (g ^ m : (a : α) → α) x = x

Tactic:
simp only [hgm, coe_one, id_eq]

Premises used: Equiv.Perm.coe_one, id_eq
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
q : ℤ := n / (↑(#g.support) : ℤ)
r : ℤ := n % (↑(#g.support) : ℤ)
m : ℕ
hm : r = (↑m : ℤ)
div_euc : (↑m : ℤ) + (↑(orderOf g) : ℤ) * q = n ∧ m < orderOf g
⊢ (g ^ m : (a : α) → α) x = x ↔ g ^ m = 1

Tactic:
have : (g ^ m) x = x ↔ g ^ m = 1 := by
    constructor
    · intro hgm
      simp only [IsCycle.pow_eq_one_iff hg]
      use x
    · intro hgm
      simp only [hgm, coe_one, id_eq]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
q : ℤ := n / (↑(#g.support) : ℤ)
r : ℤ := n % (↑(#g.support) : ℤ)
m : ℕ
hm : r = (↑m : ℤ)
div_euc : (↑m : ℤ) + (↑(orderOf g) : ℤ) * q = n ∧ m < orderOf g
this : (g ^ m : (a : α) → α) x = x ↔ g ^ m = 1
rw : g ^ m = 1 ↔ m = 0
⊢ (g ^ m : (a : α) → α) x = x ↔ m = 0

Tactic:
rw [this]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
q : ℤ := n / (↑(#g.support) : ℤ)
r : ℤ := n % (↑(#g.support) : ℤ)
m : ℕ
hm : r = (↑m : ℤ)
div_euc : (↑m : ℤ) + (↑(orderOf g) : ℤ) * q = n ∧ m < orderOf g
this : (g ^ m : (a : α) → α) x = x ↔ g ^ m = 1
pos : ∀ (hm0 : m = 0), g ^ m = 1 ↔ m = 0
neg : ∀ (hm0 : ¬m = 0), g ^ m = 1 ↔ m = 0
⊢ g ^ m = 1 ↔ m = 0

Tactic:
by_cases hm0 : m = 0
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : (g : (a : α) → α) x ≠ x
q : ℤ := n / (↑(#g.support) : ℤ)
r : ℤ := n % (↑(#g.support) : ℤ)
m : ℕ
hm : r = (↑m : ℤ)
div_euc : (↑m : ℤ) + (↑(orderOf g) : ℤ) * q = n ∧ m < orderOf g
this : (g ^ m : (a : α) → α) x = x ↔ g ^ m = 1
hm0 : m = 0
⊢ g ^ m = 1 ↔ m = 0

Tactic:
simp only [hm0, pow_zero]

Premises used: pow_zero