awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
h : f.SameCycle x y
i : ℤ
hi : (f ^ i : (a : α) → α) x = y
⊢ (f : (a : α) → α) x = x ↔ (f : (a : α) → α) y = y
have rw : (f : (a : α) → α) x = x ↔
  Eq (α := α) ((f : (a : α) → α) ((f ^ i : (a : α) → α) x : α) : α) ((f ^ i : (a : α) → α) x : α)
Tactic: rw [← hi, ← mul_apply, ← zpow_one_add, add_comm, zpow_add_one, mul_apply,
    (f ^ i).injective.eq_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
h : f.SameCycle x y
i : ℤ
hi : (f ^ i : (a : α) → α) x = y
rw :
  (f : (a : α) → α) x = x ↔
    Eq (α := α) ((f : (a : α) → α) ((f ^ i : (a : α) → α) x : α) : α) ((f ^ i : (a : α) → α) x : α)
⊢ (f : (a : α) → α) x = x ↔ (f : (a : α) → α) y = y
have rw₁ : (f : (a : α) → α) x = x ↔ Eq (α := α) ((f * f ^ i : (a : α) → α) x : α) ((f ^ i : (a : α) → α) x : α)
Tactic: rw [← hi, ← mul_apply, ← zpow_one_add, add_comm, zpow_add_one, mul_apply,
    (f ^ i).injective.eq_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
h : f.SameCycle x y
i : ℤ
hi : (f ^ i : (a : α) → α) x = y
rw :
  (f : (a : α) → α) x = x ↔
    Eq (α := α) ((f : (a : α) → α) ((f ^ i : (a : α) → α) x : α) : α) ((f ^ i : (a : α) → α) x : α)
rw₁ : (f : (a : α) → α) x = x ↔ Eq (α := α) ((f * f ^ i : (a : α) → α) x : α) ((f ^ i : (a : α) → α) x : α)
⊢ (f : (a : α) → α) x = x ↔ (f : (a : α) → α) y = y
have rw₂ : (f : (a : α) → α) x = x ↔ Eq (α := α) ((f ^ (1 + i) : (a : α) → α) x : α) ((f ^ i : (a : α) → α) x : α)
Tactic: rw [← hi, ← mul_apply, ← zpow_one_add, add_comm, zpow_add_one, mul_apply,
    (f ^ i).injective.eq_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
h : f.SameCycle x y
i : ℤ
hi : (f ^ i : (a : α) → α) x = y
rw :
  (f : (a : α) → α) x = x ↔
    Eq (α := α) ((f : (a : α) → α) ((f ^ i : (a : α) → α) x : α) : α) ((f ^ i : (a : α) → α) x : α)
rw₁ : (f : (a : α) → α) x = x ↔ Eq (α := α) ((f * f ^ i : (a : α) → α) x : α) ((f ^ i : (a : α) → α) x : α)
rw₂ : (f : (a : α) → α) x = x ↔ Eq (α := α) ((f ^ (1 + i) : (a : α) → α) x : α) ((f ^ i : (a : α) → α) x : α)
⊢ (f : (a : α) → α) x = x ↔ (f : (a : α) → α) y = y
have rw₃ : (f : (a : α) → α) x = x ↔ Eq (α := α) ((f ^ (i + 1) : (a : α) → α) x : α) ((f ^ i : (a : α) → α) x : α)
Tactic: rw [← hi, ← mul_apply, ← zpow_one_add, add_comm, zpow_add_one, mul_apply,
    (f ^ i).injective.eq_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
h : f.SameCycle x y
i : ℤ
hi : (f ^ i : (a : α) → α) x = y
rw :
  (f : (a : α) → α) x = x ↔
    Eq (α := α) ((f : (a : α) → α) ((f ^ i : (a : α) → α) x : α) : α) ((f ^ i : (a : α) → α) x : α)
rw₁ : (f : (a : α) → α) x = x ↔ Eq (α := α) ((f * f ^ i : (a : α) → α) x : α) ((f ^ i : (a : α) → α) x : α)
rw₂ : (f : (a : α) → α) x = x ↔ Eq (α := α) ((f ^ (1 + i) : (a : α) → α) x : α) ((f ^ i : (a : α) → α) x : α)
rw₃ : (f : (a : α) → α) x = x ↔ Eq (α := α) ((f ^ (i + 1) : (a : α) → α) x : α) ((f ^ i : (a : α) → α) x : α)
⊢ (f : (a : α) → α) x = x ↔ (f : (a : α) → α) y = y
have rw₄ : (f : (a : α) → α) x = x ↔ Eq (α := α) ((f ^ i * f : (a : α) → α) x : α) ((f ^ i : (a : α) → α) x : α)
Tactic: rw [← hi, ← mul_apply, ← zpow_one_add, add_comm, zpow_add_one, mul_apply,
    (f ^ i).injective.eq_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
h : f.SameCycle x y
i : ℤ
hi : (f ^ i : (a : α) → α) x = y
rw :
  (f : (a : α) → α) x = x ↔
    Eq (α := α) ((f : (a : α) → α) ((f ^ i : (a : α) → α) x : α) : α) ((f ^ i : (a : α) → α) x : α)
rw₁ : (f : (a : α) → α) x = x ↔ Eq (α := α) ((f * f ^ i : (a : α) → α) x : α) ((f ^ i : (a : α) → α) x : α)
rw₂ : (f : (a : α) → α) x = x ↔ Eq (α := α) ((f ^ (1 + i) : (a : α) → α) x : α) ((f ^ i : (a : α) → α) x : α)
rw₃ : (f : (a : α) → α) x = x ↔ Eq (α := α) ((f ^ (i + 1) : (a : α) → α) x : α) ((f ^ i : (a : α) → α) x : α)
rw₄ : (f : (a : α) → α) x = x ↔ Eq (α := α) ((f ^ i * f : (a : α) → α) x : α) ((f ^ i : (a : α) → α) x : α)
⊢ (f : (a : α) → α) x = x ↔ (f : (a : α) → α) y = y
have rw₅ : (f : (a : α) → α) x = x ↔
  Eq (α := α) ((f ^ i : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f ^ i : (a : α) → α) x : α)
Tactic: rw [← hi, ← mul_apply, ← zpow_one_add, add_comm, zpow_add_one, mul_apply,
    (f ^ i).injective.eq_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
h : f.SameCycle x y
i : ℤ
hi : (f ^ i : (a : α) → α) x = y
rw :
  (f : (a : α) → α) x = x ↔
    Eq (α := α) ((f : (a : α) → α) ((f ^ i : (a : α) → α) x : α) : α) ((f ^ i : (a : α) → α) x : α)
rw₁ : (f : (a : α) → α) x = x ↔ Eq (α := α) ((f * f ^ i : (a : α) → α) x : α) ((f ^ i : (a : α) → α) x : α)
rw₂ : (f : (a : α) → α) x = x ↔ Eq (α := α) ((f ^ (1 + i) : (a : α) → α) x : α) ((f ^ i : (a : α) → α) x : α)
rw₃ : (f : (a : α) → α) x = x ↔ Eq (α := α) ((f ^ (i + 1) : (a : α) → α) x : α) ((f ^ i : (a : α) → α) x : α)
rw₄ : (f : (a : α) → α) x = x ↔ Eq (α := α) ((f ^ i * f : (a : α) → α) x : α) ((f ^ i : (a : α) → α) x : α)
rw₅ :
  (f : (a : α) → α) x = x ↔
    Eq (α := α) ((f ^ i : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f ^ i : (a : α) → α) x : α)
⊢ (f : (a : α) → α) x = x ↔ (f : (a : α) → α) y = y
have rw₆ : (f : (a : α) → α) x = x ↔ (f : (a : α) → α) x = x
Tactic: rw [← hi, ← mul_apply, ← zpow_one_add, add_comm, zpow_add_one, mul_apply,
    (f ^ i).injective.eq_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
⊢ f.SameCycle x ((f : (a : α) → α) y) ↔ f.SameCycle x y
have rw : f.SameCycle ((f : (a : α) → α) y) x ↔ f.SameCycle x y
Tactic: rw [sameCycle_comm, sameCycle_apply_left, sameCycle_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
rw : f.SameCycle ((f : (a : α) → α) y) x ↔ f.SameCycle x y
⊢ f.SameCycle x ((f : (a : α) → α) y) ↔ f.SameCycle x y
have rw₁ : f.SameCycle y x ↔ f.SameCycle x y
Tactic: rw [sameCycle_comm, sameCycle_apply_left, sameCycle_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
rw : f.SameCycle ((f : (a : α) → α) y) x ↔ f.SameCycle x y
rw₁ : f.SameCycle y x ↔ f.SameCycle x y
⊢ f.SameCycle x ((f : (a : α) → α) y) ↔ f.SameCycle x y
have rw₂ : f.SameCycle x y ↔ f.SameCycle x y
Tactic: rw [sameCycle_comm, sameCycle_apply_left, sameCycle_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
⊢ f.SameCycle ((Equiv.symm f : (a : α) → α) x) y ↔ f.SameCycle x y
have rw : f.SameCycle ((f : (a : α) → α) ((Equiv.symm f : (a : α) → α) x : α)) y ↔ f.SameCycle x y
Tactic: rw [← sameCycle_apply_left, apply_symm_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
rw : f.SameCycle ((f : (a : α) → α) ((Equiv.symm f : (a : α) → α) x : α)) y ↔ f.SameCycle x y
⊢ f.SameCycle ((Equiv.symm f : (a : α) → α) x) y ↔ f.SameCycle x y
have rw₁ : f.SameCycle x y ↔ f.SameCycle x y
Tactic: rw [← sameCycle_apply_left, apply_symm_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
⊢ f.SameCycle x ((Equiv.symm f : (a : α) → α) y) ↔ f.SameCycle x y
have rw : f.SameCycle x ((f : (a : α) → α) ((Equiv.symm f : (a : α) → α) y : α)) ↔ f.SameCycle x y
Tactic: rw [← sameCycle_apply_right, apply_symm_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
rw : f.SameCycle x ((f : (a : α) → α) ((Equiv.symm f : (a : α) → α) y : α)) ↔ f.SameCycle x y
⊢ f.SameCycle x ((Equiv.symm f : (a : α) → α) y) ↔ f.SameCycle x y
have rw₁ : f.SameCycle x y ↔ f.SameCycle x y
Tactic: rw [← sameCycle_apply_right, apply_symm_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
n : ℤ
⊢ f.SameCycle x ((f ^ n : (a : α) → α) y) ↔ f.SameCycle x y
have rw : f.SameCycle ((f ^ n : (a : α) → α) y) x ↔ f.SameCycle x y
Tactic: rw [sameCycle_comm, sameCycle_zpow_left, sameCycle_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
n : ℤ
rw : f.SameCycle ((f ^ n : (a : α) → α) y) x ↔ f.SameCycle x y
⊢ f.SameCycle x ((f ^ n : (a : α) → α) y) ↔ f.SameCycle x y
have rw₁ : f.SameCycle y x ↔ f.SameCycle x y
Tactic: rw [sameCycle_comm, sameCycle_zpow_left, sameCycle_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
n : ℤ
rw : f.SameCycle ((f ^ n : (a : α) → α) y) x ↔ f.SameCycle x y
rw₁ : f.SameCycle y x ↔ f.SameCycle x y
⊢ f.SameCycle x ((f ^ n : (a : α) → α) y) ↔ f.SameCycle x y
have rw₂ : f.SameCycle x y ↔ f.SameCycle x y
Tactic: rw [sameCycle_comm, sameCycle_zpow_left, sameCycle_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
n : ℕ
⊢ f.SameCycle ((f ^ n : (a : α) → α) x) y ↔ f.SameCycle x y
have rw : f.SameCycle ((HPow.hPow (β := ℤ) f (↑n : ℤ) : (a : α) → α) x) y ↔ f.SameCycle x y
Tactic: rw [← zpow_natCast, sameCycle_zpow_left]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
n : ℕ
rw : f.SameCycle ((HPow.hPow (β := ℤ) f (↑n : ℤ) : (a : α) → α) x) y ↔ f.SameCycle x y
⊢ f.SameCycle ((f ^ n : (a : α) → α) x) y ↔ f.SameCycle x y
have rw₁ : f.SameCycle x y ↔ f.SameCycle x y
Tactic: rw [← zpow_natCast, sameCycle_zpow_left]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
n : ℕ
⊢ f.SameCycle x ((f ^ n : (a : α) → α) y) ↔ f.SameCycle x y
have rw : f.SameCycle x ((HPow.hPow (β := ℤ) f (↑n : ℤ) : (a : α) → α) y) ↔ f.SameCycle x y
Tactic: rw [← zpow_natCast, sameCycle_zpow_right]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
n : ℕ
rw : f.SameCycle x ((HPow.hPow (β := ℤ) f (↑n : ℤ) : (a : α) → α) y) ↔ f.SameCycle x y
⊢ f.SameCycle x ((f ^ n : (a : α) → α) y) ↔ f.SameCycle x y
have rw₁ : f.SameCycle x y ↔ f.SameCycle x y
Tactic: rw [← zpow_natCast, sameCycle_zpow_right]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
g : Perm α
x y : α
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_2 + 1, max 1 (u_3 + 1)} α (Subtype p)
n : ℤ
⊢ Eq (α := β) ((g.extendDomain (p := p) f ^ n : (a : β) → β) (↑((f : (a : α) → Subtype p) x) : β) : β)
      ((↑((f : (a : α) → Subtype p) y) : β) : β) ↔
    (g ^ n : (a : α) → α) x = y
have rw : Eq (α := β) (((g ^ n).extendDomain (p := p) f : (a : β) → β) (↑((f : (a : α) → Subtype p) x) : β) : β)
    ((↑((f : (a : α) → Subtype p) y) : β) : β) ↔
  (g ^ n : (a : α) → α) x = y
Tactic: rw [← extendDomain_zpow, extendDomain_apply_image, Subtype.coe_inj, f.injective.eq_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
g : Perm α
x y : α
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_2 + 1, max 1 (u_3 + 1)} α (Subtype p)
n : ℤ
rw :
  Eq (α := β) (((g ^ n).extendDomain (p := p) f : (a : β) → β) (↑((f : (a : α) → Subtype p) x) : β) : β)
      ((↑((f : (a : α) → Subtype p) y) : β) : β) ↔
    (g ^ n : (a : α) → α) x = y
⊢ Eq (α := β) ((g.extendDomain (p := p) f ^ n : (a : β) → β) (↑((f : (a : α) → Subtype p) x) : β) : β)
      ((↑((f : (a : α) → Subtype p) y) : β) : β) ↔
    (g ^ n : (a : α) → α) x = y
have rw₁ : Eq.{u_3 + 1} (α := β) (↑((f : (a : α) → Subtype p) ((g ^ n : (a : α) → α) x)) : β)
    (↑((f : (a : α) → Subtype p) y) : β) ↔
  (g ^ n : (a : α) → α) x = y
Tactic: rw [← extendDomain_zpow, extendDomain_apply_image, Subtype.coe_inj, f.injective.eq_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
g : Perm α
x y : α
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_2 + 1, max 1 (u_3 + 1)} α (Subtype p)
n : ℤ
rw :
  Eq (α := β) (((g ^ n).extendDomain (p := p) f : (a : β) → β) (↑((f : (a : α) → Subtype p) x) : β) : β)
      ((↑((f : (a : α) → Subtype p) y) : β) : β) ↔
    (g ^ n : (a : α) → α) x = y
rw₁ :
  Eq.{u_3 + 1} (α := β) (↑((f : (a : α) → Subtype p) ((g ^ n : (a : α) → α) x)) : β)
      (↑((f : (a : α) → Subtype p) y) : β) ↔
    (g ^ n : (a : α) → α) x = y
⊢ Eq (α := β) ((g.extendDomain (p := p) f ^ n : (a : β) → β) (↑((f : (a : α) → Subtype p) x) : β) : β)
      ((↑((f : (a : α) → Subtype p) y) : β) : β) ↔
    (g ^ n : (a : α) → α) x = y
have rw₂ : Eq.{max 1 (u_3 + 1)} (α := Subtype p) ((f : (a : α) → Subtype p) ((g ^ n : (a : α) → α) x) : Subtype p)
    ((f : (a : α) → Subtype p) y : Subtype p) ↔
  (g ^ n : (a : α) → α) x = y
Tactic: rw [← extendDomain_zpow, extendDomain_apply_image, Subtype.coe_inj, f.injective.eq_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
g : Perm α
x y : α
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_2 + 1, max 1 (u_3 + 1)} α (Subtype p)
n : ℤ
rw :
  Eq (α := β) (((g ^ n).extendDomain (p := p) f : (a : β) → β) (↑((f : (a : α) → Subtype p) x) : β) : β)
      ((↑((f : (a : α) → Subtype p) y) : β) : β) ↔
    (g ^ n : (a : α) → α) x = y
rw₁ :
  Eq.{u_3 + 1} (α := β) (↑((f : (a : α) → Subtype p) ((g ^ n : (a : α) → α) x)) : β)
      (↑((f : (a : α) → Subtype p) y) : β) ↔
    (g ^ n : (a : α) → α) x = y
rw₂ :
  Eq.{max 1 (u_3 + 1)} (α := Subtype p) ((f : (a : α) → Subtype p) ((g ^ n : (a : α) → α) x) : Subtype p)
      ((f : (a : α) → Subtype p) y : Subtype p) ↔
    (g ^ n : (a : α) → α) x = y
⊢ Eq (α := β) ((g.extendDomain (p := p) f ^ n : (a : β) → β) (↑((f : (a : α) → Subtype p) x) : β) : β)
      ((↑((f : (a : α) → Subtype p) y) : β) : β) ↔
    (g ^ n : (a : α) → α) x = y
have rw₃ : (g ^ n : (a : α) → α) x = y ↔ (g ^ n : (a : α) → α) x = y
Tactic: rw [← extendDomain_zpow, extendDomain_apply_image, Subtype.coe_inj, f.injective.eq_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x : α
inst : Finite α
k : ℤ
⊢ ∃ i < orderOf f, Eq (α := α) ((f ^ i : (a : α) → α) x : α) ((f ^ k : (a : α) → α) x : α)
have h : (k % (↑(orderOf f) : ℤ)).natAbs < orderOf f ∧
  Eq (α := α) ((f ^ (k % (↑(orderOf f) : ℤ)).natAbs : (a : α) → α) x : α) ((f ^ k : (a : α) → α) x : α)
Tactic: use (k % orderOf f).natAbs
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
Goal:
α : Type u_2
f : Perm α
x : α
inst : Finite α
k : ℤ
⊢ (k % (↑(orderOf f) : ℤ)).natAbs < orderOf f ∧
    Eq (α := α) ((f ^ (k % (↑(orderOf f) : ℤ)).natAbs : (a : α) → α) x : α) ((f ^ k : (a : α) → α) x : α)
have h₀ : LT.lt (α := ℤ) 0 (↑(orderOf f) : ℤ)
Tactic: have h₀ := Int.natCast_pos.mpr (orderOf_pos f)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
Goal:
α : Type u_2
f : Perm α
x : α
inst : Finite α
k : ℤ
h₀ : LT.lt (α := ℤ) 0 (↑(orderOf f) : ℤ)
⊢ (k % (↑(orderOf f) : ℤ)).natAbs < orderOf f ∧
    Eq (α := α) ((f ^ (k % (↑(orderOf f) : ℤ)).natAbs : (a : α) → α) x : α) ((f ^ k : (a : α) → α) x : α)
have h₁ : 0 ≤ k % (↑(orderOf f) : ℤ)
Tactic: have h₁ := Int.emod_nonneg k h₀.ne'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x : α
inst : Finite α
k : ℤ
h₀ : LT.lt (α := ℤ) 0 (↑(orderOf f) : ℤ)
h₁ : 0 ≤ k % (↑(orderOf f) : ℤ)
⊢ (k % (↑(orderOf f) : ℤ)).natAbs < orderOf f ∧
    Eq (α := α) ((f ^ (k % (↑(orderOf f) : ℤ)).natAbs : (a : α) → α) x : α) ((f ^ k : (a : α) → α) x : α)
have h : (k % (↑(orderOf f) : ℤ)).natAbs < orderOf f ∧ Eq (α := α) ((f ^ k : (a : α) → α) x : α) ((f ^ k : (a : α) → α) x : α)
Tactic: rw [← zpow_natCast, Int.natAbs_of_nonneg h₁, zpow_mod_orderOf]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x : α
inst : Finite α
k : ℤ
h₀ : LT.lt (α := ℤ) 0 (↑(orderOf f) : ℤ)
h₁ : 0 ≤ k % (↑(orderOf f) : ℤ)
⊢ (k % (↑(orderOf f) : ℤ)).natAbs < orderOf f ∧ Eq (α := α) ((f ^ k : (a : α) → α) x : α) ((f ^ k : (a : α) → α) x : α)
have h : (k % (↑(orderOf f) : ℤ)).natAbs < orderOf f
Tactic: refine ⟨?_, by rfl⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x : α
inst : Finite α
k : ℤ
h₀ : LT.lt (α := ℤ) 0 (↑(orderOf f) : ℤ)
h₁ : 0 ≤ k % (↑(orderOf f) : ℤ)
⊢ (k % (↑(orderOf f) : ℤ)).natAbs < orderOf f
have h : k % (↑(orderOf f) : ℤ) < (↑(orderOf f) : ℤ)
Tactic: rw [← Int.ofNat_lt, Int.natAbs_of_nonneg h₁]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
inst : Finite α
h : f.SameCycle x y
⊢ ∃ (i : ℕ), 0 < i ∧ i ≤ orderOf f ∧ (f ^ i : (a : α) → α) x = y
have zero : ∀ (hi : 0 < orderOf f) (h : f.SameCycle x ((HPow.hPow (β := ℕ) f 0 : (a : α) → α) x)),
  ∃ (i : ℕ),
    0 < i ∧ i ≤ orderOf f ∧ Eq (α := α) ((f ^ i : (a : α) → α) x : α) ((HPow.hPow (β := ℕ) f 0 : (a : α) → α) x : α)
Tactic: obtain ⟨_ | i, hi, rfl⟩ := h.exists_pow_eq'
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
inst : Finite α
h : f.SameCycle x y
zero :
  ∀ (hi : 0 < orderOf f) (h : f.SameCycle x ((HPow.hPow (β := ℕ) f 0 : (a : α) → α) x)),
    ∃ (i : ℕ),
      0 < i ∧ i ≤ orderOf f ∧ Eq (α := α) ((f ^ i : (a : α) → α) x : α) ((HPow.hPow (β := ℕ) f 0 : (a : α) → α) x : α)
⊢ ∃ (i : ℕ), 0 < i ∧ i ≤ orderOf f ∧ (f ^ i : (a : α) → α) x = y
have succ : ∀ (i : ℕ) (hi : i + 1 < orderOf f) (h : f.SameCycle x ((f ^ (i + 1) : (a : α) → α) x)),
  ∃ (i_1 : ℕ),
    0 < i_1 ∧ i_1 ≤ orderOf f ∧ Eq (α := α) ((f ^ i_1 : (a : α) → α) x : α) ((f ^ (i + 1) : (a : α) → α) x : α)
Tactic: obtain ⟨_ | i, hi, rfl⟩ := h.exists_pow_eq'
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x : α
inst : Finite α
hi : 0 < orderOf f
h : f.SameCycle x ((HPow.hPow (β := ℕ) f 0 : (a : α) → α) x)
⊢ ∃ (i : ℕ),
    0 < i ∧ i ≤ orderOf f ∧ Eq (α := α) ((f ^ i : (a : α) → α) x : α) ((HPow.hPow (β := ℕ) f 0 : (a : α) → α) x : α)
have zero : Eq (α := α) ((f ^ orderOf f : (a : α) → α) x : α) ((HPow.hPow (β := ℕ) f 0 : (a : α) → α) x : α)
Tactic: refine ⟨orderOf f, orderOf_pos f, le_rfl, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x : α
inst : Finite α
hi : 0 < orderOf f
h : f.SameCycle x ((HPow.hPow (β := ℕ) f 0 : (a : α) → α) x)
⊢ Eq (α := α) ((f ^ orderOf f : (a : α) → α) x : α) ((HPow.hPow (β := ℕ) f 0 : (a : α) → α) x : α)
have zero : Eq (α := α) ((1 : (a : α) → α) x : α) ((HPow.hPow (β := ℕ) f 0 : (a : α) → α) x : α)
Tactic: rw [pow_orderOf_eq_one, pow_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x : α
inst : Finite α
hi : 0 < orderOf f
h : f.SameCycle x ((HPow.hPow (β := ℕ) f 0 : (a : α) → α) x)
zero : Eq (α := α) ((1 : (a : α) → α) x : α) ((HPow.hPow (β := ℕ) f 0 : (a : α) → α) x : α)
⊢ Eq (α := α) ((f ^ orderOf f : (a : α) → α) x : α) ((HPow.hPow (β := ℕ) f 0 : (a : α) → α) x : α)
have zero₁ : Eq (α := α) ((1 : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)
Tactic: rw [pow_orderOf_eq_one, pow_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
inst : Finite α
h : f.SameCycle x y
⊢ ∃ (i : Fin (orderOf f)), (f ^ (↑i : ℕ) : (a : α) → α) x = y
have obtain : ∀ (i : ℕ) (hi : i < orderOf f) (hx : (f ^ i : (a : α) → α) x = y),
  ∃ (i : Fin (orderOf f)), (f ^ (↑i : ℕ) : (a : α) → α) x = y
Tactic: obtain ⟨i, hi, hx⟩ := SameCycle.exists_pow_eq' h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
inst : Finite α
h : f.SameCycle x y
⊢ ∃ (i : ℕ), (f ^ i : (a : α) → α) x = y
have obtain : ∀ i < orderOf f, ∀ (hi : (f ^ i : (a : α) → α) x = y), ∃ (i : ℕ), (f ^ i : (a : α) → α) x = y
Tactic: obtain ⟨i, _, hi⟩ := h.exists_pow_eq'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
hf : f.IsCycle
hx : (f : (a : α) → α) x ≠ x
hy : (f : (a : α) → α) y ≠ y
g : α
hg : (f : (a : α) → α) g ≠ g ∧ ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle g y
a : ℤ
ha : (f ^ a : (a : α) → α) g = x
b : ℤ
hb : (f ^ b : (a : α) → α) g = y
⊢ (f ^ (b - a) : (a : α) → α) x = y
have rw : (f ^ (b - a) : (a : α) → α) ((f ^ a : (a : α) → α) g : α) = y
Tactic: rw [← ha, ← mul_apply, ← zpow_add, sub_add_cancel, hb]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
hf : f.IsCycle
hx : (f : (a : α) → α) x ≠ x
hy : (f : (a : α) → α) y ≠ y
g : α
hg : (f : (a : α) → α) g ≠ g ∧ ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle g y
a : ℤ
ha : (f ^ a : (a : α) → α) g = x
b : ℤ
hb : (f ^ b : (a : α) → α) g = y
rw : (f ^ (b - a) : (a : α) → α) ((f ^ a : (a : α) → α) g : α) = y
⊢ (f ^ (b - a) : (a : α) → α) x = y
have rw₁ : (f ^ (b - a) * f ^ a : (a : α) → α) g = y
Tactic: rw [← ha, ← mul_apply, ← zpow_add, sub_add_cancel, hb]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
hf : f.IsCycle
hx : (f : (a : α) → α) x ≠ x
hy : (f : (a : α) → α) y ≠ y
g : α
hg : (f : (a : α) → α) g ≠ g ∧ ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle g y
a : ℤ
ha : (f ^ a : (a : α) → α) g = x
b : ℤ
hb : (f ^ b : (a : α) → α) g = y
rw : (f ^ (b - a) : (a : α) → α) ((f ^ a : (a : α) → α) g : α) = y
rw₁ : (f ^ (b - a) * f ^ a : (a : α) → α) g = y
⊢ (f ^ (b - a) : (a : α) → α) x = y
have rw₂ : (f ^ (b - a + a) : (a : α) → α) g = y
Tactic: rw [← ha, ← mul_apply, ← zpow_add, sub_add_cancel, hb]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
hf : f.IsCycle
hx : (f : (a : α) → α) x ≠ x
hy : (f : (a : α) → α) y ≠ y
g : α
hg : (f : (a : α) → α) g ≠ g ∧ ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle g y
a : ℤ
ha : (f ^ a : (a : α) → α) g = x
b : ℤ
hb : (f ^ b : (a : α) → α) g = y
rw : (f ^ (b - a) : (a : α) → α) ((f ^ a : (a : α) → α) g : α) = y
rw₁ : (f ^ (b - a) * f ^ a : (a : α) → α) g = y
rw₂ : (f ^ (b - a + a) : (a : α) → α) g = y
rw₃ : (f ^ b : (a : α) → α) g = y
⊢ (f ^ (b - a) : (a : α) → α) x = y
have rw₄ : y = y
Tactic: rw [← ha, ← mul_apply, ← zpow_add, sub_add_cancel, hb]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f g : Perm α
x : α
hx : (f : (a : α) → α) x ≠ x
h : ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle x y
⊢ (g * f * g⁻¹).IsCycle
have refine : ∀ (y : α) (hy : (g * f * g⁻¹ : (a : α) → α) y ≠ y), (g * f * g⁻¹).SameCycle ((g : (a : α) → α) x) y
Tactic: refine ⟨g x, by simp [coe_mul, hx], fun y hy => ?_⟩
-- 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
⊢ (g.extendDomain (p := p) f).IsCycle
have refine_1 : Ne (α := β) ((g.extendDomain (p := p) f : (a : β) → β) (↑((f : (a : α) → Subtype p) a) : β) : β)
  ((↑((f : (a : α) → Subtype p) a) : β) : β)
Tactic: refine ⟨f a, ?_, fun b hb => ?_⟩
-- 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
refine_1 :
  Ne (α := β) ((g.extendDomain (p := p) f : (a : β) → β) (↑((f : (a : α) → Subtype p) a) : β) : β)
    ((↑((f : (a : α) → Subtype p) a) : β) : β)
⊢ (g.extendDomain (p := p) f).IsCycle
have refine_2 : ∀ (b : β) (hb : (g.extendDomain (p := p) f : (a : β) → β) b ≠ b),
  (g.extendDomain (p := p) f).SameCycle (↑((f : (a : α) → Subtype p) a) : β) b
Tactic: refine ⟨f a, ?_, fun b hb => ?_⟩