awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
inst : DecidableRel f.SameCycle
h : f.SameCycle x y
z : α
⊢ Eq (α := α) (if f.SameCycle x z then (f : (a : α) → α) z else z : α) ((f.cycleOf y : (a : α) → α) z : α)
have pos : ∀ (hz : f.SameCycle x z), Eq (α := α) ((f : (a : α) → α) z : α) ((f.cycleOf y : (a : α) → α) z : α)
Tactic: split_ifs with hz
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
inst : DecidableRel f.SameCycle
h : f.SameCycle x y
z : α
pos : ∀ (hz : f.SameCycle x z), Eq (α := α) ((f : (a : α) → α) z : α) ((f.cycleOf y : (a : α) → α) z : α)
⊢ Eq (α := α) (if f.SameCycle x z then (f : (a : α) → α) z else z : α) ((f.cycleOf y : (a : α) → α) z : α)
have neg : ∀ (hz : ¬f.SameCycle x z), z = (f.cycleOf y : (a : α) → α) z
Tactic: split_ifs with hz
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x : α
k : ℤ
⊢ Eq (α := α) ((f.cycleOf x : (a : α) → α) ((f ^ k : (a : α) → α) x : α) : α) ((f ^ (k + 1) : (a : α) → α) x : α)
have rw : Eq (α := α) ((f : (a : α) → α) ((f ^ k : (a : α) → α) x : α) : α) ((f ^ (k + 1) : (a : α) → α) x : α)
Tactic: rw [SameCycle.cycleOf_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x : α
k : ℤ
rw : Eq (α := α) ((f : (a : α) → α) ((f ^ k : (a : α) → α) x : α) : α) ((f ^ (k + 1) : (a : α) → α) x : α)
⊢ Eq (α := α) ((f.cycleOf x : (a : α) → α) ((f ^ k : (a : α) → α) x : α) : α) ((f ^ (k + 1) : (a : α) → α) x : α)
have rw₁ : f.SameCycle x ((f ^ k : (a : α) → α) x)
Tactic: rw [SameCycle.cycleOf_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x : α
k : ℤ
⊢ Eq (α := α) ((f : (a : α) → α) ((f ^ k : (a : α) → α) x : α) : α) ((f ^ (k + 1) : (a : α) → α) x : α)
have rw : Eq (α := α) ((f : (a : α) → α) ((f ^ k : (a : α) → α) x : α) : α) ((f ^ (1 + k) : (a : α) → α) x : α)
Tactic: rw [add_comm, zpow_add, zpow_one, mul_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x : α
k : ℤ
rw : Eq (α := α) ((f : (a : α) → α) ((f ^ k : (a : α) → α) x : α) : α) ((f ^ (1 + k) : (a : α) → α) x : α)
⊢ Eq (α := α) ((f : (a : α) → α) ((f ^ k : (a : α) → α) x : α) : α) ((f ^ (k + 1) : (a : α) → α) x : α)
have rw₁ : Eq (α := α) ((f : (a : α) → α) ((f ^ k : (a : α) → α) x : α) : α) ((HPow.hPow (β := ℤ) f 1 * f ^ k : (a : α) → α) x : α)
Tactic: rw [add_comm, zpow_add, zpow_one, mul_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x : α
k : ℤ
rw : Eq (α := α) ((f : (a : α) → α) ((f ^ k : (a : α) → α) x : α) : α) ((f ^ (1 + k) : (a : α) → α) x : α)
rw₁ :
  Eq (α := α) ((f : (a : α) → α) ((f ^ k : (a : α) → α) x : α) : α)
    ((HPow.hPow (β := ℤ) f 1 * f ^ k : (a : α) → α) x : α)
⊢ Eq (α := α) ((f : (a : α) → α) ((f ^ k : (a : α) → α) x : α) : α) ((f ^ (k + 1) : (a : α) → α) x : α)
have rw₂ : Eq (α := α) ((f : (a : α) → α) ((f ^ k : (a : α) → α) x : α) : α) ((f * f ^ k : (a : α) → α) x : α)
Tactic: rw [add_comm, zpow_add, zpow_one, mul_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
x : α
k : ℤ
rw : Eq (α := α) ((f : (a : α) → α) ((f ^ k : (a : α) → α) x : α) : α) ((f ^ (1 + k) : (a : α) → α) x : α)
rw₁ :
  Eq (α := α) ((f : (a : α) → α) ((f ^ k : (a : α) → α) x : α) : α)
    ((HPow.hPow (β := ℤ) f 1 * f ^ k : (a : α) → α) x : α)
rw₂ : Eq (α := α) ((f : (a : α) → α) ((f ^ k : (a : α) → α) x : α) : α) ((f * f ^ k : (a : α) → α) x : α)
⊢ Eq (α := α) ((f : (a : α) → α) ((f ^ k : (a : α) → α) x : α) : α) ((f ^ (k + 1) : (a : α) → α) x : α)
have rw₃ : Eq (α := α) ((f : (a : α) → α) ((f ^ k : (a : α) → α) x : α) : α) ((f : (a : α) → α) ((f ^ k : (a : α) → α) x : α) : α)
Tactic: rw [add_comm, zpow_add, zpow_one, mul_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
x : α
inst : DecidableRel f.SameCycle
hf : f.IsCycle
hx : (f : (a : α) → α) x ≠ x
y : α
h : f.SameCycle x y
⊢ Eq (α := α) ((f.cycleOf x : (a : α) → α) y : α) ((f : (a : α) → α) y : α)
have rw : Eq (α := α) ((f : (a : α) → α) y : α) ((f : (a : α) → α) y : α)
Tactic: rw [h.cycleOf_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
x : α
inst : DecidableRel f.SameCycle
hf : f.IsCycle
hx : (f : (a : α) → α) x ≠ x
y : α
h : ¬f.SameCycle x y
⊢ Eq (α := α) ((f.cycleOf x : (a : α) → α) y : α) ((f : (a : α) → α) y : α)
have rw : y = (f : (a : α) → α) y
Tactic: rw [cycleOf_apply_of_not_sameCycle h,
        Classical.not_not.1 (mt ((isCycle_iff_sameCycle hx).1 hf).2 h)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
x : α
inst : DecidableRel f.SameCycle
hf : f.IsCycle
hx : (f : (a : α) → α) x ≠ x
y : α
h : ¬f.SameCycle x y
rw : y = (f : (a : α) → α) y
⊢ Eq (α := α) ((f.cycleOf x : (a : α) → α) y : α) ((f : (a : α) → α) y : α)
have rw₁ : y = y
Tactic: rw [cycleOf_apply_of_not_sameCycle h,
        Classical.not_not.1 (mt ((isCycle_iff_sameCycle hx).1 hf).2 h)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
x : α
f : Perm α
inst : DecidableRel f.SameCycle
⊢ f.cycleOf x = 1 ↔ (f : (a : α) → α) x = x
have simp_rw : (∀ (x_1 : α), (if f.SameCycle x x_1 then (f : (a : α) → α) x_1 else x_1) = x_1) ↔ (f : (a : α) → α) x = x
Tactic: simp_rw [Perm.ext_iff, cycleOf_apply, one_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
x : α
f : Perm α
inst : DecidableRel f.SameCycle
⊢ (∀ (x_1 : α), (if f.SameCycle x x_1 then (f : (a : α) → α) x_1 else x_1) = x_1) ↔ (f : (a : α) → α) x = x
have refine : ∀ (h : (f : (a : α) → α) x = x) (y : α), (if f.SameCycle x y then (f : (a : α) → α) y else y) = y
Tactic: refine ⟨fun h => (if_pos (SameCycle.refl f x)).symm.trans (h x), fun h y => ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
x : α
f : Perm α
inst : DecidableRel f.SameCycle
h : (f : (a : α) → α) x = x
y : α
⊢ (if f.SameCycle x y then (f : (a : α) → α) y else y) = y
have pos : ∀ (hy : (f : (a : α) → α) y = y), (if f.SameCycle x y then (f : (a : α) → α) y else y) = y
Tactic: by_cases hy : f y = y
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
x : α
f : Perm α
inst : DecidableRel f.SameCycle
h : (f : (a : α) → α) x = x
y : α
pos : ∀ (hy : (f : (a : α) → α) y = y), (if f.SameCycle x y then (f : (a : α) → α) y else y) = y
⊢ (if f.SameCycle x y then (f : (a : α) → α) y else y) = y
have neg : ∀ (hy : ¬(f : (a : α) → α) y = y), (if f.SameCycle x y then (f : (a : α) → α) y else y) = y
Tactic: by_cases hy : f y = y
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
x : α
f : Perm α
inst : DecidableRel f.SameCycle
h : (f : (a : α) → α) x = x
y : α
hy : (f : (a : α) → α) y = y
⊢ (if f.SameCycle x y then (f : (a : α) → α) y else y) = y
have pos : (if f.SameCycle x y then y else y) = y
Tactic: rw [hy, ite_self]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
x : α
f : Perm α
inst : DecidableRel f.SameCycle
h : (f : (a : α) → α) x = x
y : α
hy : (f : (a : α) → α) y = y
pos : (if f.SameCycle x y then y else y) = y
⊢ (if f.SameCycle x y then (f : (a : α) → α) y else y) = y
have pos₁ : y = y
Tactic: rw [hy, ite_self]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
x : α
f : Perm α
inst : DecidableRel f.SameCycle
h : (f : (a : α) → α) x = x
y : α
hy : ¬(f : (a : α) → α) y = y
⊢ ¬((f : (a : α) → α) x = x ↔ (f : (a : α) → α) y = y)
have inl : (f : (a : α) → α) x = x → (f : (a : α) → α) y = y → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
x : α
f : Perm α
inst : DecidableRel f.SameCycle
h : (f : (a : α) → α) x = x
y : α
hy : ¬(f : (a : α) → α) y = y
inl : (f : (a : α) → α) x = x → (f : (a : α) → α) y = y → False
⊢ ¬((f : (a : α) → α) x = x ↔ (f : (a : α) → α) y = y)
have inr : ¬(f : (a : α) → α) x = x → ¬(f : (a : α) → α) y = y → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
x : α
inst : DecidableRel f.SameCycle
inst_1 : DecidableEq α
hf : f.IsCycle
⊢ f.cycleOf x = if (f : (a : α) → α) x = x then 1 else f
have pos : ∀ (hx : (f : (a : α) → α) x = x), f.cycleOf x = if (f : (a : α) → α) x = x then 1 else f
Tactic: by_cases hx : f x = x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
x : α
inst : DecidableRel f.SameCycle
inst_1 : DecidableEq α
hf : f.IsCycle
pos : ∀ (hx : (f : (a : α) → α) x = x), f.cycleOf x = if (f : (a : α) → α) x = x then 1 else f
⊢ f.cycleOf x = if (f : (a : α) → α) x = x then 1 else f
have neg : ∀ (hx : ¬(f : (a : α) → α) x = x), f.cycleOf x = if (f : (a : α) → α) x = x then 1 else f
Tactic: by_cases hx : f x = x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
x : α
inst : DecidableRel f.SameCycle
inst_1 : DecidableEq α
hf : f.IsCycle
hx : (f : (a : α) → α) x = x
⊢ f.cycleOf x = if (f : (a : α) → α) x = x then 1 else f
have pos : f.cycleOf x = 1
Tactic: rwa [if_pos hx, cycleOf_eq_one_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
x : α
inst : DecidableRel f.SameCycle
inst_1 : DecidableEq α
hf : f.IsCycle
hx : ¬(f : (a : α) → α) x = x
⊢ f.cycleOf x = if (f : (a : α) → α) x = x then 1 else f
have neg : f.cycleOf x = f
Tactic: rwa [if_neg hx, hf.cycleOf_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
x : α
inst : DecidableRel f.SameCycle
inst_1 : DecidableEq α
hf : f.IsCycle
hx : ¬(f : (a : α) → α) x = x
neg : f.cycleOf x = f
⊢ f.cycleOf x = if (f : (a : α) → α) x = x then 1 else f
have neg₁ : f = f
Tactic: rwa [if_neg hx, hf.cycleOf_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
x : α
inst : DecidableRel f.SameCycle
inst_1 : DecidableEq α
hf : f.IsCycle
hx : ¬(f : (a : α) → α) x = x
neg : f.cycleOf x = f
neg₁ : f = f
⊢ f.cycleOf x = if (f : (a : α) → α) x = x then 1 else f
have neg₂ : (f : (a : α) → α) x ≠ x
Tactic: rwa [if_neg hx, hf.cycleOf_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
x : α
f : Perm α
inst : DecidableRel f.SameCycle
hx : (f : (a : α) → α) x ≠ x
this : (f.cycleOf x : (a : α) → α) x ≠ x
y : α
h : (f.cycleOf x : (a : α) → α) y ≠ y
hxy : f.SameCycle x y
i : ℤ
hi rw : (f ^ i : (a : α) → α) x = y
⊢ (f.cycleOf x ^ i : (a : α) → α) x = y
have rw₁ : y = y
Tactic: rw [cycleOf_zpow_apply_self, hi]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
Goal:
α : Type u_2
x : α
f : Perm α
inst : DecidableRel f.SameCycle
hx : (f : (a : α) → α) x ≠ x
this : (f.cycleOf x : (a : α) → α) x ≠ x
y : α
h : (f.cycleOf x : (a : α) → α) y ≠ y
hxy : ¬f.SameCycle x y
⊢ (f.cycleOf x).SameCycle x y
have h₁ : y ≠ y
Tactic: rw [cycleOf_apply_of_not_sameCycle hxy] at h
Cleared hypotheses: h, hxy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
n : ℕ
x : α
⊢ Eq (α := α) ((f ^ (n % orderOf (f.cycleOf x)) : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α)
have rw : Eq (α := α) ((f.cycleOf x ^ (n % orderOf (f.cycleOf x)) : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α)
Tactic: rw [← cycleOf_pow_apply_self f, ← cycleOf_pow_apply_self f, pow_mod_orderOf]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
n : ℕ
x : α
rw : Eq (α := α) ((f.cycleOf x ^ (n % orderOf (f.cycleOf x)) : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α)
⊢ Eq (α := α) ((f ^ (n % orderOf (f.cycleOf x)) : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α)
have rw₁ : Eq (α := α) ((f.cycleOf x ^ (n % orderOf (f.cycleOf x)) : (a : α) → α) x : α) ((f.cycleOf x ^ n : (a : α) → α) x : α)
Tactic: rw [← cycleOf_pow_apply_self f, ← cycleOf_pow_apply_self f, pow_mod_orderOf]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableRel f.SameCycle
n : ℕ
x : α
rw : Eq (α := α) ((f.cycleOf x ^ (n % orderOf (f.cycleOf x)) : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α)
rw₁ :
  Eq (α := α) ((f.cycleOf x ^ (n % orderOf (f.cycleOf x)) : (a : α) → α) x : α) ((f.cycleOf x ^ n : (a : α) → α) x : α)
⊢ Eq (α := α) ((f ^ (n % orderOf (f.cycleOf x)) : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α)
have rw₂ : Eq (α := α) ((f.cycleOf x ^ n : (a : α) → α) x : α) ((f.cycleOf x ^ n : (a : α) → α) x : α)
Tactic: rw [← cycleOf_pow_apply_self f, ← cycleOf_pow_apply_self f, pow_mod_orderOf]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f g : Perm α
inst : DecidableRel f.SameCycle
inst_1 : DecidableRel (f * g).SameCycle
h : Commute f g
x : α
hx : (g : (a : α) → α) x = x
⊢ (f * g).cycleOf x = f.cycleOf x
have H : ∀ (y : α), Eq (α := α) (((f * g).cycleOf x : (a : α) → α) y : α) ((f.cycleOf x : (a : α) → α) y : α)
Tactic: ext y
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f g : Perm α
inst : DecidableRel f.SameCycle
inst_1 : DecidableRel (f * g).SameCycle
h : Commute f g
x : α
hx : (g : (a : α) → α) x = x
y : α
⊢ Eq (α := α) (((f * g).cycleOf x : (a : α) → α) y : α) ((f.cycleOf x : (a : α) → α) y : α)
have pos : ∀ (hxy : (f * g).SameCycle x y),
  Eq (α := α) (((f * g).cycleOf x : (a : α) → α) y : α) ((f.cycleOf x : (a : α) → α) y : α)
Tactic: by_cases hxy : (f * g).SameCycle x y
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f g : Perm α
inst : DecidableRel f.SameCycle
inst_1 : DecidableRel (f * g).SameCycle
h : Commute f g
x : α
hx : (g : (a : α) → α) x = x
y : α
pos :
  ∀ (hxy : (f * g).SameCycle x y),
    Eq (α := α) (((f * g).cycleOf x : (a : α) → α) y : α) ((f.cycleOf x : (a : α) → α) y : α)
⊢ Eq (α := α) (((f * g).cycleOf x : (a : α) → α) y : α) ((f.cycleOf x : (a : α) → α) y : α)
have neg : ∀ (hxy : ¬(f * g).SameCycle x y),
  Eq (α := α) (((f * g).cycleOf x : (a : α) → α) y : α) ((f.cycleOf x : (a : α) → α) y : α)
Tactic: by_cases hxy : (f * g).SameCycle x y
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f g : Perm α
inst : DecidableRel f.SameCycle
inst_1 : DecidableRel (f * g).SameCycle
h : Commute f g
x : α
hx : (g : (a : α) → α) x = x
y : α
hxy : (f * g).SameCycle x y
⊢ Eq (α := α) (((f * g).cycleOf x : (a : α) → α) y : α) ((f.cycleOf x : (a : α) → α) y : α)
have pos : ∀ (z : ℤ),
  Eq (α := α) (((f * g).cycleOf x : (a : α) → α) (((f * g) ^ z : (a : α) → α) x : α) : α)
    ((f.cycleOf x : (a : α) → α) (((f * g) ^ z : (a : α) → α) x : α) : α)
Tactic: obtain ⟨z, rfl⟩ := hxy
Cleared hypotheses: y, hxy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f g : Perm α
inst : DecidableRel f.SameCycle
inst_1 : DecidableRel (f * g).SameCycle
h : Commute f g
x : α
hx : (g : (a : α) → α) x = x
z : ℤ
⊢ Eq (α := α) (((f * g).cycleOf x : (a : α) → α) (((f * g) ^ z : (a : α) → α) x : α) : α)
    ((f.cycleOf x : (a : α) → α) (((f * g) ^ z : (a : α) → α) x : α) : α)
have pos : Eq (α := α) (((f * g) ^ (z + 1) : (a : α) → α) x : α)
  ((f.cycleOf x : (a : α) → α) (((f * g) ^ z : (a : α) → α) x : α) : α)
Tactic: rw [cycleOf_apply_apply_zpow_self]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f g : Perm α
inst : DecidableRel f.SameCycle
inst_1 : DecidableRel (f * g).SameCycle
h : Commute f g
x : α
hx : (g : (a : α) → α) x = x
y : α
hxy : ¬(f * g).SameCycle x y
⊢ Eq (α := α) (((f * g).cycleOf x : (a : α) → α) y : α) ((f.cycleOf x : (a : α) → α) y : α)
have neg : ¬f.SameCycle x y
Tactic: rw [cycleOf_apply_of_not_sameCycle hxy, cycleOf_apply_of_not_sameCycle]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f g : Perm α
inst : DecidableRel f.SameCycle
inst_1 : DecidableRel (f * g).SameCycle
h : Commute f g
x : α
hx : (g : (a : α) → α) x = x
y : α
hxy : ¬(f * g).SameCycle x y
⊢ ¬f.SameCycle x y
have neg : ∀ (hxy : f.SameCycle x y), (f * g).SameCycle x y
Tactic: contrapose hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f g : Perm α
inst : DecidableRel f.SameCycle
inst_1 : DecidableRel (f * g).SameCycle
h : Commute f g
x : α
hx : (g : (a : α) → α) x = x
y : α
hxy : f.SameCycle x y
⊢ (f * g).SameCycle x y
have neg : ∀ (z : ℤ), (f * g).SameCycle x ((f ^ z : (a : α) → α) x)
Tactic: obtain ⟨z, rfl⟩ := hxy
Cleared hypotheses: y, hxy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f g : Perm α
inst : DecidableRel f.SameCycle
inst_1 : DecidableRel (f * g).SameCycle
h : Commute f g
x : α
hx : (g : (a : α) → α) x = x
z : ℤ
⊢ (f * g).SameCycle x ((f ^ z : (a : α) → α) x)
have neg : Eq (α := α) (((f * g) ^ z : (a : α) → α) x : α) ((f ^ z : (a : α) → α) x : α)
Tactic: refine ⟨z, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f g : Perm α
inst : DecidableRel f.SameCycle
inst_1 : DecidableRel g.SameCycle
inst_2 : DecidableRel (f * g).SameCycle
h : f.Disjoint g
x : α
⊢ (f * g).cycleOf x = f.cycleOf x * g.cycleOf x
have inl : ∀ (hfx : (f : (a : α) → α) x = x), (f * g).cycleOf x = f.cycleOf x * g.cycleOf x
Tactic: rcases (disjoint_iff_eq_or_eq.mp h) x with hfx | hgx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f g : Perm α
inst : DecidableRel f.SameCycle
inst_1 : DecidableRel g.SameCycle
inst_2 : DecidableRel (f * g).SameCycle
h : f.Disjoint g
x : α
inl : ∀ (hfx : (f : (a : α) → α) x = x), (f * g).cycleOf x = f.cycleOf x * g.cycleOf x
⊢ (f * g).cycleOf x = f.cycleOf x * g.cycleOf x
have inr : ∀ (hgx : (g : (a : α) → α) x = x), (f * g).cycleOf x = f.cycleOf x * g.cycleOf x
Tactic: rcases (disjoint_iff_eq_or_eq.mp h) x with hfx | hgx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f g : Perm α
inst : DecidableRel f.SameCycle
inst_1 : DecidableRel g.SameCycle
inst_2 : DecidableRel (f * g).SameCycle
h : f.Disjoint g
x : α
⊢ (f * g).cycleOf x = f.cycleOf x * g.cycleOf x
have inl : ∀ (hfx : (f : (a : α) → α) x = x), (f * g).cycleOf x = f.cycleOf x * g.cycleOf x
Tactic: classical
  rcases (disjoint_iff_eq_or_eq.mp h) x with hfx | hgx
  · simp [h.commute.eq, cycleOf_mul_of_apply_right_eq_self h.symm.commute, hfx]
  · simp [cycleOf_mul_of_apply_right_eq_self h.commute, hgx]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f g : Perm α
inst : DecidableRel f.SameCycle
inst_1 : DecidableRel g.SameCycle
inst_2 : DecidableRel (f * g).SameCycle
h : f.Disjoint g
x : α
inl : ∀ (hfx : (f : (a : α) → α) x = x), (f * g).cycleOf x = f.cycleOf x * g.cycleOf x
⊢ (f * g).cycleOf x = f.cycleOf x * g.cycleOf x
have inr : ∀ (hgx : (g : (a : α) → α) x = x), (f * g).cycleOf x = f.cycleOf x * g.cycleOf x
Tactic: classical
  rcases (disjoint_iff_eq_or_eq.mp h) x with hfx | hgx
  · simp [h.commute.eq, cycleOf_mul_of_apply_right_eq_self h.symm.commute, hfx]
  · simp [cycleOf_mul_of_apply_right_eq_self h.commute, hgx]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
inst : DecidableRel f.SameCycle
inst_1 : DecidableEq α
inst_2 : Fintype α
⊢ y ∈ (f.cycleOf x).support ↔ f.SameCycle x y ∧ x ∈ f.support
have pos : ∀ (hx : (f : (a : α) → α) x = x), y ∈ (f.cycleOf x).support ↔ f.SameCycle x y ∧ x ∈ f.support
Tactic: by_cases hx : f x = x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
inst : DecidableRel f.SameCycle
inst_1 : DecidableEq α
inst_2 : Fintype α
pos : ∀ (hx : (f : (a : α) → α) x = x), y ∈ (f.cycleOf x).support ↔ f.SameCycle x y ∧ x ∈ f.support
⊢ y ∈ (f.cycleOf x).support ↔ f.SameCycle x y ∧ x ∈ f.support
have neg : ∀ (hx : ¬(f : (a : α) → α) x = x), y ∈ (f.cycleOf x).support ↔ f.SameCycle x y ∧ x ∈ f.support
Tactic: by_cases hx : f x = x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
inst : DecidableRel f.SameCycle
inst_1 : DecidableEq α
inst_2 : Fintype α
hx : (f : (a : α) → α) x = x
⊢ y ∈ (f.cycleOf x).support ↔ f.SameCycle x y ∧ x ∈ f.support
have pos : Membership.mem (γ := Finset α) (support 1) y ↔ f.SameCycle x y ∧ x ∈ f.support
Tactic: rw [(cycleOf_eq_one_iff _).mpr hx]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
inst : DecidableRel f.SameCycle
inst_1 : DecidableEq α
inst_2 : Fintype α
hx : ¬(f : (a : α) → α) x = x
⊢ y ∈ (f.cycleOf x).support ↔ f.SameCycle x y ∧ x ∈ f.support
have neg : (if f.SameCycle x y then (f : (a : α) → α) y else y) ≠ y ↔ f.SameCycle x y ∧ x ∈ f.support
Tactic: rw [mem_support, cycleOf_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
inst : DecidableRel f.SameCycle
inst_1 : DecidableEq α
inst_2 : Fintype α
hx : ¬(f : (a : α) → α) x = x
⊢ (if f.SameCycle x y then (f : (a : α) → α) y else y) ≠ y ↔ f.SameCycle x y ∧ x ∈ f.support
have pos : ∀ (hy : f.SameCycle x y), (f : (a : α) → α) y ≠ y ↔ f.SameCycle x y ∧ x ∈ f.support
Tactic: split_ifs with hy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
inst : DecidableRel f.SameCycle
inst_1 : DecidableEq α
inst_2 : Fintype α
hx : ¬(f : (a : α) → α) x = x
pos : ∀ (hy : f.SameCycle x y), (f : (a : α) → α) y ≠ y ↔ f.SameCycle x y ∧ x ∈ f.support
⊢ (if f.SameCycle x y then (f : (a : α) → α) y else y) ≠ y ↔ f.SameCycle x y ∧ x ∈ f.support
have neg : ∀ (hy : ¬f.SameCycle x y), y ≠ y ↔ f.SameCycle x y ∧ x ∈ f.support
Tactic: split_ifs with hy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
inst : DecidableRel f.SameCycle
inst_1 : DecidableEq α
inst_2 : Fintype α
hx : ¬(f : (a : α) → α) x = x
hy : f.SameCycle x y
⊢ (f : (a : α) → α) y ≠ y ↔ f.SameCycle x y ∧ x ∈ f.support
have pos : ¬(f : (a : α) → α) y = y ↔ True
Tactic: simp only [hx, hy, Ne, not_false_iff, and_self_iff, mem_support]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
inst : DecidableRel f.SameCycle
inst_1 : DecidableEq α
inst_2 : Fintype α
hx : ¬(f : (a : α) → α) x = x
hy : f.SameCycle x y
⊢ ¬(f : (a : α) → α) y = y ↔ True
have pos : ∀ (k : ℤ), ¬Eq (α := α) ((f : (a : α) → α) ((f ^ k : (a : α) → α) x : α) : α) ((f ^ k : (a : α) → α) x : α) ↔ True
Tactic: rcases hy with ⟨k, rfl⟩
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
x : α
inst : DecidableRel f.SameCycle
inst_1 : DecidableEq α
inst_2 : Fintype α
hx : ¬(f : (a : α) → α) x = x
k : ℤ
⊢ ¬Eq (α := α) ((f : (a : α) → α) ((f ^ k : (a : α) → α) x : α) : α) ((f ^ k : (a : α) → α) x : α) ↔ True
have pos : ¬((f ^ k : (a : α) → α) x : α) ∉ f.support ↔ True
Tactic: rw [← notMem_support]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
f : Perm α
x y : α
hx : (f : (a : α) → α) x ≠ x
inst : DecidableRel f.SameCycle
inst_1 : DecidableEq α
inst_2 : Fintype α
⊢ y ∈ (f.cycleOf x).support ↔ f.SameCycle x y
have rw : f.SameCycle x y ∧ x ∈ f.support ↔ f.SameCycle x y
Tactic: rw [mem_support_cycleOf_iff_aux, and_iff_left (mem_support.2 hx)]