awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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 :
          α)
⊢ (∀ (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 :
        α)
have 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) sorry) :
              Perm α) :
            (a : α) → α)
          a :
        α)
Tactic: by_cases ha : a ∈ c.support
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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
⊢ (∀ (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 :
        α)
have 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) sorry) :
            Perm α) :
          (a : α) → α)
        a :
      α)
Tactic: rw [imp_iff_right ha, ofSubtype_subtypePerm_of_mem hc' ha]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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 :
        α)
⊢ (∀ (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 :
        α)
have pos₁ : Eq (α := α) ((c ^ k : (a : α) → α) a : α) ((g : (a : α) → α) a : α) ↔
  Eq (α := α) ((c ^ k : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
Tactic: rw [imp_iff_right ha, ofSubtype_subtypePerm_of_mem hc' ha]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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
⊢ (∀ (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 :
        α)
have neg : a ∉ (c ^ k).support
Tactic: rw [iff_true_left (fun b ↦ (ha b).elim), ofSubtype_apply_of_not_mem, ← notMem_support]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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 : ℤ
⊢ 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
have 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) sorry ^ n = g.subtypePerm (p := Membership.mem s) hg
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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
⊢ 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
have mpr : c.subtypePerm (p := Membership.mem s) sorry ^ 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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)
⊢ c.subtypePerm (p := Membership.mem s) ⋯ ^ n = g.subtypePerm (p := Membership.mem s) hg
have mp : ∀ (x : α) (hx : x ∈ s),
  Eq.{u_2 + 1} (α := α)
    (↑((c.subtypePerm (p := Membership.mem s) sorry ^ 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: ext ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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
⊢ c ^ n = (ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg)
have 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 :
      α)
Tactic: ext x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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 : α
⊢ 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 :
      α)
have mpr : Eq (α := α) ((c ^ n : (a : α) → α) x : α)
  ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (c.subtypePerm (p := Membership.mem s) sorry ^ n) :
          Perm α) :
        (a : α) → α)
      x :
    α)
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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 : α
⊢ 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 :
      α)
have 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) sorry ^ n) :
            Perm α) :
          (a : α) → α)
        x :
      α)
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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 :
        α)
⊢ 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 :
      α)
have 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) sorry ^ n) :
            Perm α) :
          (a : α) → α)
        x :
      α)
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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
⊢ 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 :
      α)
have pos : Eq (α := α) ((c ^ n : (a : α) → α) x : α)
  ((↑((c.subtypePerm (p := Membership.mem s) sorry ^ n : (a : ↥s) → ↥s) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)) : α) :
    α)
Tactic: rw [ofSubtype_apply_of_mem (subtypePerm c _ ^ n) hx,
        subtypePerm_zpow, subtypePerm_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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)) :
        α) :
      α)
⊢ 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 :
      α)
have pos₁ : Eq (α := α) ((c ^ n : (a : α) → α) x : α)
  ((↑(((c ^ n).subtypePerm (p := Membership.mem s) sorry : (a : ↥s) → ↥s) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)) :
      α) :
    α)
Tactic: rw [ofSubtype_apply_of_mem (subtypePerm c _ ^ n) hx,
        subtypePerm_zpow, subtypePerm_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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)) :
        α) :
      α)
⊢ 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 :
      α)
have 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) : α))
          sorry) :
      α) :
    α)
Tactic: rw [ofSubtype_apply_of_mem (subtypePerm c _ ^ n) hx,
        subtypePerm_zpow, subtypePerm_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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
⊢ 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 :
      α)
have neg : x ∉ (c ^ n).support
Tactic: rw [ofSubtype_apply_of_not_mem (subtypePerm c _ ^ n) hx,
        ← notMem_support]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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) : ℤ)
have rw : n / (↑(#g.support) : ℤ) = q ∧ n % (↑(#g.support) : ℤ) = r
Tactic: rw [← Int.ediv_emod_unique _]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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
⊢ r + (↑(#g.support) : ℤ) * q = n ∧ 0 ≤ r ∧ r < (↑(#g.support) : ℤ)
have rw₁ : LT.lt (α := ℤ) 0 (↑(#g.support) : ℤ)
Tactic: rw [← Int.ediv_emod_unique _]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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 (↑(#g.support) : ℤ)
have simp : 0 < #g.support
Tactic: simp only [Int.natCast_pos]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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) : ℤ)
⊢ 0 < #g.support
have apply : LT.lt (α := ℕ) 0 2
Tactic: apply lt_of_lt_of_le _ (IsCycle.two_le_card_support hg)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
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) : ℤ)
⊢ (g ^ n : (a : α) → α) x = x ↔ r = 0
have div_euc : 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
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
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) : ℤ)
⊢ (g ^ n : (a : α) → α) x = x ↔ r = 0
have div_euc₁ : r + (↑(orderOf g) : ℤ) * q = n ∧ 0 ≤ r ∧ r < (↑(orderOf g) : ℤ)
Tactic: simp only [← hg.orderOf] at div_euc
Cleared hypotheses: div_euc
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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) : ℤ)
⊢ (g ^ n : (a : α) → α) x = x ↔ r = 0
have obtain : ∀ (m : ℕ) (hm : r = (↑m : ℤ)), (g ^ n : (a : α) → α) x = x ↔ r = 0
Tactic: obtain ⟨m, hm⟩ := Int.eq_ofNat_of_zero_le div_euc.2.1
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
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 : ℤ)
⊢ (g ^ n : (a : α) → α) x = x ↔ r = 0
have div_euc₁ : (↑m : ℤ) + (↑(orderOf g) : ℤ) * q = n ∧ m < orderOf g
Tactic: simp only [hm, Nat.cast_nonneg, Nat.cast_lt, true_and] at div_euc
Cleared hypotheses: div_euc
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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 ^ n : (a : α) → α) x = x ↔ r = 0
have rw : (HPow.hPow (β := ℤ) g (↑m : ℤ) * g ^ ((↑(orderOf g) : ℤ) * q) : (a : α) → α) x = x ↔ r = 0
Tactic: rw [← div_euc.1, zpow_add g]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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
⊢ (HPow.hPow (β := ℤ) g (↑m : ℤ) * g ^ ((↑(orderOf g) : ℤ) * q) : (a : α) → α) x = x ↔ r = 0
have simp : (g ^ m : (a : α) → α) x = x ↔ m = 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]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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
have mp : (g ^ m : (a : α) → α) x = x → g ^ m = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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
⊢ (g ^ m : (a : α) → α) x = x ↔ g ^ m = 1
have mpr : g ^ m = 1 → (g ^ m : (a : α) → α) x = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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
⊢ g ^ m = 1
have mp : ∃ (x : α), (g : (a : α) → α) x ≠ x ∧ (g ^ m : (a : α) → α) x = x
Tactic: simp only [IsCycle.pow_eq_one_iff hg]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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 : α
⊢ ∃ (x : α), (g : (a : α) → α) x ≠ x ∧ (g ^ m : (a : α) → α) x = x
have h : (g : (a : α) → α) x ≠ x ∧ (g ^ m : (a : α) → α) x = x
Tactic: use x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
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 ↔ m = 0
have this : (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]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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
⊢ (g ^ m : (a : α) → α) x = x ↔ m = 0
have rw : g ^ m = 1 ↔ m = 0
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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
⊢ g ^ m = 1 ↔ m = 0
have pos : ∀ (hm0 : m = 0), g ^ m = 1 ↔ m = 0
Tactic: by_cases hm0 : m = 0
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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
⊢ g ^ m = 1 ↔ m = 0
have neg : ∀ (hm0 : ¬m = 0), g ^ m = 1 ↔ m = 0
Tactic: by_cases hm0 : m = 0
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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
have neg : ¬g ^ m = 1
Tactic: simp only [hm0, iff_false]