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 : Perm α
hg : g.IsCycle
⊢ g.support.Nonempty
have rw : ¬g = 1
Tactic: rw [Finset.nonempty_iff_ne_empty, ne_eq, support_eq_empty_iff]
-- 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
⊢ Commute g c ↔
    ∃ (hc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support),
      Membership.mem (γ := Subgroup (Perm ↥c.support)) (Subgroup.zpowers c.subtypePermOfSupport)
        (g.subtypePerm (p := Membership.mem c.support) hc')
have mp : Commute g c →
  ∃ (hc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support),
    Membership.mem (γ := Subgroup (Perm ↥c.support)) (Subgroup.zpowers c.subtypePermOfSupport)
      (g.subtypePerm (p := Membership.mem c.support) hc')
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 α
hc : c.IsCycle
mp :
  Commute g c →
    ∃ (hc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support),
      Membership.mem (γ := Subgroup (Perm ↥c.support)) (Subgroup.zpowers c.subtypePermOfSupport)
        (g.subtypePerm (p := Membership.mem c.support) hc')
⊢ Commute g c ↔
    ∃ (hc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support),
      Membership.mem (γ := Subgroup (Perm ↥c.support)) (Subgroup.zpowers c.subtypePermOfSupport)
        (g.subtypePerm (p := Membership.mem c.support) hc')
have mpr : (∃ (hc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support),
    Membership.mem (γ := Subgroup (Perm ↥c.support)) (Subgroup.zpowers c.subtypePermOfSupport)
      (g.subtypePerm (p := Membership.mem c.support) hc')) →
  Commute g c
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
g c : Perm α
hc : c.IsCycle
hgc : Commute g c
⊢ ∃ (hc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support),
    Membership.mem (γ := Subgroup (Perm ↥c.support)) (Subgroup.zpowers c.subtypePermOfSupport)
      (g.subtypePerm (p := Membership.mem c.support) hc')
have hgc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support
Tactic: have hgc' := mem_support_iff_of_commute hgc
-- 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
hgc : Commute g c
hgc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support
⊢ ∃ (hc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support),
    Membership.mem (γ := Subgroup (Perm ↥c.support)) (Subgroup.zpowers c.subtypePermOfSupport)
      (g.subtypePerm (p := Membership.mem c.support) hc')
have h : Membership.mem (γ := Subgroup (Perm ↥c.support)) (Subgroup.zpowers c.subtypePermOfSupport)
  (g.subtypePerm (p := Membership.mem c.support) hgc')
Tactic: use hgc'
-- 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
hgc : Commute g c
hgc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support
⊢ Membership.mem (γ := Subgroup (Perm ↥c.support)) (Subgroup.zpowers c.subtypePermOfSupport)
    (g.subtypePerm (p := Membership.mem c.support) hgc')
have h : ∀ (a : α) (ha : a ∈ c.support),
  Membership.mem (γ := Subgroup (Perm ↥c.support)) (Subgroup.zpowers c.subtypePermOfSupport)
    (g.subtypePerm (p := Membership.mem c.support) hgc')
Tactic: obtain ⟨a, ha⟩ := IsCycle.nonempty_support hc
-- 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
hgc : Commute g c
hgc' : ∀ (x : α), Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support
a : α
ha : a ∈ c.support
⊢ Membership.mem (γ := Subgroup (Perm ↥c.support)) (Subgroup.zpowers c.subtypePermOfSupport)
    (g.subtypePerm (p := Membership.mem c.support) hgc')
have 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')
Tactic: obtain ⟨i, hi⟩ := hc.sameCycle (mem_support.mp ha) (mem_support.mp ((hgc' a).mpr 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
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 : α)
⊢ Membership.mem (γ := Subgroup (Perm ↥c.support)) (Subgroup.zpowers c.subtypePermOfSupport)
    (g.subtypePerm (p := Membership.mem c.support) hgc')
have h : (fun (x : ℤ) ↦ HPow.hPow (α := Perm ↥c.support) c.subtypePermOfSupport x) i =
  g.subtypePerm (p := Membership.mem c.support) hgc'
Tactic: use i
-- 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
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 : α)
⊢ (fun (x : ℤ) ↦ HPow.hPow (α := Perm ↥c.support) c.subtypePermOfSupport x) i =
    g.subtypePerm (p := Membership.mem c.support) hgc'
have 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)) :
      α)
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 α
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
⊢ 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)) :
      α)
have h : Eq (α := α)
  ((↑((HPow.hPow (α := Perm ↥c.support) (c.subtypePerm (p := Membership.mem c.support) sorry) i :
            (a : ↥c.support) → ↥c.support)
          (Subtype.mk (p := fun (x : α) ↦ x ∈ c.support) x hx)) :
      α) :
    α)
  ((g : (a : α) → α) x : α)
Tactic: simp only [subtypePermOfSupport, Subtype.coe_mk, 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 α
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
⊢ 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 : α)
have h : Eq (α := α) ((c ^ i : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
Tactic: rw [subtypePerm_apply_zpow_of_mem]
-- 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
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
⊢ Eq (α := α) ((c ^ i : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
have 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 : α) : α)
Tactic: obtain ⟨j, rfl⟩ := hc.sameCycle (mem_support.mp ha) (mem_support.mp hx)
Cleared hypotheses: 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 α
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 : α) → α) ((c ^ j : (a : α) → α) a : α) : α)
    ((g : (a : α) → α) ((c ^ j : (a : α) → α) a : α) : α)
have h : Eq (α := α) ((c ^ i * c ^ j : (a : α) → α) a : α) ((c ^ j * g : (a : α) → α) a : α)
Tactic: simp only [← mul_apply, Commute.eq (Commute.zpow_right hgc j)]
-- 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
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 * c ^ j : (a : α) → α) a : α) ((c ^ j * g : (a : α) → α) a : α)
have h : Eq (α := α) ((c ^ j * c ^ i : (a : α) → α) a : α) ((c ^ j * g : (a : α) → α) a : α)
Tactic: rw [← zpow_add, add_comm i j, zpow_add]
-- 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
i : ℤ
hi :
  (fun (x : ℤ) ↦ HPow.hPow (α := Perm ↥c.support) c.subtypePermOfSupport x) i =
    g.subtypePerm (p := Membership.mem c.support) hc'
⊢ Commute g c
have mpr : ∀ (x : α), Eq (α := α) ((g * c : (a : α) → α) x : α) ((c * g : (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 α
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 : α
⊢ Eq (α := α) ((g * c : (a : α) → α) x : α) ((c * g : (a : α) → α) x : α)
have mpr : Eq (α := α) ((g : (a : α) → α) ((c : (a : α) → α) x : α) : α) ((c : (a : α) → α) ((g : (a : α) → α) x : α) : α)
Tactic: simp only [coe_mul, Function.comp_apply]
-- 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
i : ℤ
hi :
  (fun (x : ℤ) ↦ HPow.hPow (α := Perm ↥c.support) c.subtypePermOfSupport x) i =
    g.subtypePerm (p := Membership.mem c.support) hc'
x : α
⊢ Eq (α := α) ((g : (a : α) → α) ((c : (a : α) → α) x : α) : α) ((c : (a : α) → α) ((g : (a : α) → α) x : α) : α)
have pos : ∀ (hx : x ∈ c.support),
  Eq (α := α) ((g : (a : α) → α) ((c : (a : α) → α) x : α) : α) ((c : (a : α) → α) ((g : (a : α) → α) x : α) : α)
Tactic: by_cases hx : x ∈ 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
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 : α) : α)
⊢ Eq (α := α) ((g : (a : α) → α) ((c : (a : α) → α) x : α) : α) ((c : (a : α) → α) ((g : (a : α) → α) x : α) : α)
have neg : ∀ (hx : x ∉ c.support),
  Eq (α := α) ((g : (a : α) → α) ((c : (a : α) → α) x : α) : α) ((c : (a : α) → α) ((g : (a : α) → α) x : α) : α)
Tactic: by_cases hx : x ∈ 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
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 (α := α) ((g : (a : α) → α) ((c : (a : α) → α) x : α) : α) ((c : (a : α) → α) ((g : (a : α) → α) x : α) : α)
have rw : Eq (α := α) ((c ^ i : (a : α) → α) ((c : (a : α) → α) x : α) : α) ((c : (a : α) → α) ((c ^ i : (a : α) → α) x : α) : α)
Tactic: rw [hi' x hx, hi' (c x) (apply_mem_support.mpr hx)]
-- 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
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
⊢ Eq (α := α) ((g : (a : α) → α) ((c : (a : α) → α) x : α) : α) ((c : (a : α) → α) ((g : (a : α) → α) x : α) : α)
have pos : ∀ x ∈ c.support, Eq (α := α) ((g : (a : α) → α) x : α) ((c ^ i : (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]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
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 (α := α) ((g : (a : α) → α) x : α) ((c ^ i : (a : α) → α) x : α)
have 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)
Tactic: have hix := Perm.congr_fun hi ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
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 (α := α) ((g : (a : α) → α) x : α) ((c ^ i : (a : α) → α) x : α)
have hix₁ : Eq (α := α) ((c ^ i : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
Tactic: simp only [← Subtype.coe_inj, subtypePermOfSupport, subtypePerm_apply,
        subtypePerm_apply_zpow_of_mem] at hix
Cleared hypotheses: hix
-- 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
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
⊢ Eq (α := α) ((g : (a : α) → α) ((c : (a : α) → α) x : α) : α) ((c : (a : α) → α) ((g : (a : α) → α) x : α) : α)
have neg : ((g : (a : α) → α) x : α) ∉ c.support
Tactic: rw [notMem_support.mp hx, eq_comm, ← 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 α
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
⊢ ((g : (a : α) → α) x : α) ∉ c.support
have neg : ∀ (hx : Membership.mem (α := α) c.support ((g : (a : α) → α) x : α)), x ∈ c.support
Tactic: contrapose hx
Cleared hypotheses: hx
-- 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
⊢ 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 α)
have 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) sorry) ↔
  ∃ (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) sorry)
Tactic: simp_rw [hc.commute_iff', Subgroup.mem_zpowers_iff]
-- 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
⊢ (∃ (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) ⋯)
have 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) sorry ↔
    c ^ k =
      (ofSubtype (p := fun (x : α) ↦ x ∈ c.support) : (a : Perm ↥c.support) → Perm α)
        (g.subtypePerm (p := Membership.mem c.support) sorry)
Tactic: refine exists_congr fun hc' => exists_congr fun k => ?_
-- 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 : ℤ
⊢ 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) ⋯)
have rw : (c ^ k).subtypePerm (p := Membership.mem c.support) sorry = g.subtypePerm (p := Membership.mem c.support) sorry ↔
  c ^ k =
    (ofSubtype (p := fun (x : α) ↦ x ∈ c.support) : (a : Perm ↥c.support) → Perm α)
      (g.subtypePerm (p := Membership.mem c.support) sorry)
Tactic: rw [subtypePermOfSupport, subtypePerm_zpow c k]
-- 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 : ℤ
⊢ (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) ⋯)
have 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) sorry) :
              Perm α) :
            (a : α) → α)
          x :
        α)
Tactic: simp only [Perm.ext_iff, subtypePerm_apply, Subtype.mk.injEq, Subtype.forall]
-- 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 : α) (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 :
          α)
have 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) sorry) :
              Perm α) :
            (a : α) → α)
          a :
        α)
Tactic: apply forall_congr'
-- 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 : α
⊢ (∀ (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 : ∀ (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