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 : ℕ
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
⊢ ((swap x ((f : (a : α) → α) x) * f) ^ (i + 1) : (a : α) → α) ((f : (a : α) → α) x : α) = b
have succ₃ : (HPow.hPow (β := ℤ) (swap x ((f : (a : α) → α) x) * f) 1 : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) = 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]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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
⊢ ((swap x ((f : (a : α) → α) x) * f) ^ (i + 1) : (a : α) → α) ((f : (a : α) → α) x : α) = b
have succ₄ : (swap x ((f : (a : α) → α) x) * f : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) = 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]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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
⊢ ((swap x ((f : (a : α) → α) x) * f) ^ (i + 1) : (a : α) → α) ((f : (a : α) → α) x : α) = b
have succ₅ : (swap x ((f : (a : α) → α) x) : (a : α) → α) ((f : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) : α) = 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]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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
⊢ ((swap x ((f : (a : α) → α) x) * f) ^ (i + 1) : (a : α) → α) ((f : (a : α) → α) x : α) = b
have succ₆ : (swap x ((f : (a : α) → α) x) : (a : α) → α) b = 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]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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
⊢ ((swap x ((f : (a : α) → α) x) * f) ^ (i + 1) : (a : α) → α) ((f : (a : α) → α) x : α) = b
have succ₇ : b = 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]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
Goal:
α : Type u_4
inst : DecidableEq α
n : ℕ
⊢ ∀ {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
have 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
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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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
⊢ ∀ {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
have 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
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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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
⊢ ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
have inl : ∀ (hfxb : (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
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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
⊢ ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
have inr : ∀ (hfxb : (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
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
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
have hfb : (f : (a : α) → α) b ≠ b
Tactic: obtain ⟨hfb, hbx⟩ : f b ≠ b ∧ b ≠ x := ne_and_ne_of_swap_mul_apply_ne_self hb
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
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
⊢ ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
have hbx : b ≠ x
Tactic: obtain ⟨hfb, hbx⟩ : f b ≠ b ∧ b ≠ x := ne_and_ne_of_swap_mul_apply_ne_self hb
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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 : α)
have 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 : α)
Tactic: rw [mul_apply, swap_apply_def]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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 (α := α)
    (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 : α)
have pos : (f⁻¹ : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) = x →
  Ne (α := α) ((Equiv.symm f : (a : α) → α) x : α) ((Equiv.symm f : (a : α) → α) b : α)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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 : α)
⊢ 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 : α)
have 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
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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
⊢ 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 : α)
have 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 : α)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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
⊢ Ne (α := α) ((Equiv.symm f : (a : α) → α) x : α) ((Equiv.symm f : (a : α) → α) b : α)
have pos : ∀ (h : Eq (α := α) ((f : (a : α) → α) x : α) ((f ^ (n + 1) : (a : α) → α) b : α)),
  b = (f : (a : α) → α) ((f : (a : α) → α) x : α) → ¬x = b
Tactic: simp [symm_apply_eq, eq_symm_apply] at *
Cleared hypotheses: h, h_1
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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 : α)
⊢ x ≠ (Equiv.symm f : (a : α) → α) b
have 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
Tactic: simp [symm_apply_eq, eq_symm_apply] at *
Cleared hypotheses: h, h_1, h_2
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (goal)
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 : α)
⊢ Ne (α := α) ((f⁻¹ : (a : α) → α) ((Equiv.symm f : (a : α) → α) b : α) : α) ((Equiv.symm f : (a : α) → α) b : α)
have 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
Tactic: simp [symm_apply_eq, eq_symm_apply] at *
Cleared hypotheses: h, h_1, h_2
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Basic (hypothesis)
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
⊢ ∃ (i : ℤ), ((swap x ((f : (a : α) → α) x) * f) ^ i : (a : α) → α) ((f : (a : α) → α) x : α) = b
have hb₁ : 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
Cleared hypotheses: hb
-- 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 : α)
⊢ Eq (α := α) ((Equiv.symm f ^ n : (a : α) → α) ((Equiv.symm f : (a : α) → α) x : α) : α)
    ((Equiv.symm f : (a : α) → α) b : α)
have rw : Eq (α := α) ((Equiv.symm f ^ (n + 1) : (a : α) → α) x : α) ((Equiv.symm f : (a : α) → α) b : α)
Tactic: rw [← mul_apply, ← pow_succ]