awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
b x : α
f : Perm α
h : (f ^ Int.negSucc n : (a : α) → α) ((f : (a : α) → α) x : α) = b
hfxb : (f : (a : α) → α) x ≠ b
hfb : (f : (a : α) → α) b ≠ b
hbx : b ≠ x
hb :
  Ne (α := α) ((swap x ((Equiv.symm f : (a : α) → α) x) * f⁻¹ : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) : α)
    ((Equiv.symm f : (a : α) → α) b : α)
⊢ ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
have inr : ∀ (i : ℤ)
  (hi :
    Eq (α := α)
      (((swap x ((Equiv.symm f : (a : α) → α) x) * Equiv.symm f) ^ i : (a : α) → α)
          ((Equiv.symm f : (a : α) → α) x : α) :
        α)
      ((Equiv.symm f : (a : α) → α) b : α)),
  ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
Tactic: obtain ⟨i, hi⟩ := isCycle_swap_mul_aux₁ n hb <| by
      rw [← mul_apply, ← pow_succ]; simpa [pow_succ', eq_symm_apply] using h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
b x : α
f : Perm α
h : (f ^ Int.negSucc n : (a : α) → α) ((f : (a : α) → α) x : α) = b
hfxb : (f : (a : α) → α) x ≠ b
hfb : (f : (a : α) → α) b ≠ b
hbx : b ≠ x
hb :
  Ne (α := α) ((swap x ((Equiv.symm f : (a : α) → α) x) * f⁻¹ : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) : α)
    ((Equiv.symm f : (a : α) → α) b : α)
i : ℤ
hi :
  Eq (α := α)
    (((swap x ((Equiv.symm f : (a : α) → α) x) * Equiv.symm f) ^ i : (a : α) → α) ((Equiv.symm f : (a : α) → α) x : α) :
      α)
    ((Equiv.symm f : (a : α) → α) b : α)
⊢ ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
have inr : Eq (α := α)
  ((swap x ((f⁻¹ : (a : α) → α) x) * f⁻¹ : (a : α) → α)
      (((swap x ((f : (a : α) → α) x) * f) ^ (-i) : (a : α) → α) ((f : (a : α) → α) x : α) : α) :
    α)
  ((swap x ((f⁻¹ : (a : α) → α) x) * f⁻¹ : (a : α) → α) b : α)
Tactic: refine ⟨-i, (swap x (f⁻¹ x) * f⁻¹).injective ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
b x : α
f : Perm α
h : (f ^ Int.negSucc n : (a : α) → α) ((f : (a : α) → α) x : α) = b
hfxb : (f : (a : α) → α) x ≠ b
hfb : (f : (a : α) → α) b ≠ b
hbx : b ≠ x
hb :
  Ne (α := α) ((swap x ((Equiv.symm f : (a : α) → α) x) * f⁻¹ : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) : α)
    ((Equiv.symm f : (a : α) → α) b : α)
i : ℤ
hi :
  Eq (α := α)
    (((swap x ((Equiv.symm f : (a : α) → α) x) * Equiv.symm f) ^ i : (a : α) → α) ((Equiv.symm f : (a : α) → α) x : α) :
      α)
    ((Equiv.symm f : (a : α) → α) b : α)
⊢ Eq (α := α)
    ((swap x ((f⁻¹ : (a : α) → α) x) * f⁻¹ : (a : α) → α)
        (((swap x ((f : (a : α) → α) x) * f) ^ (-i) : (a : α) → α) ((f : (a : α) → α) x : α) : α) :
      α)
    ((swap x ((f⁻¹ : (a : α) → α) x) * f⁻¹ : (a : α) → α) b : α)
have h₁ : Eq (α := α)
  ((swap x ((f⁻¹ : (a : α) → α) x) * f⁻¹ : (a : α) → α)
      (((swap x ((f : (a : α) → α) x) * f) ^ (-i) : (a : α) → α) ((f : (a : α) → α) x : α) : α) :
    α)
  (((swap x ((Equiv.symm f : (a : α) → α) x) * Equiv.symm f) ^ i : (a : α) → α) ((Equiv.symm f : (a : α) → α) x : α) :
    α)
Tactic: convert! hi using 1
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
b x : α
f : Perm α
h : (f ^ Int.negSucc n : (a : α) → α) ((f : (a : α) → α) x : α) = b
hfxb : (f : (a : α) → α) x ≠ b
hfb : (f : (a : α) → α) b ≠ b
hbx : b ≠ x
hb :
  Ne (α := α) ((swap x ((Equiv.symm f : (a : α) → α) x) * f⁻¹ : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) : α)
    ((Equiv.symm f : (a : α) → α) b : α)
i : ℤ
hi :
  Eq (α := α)
    (((swap x ((Equiv.symm f : (a : α) → α) x) * Equiv.symm f) ^ i : (a : α) → α) ((Equiv.symm f : (a : α) → α) x : α) :
      α)
    ((Equiv.symm f : (a : α) → α) b : α)
h₁ :
  Eq (α := α)
    ((swap x ((f⁻¹ : (a : α) → α) x) * f⁻¹ : (a : α) → α)
        (((swap x ((f : (a : α) → α) x) * f) ^ (-i) : (a : α) → α) ((f : (a : α) → α) x : α) : α) :
      α)
    (((swap x ((Equiv.symm f : (a : α) → α) x) * Equiv.symm f) ^ i : (a : α) → α) ((Equiv.symm f : (a : α) → α) x : α) :
      α)
⊢ Eq (α := α)
    ((swap x ((f⁻¹ : (a : α) → α) x) * f⁻¹ : (a : α) → α)
        (((swap x ((f : (a : α) → α) x) * f) ^ (-i) : (a : α) → α) ((f : (a : α) → α) x : α) : α) :
      α)
    ((swap x ((f⁻¹ : (a : α) → α) x) * f⁻¹ : (a : α) → α) b : α)
have h₂ : Eq (α := α) ((swap x ((f⁻¹ : (a : α) → α) x) * f⁻¹ : (a : α) → α) b : α) ((Equiv.symm f : (a : α) → α) b : α)
Tactic: convert! hi using 1
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
b x : α
f : Perm α
h : (f ^ Int.negSucc n : (a : α) → α) ((f : (a : α) → α) x : α) = b
hfxb : (f : (a : α) → α) x ≠ b
hfb : (f : (a : α) → α) b ≠ b
hbx : b ≠ x
hb :
  Ne (α := α) ((swap x ((Equiv.symm f : (a : α) → α) x) * f⁻¹ : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) : α)
    ((Equiv.symm f : (a : α) → α) b : α)
i : ℤ
hi :
  Eq (α := α)
    (((swap x ((Equiv.symm f : (a : α) → α) x) * Equiv.symm f) ^ i : (a : α) → α) ((Equiv.symm f : (a : α) → α) x : α) :
      α)
    ((Equiv.symm f : (a : α) → α) b : α)
⊢ Eq (α := α)
    ((swap x ((f⁻¹ : (a : α) → α) x) * f⁻¹ : (a : α) → α)
        (((swap x ((f : (a : α) → α) x) * f) ^ (-i) : (a : α) → α) ((f : (a : α) → α) x : α) : α) :
      α)
    (((swap x ((Equiv.symm f : (a : α) → α) x) * Equiv.symm f) ^ i : (a : α) → α) ((Equiv.symm f : (a : α) → α) x : α) :
      α)
have h₁ : Eq (α := α)
  ((swap x ((f⁻¹ : (a : α) → α) x) * f⁻¹ *
          HMul.hMul (α := Perm α)
              (swap ((f⁻¹ : (a : α) → α) x) ((f⁻¹ : (a : α) → α) ((f : (a : α) → α) x : α)) : Perm α) f⁻¹ ^
            i :
        (a : α) → α)
      ((f : (a : α) → α) x : α) :
    α)
  (((swap x ((Equiv.symm f : (a : α) → α) x) * Equiv.symm f) ^ i : (a : α) → α) ((Equiv.symm f : (a : α) → α) x : α) :
    α)
Tactic: rw [zpow_neg, ← inv_zpow, ← mul_apply, mul_inv_rev, swap_inv, mul_swap_eq_swap_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
b x : α
f : Perm α
h : (f ^ Int.negSucc n : (a : α) → α) ((f : (a : α) → α) x : α) = b
hfxb : (f : (a : α) → α) x ≠ b
hfb : (f : (a : α) → α) b ≠ b
hbx : b ≠ x
hb :
  Ne (α := α) ((swap x ((Equiv.symm f : (a : α) → α) x) * f⁻¹ : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) : α)
    ((Equiv.symm f : (a : α) → α) b : α)
i : ℤ
hi :
  Eq (α := α)
    (((swap x ((Equiv.symm f : (a : α) → α) x) * Equiv.symm f) ^ i : (a : α) → α) ((Equiv.symm f : (a : α) → α) x : α) :
      α)
    ((Equiv.symm f : (a : α) → α) b : α)
⊢ Eq (α := α)
    ((swap x ((f⁻¹ : (a : α) → α) x) * f⁻¹ *
            HMul.hMul (α := Perm α)
                (swap ((f⁻¹ : (a : α) → α) x) ((f⁻¹ : (a : α) → α) ((f : (a : α) → α) x : α)) : Perm α) f⁻¹ ^
              i :
          (a : α) → α)
        ((f : (a : α) → α) x : α) :
      α)
    (((swap x ((Equiv.symm f : (a : α) → α) x) * Equiv.symm f) ^ i : (a : α) → α) ((Equiv.symm f : (a : α) → α) x : α) :
      α)
have h₁ : Eq (α := α) (((swap x ((f⁻¹ : (a : α) → α) x) * f⁻¹) ^ i * swap x ((f⁻¹ : (a : α) → α) x) : (a : α) → α) x : α)
  (((swap x ((f⁻¹ : (a : α) → α) x) * f⁻¹) ^ i * f⁻¹ : (a : α) → α) x : α)
Tactic: simp [swap_comm _ x, ← mul_apply, -coe_mul, ← inv_def, -coe_inv, ← inv_def, mul_assoc _ f⁻¹,
        ← mul_zpow_mul, mul_assoc _ _ f]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_4
inst : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hfx : (f : (a : α) → α) x ≠ x
hffx : (f : (a : α) → α) ((f : (a : α) → α) x : α) = x
y z : α
hz : (f : (a : α) → α) z ≠ z ∧ ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle z y
i : ℤ
hi : (f ^ i : (a : α) → α) z = x
hyx : ¬y = x
hfyx : ¬y = (f : (a : α) → α) x
⊢ Eq (α := α) ((f : (a : α) → α) y : α) ((swap x ((f : (a : α) → α) x) : (a : α) → α) y : α)
have rw : (f : (a : α) → α) y = y
Tactic: rw [swap_apply_of_ne_of_ne hyx hfyx]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_4
inst : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hfx : (f : (a : α) → α) x ≠ x
hffx : (f : (a : α) → α) ((f : (a : α) → α) x : α) = x
y z : α
hz : (f : (a : α) → α) z ≠ z ∧ ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle z y
i : ℤ
hi : (f ^ i : (a : α) → α) z = x
hyx : ¬y = x
hfyx : ¬y = (f : (a : α) → α) x
⊢ (f : (a : α) → α) y = y
have refine : ∀ (hy : ¬(f : (a : α) → α) y = y), False
Tactic: refine by_contradiction fun hy => ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_4
inst : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hfx : (f : (a : α) → α) x ≠ x
hffx : (f : (a : α) → α) ((f : (a : α) → α) x : α) = x
y z : α
hz : (f : (a : α) → α) z ≠ z ∧ ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle z y
i : ℤ
hi : (f ^ i : (a : α) → α) z = x
hyx : ¬y = x
hfyx : ¬y = (f : (a : α) → α) x
hy : ¬(f : (a : α) → α) y = y
⊢ False
have obtain : ∀ (j : ℤ) (hj : (f ^ j : (a : α) → α) z = y), False
Tactic: obtain ⟨j, hj⟩ := hz.2 hy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
Goal:
α : Type u_4
inst : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hfx : (f : (a : α) → α) x ≠ x
hffx : (f : (a : α) → α) ((f : (a : α) → α) x : α) = x
y z : α
hz : (f : (a : α) → α) z ≠ z ∧ ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle z y
i : ℤ
hi : (f ^ i : (a : α) → α) z = x
hyx : ¬y = x
hfyx : ¬y = (f : (a : α) → α) x
hy : ¬(f : (a : α) → α) y = y
j : ℤ
hj : (f ^ j : (a : α) → α) z = y
⊢ False
have hj₁ : (f ^ (j - i) : (a : α) → α) x = y
Tactic: rw [← sub_add_cancel j i, zpow_add, mul_apply, hi] at hj
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_4
inst : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hfx : (f : (a : α) → α) x ≠ x
hffx : (f : (a : α) → α) ((f : (a : α) → α) x : α) = x
y z : α
hz : (f : (a : α) → α) z ≠ z ∧ ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle z y
i : ℤ
hi : (f ^ i : (a : α) → α) z = x
hyx : ¬y = x
hfyx : ¬y = (f : (a : α) → α) x
hy : ¬(f : (a : α) → α) y = y
j : ℤ
hj : (f ^ (j - i) : (a : α) → α) x = y
⊢ False
have inl : ∀ (hji : (f ^ (j - i) : (a : α) → α) x = x), False
Tactic: rcases zpow_apply_eq_of_apply_apply_eq_self hffx (j - i) with hji | hji
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_4
inst : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hfx : (f : (a : α) → α) x ≠ x
hffx : (f : (a : α) → α) ((f : (a : α) → α) x : α) = x
y z : α
hz : (f : (a : α) → α) z ≠ z ∧ ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle z y
i : ℤ
hi : (f ^ i : (a : α) → α) z = x
hyx : ¬y = x
hfyx : ¬y = (f : (a : α) → α) x
hy : ¬(f : (a : α) → α) y = y
j : ℤ
hj : (f ^ (j - i) : (a : α) → α) x = y
inl : ∀ (hji : (f ^ (j - i) : (a : α) → α) x = x), False
⊢ False
have inr : ∀ (hji : Eq (α := α) ((f ^ (j - i) : (a : α) → α) x : α) ((f : (a : α) → α) x : α)), False
Tactic: rcases zpow_apply_eq_of_apply_apply_eq_self hffx (j - i) with hji | hji
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
Goal:
α : Type u_4
inst : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hfx : (f : (a : α) → α) x ≠ x
hffx : (f : (a : α) → α) ((f : (a : α) → α) x : α) = x
y z : α
hz : (f : (a : α) → α) z ≠ z ∧ ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle z y
i : ℤ
hi : (f ^ i : (a : α) → α) z = x
hyx : ¬y = x
hfyx : ¬y = (f : (a : α) → α) x
hy : ¬(f : (a : α) → α) y = y
j : ℤ
hj : (f ^ (j - i) : (a : α) → α) x = y
hji : (f ^ (j - i) : (a : α) → α) x = x
⊢ False
have hyx₁ : ¬x = x
Tactic: rw [← hj, hji] at hyx
Cleared hypotheses: hyx, hj, hji
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
Goal:
α : Type u_4
inst : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hfx : (f : (a : α) → α) x ≠ x
hffx : (f : (a : α) → α) ((f : (a : α) → α) x : α) = x
y z : α
hz : (f : (a : α) → α) z ≠ z ∧ ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle z y
i : ℤ
hi : (f ^ i : (a : α) → α) z = x
hyx : ¬y = x
hfyx : ¬y = (f : (a : α) → α) x
hy : ¬(f : (a : α) → α) y = y
j : ℤ
hj : (f ^ (j - i) : (a : α) → α) x = y
hji : Eq (α := α) ((f ^ (j - i) : (a : α) → α) x : α) ((f : (a : α) → α) x : α)
⊢ False
have hfyx₁ : ¬Eq (α := α) ((f : (a : α) → α) x : α) ((f : (a : α) → α) x : α)
Tactic: rw [← hj, hji] at hfyx
Cleared hypotheses: hfyx, hj, hji
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_4
inst : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hx : (f : (a : α) → α) x ≠ x
hffx : (f : (a : α) → α) ((f : (a : α) → α) x : α) ≠ x
⊢ (swap x ((f : (a : α) → α) x) * f).IsCycle
have refine_1 : Ne (α := α) ((swap x ((f : (a : α) → α) x) * f : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α)
Tactic: refine ⟨f x, ?_, fun y hy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_4
inst : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hx : (f : (a : α) → α) x ≠ x
hffx : (f : (a : α) → α) ((f : (a : α) → α) x : α) ≠ x
refine_1 :
  Ne (α := α) ((swap x ((f : (a : α) → α) x) * f : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α)
⊢ (swap x ((f : (a : α) → α) x) * f).IsCycle
have refine_2 : ∀ (y : α) (hy : (swap x ((f : (a : α) → α) x) * f : (a : α) → α) y ≠ y),
  (swap x ((f : (a : α) → α) x) * f).SameCycle ((f : (a : α) → α) x) y
Tactic: refine ⟨f x, ?_, fun y hy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_4
inst : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hx : (f : (a : α) → α) x ≠ x
hffx : (f : (a : α) → α) ((f : (a : α) → α) x : α) ≠ x
y : α
hy : (swap x ((f : (a : α) → α) x) * f : (a : α) → α) y ≠ y
⊢ (swap x ((f : (a : α) → α) x) * f).SameCycle ((f : (a : α) → α) x) y
have refine_2 : ∀ (i : ℤ)
  (hy :
    Ne (α := α) ((swap x ((f : (a : α) → α) x) * f : (a : α) → α) ((f ^ i : (a : α) → α) x : α) : α)
      ((f ^ i : (a : α) → α) x : α)),
  (swap x ((f : (a : α) → α) x) * f).SameCycle ((f : (a : α) → α) x) ((f ^ i : (a : α) → α) x)
Tactic: obtain ⟨i, rfl⟩ := hf.exists_zpow_eq hx (ne_and_ne_of_swap_mul_apply_ne_self hy).1
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : (f : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle x y
h1 : (f : (a : α) → α) ((f : (a : α) → α) x : α) = x
⊢ Equiv.trans f (swap x ((f : (a : α) → α) x)) = Equiv.refl α
have rw : Equiv.trans (swap x ((f : (a : α) → α) x)) (swap x ((swap x ((f : (a : α) → α) x) : (a : α) → α) x)) = Equiv.refl α
Tactic: rw [hf.eq_swap_of_apply_apply_eq_self hx.1 h1, swap_apply_left, swap_swap]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : (f : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle x y
h1 : (f : (a : α) → α) ((f : (a : α) → α) x : α) = x
rw : Equiv.trans (swap x ((f : (a : α) → α) x)) (swap x ((swap x ((f : (a : α) → α) x) : (a : α) → α) x)) = Equiv.refl α
⊢ Equiv.trans f (swap x ((f : (a : α) → α) x)) = Equiv.refl α
have rw₁ : Equiv.trans (swap x ((f : (a : α) → α) x)) (swap x ((f : (a : α) → α) x)) = Equiv.refl α
Tactic: rw [hf.eq_swap_of_apply_apply_eq_self hx.1 h1, swap_apply_left, swap_swap]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : (f : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle x y
h1 : (f : (a : α) → α) ((f : (a : α) → α) x : α) = x
rw : Equiv.trans (swap x ((f : (a : α) → α) x)) (swap x ((swap x ((f : (a : α) → α) x) : (a : α) → α) x)) = Equiv.refl α
rw₁ : Equiv.trans (swap x ((f : (a : α) → α) x)) (swap x ((f : (a : α) → α) x)) = Equiv.refl α
⊢ Equiv.trans f (swap x ((f : (a : α) → α) x)) = Equiv.refl α
have rw₂ : Equiv.refl α = Equiv.refl α
Tactic: rw [hf.eq_swap_of_apply_apply_eq_self hx.1 h1, swap_apply_left, swap_swap]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : (f : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle x y
h1 : (f : (a : α) → α) ((f : (a : α) → α) x : α) = x
⊢ ((Perm.sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap x ((f : (a : α) → α) x) * (swap x ((f : (a : α) → α) x) * f)) =
    -HPow.hPow (α := ℤˣ) (-1) #f.support
have h : swap x ((f : (a : α) → α) x) * f = 1
Tactic: have h : swap x (f x) * f = 1 := by
          simp only [mul_def, one_def]
          rw [hf.eq_swap_of_apply_apply_eq_self hx.1 h1, swap_apply_left, swap_swap]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : (f : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle x y
h1 : (f : (a : α) → α) ((f : (a : α) → α) x : α) = x
h : swap x ((f : (a : α) → α) x) * f = 1
⊢ ((Perm.sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap x ((f : (a : α) → α) x) * (swap x ((f : (a : α) → α) x) * f)) =
    -HPow.hPow (α := ℤˣ) (-1) #f.support
have rw : HMul.hMul (α := ℤˣ) (-1) 1 = -HPow.hPow (α := ℤˣ) (β := ℕ) (-1) 2
Tactic: rw [sign_mul, sign_swap hx.1.symm, h, sign_one,
          hf.eq_swap_of_apply_apply_eq_self hx.1 h1, card_support_swap hx.1.symm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : (f : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle x y
h1 : ¬(f : (a : α) → α) ((f : (a : α) → α) x : α) = x
⊢ #(swap x ((f : (a : α) → α) x) * f).support + 1 = #f.support
have rw : #(swap x ((f : (a : α) → α) x) * f).support + 1 = #(insert x (f.support.erase x))
Tactic: rw [← insert_erase (mem_support.2 hx.1), support_swap_mul_eq _ _ h1,
            card_insert_of_notMem (notMem_erase _ _), sdiff_singleton_eq_erase]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : (f : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle x y
h1 : ¬(f : (a : α) → α) ((f : (a : α) → α) x : α) = x
rw : #(swap x ((f : (a : α) → α) x) * f).support + 1 = #(insert x (f.support.erase x))
⊢ #(swap x ((f : (a : α) → α) x) * f).support + 1 = #f.support
have rw₁ : #(f.support \ {x}) + 1 = #(insert x (f.support.erase x))
Tactic: rw [← insert_erase (mem_support.2 hx.1), support_swap_mul_eq _ _ h1,
            card_insert_of_notMem (notMem_erase _ _), sdiff_singleton_eq_erase]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : (f : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle x y
h1 : ¬(f : (a : α) → α) ((f : (a : α) → α) x : α) = x
rw : #(swap x ((f : (a : α) → α) x) * f).support + 1 = #(insert x (f.support.erase x))
rw₁ : #(f.support \ {x}) + 1 = #(insert x (f.support.erase x))
⊢ #(swap x ((f : (a : α) → α) x) * f).support + 1 = #f.support
have rw₂ : #(f.support \ {x}) + 1 = #(f.support.erase x) + 1
Tactic: rw [← insert_erase (mem_support.2 hx.1), support_swap_mul_eq _ _ h1,
            card_insert_of_notMem (notMem_erase _ _), sdiff_singleton_eq_erase]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : (f : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle x y
h1 : ¬(f : (a : α) → α) ((f : (a : α) → α) x : α) = x
rw : #(swap x ((f : (a : α) → α) x) * f).support + 1 = #(insert x (f.support.erase x))
rw₁ : #(f.support \ {x}) + 1 = #(insert x (f.support.erase x))
rw₂ : #(f.support \ {x}) + 1 = #(f.support.erase x) + 1
⊢ #(swap x ((f : (a : α) → α) x) * f).support + 1 = #f.support
have rw₃ : #(f.support.erase x) + 1 = #(f.support.erase x) + 1
Tactic: rw [← insert_erase (mem_support.2 hx.1), support_swap_mul_eq _ _ h1,
            card_insert_of_notMem (notMem_erase _ _), sdiff_singleton_eq_erase]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : (f : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle x y
h1 : ¬(f : (a : α) → α) ((f : (a : α) → α) x : α) = x
⊢ ((Perm.sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap x ((f : (a : α) → α) x) * (swap x ((f : (a : α) → α) x) * f)) =
    -HPow.hPow (α := ℤˣ) (-1) #f.support
have h : #(swap x ((f : (a : α) → α) x) * f).support + 1 = #f.support
Tactic: have h : #(swap x (f x) * f).support + 1 = #f.support := by
          rw [← insert_erase (mem_support.2 hx.1), support_swap_mul_eq _ _ h1,
            card_insert_of_notMem (notMem_erase _ _), sdiff_singleton_eq_erase]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : (f : (a : α) → α) x ≠ x ∧ ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle x y
h1 : ¬(f : (a : α) → α) ((f : (a : α) → α) x : α) = x
h : #(swap x ((f : (a : α) → α) x) * f).support + 1 = #f.support
⊢ ((Perm.sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap x ((f : (a : α) → α) x) * (swap x ((f : (a : α) → α) x) * f)) =
    -HPow.hPow (α := ℤˣ) (-1) #f.support
have rw : -1 * -HPow.hPow (α := ℤˣ) (-1) #(swap x ((f : (a : α) → α) x) * f).support =
  -HPow.hPow (α := ℤˣ) (-1) (#(swap x ((f : (a : α) → α) x) * f).support + 1)
Tactic: rw [sign_mul, sign_swap hx.1.symm, (hf.swap_mul hx.1 h1).sign, ← h]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
h1 : (f ^ n).IsCycle
h2 : f.support ⊆ (f ^ n).support
⊢ ∀ (x : α), (f ^ n : (a : α) → α) x ≠ x ↔ (f : (a : α) → α) x ≠ x
have simp_rw : (f ^ n).support = f.support
Tactic: simp_rw [← mem_support, ← Finset.ext_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
h1 : (f ^ n).IsCycle
h2 : f.support ⊆ (f ^ n).support
⊢ f.IsCycle
have key : ∀ (x : α), (f ^ n : (a : α) → α) x ≠ x ↔ (f : (a : α) → α) x ≠ x
Tactic: have key : ∀ x : α, (f ^ n) x ≠ x ↔ f x ≠ x := by
    simp_rw [← mem_support, ← Finset.ext_iff]
    exact (support_pow_le _ n).antisymm h2
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
h1 : (f ^ n).IsCycle
h2 : f.support ⊆ (f ^ n).support
key : ∀ (x : α), (f ^ n : (a : α) → α) x ≠ x ↔ (f : (a : α) → α) x ≠ x
⊢ f.IsCycle
have obtain : ∀ (x : α) (hx1 : (f ^ n : (a : α) → α) x ≠ x) (hx2 : ∀ ⦃y : α⦄, (f ^ n : (a : α) → α) y ≠ y → (f ^ n).SameCycle x y),
  f.IsCycle
Tactic: obtain ⟨x, hx1, hx2⟩ := h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
h2 : f.support ⊆ (f ^ n).support
key : ∀ (x : α), (f ^ n : (a : α) → α) x ≠ x ↔ (f : (a : α) → α) x ≠ x
x : α
hx1 : (f ^ n : (a : α) → α) x ≠ x
hx2 : ∀ ⦃y : α⦄, (f ^ n : (a : α) → α) y ≠ y → (f ^ n).SameCycle x y
⊢ f.IsCycle
have refine : ∀ (y : α) (hy : (f : (a : α) → α) y ≠ y), f.SameCycle x y
Tactic: refine ⟨x, (key x).mp hx1, fun y hy => ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
h2 : f.support ⊆ (f ^ n).support
key : ∀ (x : α), (f ^ n : (a : α) → α) x ≠ x ↔ (f : (a : α) → α) x ≠ x
x : α
hx1 : (f ^ n : (a : α) → α) x ≠ x
hx2 : ∀ ⦃y : α⦄, (f ^ n : (a : α) → α) y ≠ y → (f ^ n).SameCycle x y
y : α
hy : (f : (a : α) → α) y ≠ y
⊢ f.SameCycle x y
have obtain : ∀ (i : ℤ), ((f ^ n) ^ i : (a : α) → α) x = y → f.SameCycle x y
Tactic: obtain ⟨i, _⟩ := hx2 ((key y).mpr hy)