awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
hn :
  ∀ {b x : α} {f : Perm α},
    (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b →
      (f ^ n : (a : α) → α) ((f : (a : α) → α) x : α) = b →
        ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
b x : α
f : Perm α
hb : (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b
h : (f ^ (n + 1) : (a : α) → α) ((f : (a : α) → α) x : α) = b
hfbx : (f : (a : α) → α) x ≠ b
this : (f : (a : α) → α) b ≠ b ∧ b ≠ x
hb' :
  Ne (α := α) ((swap x ((f : (a : α) → α) x) * f : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) : α)
    ((Equiv.symm f : (a : α) → α) b : α)
⊢ Eq (α := α) ((f : (a : α) → α) ((f ^ n : (a : α) → α) ((f : (a : α) → α) x : α) : α) : α)
    ((f : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) : α)

Tactic:
simpa [pow_succ'] using h

Premises used: pow_succ'
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
hn :
  ∀ {b x : α} {f : Perm α},
    (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b →
      (f ^ n : (a : α) → α) ((f : (a : α) → α) x : α) = b →
        ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
b x : α
f : Perm α
hb : (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b
h : (f ^ (n + 1) : (a : α) → α) ((f : (a : α) → α) x : α) = b
hfbx : (f : (a : α) → α) x ≠ b
this : (f : (a : α) → α) b ≠ b ∧ b ≠ x
hb' :
  Ne (α := α) ((swap x ((f : (a : α) → α) x) * f : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) : α)
    ((Equiv.symm f : (a : α) → α) b : α)
succ :
  ∀ (i : ℤ)
    (hi :
      Eq (α := α) (((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) : α)
        ((Equiv.symm f : (a : α) → α) b : α)),
    ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
⊢ ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b

Tactic:
obtain ⟨i, hi⟩ := hn hb' <| f.injective <| by simpa [pow_succ'] using h

Premises used: Equiv.injective
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
hn :
  ∀ {b x : α} {f : Perm α},
    (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b →
      (f ^ n : (a : α) → α) ((f : (a : α) → α) x : α) = b →
        ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
b x : α
f : Perm α
hb : (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b
h : (f ^ (n + 1) : (a : α) → α) ((f : (a : α) → α) x : α) = b
hfbx : (f : (a : α) → α) x ≠ b
this : (f : (a : α) → α) b ≠ b ∧ b ≠ x
hb' :
  Ne (α := α) ((swap x ((f : (a : α) → α) x) * f : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) : α)
    ((Equiv.symm f : (a : α) → α) b : α)
i : ℤ
hi :
  Eq (α := α) (((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) : α)
    ((Equiv.symm f : (a : α) → α) b : α)
⊢ ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b

Tactic:
⟨i + 1, ?_⟩

Premises used: HAdd.hAdd, Exists.intro, OfNat.ofNat
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
hn :
  ∀ {b x : α} {f : Perm α},
    (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b →
      (f ^ n : (a : α) → α) ((f : (a : α) → α) x : α) = b →
        ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
b x : α
f : Perm α
hb : (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b
h : (f ^ (n + 1) : (a : α) → α) ((f : (a : α) → α) x : α) = b
hfbx : (f : (a : α) → α) x ≠ b
this : (f : (a : α) → α) b ≠ b ∧ b ≠ x
hb' :
  Ne (α := α) ((swap x ((f : (a : α) → α) x) * f : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) : α)
    ((Equiv.symm f : (a : α) → α) b : α)
i : ℤ
hi :
  Eq (α := α) (((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) : α)
    ((Equiv.symm f : (a : α) → α) b : α)
succ : ((swap x ((f : (a : α) → α) x) * f) ^ (i + 1) : (a : α) → α) ((f : (a : α) → α) x : α) = b
⊢ ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b

Tactic:
refine ⟨i + 1, ?_⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
hn :
  ∀ {b x : α} {f : Perm α},
    (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b →
      (f ^ n : (a : α) → α) ((f : (a : α) → α) x : α) = b →
        ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
b x : α
f : Perm α
hb : (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b
h : (f ^ (n + 1) : (a : α) → α) ((f : (a : α) → α) x : α) = b
hfbx : (f : (a : α) → α) x ≠ b
this : (f : (a : α) → α) b ≠ b ∧ b ≠ x
hb' :
  Ne (α := α) ((swap x ((f : (a : α) → α) x) * f : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) : α)
    ((Equiv.symm f : (a : α) → α) b : α)
i : ℤ
hi :
  Eq (α := α) (((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) : α)
    ((Equiv.symm f : (a : α) → α) b : α)
succ : ((swap x ((f : (a : α) → α) x) * f) ^ (1 + i) : (a : α) → α) ((f : (a : α) → α) x : α) = b
succ₁ :
  (HPow.hPow (β := ℤ) (swap x ((f : (a : α) → α) x) * f) 1 * (swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α)
      ((f : (a : α) → α) x : α) =
    b
succ₂ :
  (HPow.hPow (β := ℤ) (swap x ((f : (a : α) → α) x) * f) 1 : (a : α) → α)
      (((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) : α) =
    b
succ₃ : (HPow.hPow (β := ℤ) (swap x ((f : (a : α) → α) x) * f) 1 : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) = b
succ₄ : (swap x ((f : (a : α) → α) x) * f : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) = b
succ₅ : (swap x ((f : (a : α) → α) x) : (a : α) → α) ((f : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) : α) = b
succ₆ : (swap x ((f : (a : α) → α) x) : (a : α) → α) b = b
succ₇ succ₈ : b = b
⊢ ((swap x ((f : (a : α) → α) x) * f) ^ (i + 1) : (a : α) → α) ((f : (a : α) → α) x : α) = b

Tactic:
rw [add_comm, zpow_add, mul_apply, hi, zpow_one, mul_apply, apply_symm_apply,
      swap_apply_of_ne_of_ne (ne_and_ne_of_swap_mul_apply_ne_self hb).2 hfbx.symm]

Premises used: Equiv.apply_symm_apply, zpow_add, zpow_one, Ne.symm, add_comm, Equiv.swap_apply_of_ne_of_ne, Equiv.Perm.ne_and_ne_of_swap_mul_apply_ne_self, And.right, Equiv.Perm.mul_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
zero :
  ∀ {b x : α} {f : Perm α},
    (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b →
      (HPow.hPow (β := ℕ) f 0 : (a : α) → α) ((f : (a : α) → α) x : α) = b →
        ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
succ :
  ∀ (n : ℕ)
    (hn :
      ∀ {b x : α} {f : Perm α},
        (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b →
          (f ^ n : (a : α) → α) ((f : (a : α) → α) x : α) = b →
            ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b)
    {b x : α} {f : Perm α},
    (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b →
      (f ^ (n + 1) : (a : α) → α) ((f : (a : α) → α) x : α) = b →
        ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
⊢ ∀ {b x : α} {f : Perm α},
    (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b →
      (f ^ n : (a : α) → α) ((f : (a : α) → α) x : α) = b →
        ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b

Tactic:
induction n with
  | zero => exact fun _ h => ⟨0, h⟩
  | succ n hn =>
    intro b x f hb h
    obtain hfbx | hfbx := eq_or_ne (f x) b
    · exact ⟨0, hfbx⟩
    have : f b ≠ b ∧ b ≠ x := ne_and_ne_of_swap_mul_apply_ne_self hb
    have hb' : (swap x (f x) * f) (f.symm b) ≠ f.symm b := by
      simpa [swap_apply_of_ne_of_ne this.2 hfbx.symm, eq_symm_apply, f.injective.eq_iff]
        using this.1
    obtain ⟨i, hi⟩ := hn hb' <| f.injective <| by simpa [pow_succ'] using h
    refine ⟨i + 1, ?_⟩
    rw [add_comm, zpow_add, mul_apply, hi, zpow_one, mul_apply, apply_symm_apply,
      swap_apply_of_ne_of_ne (ne_and_ne_of_swap_mul_apply_ne_self hb).2 hfbx.symm]

Premises used: Equiv.apply_symm_apply, zpow_add, zpow_one, add_comm, Equiv.Perm.mul_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b
h : (f ^ Int.negSucc n : (a : α) → α) ((f : (a : α) → α) x : α) = b
inl :
  ∀ (hfxb : (f : (a : α) → α) x = b),
    ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
inr :
  ∀ (hfxb : (f : (a : α) → α) x ≠ b),
    ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
⊢ ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b

Tactic:
obtain hfxb | hfxb := eq_or_ne (f x) b

Premises used: eq_or_ne, DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b
h : (f ^ Int.negSucc n : (a : α) → α) ((f : (a : α) → α) x : α) = b
hfxb : (f : (a : α) → α) x = b
⊢ ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b

Tactic:
⟨0, hfxb⟩

Premises used: Exists.intro, OfNat.ofNat
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b
h : (f ^ Int.negSucc n : (a : α) → α) ((f : (a : α) → α) x : α) = b
hfxb : (f : (a : α) → α) x = b
⊢ ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b

Tactic:
exact ⟨0, hfxb⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b
h : (f ^ Int.negSucc n : (a : α) → α) ((f : (a : α) → α) x : α) = b
hfxb : (f : (a : α) → α) x ≠ b
⊢ (f : (a : α) → α) b ≠ b ∧ b ≠ x

Tactic:
ne_and_ne_of_swap_mul_apply_ne_self hb

Premises used: Equiv.Perm.ne_and_ne_of_swap_mul_apply_ne_self
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b
h : (f ^ Int.negSucc n : (a : α) → α) ((f : (a : α) → α) x : α) = b
hfxb : (f : (a : α) → α) x ≠ b
⊢ (f : (a : α) → α) b ≠ b

Tactic:
obtain ⟨hfb, hbx⟩ : f b ≠ b ∧ b ≠ x := ne_and_ne_of_swap_mul_apply_ne_self hb

Premises used: Equiv.Perm.ne_and_ne_of_swap_mul_apply_ne_self, DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b
h : (f ^ Int.negSucc n : (a : α) → α) ((f : (a : α) → α) x : α) = b
hfxb : (f : (a : α) → α) x ≠ b
hfb : (f : (a : α) → α) b ≠ b
⊢ b ≠ x

Tactic:
obtain ⟨hfb, hbx⟩ : f b ≠ b ∧ b ≠ x := ne_and_ne_of_swap_mul_apply_ne_self hb

Premises used: Equiv.Perm.ne_and_ne_of_swap_mul_apply_ne_self, DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b
h : (f ^ Int.negSucc n : (a : α) → α) ((f : (a : α) → α) x : α) = b
hfxb : (f : (a : α) → α) x ≠ b
hfb : (f : (a : α) → α) b ≠ b
hbx : b ≠ x
rw :
  Ne (α := α)
    (if (f⁻¹ : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) = x then (Equiv.symm f : (a : α) → α) x
      else
        if
            Eq (α := α) ((f⁻¹ : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) : α)
              ((Equiv.symm f : (a : α) → α) x : α) then
          x
        else (f⁻¹ : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) :
      α)
    ((Equiv.symm f : (a : α) → α) b : α)
⊢ Ne (α := α) ((swap x ((Equiv.symm f : (a : α) → α) x) * f⁻¹ : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) : α)
    ((Equiv.symm f : (a : α) → α) b : α)

Tactic:
rw [mul_apply, swap_apply_def]

Premises used: Equiv.swap_apply_def, Equiv.Perm.mul_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b
h : (f ^ Int.negSucc n : (a : α) → α) ((f : (a : α) → α) x : α) = b
hfxb : (f : (a : α) → α) x ≠ b
hfb : (f : (a : α) → α) b ≠ b
hbx : b ≠ x
pos :
  (f⁻¹ : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) = x →
    Ne (α := α) ((Equiv.symm f : (a : α) → α) x : α) ((Equiv.symm f : (a : α) → α) b : α)
pos₁ :
  ¬(f⁻¹ : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) = x →
    Eq (α := α) ((f⁻¹ : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) : α) ((Equiv.symm f : (a : α) → α) x : α) →
      x ≠ (Equiv.symm f : (a : α) → α) b
neg :
  ¬(f⁻¹ : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) = x →
    ¬Eq (α := α) ((f⁻¹ : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) : α) ((Equiv.symm f : (a : α) → α) x : α) →
      Ne (α := α) ((f⁻¹ : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) : α) ((Equiv.symm f : (a : α) → α) b : α)
⊢ Ne (α := α)
    (if (f⁻¹ : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) = x then (Equiv.symm f : (a : α) → α) x
      else
        if
            Eq (α := α) ((f⁻¹ : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) : α)
              ((Equiv.symm f : (a : α) → α) x : α) then
          x
        else (f⁻¹ : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) :
      α)
    ((Equiv.symm f : (a : α) → α) b : α)

Tactic:
split_ifs
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b
h : (f ^ Int.negSucc n : (a : α) → α) ((f : (a : α) → α) x : α) = b
hfxb : (f : (a : α) → α) x ≠ b
hfb : (f : (a : α) → α) b ≠ b
hbx : b ≠ x
h_1 : (f⁻¹ : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) = x
pos :
  ∀ (h : Eq (α := α) ((f : (a : α) → α) x : α) ((f ^ (n + 1) : (a : α) → α) b : α)),
    b = (f : (a : α) → α) ((f : (a : α) → α) x : α) → ¬x = b
⊢ Ne (α := α) ((Equiv.symm f : (a : α) → α) x : α) ((Equiv.symm f : (a : α) → α) b : α)

Tactic:
simp [symm_apply_eq, eq_symm_apply] at *

Premises used: Equiv.symm_apply_eq, Equiv.eq_symm_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b
h : (f ^ Int.negSucc n : (a : α) → α) ((f : (a : α) → α) x : α) = b
hfxb : (f : (a : α) → α) x ≠ b
hfb : (f : (a : α) → α) b ≠ b
hbx : b ≠ x
h_1 : ¬(f⁻¹ : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) = x
h_2 : Eq (α := α) ((f⁻¹ : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) : α) ((Equiv.symm f : (a : α) → α) x : α)
pos :
  ∀ (h : Eq (α := α) ((f : (a : α) → α) x : α) ((f ^ (n + 1) : (a : α) → α) b : α)),
    ¬b = (f : (a : α) → α) ((f : (a : α) → α) x : α) → b = (f : (a : α) → α) x → ¬(f : (a : α) → α) x = b
⊢ x ≠ (Equiv.symm f : (a : α) → α) b

Tactic:
simp [symm_apply_eq, eq_symm_apply] at *

Premises used: Equiv.symm_apply_eq, Equiv.eq_symm_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b
h : (f ^ Int.negSucc n : (a : α) → α) ((f : (a : α) → α) x : α) = b
hfxb : (f : (a : α) → α) x ≠ b
hfb : (f : (a : α) → α) b ≠ b
hbx : b ≠ x
h_1 : ¬(f⁻¹ : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) = x
h_2 : ¬Eq (α := α) ((f⁻¹ : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) : α) ((Equiv.symm f : (a : α) → α) x : α)
neg :
  ∀ (h : Eq (α := α) ((f : (a : α) → α) x : α) ((f ^ (n + 1) : (a : α) → α) b : α)),
    ¬b = (f : (a : α) → α) ((f : (a : α) → α) x : α) → ¬b = (f : (a : α) → α) x → ¬b = (f : (a : α) → α) b
⊢ Ne (α := α) ((f⁻¹ : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) : α) ((Equiv.symm f : (a : α) → α) b : α)

Tactic:
simp [symm_apply_eq, eq_symm_apply] at *

Premises used: Equiv.symm_apply_eq, Equiv.eq_symm_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : ¬(swap x ((f : (a : α) → α) x) : (a : α) → α) ((f : (a : α) → α) b : α) = b
hfxb : ¬(f : (a : α) → α) x = b
hfb : ¬(f : (a : α) → α) b = b
hbx : ¬b = x
h : Eq (α := α) ((f : (a : α) → α) x : α) ((f ^ (n + 1) : (a : α) → α) b : α)
h_1 : b = (f : (a : α) → α) ((f : (a : α) → α) x : α)
pos pos₁ pos₂ pos₃ pos₄ pos₅ pos₆ pos₇ : x = b → False
⊢ ¬x = b

Tactic:
tauto
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : ¬(swap x ((f : (a : α) → α) x) : (a : α) → α) ((f : (a : α) → α) b : α) = b
hfxb : ¬(f : (a : α) → α) x = b
hfb : ¬(f : (a : α) → α) b = b
hbx : ¬b = x
h : Eq (α := α) ((f : (a : α) → α) x : α) ((f ^ (n + 1) : (a : α) → α) b : α)
h_1 : ¬b = (f : (a : α) → α) ((f : (a : α) → α) x : α)
h_2 : b = (f : (a : α) → α) x
⊢ ¬(f : (a : α) → α) x = b

Tactic:
tauto
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : ¬(swap x ((f : (a : α) → α) x) : (a : α) → α) ((f : (a : α) → α) b : α) = b
hfxb : ¬(f : (a : α) → α) x = b
hfb : ¬(f : (a : α) → α) b = b
hbx : ¬b = x
h : Eq (α := α) ((f : (a : α) → α) x : α) ((f ^ (n + 1) : (a : α) → α) b : α)
h_1 : ¬b = (f : (a : α) → α) ((f : (a : α) → α) x : α)
h_2 : ¬b = (f : (a : α) → α) x
neg neg₁ neg₂ neg₃ neg₄ neg₅ neg₆ neg₇ : b = (f : (a : α) → α) b → False
⊢ ¬b = (f : (a : α) → α) b

Tactic:
tauto
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : (swap x ((f : (a : α) → α) x) * f : (a : α) → α) b ≠ b
h : (f ^ Int.negSucc n : (a : α) → α) ((f : (a : α) → α) x : α) = b
hfxb : (f : (a : α) → α) x ≠ b
hfb : (f : (a : α) → α) b ≠ b
hbx : b ≠ x
⊢ Ne (α := α) ((swap x ((Equiv.symm f : (a : α) → α) x) * f⁻¹ : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) : α)
    ((Equiv.symm f : (a : α) → α) b : α)

Tactic:
replace hb : (swap x (f.symm x) * f⁻¹) (f.symm b) ≠ f.symm b := by
      rw [mul_apply, swap_apply_def]
      split_ifs <;> simp [symm_apply_eq, eq_symm_apply] at * <;> tauto
-- 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 : α)
rw : Eq (α := α) ((Equiv.symm f ^ (n + 1) : (a : α) → α) x : α) ((Equiv.symm f : (a : α) → α) b : α)
⊢ Eq (α := α) ((Equiv.symm f ^ n : (a : α) → α) ((Equiv.symm f : (a : α) → α) x : α) : α)
    ((Equiv.symm f : (a : α) → α) b : α)

Tactic:
rw [← mul_apply, ← pow_succ]

Premises used: pow_succ, Equiv.Perm.mul_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 : α)
⊢ Eq (α := α) ((Equiv.symm f ^ (n + 1) : (a : α) → α) x : α) ((Equiv.symm f : (a : α) → α) b : α)

Tactic:
simpa [pow_succ', eq_symm_apply] using h

Premises used: pow_succ', 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 : α)
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
⊢ ∃ (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

Premises used: Equiv.Perm.isCycle_swap_mul_aux₁
-- 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 : α)
⊢ ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b

Tactic:
⟨-i, (swap x (f⁻¹ x) * f⁻¹).injective ?_⟩

Premises used: HMul.hMul, Equiv.swap, Inv.inv, Exists.intro, Equiv.injective, DFunLike.coe, Neg.neg
-- 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 : α)
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 : α)
⊢ ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b

Tactic:
refine ⟨-i, (swap x (f⁻¹ x) * f⁻¹).injective ?_⟩
-- 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 ((Equiv.symm f : (a : α) → α) x) * Equiv.symm f) ^ i : (a : α) → α) ((Equiv.symm f : (a : α) → α) x : α) :
      α)
    ((Equiv.symm f : (a : α) → α) b : α)

Tactic:
hi