awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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 : α) :
      α)
h₂ : Eq (α := α) ((swap x ((f⁻¹ : (a : α) → α) x) * f⁻¹ : (a : α) → α) b : α) ((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 : α)

Tactic:
convert! hi using 1
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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⁻¹ *
            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 : α) :
      α)
⊢ 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:
rw [zpow_neg, ← inv_zpow, ← mul_apply, mul_inv_rev, swap_inv, mul_swap_eq_swap_mul]

Premises used: inv_zpow, Equiv.mul_swap_eq_swap_mul, Equiv.swap_inv, zpow_neg, Equiv.Perm.mul_apply, mul_inv_rev
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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⁻¹) ^ i * swap x ((f⁻¹ : (a : α) → α) x) : (a : α) → α) x : α)
    (((swap x ((f⁻¹ : (a : α) → α) x) * f⁻¹) ^ i * f⁻¹ : (a : α) → α) x : α)
⊢ 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:
simp [swap_comm _ x, ← mul_apply, -coe_mul, ← inv_def, -coe_inv, ← inv_def, mul_assoc _ f⁻¹,
        ← mul_zpow_mul, mul_assoc _ _ f]

Premises used: Equiv.swap_comm, Equiv.Perm.coe_mul, mul_assoc, Equiv.Perm.coe_inv, Inv.inv, Equiv.Perm.inv_def, Equiv.Perm.mul_apply, mul_zpow_mul
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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⁻¹) ^ i * swap x ((f⁻¹ : (a : α) → α) x) : (a : α) → α) x : α)
    (((swap x ((f⁻¹ : (a : α) → α) x) * f⁻¹) ^ i * f⁻¹ : (a : α) → α) x : α)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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 : α)
⊢ (f⁻¹ : (a : α) → α) b ≠ x

Tactic:
simpa [eq_comm, eq_symm_apply, symm_apply_eq] using hfxb

Premises used: Equiv.symm_apply_eq, eq_comm, Equiv.eq_symm_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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 : α)
⊢ Ne (α := α) ((f⁻¹ : (a : α) → α) b : α) ((f⁻¹ : (a : α) → α) x : α)

Tactic:
simpa [eq_comm, eq_symm_apply, symm_apply_eq]

Premises used: Equiv.symm_apply_eq, eq_comm, Equiv.eq_symm_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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 : α) → α) b : α) ((Equiv.symm f : (a : α) → α) b : α)

Tactic:
exact swap_apply_of_ne_of_ne (by simpa [eq_comm, eq_symm_apply, symm_apply_eq] using hfxb)
        (by simpa [eq_comm, eq_symm_apply, symm_apply_eq])

Premises used: Equiv.swap_apply_of_ne_of_ne
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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
⊢ Eq (α := α) ((f : (a : α) → α) y : α) ((swap x ((f : (a : α) → α) x) : (a : α) → α) y : α)

Tactic:
simp [hyx]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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 : α)

Tactic:
simp [hfyx, hffx]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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
rw : (f : (a : α) → α) y = y
⊢ Eq (α := α) ((f : (a : α) → α) y : α) ((swap x ((f : (a : α) → α) x) : (a : α) → α) y : α)

Tactic:
rw [swap_apply_of_ne_of_ne hyx hfyx]

Premises used: Equiv.swap_apply_of_ne_of_ne
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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

Tactic:
by_contradiction fun hy => ?_

Premises used: by_contradiction
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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
refine : ∀ (hy : ¬(f : (a : α) → α) y = y), False
⊢ (f : (a : α) → α) y = y

Tactic:
refine by_contradiction fun hy => ?_

Premises used: by_contradiction
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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
obtain : ∀ (j : ℤ) (hj : (f ^ j : (a : α) → α) z = y), False
⊢ False

Tactic:
obtain ⟨j, hj⟩ := hz.2 hy

Premises used: And.right
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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
⊢ (f ^ (j - i) : (a : α) → α) x = y

Tactic:
rw [← sub_add_cancel j i, zpow_add, mul_apply, hi] at hj

Premises used: zpow_add, Equiv.Perm.mul_apply, sub_add_cancel
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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
inr : ∀ (hji : Eq (α := α) ((f ^ (j - i) : (a : α) → α) x : α) ((f : (a : α) → α) x : α)), False
⊢ False

Tactic:
rcases zpow_apply_eq_of_apply_apply_eq_self hffx (j - i) with hji | hji

Premises used: Equiv.Perm.zpow_apply_eq_of_apply_apply_eq_self, HSub.hSub
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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
⊢ ¬x = x

Tactic:
rw [← hj, hji] at hyx
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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
hyx₁ : ¬x = x
⊢ (f ^ (j - i) : (a : α) → α) x = y

Tactic:
rw [← hj, hji] at hyx
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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
hyx₁ : ¬x = x
hj₁ : (f ^ (j - i) : (a : α) → α) x = y
⊢ (f ^ (j - i) : (a : α) → α) x = x

Tactic:
rw [← hj, hji] at hyx
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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
hfyx : ¬y = (f : (a : α) → α) x
hy : ¬(f : (a : α) → α) y = y
j : ℤ
hyx : ¬x = x
hj : (f ^ (j - i) : (a : α) → α) x = y
hji : (f ^ (j - i) : (a : α) → α) x = x
⊢ False

Tactic:
tauto
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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 : α)
⊢ ¬Eq (α := α) ((f : (a : α) → α) x : α) ((f : (a : α) → α) x : α)

Tactic:
rw [← hj, hji] at hfyx
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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 : α)
hfyx₁ : ¬Eq (α := α) ((f : (a : α) → α) x : α) ((f : (a : α) → α) x : α)
⊢ (f ^ (j - i) : (a : α) → α) x = y

Tactic:
rw [← hj, hji] at hfyx
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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 : α)
hfyx₁ : ¬Eq (α := α) ((f : (a : α) → α) x : α) ((f : (a : α) → α) x : α)
hj₁ : (f ^ (j - i) : (a : α) → α) x = y
⊢ Eq (α := α) ((f ^ (j - i) : (a : α) → α) x : α) ((f : (a : α) → α) x : α)

Tactic:
rw [← hj, hji] at hfyx
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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
hy : ¬(f : (a : α) → α) y = y
j : ℤ
hfyx : ¬Eq (α := α) ((f : (a : α) → α) x : α) ((f : (a : α) → α) x : α)
hj : (f ^ (j - i) : (a : α) → α) x = y
hji : Eq (α := α) ((f ^ (j - i) : (a : α) → α) x : α) ((f : (a : α) → α) x : α)
⊢ False

Tactic:
tauto
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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

Tactic:
⟨f x, ?_, fun y hy ↦ ?_⟩

Premises used: Equiv.Perm.IsCycle, And.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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 : α)
refine_2 :
  ∀ (y : α) (hy : (swap x ((f : (a : α) → α) x) * f : (a : α) → α) y ≠ y),
    (swap x ((f : (a : α) → α) x) * f).SameCycle ((f : (a : α) → α) x) y
⊢ (swap x ((f : (a : α) → α) x) * f).IsCycle

Tactic:
refine ⟨f x, ?_, fun y hy ↦ ?_⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_4
inst : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hx : (f : (a : α) → α) x ≠ x
hffx : (f : (a : α) → α) ((f : (a : α) → α) x : α) ≠ x
⊢ Ne (α := α) ((swap x ((f : (a : α) → α) x) * f : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α)

Tactic:
simp [swap_apply_def, mul_apply, if_neg hffx, f.injective.eq_iff, hx]

Premises used: Function.Injective.eq_iff, Equiv.swap_apply_def, Equiv.Perm.mul_apply, Equiv.injective, if_neg
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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
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)
⊢ (swap x ((f : (a : α) → α) x) * f).SameCycle ((f : (a : α) → α) x) y

Tactic:
obtain ⟨i, rfl⟩ := hf.exists_zpow_eq hx (ne_and_ne_of_swap_mul_apply_ne_self hy).1

Premises used: Equiv.Perm.ne_and_ne_of_swap_mul_apply_ne_self, Equiv.Perm.IsCycle.exists_zpow_eq, And.left, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_4
inst : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hx : (f : (a : α) → α) x ≠ x
hffx : (f : (a : α) → α) ((f : (a : α) → α) x : α) ≠ x
i : ℤ
hy :
  Ne (α := α) ((swap x ((f : (a : α) → α) x) * f : (a : α) → α) ((f ^ i : (a : α) → α) x : α) : α)
    ((f ^ i : (a : α) → α) x : α)
⊢ Eq (α := α) ((f ^ (i - 1) : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f ^ i : (a : α) → α) x : α)

Tactic:
simp [← mul_apply, -coe_mul, ← zpow_add_one]

Premises used: Equiv.Perm.coe_mul, zpow_add_one, Equiv.Perm.mul_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_4
inst : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hx : (f : (a : α) → α) x ≠ x
hffx : (f : (a : α) → α) ((f : (a : α) → α) x : α) ≠ x
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:
exact isCycle_swap_mul_aux₂ (i - 1) hy (by simp [← mul_apply, -coe_mul, ← zpow_add_one])

Premises used: HSub.hSub, Equiv.Perm.isCycle_swap_mul_aux₂, OfNat.ofNat
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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
⊢ Eq (α := ℤˣ) (((Perm.sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
    (((Perm.sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ)
        (swap x ((f : (a : α) → α) x) * (swap x ((f : (a : α) → α) x) * f)) :
      ℤˣ)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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 α
rw₂ rw₃ : Equiv.refl α = Equiv.refl α
⊢ Equiv.trans f (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]

Premises used: Equiv.Perm.IsCycle.eq_swap_of_apply_apply_eq_self, And.left, Equiv.swap_apply_left, Equiv.swap_swap
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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 = 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]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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
rw : HMul.hMul (α := ℤˣ) (-1) 1 = -HPow.hPow (α := ℤˣ) (β := ℕ) (-1) 2
⊢ ((Perm.sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap x ((f : (a : α) → α) x) * (swap x ((f : (a : α) → α) x) * f)) =
    -HPow.hPow (α := ℤˣ) (-1) #f.support

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]

Premises used: Equiv.Perm.IsCycle.eq_swap_of_apply_apply_eq_self, Ne.symm, Equiv.Perm.sign_mul, Equiv.Perm.card_support_swap, And.left, Equiv.Perm.sign_one, Equiv.Perm.sign_swap
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
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
⊢ HMul.hMul (α := ℤˣ) (-1) 1 = -HPow.hPow (α := ℤˣ) (β := ℕ) (-1) 2

Tactic:
rfl