awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
g : Perm α
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_2 + 1, max 1 (u_3 + 1)} α (Subtype p)
a : α
ha : (g : (a : α) → α) a ≠ a
ha' : ∀ ⦃y : α⦄, (g : (a : α) → α) y ≠ y → g.SameCycle a y
⊢ Ne (α := β) ((g.extendDomain (p := p) f : (a : β) → β) (↑((f : (a : α) → Subtype p) a) : β) : β)
    ((↑((f : (a : α) → Subtype p) a) : β) : β)
have refine_1 : Ne.{u_3 + 1} (α := β) (↑((f : (a : α) → Subtype p) ((g : (a : α) → α) a)) : β) (↑((f : (a : α) → Subtype p) a) : β)
Tactic: rw [extendDomain_apply_image]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
g : Perm α
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_2 + 1, max 1 (u_3 + 1)} α (Subtype p)
a : α
ha : (g : (a : α) → α) a ≠ a
ha' : ∀ ⦃y : α⦄, (g : (a : α) → α) y ≠ y → g.SameCycle a y
b : β
hb : (g.extendDomain (p := p) f : (a : β) → β) b ≠ b
⊢ b = (↑((f : (a : α) → Subtype p) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b ⋯))) : β)
have rw : b = (↑(Subtype.mk (p := p) b sorry) : β)
Tactic: rw [apply_symm_apply, Subtype.coe_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
g : Perm α
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_2 + 1, max 1 (u_3 + 1)} α (Subtype p)
a : α
ha : (g : (a : α) → α) a ≠ a
ha' : ∀ ⦃y : α⦄, (g : (a : α) → α) y ≠ y → g.SameCycle a y
b : β
hb : (g.extendDomain (p := p) f : (a : β) → β) b ≠ b
rw : b = (↑(Subtype.mk (p := p) b ⋯) : β)
⊢ b = (↑((f : (a : α) → Subtype p) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b ⋯))) : β)
have rw₁ : b = b
Tactic: rw [apply_symm_apply, Subtype.coe_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
Goal:
α : Type u_2
β : Type u_3
g : Perm α
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_2 + 1, max 1 (u_3 + 1)} α (Subtype p)
a : α
ha : (g : (a : α) → α) a ≠ a
ha' : ∀ ⦃y : α⦄, (g : (a : α) → α) y ≠ y → g.SameCycle a y
b : β
hb : (g.extendDomain (p := p) f : (a : β) → β) b ≠ b
⊢ (g.extendDomain (p := p) f).SameCycle (↑((f : (a : α) → Subtype p) a) : β) b
have h : b = (↑((f : (a : α) → Subtype p) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b sorry))) : β)
Tactic: have h : b = f (f.symm ⟨b, of_not_not <| hb ∘ extendDomain_apply_not_subtype _ _⟩) := by
    rw [apply_symm_apply, Subtype.coe_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
g : Perm α
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_2 + 1, max 1 (u_3 + 1)} α (Subtype p)
a : α
ha : (g : (a : α) → α) a ≠ a
ha' : ∀ ⦃y : α⦄, (g : (a : α) → α) y ≠ y → g.SameCycle a y
b : β
hb : (g.extendDomain (p := p) f : (a : β) → β) b ≠ b
h : b = (↑((f : (a : α) → Subtype p) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b ⋯))) : β)
⊢ (g.extendDomain (p := p) f).SameCycle (↑((f : (a : α) → Subtype p) a) : β) b
have refine_2 : ∀
  (hb_1 :
    Ne (α := β)
      ((g.extendDomain (p := p) f : (a : β) → β)
          (↑((f : (a : α) → Subtype p) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b sorry))) : β) :
        β)
      ((↑((f : (a : α) → Subtype p) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b sorry))) : β) : β))
  (h : b = (↑((f : (a : α) → Subtype p) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b sorry))) : β)),
  (g.extendDomain (p := p) f).SameCycle (↑((f : (a : α) → Subtype p) a) : β)
    (↑((f : (a : α) → Subtype p) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b sorry))) : β)
Tactic: rw [h] at hb ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
Goal:
α : Type u_2
β : Type u_3
g : Perm α
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_2 + 1, max 1 (u_3 + 1)} α (Subtype p)
a : α
ha : (g : (a : α) → α) a ≠ a
ha' : ∀ ⦃y : α⦄, (g : (a : α) → α) y ≠ y → g.SameCycle a y
b : β
hb_1 : (g.extendDomain (p := p) f : (a : β) → β) b ≠ b
hb :
  Ne (α := β)
    ((g.extendDomain (p := p) f : (a : β) → β)
        (↑((f : (a : α) → Subtype p) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b ⋯))) : β) :
      β)
    ((↑((f : (a : α) → Subtype p) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b ⋯))) : β) : β)
h : b = (↑((f : (a : α) → Subtype p) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b ⋯))) : β)
⊢ (g.extendDomain (p := p) f).SameCycle (↑((f : (a : α) → Subtype p) a) : β)
    (↑((f : (a : α) → Subtype p) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b ⋯))) : β)
have hb₁ : Ne (α := α) ((g : (a : α) → α) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b sorry) : α) : α)
  ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b sorry) : α)
Tactic: simp only [extendDomain_apply_image, Subtype.coe_injective.ne_iff, f.injective.ne_iff] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
Goal:
α : Type u_2
f : Perm α
x : α
hx : (f : (a : α) → α) x ≠ x
hf : f.IsCycle
y : α
h : f.SameCycle x y
hy : (f : (a : α) → α) y = y
i : ℤ
hi : (f ^ i : (a : α) → α) x = y
⊢ (f : (a : α) → α) x = x
have hi₁ : x = y
Tactic: rw [← zpow_apply_eq_self_of_apply_eq_self hy i, (f ^ i).injective.eq_iff] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x : α
hx : (f : (a : α) → α) x ≠ x
hf : f.IsCycle
y : α
h : f.SameCycle x y
hy : (f : (a : α) → α) y = y
i : ℤ
hi : x = y
rw : (f : (a : α) → α) y = y
⊢ (f : (a : α) → α) x = x
have rw₁ : y = y
Tactic: rw [hi, hy]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
inst : Finite α
hf : f.IsCycle
hx : (f : (a : α) → α) x ≠ x
hy : (f : (a : α) → α) y ≠ y
⊢ ∃ (i : ℕ), (f ^ i : (a : α) → α) x = y
have let : ∀ (n : ℤ) (hn : (f ^ n : (a : α) → α) x = y), ∃ (i : ℕ), (f ^ i : (a : α) → α) x = y
Tactic: let ⟨n, hn⟩ := hf.exists_zpow_eq hx hy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
Goal:
α : Type u_2
f : Perm α
x y : α
inst : Finite α
hf : f.IsCycle
hx : (f : (a : α) → α) x ≠ x
hy : (f : (a : α) → α) y ≠ y
n : ℤ
hn : (f ^ n : (a : α) → α) x = y
⊢ (f ^ (n % (↑(orderOf f) : ℤ)).toNat : (a : α) → α) x = y
have this : 0 ≤ n % (↑(orderOf f) : ℤ)
Tactic: have := n.emod_nonneg (Int.natCast_ne_zero.mpr (ne_of_gt (orderOf_pos f)))
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
inst : Finite α
hf : f.IsCycle
hx : (f : (a : α) → α) x ≠ x
hy : (f : (a : α) → α) y ≠ y
n : ℤ
hn : (f ^ n : (a : α) → α) x = y
this : 0 ≤ n % (↑(orderOf f) : ℤ)
⊢ (f ^ (n % (↑(orderOf f) : ℤ)).toNat : (a : α) → α) x = y
have rwa : (HPow.hPow (β := ℤ) f (↑(n % (↑(orderOf f) : ℤ)).toNat : ℤ) : (a : α) → α) x = y
Tactic: rwa [← zpow_natCast, Int.toNat_of_nonneg this, zpow_mod_orderOf]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
inst : Finite α
hf : f.IsCycle
hx : (f : (a : α) → α) x ≠ x
hy : (f : (a : α) → α) y ≠ y
n : ℤ
hn : (f ^ n : (a : α) → α) x = y
this : 0 ≤ n % (↑(orderOf f) : ℤ)
rwa : (HPow.hPow (β := ℤ) f (↑(n % (↑(orderOf f) : ℤ)).toNat : ℤ) : (a : α) → α) x = y
⊢ (f ^ (n % (↑(orderOf f) : ℤ)).toNat : (a : α) → α) x = y
have rwa₁ : (f ^ (n % (↑(orderOf f) : ℤ)) : (a : α) → α) x = y
Tactic: rwa [← zpow_natCast, Int.toNat_of_nonneg this, zpow_mod_orderOf]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
inst : Finite α
hf : f.IsCycle
hx : (f : (a : α) → α) x ≠ x
hy : (f : (a : α) → α) y ≠ y
n : ℤ
hn : (f ^ n : (a : α) → α) x = y
⊢ (f ^ (n % (↑(orderOf f) : ℤ)).toNat : (a : α) → α) x = y
have rwa : ∀ (this : 0 ≤ n % (↑(orderOf f) : ℤ)), (f ^ (n % (↑(orderOf f) : ℤ)).toNat : (a : α) → α) x = y
Tactic: {have := n.emod_nonneg (Int.natCast_ne_zero.mpr (ne_of_gt (orderOf_pos f)))
         rwa [← zpow_natCast, Int.toNat_of_nonneg this, zpow_mod_orderOf]}
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
hxy : x ≠ y
a : α
ha : (if a = x then y else if a = y then x else a) ≠ a
hya : ¬y = a
⊢ (HPow.hPow (β := ℤ) (swap x y) 1 : (a : α) → α) y = a
have rw : (if y = x then y else if y = y then x else y) = a
Tactic: rw [zpow_one, swap_apply_def]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
hxy : x ≠ y
a : α
ha : (if a = x then y else if a = y then x else a) ≠ a
hya : ¬y = a
⊢ (if y = x then y else if y = y then x else y) = a
have pos : y = x → a = x → ∀ (ha : y ≠ a), y = a
Tactic: split_ifs at *
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
hxy : x ≠ y
a : α
ha : (if a = x then y else if a = y then x else a) ≠ a
hya : ¬y = a
pos : y = x → a = x → ∀ (ha : y ≠ a), y = a
⊢ (if y = x then y else if y = y then x else y) = a
have pos₁ : y = x → ¬a = x → a = y → ∀ (ha : x ≠ a), y = a
Tactic: split_ifs at *
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
hxy : x ≠ y
a : α
ha : (if a = x then y else if a = y then x else a) ≠ a
hya : ¬y = a
pos : y = x → a = x → ∀ (ha : y ≠ a), y = a
pos₁ : y = x → ¬a = x → a = y → ∀ (ha : x ≠ a), y = a
⊢ (if y = x then y else if y = y then x else y) = a
have neg : y = x → ¬a = x → ¬a = y → ∀ (ha : a ≠ a), y = a
Tactic: split_ifs at *
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
hxy : x ≠ y
a : α
ha : (if a = x then y else if a = y then x else a) ≠ a
hya : ¬y = a
pos : y = x → a = x → ∀ (ha : y ≠ a), y = a
pos₁ : y = x → ¬a = x → a = y → ∀ (ha : x ≠ a), y = a
neg : y = x → ¬a = x → ¬a = y → ∀ (ha : a ≠ a), y = a
⊢ (if y = x then y else if y = y then x else y) = a
have pos₂ : ¬y = x → y = y → a = x → ∀ (ha : y ≠ a), x = a
Tactic: split_ifs at *
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
hxy : x ≠ y
a : α
ha : (if a = x then y else if a = y then x else a) ≠ a
hya : ¬y = a
pos : y = x → a = x → ∀ (ha : y ≠ a), y = a
pos₁ : y = x → ¬a = x → a = y → ∀ (ha : x ≠ a), y = a
neg : y = x → ¬a = x → ¬a = y → ∀ (ha : a ≠ a), y = a
pos₂ : ¬y = x → y = y → a = x → ∀ (ha : y ≠ a), x = a
⊢ (if y = x then y else if y = y then x else y) = a
have pos₃ : ¬y = x → y = y → ¬a = x → a = y → ∀ (ha : x ≠ a), x = a
Tactic: split_ifs at *
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
hxy : x ≠ y
a : α
ha : (if a = x then y else if a = y then x else a) ≠ a
hya : ¬y = a
pos : y = x → a = x → ∀ (ha : y ≠ a), y = a
pos₁ : y = x → ¬a = x → a = y → ∀ (ha : x ≠ a), y = a
neg : y = x → ¬a = x → ¬a = y → ∀ (ha : a ≠ a), y = a
pos₂ : ¬y = x → y = y → a = x → ∀ (ha : y ≠ a), x = a
pos₃ : ¬y = x → y = y → ¬a = x → a = y → ∀ (ha : x ≠ a), x = a
⊢ (if y = x then y else if y = y then x else y) = a
have neg₁ : ¬y = x → y = y → ¬a = x → ¬a = y → ∀ (ha : a ≠ a), x = a
Tactic: split_ifs at *
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
hxy : x ≠ y
a : α
ha : (if a = x then y else if a = y then x else a) ≠ a
hya : ¬y = a
pos : y = x → a = x → ∀ (ha : y ≠ a), y = a
pos₁ : y = x → ¬a = x → a = y → ∀ (ha : x ≠ a), y = a
neg : y = x → ¬a = x → ¬a = y → ∀ (ha : a ≠ a), y = a
pos₂ : ¬y = x → y = y → a = x → ∀ (ha : y ≠ a), x = a
pos₃ : ¬y = x → y = y → ¬a = x → a = y → ∀ (ha : x ≠ a), x = a
neg₁ : ¬y = x → y = y → ¬a = x → ¬a = y → ∀ (ha : a ≠ a), x = a
⊢ (if y = x then y else if y = y then x else y) = a
have pos₄ : ¬y = x → ¬y = y → a = x → ∀ (ha : y ≠ a), y = a
Tactic: split_ifs at *
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
hxy : x ≠ y
a : α
ha : (if a = x then y else if a = y then x else a) ≠ a
hya : ¬y = a
pos : y = x → a = x → ∀ (ha : y ≠ a), y = a
pos₁ : y = x → ¬a = x → a = y → ∀ (ha : x ≠ a), y = a
neg : y = x → ¬a = x → ¬a = y → ∀ (ha : a ≠ a), y = a
pos₂ : ¬y = x → y = y → a = x → ∀ (ha : y ≠ a), x = a
pos₃ : ¬y = x → y = y → ¬a = x → a = y → ∀ (ha : x ≠ a), x = a
neg₁ : ¬y = x → y = y → ¬a = x → ¬a = y → ∀ (ha : a ≠ a), x = a
pos₄ : ¬y = x → ¬y = y → a = x → ∀ (ha : y ≠ a), y = a
⊢ (if y = x then y else if y = y then x else y) = a
have pos₅ : ¬y = x → ¬y = y → ¬a = x → a = y → ∀ (ha : x ≠ a), y = a
Tactic: split_ifs at *
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
x y : α
inst : DecidableEq α
hxy : x ≠ y
a : α
ha : (if a = x then y else if a = y then x else a) ≠ a
hya : ¬y = a
pos : y = x → a = x → ∀ (ha : y ≠ a), y = a
pos₁ : y = x → ¬a = x → a = y → ∀ (ha : x ≠ a), y = a
neg : y = x → ¬a = x → ¬a = y → ∀ (ha : a ≠ a), y = a
pos₂ : ¬y = x → y = y → a = x → ∀ (ha : y ≠ a), x = a
pos₃ : ¬y = x → y = y → ¬a = x → a = y → ∀ (ha : x ≠ a), x = a
neg₁ : ¬y = x → y = y → ¬a = x → ¬a = y → ∀ (ha : a ≠ a), x = a
pos₄ : ¬y = x → ¬y = y → a = x → ∀ (ha : y ≠ a), y = a
pos₅ : ¬y = x → ¬y = y → ¬a = x → a = y → ∀ (ha : x ≠ a), y = a
⊢ (if y = x then y else if y = y then x else y) = a
have neg₂ : ¬y = x → ¬y = y → ¬a = x → ¬a = y → ∀ (ha : a ≠ a), y = a
Tactic: split_ifs at *
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
a b : α
⊢ (swap a b).IsSwap ↔ a ≠ b
have mp : (swap a b).IsSwap → a ≠ b
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
a b : α
mp : (swap a b).IsSwap → a ≠ b
⊢ (swap a b).IsSwap ↔ a ≠ b
have mpr : a ≠ b → (swap a b).IsSwap
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
a b : α
h : (swap a b).IsSwap
hab : a = b
⊢ False
have mp : swap a b = 1
Tactic: apply h.isCycle.ne_one
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
a b : α
h : a ≠ b
w w₁ : α
⊢ (swap a b).IsSwap
have h₁ : a ≠ b ∧ swap a b = swap a b
Tactic: use a, b
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y : α
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
hσ : σ.IsCycle
τ : (↑(↑(Subgroup.zpowers σ) : Set (Perm α)) : Type u_2)
⊢ Membership.mem (α := α) σ.support
    (((↑τ : Perm α) : (a : α) → α)
        (Classical.choose (p := fun (x : α) ↦
          (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) :
      α)
have obtain : ∀ (n : ℤ),
  ((↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ (↑(Subgroup.zpowers σ) : Set (Perm α))) ((fun (x : ℤ) ↦ σ ^ x) n) sorry) :
          Perm α) :
        (a : α) → α)
      (Classical.choose (p := fun (x : α) ↦
        (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) ∈
    σ.support
Tactic: obtain ⟨τ, n, rfl⟩ := τ
Cleared hypotheses: τ
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y : α
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
hσ : σ.IsCycle
n : ℤ
⊢ ((↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ (↑(Subgroup.zpowers σ) : Set (Perm α))) ((fun (x : ℤ) ↦ σ ^ x) n) ⋯) :
          Perm α) :
        (a : α) → α)
      (Classical.choose (p := fun (x : α) ↦
        (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) ∈
    σ.support
have rw : (σ : (a : α) → α)
    (Classical.choose (p := fun (x : α) ↦
      (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ) ≠
  Classical.choose (p := fun (x : α) ↦ (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y)
    hσ
Tactic: rw [Subtype.coe_mk, zpow_apply_mem_support, mem_support]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y : α
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
hσ : σ.IsCycle
⊢ Bijective (β := ↥σ.support) fun (τ : (↑(↑(Subgroup.zpowers σ) : Set (Perm α)) : Type u_2)) ↦
    Subtype.mk (p := fun (x : α) ↦ x ∈ σ.support)
      (((↑τ : Perm α) : (a : α) → α)
        (Classical.choose (p := fun (x : α) ↦
          (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ))
      ⋯
have left : Injective (β := ↥σ.support) fun (τ : (↑(↑(Subgroup.zpowers σ) : Set (Perm α)) : Type u_2)) ↦
  Subtype.mk (p := fun (x : α) ↦ x ∈ σ.support)
    (((↑τ : Perm α) : (a : α) → α)
      (Classical.choose (p := fun (x : α) ↦
        (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ))
    sorry
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y : α
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
hσ : σ.IsCycle
left :
  Injective (β := ↥σ.support) fun (τ : (↑(↑(Subgroup.zpowers σ) : Set (Perm α)) : Type u_2)) ↦
    Subtype.mk (p := fun (x : α) ↦ x ∈ σ.support)
      (((↑τ : Perm α) : (a : α) → α)
        (Classical.choose (p := fun (x : α) ↦
          (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ))
      ⋯
⊢ Bijective (β := ↥σ.support) fun (τ : (↑(↑(Subgroup.zpowers σ) : Set (Perm α)) : Type u_2)) ↦
    Subtype.mk (p := fun (x : α) ↦ x ∈ σ.support)
      (((↑τ : Perm α) : (a : α) → α)
        (Classical.choose (p := fun (x : α) ↦
          (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ))
      ⋯
have right : Surjective (β := ↥σ.support) fun (τ : (↑(↑(Subgroup.zpowers σ) : Set (Perm α)) : Type u_2)) ↦
  Subtype.mk (p := fun (x : α) ↦ x ∈ σ.support)
    (((↑τ : Perm α) : (a : α) → α)
      (Classical.choose (p := fun (x : α) ↦
        (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ))
    sorry
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y : α
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
hσ : σ.IsCycle
m n : ℤ
h :
  Eq.{u_2 + 1} (α := ↥σ.support)
    ((fun (τ : (↑(↑(Subgroup.zpowers σ) : Set (Perm α)) : Type u_2)) ↦
        (Subtype.mk (p := fun (x : α) ↦ x ∈ σ.support)
            (((↑τ : Perm α) : (a : α) → α)
              (Classical.choose (p := fun (x : α) ↦
                (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ))
            ⋯ :
          ↥σ.support))
      (Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
        ((fun (x : ℤ) ↦ σ ^ x) m) ⋯))
    ((fun (τ : (↑(↑(Subgroup.zpowers σ) : Set (Perm α)) : Type u_2)) ↦
        (Subtype.mk (p := fun (x : α) ↦ x ∈ σ.support)
            (((↑τ : Perm α) : (a : α) → α)
              (Classical.choose (p := fun (x : α) ↦
                (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ))
            ⋯ :
          ↥σ.support))
      (Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
        ((fun (x : ℤ) ↦ σ ^ x) n) ⋯))
⊢ Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
      ((fun (x : ℤ) ↦ σ ^ x) m) ⋯ =
    Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
      ((fun (x : ℤ) ↦ σ ^ x) n) ⋯
have left : ∀ (y : α),
  Eq (α := α)
    (((↑(Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
                ((fun (x : ℤ) ↦ σ ^ x) m) sorry) :
            Perm α) :
          (a : α) → α)
        y :
      α)
    (((↑(Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
                ((fun (x : ℤ) ↦ σ ^ x) n) sorry) :
            Perm α) :
          (a : α) → α)
        y :
      α)
Tactic: ext y
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y_1 : α
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
hσ : σ.IsCycle
m n : ℤ
h :
  Eq.{u_2 + 1} (α := ↥σ.support)
    ((fun (τ : (↑(↑(Subgroup.zpowers σ) : Set (Perm α)) : Type u_2)) ↦
        (Subtype.mk (p := fun (x : α) ↦ x ∈ σ.support)
            (((↑τ : Perm α) : (a : α) → α)
              (Classical.choose (p := fun (x : α) ↦
                (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ))
            ⋯ :
          ↥σ.support))
      (Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
        ((fun (x : ℤ) ↦ σ ^ x) m) ⋯))
    ((fun (τ : (↑(↑(Subgroup.zpowers σ) : Set (Perm α)) : Type u_2)) ↦
        (Subtype.mk (p := fun (x : α) ↦ x ∈ σ.support)
            (((↑τ : Perm α) : (a : α) → α)
              (Classical.choose (p := fun (x : α) ↦
                (σ : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (σ : (a : α) → α) y ≠ y → σ.SameCycle x y) hσ))
            ⋯ :
          ↥σ.support))
      (Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
        ((fun (x : ℤ) ↦ σ ^ x) n) ⋯))
y : α
⊢ Eq (α := α)
    (((↑(Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
                ((fun (x : ℤ) ↦ σ ^ x) m) ⋯) :
            Perm α) :
          (a : α) → α)
        y :
      α)
    (((↑(Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
                ((fun (x : ℤ) ↦ σ ^ x) n) ⋯) :
            Perm α) :
          (a : α) → α)
        y :
      α)
have pos : ∀ (hy : (σ : (a : α) → α) y = y),
  Eq (α := α)
    (((↑(Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
                ((fun (x : ℤ) ↦ σ ^ x) m) sorry) :
            Perm α) :
          (a : α) → α)
        y :
      α)
    (((↑(Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.zpowers σ) x)
                ((fun (x : ℤ) ↦ σ ^ x) n) sorry) :
            Perm α) :
          (a : α) → α)
        y :
      α)
Tactic: by_cases hy : σ y = y