awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_2 : α), (f : (a : α) → α) x_2 ≠ x_2 → x_2 ∈ x :: l
hfx : ¬x = (f : (a : α) → α) x
hy : ∀ (y : α), (swap x ((f : (a : α) → α) x) * f : (a : α) → α) y ≠ y → y ∈ l
x_1 : Fin n
⊢ (↑(((e.symm.trans (swap x ((f : (a : α) → α) x) * f)).trans e : (a : Fin n) → Fin n) x_1) : ℕ) =
    (↑((HMul.hMul (α := Perm (Fin n))
              (swap ((e : (a : α) → Fin n) x) ((e : (a : α) → Fin n) ((f : (a : α) → α) x)) : Perm (Fin n))
              ((e.symm.trans f).trans e) :
            (a : Fin n) → Fin n)
          x_1) :
      ℕ)
have H : (↑(((e.symm.trans (Equiv.trans f (swap x ((f : (a : α) → α) x)))).trans e : (a : Fin n) → Fin n) x_1) : ℕ) =
  (↑((((e.symm.trans f).trans e).trans (swap ((e : (a : α) → Fin n) x) ((e : (a : α) → Fin n) ((f : (a : α) → α) x))) :
          (a : Fin n) → Fin n)
        x_1) :
    ℕ)
Tactic: rw [← Equiv.symm_trans_swap_trans, mul_def, Equiv.symm_trans_swap_trans, mul_def]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_2 : α), (f : (a : α) → α) x_2 ≠ x_2 → x_2 ∈ x :: l
hfx : ¬x = (f : (a : α) → α) x
hy : ∀ (y : α), (swap x ((f : (a : α) → α) x) * f : (a : α) → α) y ≠ y → y ∈ l
x_1 : Fin n
⊢ (↑(((e.symm.trans (Equiv.trans f (swap x ((f : (a : α) → α) x)))).trans e : (a : Fin n) → Fin n) x_1) : ℕ) =
    (↑((((e.symm.trans f).trans e).trans
              (swap ((e : (a : α) → Fin n) x) ((e : (a : α) → Fin n) ((f : (a : α) → α) x))) :
            (a : Fin n) → Fin n)
          x_1) :
      ℕ)
have H : (↑((e : (a : α) → Fin n) ((e.symm.trans (Equiv.trans f (swap x ((f : (a : α) → α) x))) : (a : Fin n) → α) x_1)) : ℕ) =
  (↑((((e.symm.trans f).trans e).trans (swap ((e : (a : α) → Fin n) x) ((e : (a : α) → Fin n) ((f : (a : α) → α) x))) :
          (a : Fin n) → Fin n)
        x_1) :
    ℕ)
Tactic: rw [trans_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_2 : α), (f : (a : α) → α) x_2 ≠ x_2 → x_2 ∈ x :: l
hfx : ¬x = (f : (a : α) → α) x
hy : ∀ (y : α), (swap x ((f : (a : α) → α) x) * f : (a : α) → α) y ≠ y → y ∈ l
x_1 : Fin n
⊢ (↑((e : (a : α) → Fin n) ((e.symm.trans (Equiv.trans f (swap x ((f : (a : α) → α) x))) : (a : Fin n) → α) x_1)) : ℕ) =
    (↑((((e.symm.trans f).trans e).trans
              (swap ((e : (a : α) → Fin n) x) ((e : (a : α) → Fin n) ((f : (a : α) → α) x))) :
            (a : Fin n) → Fin n)
          x_1) :
      ℕ)
have H : (↑((e : (a : α) → Fin n)
        ((Equiv.trans f (swap x ((f : (a : α) → α) x)) : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α))) :
    ℕ) =
  (↑((((e.symm.trans f).trans e).trans (swap ((e : (a : α) → Fin n) x) ((e : (a : α) → Fin n) ((f : (a : α) → α) x))) :
          (a : Fin n) → Fin n)
        x_1) :
    ℕ)
Tactic: rw [trans_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_2 : α), (f : (a : α) → α) x_2 ≠ x_2 → x_2 ∈ x :: l
hfx : ¬x = (f : (a : α) → α) x
hy : ∀ (y : α), (swap x ((f : (a : α) → α) x) * f : (a : α) → α) y ≠ y → y ∈ l
x_1 : Fin n
⊢ (↑((e : (a : α) → Fin n)
          ((Equiv.trans f (swap x ((f : (a : α) → α) x)) : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α))) :
      ℕ) =
    (↑((((e.symm.trans f).trans e).trans
              (swap ((e : (a : α) → Fin n) x) ((e : (a : α) → Fin n) ((f : (a : α) → α) x))) :
            (a : Fin n) → Fin n)
          x_1) :
      ℕ)
have H : (↑((e : (a : α) → Fin n)
        ((swap x ((f : (a : α) → α) x) : (a : α) → α) ((f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α) : α))) :
    ℕ) =
  (↑((((e.symm.trans f).trans e).trans (swap ((e : (a : α) → Fin n) x) ((e : (a : α) → Fin n) ((f : (a : α) → α) x))) :
          (a : Fin n) → Fin n)
        x_1) :
    ℕ)
Tactic: rw [trans_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_2 : α), (f : (a : α) → α) x_2 ≠ x_2 → x_2 ∈ x :: l
hfx : ¬x = (f : (a : α) → α) x
hy : ∀ (y : α), (swap x ((f : (a : α) → α) x) * f : (a : α) → α) y ≠ y → y ∈ l
x_1 : Fin n
⊢ (↑((e : (a : α) → Fin n)
          ((swap x ((f : (a : α) → α) x) : (a : α) → α) ((f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α) : α))) :
      ℕ) =
    (↑((((e.symm.trans f).trans e).trans
              (swap ((e : (a : α) → Fin n) x) ((e : (a : α) → Fin n) ((f : (a : α) → α) x))) :
            (a : Fin n) → Fin n)
          x_1) :
      ℕ)
have H : (↑((e : (a : α) → Fin n)
        ((swap x ((f : (a : α) → α) x) : (a : α) → α) ((f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α) : α))) :
    ℕ) =
  (↑(((swap ((e : (a : α) → Fin n) x) ((e : (a : α) → Fin n) ((f : (a : α) → α) x)) : Perm (Fin n)) :
          (a : Fin n) → Fin n)
        (((e.symm.trans f).trans e : (a : Fin n) → Fin n) x_1)) :
    ℕ)
Tactic: rw [trans_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_2 : α), (f : (a : α) → α) x_2 ≠ x_2 → x_2 ∈ x :: l
hfx : ¬x = (f : (a : α) → α) x
hy : ∀ (y : α), (swap x ((f : (a : α) → α) x) * f : (a : α) → α) y ≠ y → y ∈ l
x_1 : Fin n
⊢ (↑((e : (a : α) → Fin n)
          ((swap x ((f : (a : α) → α) x) : (a : α) → α) ((f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α) : α))) :
      ℕ) =
    (↑(((swap ((e : (a : α) → Fin n) x) ((e : (a : α) → Fin n) ((f : (a : α) → α) x)) : Perm (Fin n)) :
            (a : Fin n) → Fin n)
          (((e.symm.trans f).trans e : (a : Fin n) → Fin n) x_1)) :
      ℕ)
have H : (↑((e : (a : α) → Fin n)
        ((swap x ((f : (a : α) → α) x) : (a : α) → α) ((f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α) : α))) :
    ℕ) =
  (↑(((swap ((e : (a : α) → Fin n) x) ((e : (a : α) → Fin n) ((f : (a : α) → α) x)) : Perm (Fin n)) :
          (a : Fin n) → Fin n)
        ((e : (a : α) → Fin n) ((e.symm.trans f : (a : Fin n) → α) x_1))) :
    ℕ)
Tactic: rw [trans_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_2 : α), (f : (a : α) → α) x_2 ≠ x_2 → x_2 ∈ x :: l
hfx : ¬x = (f : (a : α) → α) x
hy : ∀ (y : α), (swap x ((f : (a : α) → α) x) * f : (a : α) → α) y ≠ y → y ∈ l
x_1 : Fin n
⊢ (↑((e : (a : α) → Fin n)
          ((swap x ((f : (a : α) → α) x) : (a : α) → α) ((f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α) : α))) :
      ℕ) =
    (↑(((swap ((e : (a : α) → Fin n) x) ((e : (a : α) → Fin n) ((f : (a : α) → α) x)) : Perm (Fin n)) :
            (a : Fin n) → Fin n)
          ((e : (a : α) → Fin n) ((e.symm.trans f : (a : Fin n) → α) x_1))) :
      ℕ)
have H : (↑((e : (a : α) → Fin n)
        ((swap x ((f : (a : α) → α) x) : (a : α) → α) ((f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α) : α))) :
    ℕ) =
  (↑(((swap ((e : (a : α) → Fin n) x) ((e : (a : α) → Fin n) ((f : (a : α) → α) x)) : Perm (Fin n)) :
          (a : Fin n) → Fin n)
        ((e : (a : α) → Fin n) ((f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α)))) :
    ℕ)
Tactic: rw [trans_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_2 : α), (f : (a : α) → α) x_2 ≠ x_2 → x_2 ∈ x :: l
hfx : ¬x = (f : (a : α) → α) x
hy : ∀ (y : α), (swap x ((f : (a : α) → α) x) * f : (a : α) → α) y ≠ y → y ∈ l
x_1 : Fin n
⊢ (↑(((e.symm.trans (Equiv.trans f (swap x ((f : (a : α) → α) x)))).trans e : (a : Fin n) → Fin n) x_1) : ℕ) =
    (↑((((e.symm.trans f).trans e).trans
              (swap ((e : (a : α) → Fin n) x) ((e : (a : α) → Fin n) ((f : (a : α) → α) x))) :
            (a : Fin n) → Fin n)
          x_1) :
      ℕ)
have H : (↑((e : (a : α) → Fin n)
        ((swap x ((f : (a : α) → α) x) : (a : α) → α) ((f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α) : α))) :
    ℕ) =
  (↑(((swap ((e : (a : α) → Fin n) x) ((e : (a : α) → Fin n) ((f : (a : α) → α) x)) : Perm (Fin n)) :
          (a : Fin n) → Fin n)
        ((e : (a : α) → Fin n) ((f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α)))) :
    ℕ)
Tactic: repeat (rw [trans_apply])
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_2 : α), (f : (a : α) → α) x_2 ≠ x_2 → x_2 ∈ x :: l
hfx : ¬x = (f : (a : α) → α) x
hy : ∀ (y : α), (swap x ((f : (a : α) → α) x) * f : (a : α) → α) y ≠ y → y ∈ l
x_1 : Fin n
⊢ (↑((e : (a : α) → Fin n)
          ((swap x ((f : (a : α) → α) x) : (a : α) → α) ((f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α) : α))) :
      ℕ) =
    (↑(((swap ((e : (a : α) → Fin n) x) ((e : (a : α) → Fin n) ((f : (a : α) → α) x)) : Perm (Fin n)) :
            (a : Fin n) → Fin n)
          ((e : (a : α) → Fin n) ((f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α)))) :
      ℕ)
have H : (↑((e : (a : α) → Fin n)
        (if (f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α) = x then (f : (a : α) → α) x
        else
          if (e.symm : (a : Fin n) → α) x_1 = x then x else (f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α))) :
    ℕ) =
  (↑(if (f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α) = x then (e : (a : α) → Fin n) ((f : (a : α) → α) x)
      else
        if (e.symm : (a : Fin n) → α) x_1 = x then (e : (a : α) → Fin n) x
        else (e : (a : α) → Fin n) ((f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α))) :
    ℕ)
Tactic: simp [swap, swapCore]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_2 : α), (f : (a : α) → α) x_2 ≠ x_2 → x_2 ∈ x :: l
hfx : ¬x = (f : (a : α) → α) x
hy : ∀ (y : α), (swap x ((f : (a : α) → α) x) * f : (a : α) → α) y ≠ y → y ∈ l
x_1 : Fin n
⊢ (↑((e : (a : α) → Fin n)
          (if (f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α) = x then (f : (a : α) → α) x
          else
            if (e.symm : (a : Fin n) → α) x_1 = x then x else (f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α))) :
      ℕ) =
    (↑(if (f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α) = x then (e : (a : α) → Fin n) ((f : (a : α) → α) x)
        else
          if (e.symm : (a : Fin n) → α) x_1 = x then (e : (a : α) → Fin n) x
          else (e : (a : α) → Fin n) ((f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α))) :
      ℕ)
have pos : (f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α) = x →
  (↑((e : (a : α) → Fin n) ((f : (a : α) → α) x)) : ℕ) = (↑((e : (a : α) → Fin n) ((f : (a : α) → α) x)) : ℕ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_2 : α), (f : (a : α) → α) x_2 ≠ x_2 → x_2 ∈ x :: l
hfx : ¬x = (f : (a : α) → α) x
hy : ∀ (y : α), (swap x ((f : (a : α) → α) x) * f : (a : α) → α) y ≠ y → y ∈ l
x_1 : Fin n
pos :
  (f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α) = x →
    (↑((e : (a : α) → Fin n) ((f : (a : α) → α) x)) : ℕ) = (↑((e : (a : α) → Fin n) ((f : (a : α) → α) x)) : ℕ)
⊢ (↑((e : (a : α) → Fin n)
          (if (f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α) = x then (f : (a : α) → α) x
          else
            if (e.symm : (a : Fin n) → α) x_1 = x then x else (f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α))) :
      ℕ) =
    (↑(if (f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α) = x then (e : (a : α) → Fin n) ((f : (a : α) → α) x)
        else
          if (e.symm : (a : Fin n) → α) x_1 = x then (e : (a : α) → Fin n) x
          else (e : (a : α) → Fin n) ((f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α))) :
      ℕ)
have pos₁ : ¬(f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α) = x →
  (e.symm : (a : Fin n) → α) x_1 = x → (↑((e : (a : α) → Fin n) x) : ℕ) = (↑((e : (a : α) → Fin n) x) : ℕ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_2 : α), (f : (a : α) → α) x_2 ≠ x_2 → x_2 ∈ x :: l
hfx : ¬x = (f : (a : α) → α) x
hy : ∀ (y : α), (swap x ((f : (a : α) → α) x) * f : (a : α) → α) y ≠ y → y ∈ l
x_1 : Fin n
pos :
  (f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α) = x →
    (↑((e : (a : α) → Fin n) ((f : (a : α) → α) x)) : ℕ) = (↑((e : (a : α) → Fin n) ((f : (a : α) → α) x)) : ℕ)
pos₁ :
  ¬(f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α) = x →
    (e.symm : (a : Fin n) → α) x_1 = x → (↑((e : (a : α) → Fin n) x) : ℕ) = (↑((e : (a : α) → Fin n) x) : ℕ)
⊢ (↑((e : (a : α) → Fin n)
          (if (f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α) = x then (f : (a : α) → α) x
          else
            if (e.symm : (a : Fin n) → α) x_1 = x then x else (f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α))) :
      ℕ) =
    (↑(if (f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α) = x then (e : (a : α) → Fin n) ((f : (a : α) → α) x)
        else
          if (e.symm : (a : Fin n) → α) x_1 = x then (e : (a : α) → Fin n) x
          else (e : (a : α) → Fin n) ((f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α))) :
      ℕ)
have neg : ¬(f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α) = x →
  ¬(e.symm : (a : Fin n) → α) x_1 = x →
    (↑((e : (a : α) → Fin n) ((f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α))) : ℕ) =
      (↑((e : (a : α) → Fin n) ((f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α))) : ℕ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (hypothesis)
Goal:
α : Type u
inst : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), (f : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = (f : (a : α) → α) x
hy : ∀ (y : α), (swap x ((f : (a : α) → α) x) * f : (a : α) → α) y ≠ y → y ∈ l
⊢ signAux ((e.symm.trans f).trans e) =
    if x = (f : (a : α) → α) x then signAux2 l f else -signAux2 l (swap x ((f : (a : α) → α) x) * f)
have this : (e.symm.trans (swap x ((f : (a : α) → α) x) * f)).trans e =
  HMul.hMul (α := Perm (Fin n))
    (swap ((e : (a : α) → Fin n) x) ((e : (a : α) → Fin n) ((f : (a : α) → α) x)) : Perm (Fin n))
    ((e.symm.trans f).trans e)
Tactic: have : (e.symm.trans (swap x (f x) * f)).trans e =
          swap (e x) (e (f x)) * (e.symm.trans f).trans e := by
        ext
        rw [← Equiv.symm_trans_swap_trans, mul_def, Equiv.symm_trans_swap_trans, mul_def]
        repeat (rw [trans_apply])
        simp [swap, swapCore]
        split_ifs <;> rfl
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (hypothesis)
Goal:
α : Type u
inst : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), (f : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = (f : (a : α) → α) x
hy : ∀ (y : α), (swap x ((f : (a : α) → α) x) * f : (a : α) → α) y ≠ y → y ∈ l
this :
  (e.symm.trans (swap x ((f : (a : α) → α) x) * f)).trans e =
    HMul.hMul (α := Perm (Fin n))
      (swap ((e : (a : α) → Fin n) x) ((e : (a : α) → Fin n) ((f : (a : α) → α) x)) : Perm (Fin n))
      ((e.symm.trans f).trans e)
⊢ signAux ((e.symm.trans f).trans e) =
    if x = (f : (a : α) → α) x then signAux2 l f else -signAux2 l (swap x ((f : (a : α) → α) x) * f)
have hefx : Ne (α := Fin n) ((e : (a : α) → Fin n) x : Fin n) ((e : (a : α) → Fin n) ((f : (a : α) → α) x) : Fin n)
Tactic: have hefx : e x ≠ e (f x) := mt e.injective.eq_iff.1 hfx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), (f : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = (f : (a : α) → α) x
hy : ∀ (y : α), (swap x ((f : (a : α) → α) x) * f : (a : α) → α) y ≠ y → y ∈ l
this :
  (e.symm.trans (swap x ((f : (a : α) → α) x) * f)).trans e =
    HMul.hMul (α := Perm (Fin n))
      (swap ((e : (a : α) → Fin n) x) ((e : (a : α) → Fin n) ((f : (a : α) → α) x)) : Perm (Fin n))
      ((e.symm.trans f).trans e)
hefx : Ne (α := Fin n) ((e : (a : α) → Fin n) x : Fin n) ((e : (a : α) → Fin n) ((f : (a : α) → α) x) : Fin n)
⊢ signAux ((e.symm.trans f).trans e) =
    if x = (f : (a : α) → α) x then signAux2 l f else -signAux2 l (swap x ((f : (a : α) → α) x) * f)
have neg : signAux ((e.symm.trans f).trans e) = -(-1 * signAux ((e.symm.trans f).trans e))
Tactic: rw [if_neg hfx, ← signAux_eq_signAux2 _ _ e hy, this, signAux_mul, signAux_swap hefx]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Finite α
f : Perm α
s : Multiset α
l₁ l₂ : List α
h : l₁ ≈ l₂
⊢ HEq (α := (∀ (x : α), x ∈ ⟦l₁⟧) → ℤˣ) fun (x : ∀ (x : α), x ∈ ⟦l₁⟧) ↦ signAux2 l₁ f (β := (∀ (x : α), x ∈ ⟦l₂⟧) → ℤˣ)
    fun (x : ∀ (x : α), x ∈ ⟦l₂⟧) ↦ signAux2 l₂ f
have rcases : ∀ (n : ℕ) (e : α ≃ Fin n),
  HEq (α := (∀ (x : α), x ∈ ⟦l₁⟧) → ℤˣ) fun (x : ∀ (x : α), x ∈ ⟦l₁⟧) ↦ signAux2 l₁ f (β := (∀ (x : α), x ∈ ⟦l₂⟧) → ℤˣ)
    fun (x : ∀ (x : α), x ∈ ⟦l₂⟧) ↦ signAux2 l₂ f
Tactic: rcases Finite.exists_equiv_fin α with ⟨n, ⟨e⟩⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Finite α
f : Perm α
s : Multiset α
l₁ l₂ : List α
h : l₁ ≈ l₂
n : ℕ
e : α ≃ Fin n
⊢ HEq (α := (∀ (x : α), x ∈ ⟦l₁⟧) → ℤˣ) fun (x : ∀ (x : α), x ∈ ⟦l₁⟧) ↦ signAux2 l₁ f (β := (∀ (x : α), x ∈ ⟦l₂⟧) → ℤˣ)
    fun (x : ∀ (x : α), x ∈ ⟦l₂⟧) ↦ signAux2 l₂ f
have refine : ∀ (h₁ : ∀ (x : α), x ∈ ⟦l₁⟧) (h₂ : ∀ (x : α), x ∈ ⟦l₂⟧), h₁ ≍ h₂ → signAux2 l₁ f ≍ signAux2 l₂ f
Tactic: refine Function.hfunext (forall_congr fun _ ↦ propext h.mem_iff) fun h₁ h₂ _ ↦ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Finite α
f : Perm α
s : Multiset α
l₁ l₂ : List α
h : l₁ ≈ l₂
n : ℕ
e : α ≃ Fin n
h₁ : ∀ (x : α), x ∈ ⟦l₁⟧
h₂ : ∀ (x : α), x ∈ ⟦l₂⟧
h_1 : h₁ ≍ h₂
⊢ signAux2 l₁ f ≍ signAux2 l₂ f
have rw : signAux ((e.symm.trans f).trans e) ≍ signAux2 l₂ f
Tactic: rw [← signAux_eq_signAux2 _ _ e fun _ _ => h₁ _, ← signAux_eq_signAux2 _ _ e fun _ _ => h₂ _]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Finite α
f : Perm α
s : Multiset α
l₁ l₂ : List α
h : l₁ ≈ l₂
n : ℕ
e : α ≃ Fin n
h₁ : ∀ (x : α), x ∈ ⟦l₁⟧
h₂ : ∀ (x : α), x ∈ ⟦l₂⟧
h_1 : h₁ ≍ h₂
rw : signAux ((e.symm.trans f).trans e) ≍ signAux2 l₂ f
⊢ signAux2 l₁ f ≍ signAux2 l₂ f
have rw₁ : signAux ((e.symm.trans f).trans e) ≍ signAux ((e.symm.trans f).trans e)
Tactic: rw [← signAux_eq_signAux2 _ _ e fun _ _ => h₁ _, ← signAux_eq_signAux2 _ _ e fun _ _ => h₂ _]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
f g : Perm α
s : Multiset α
hs : ∀ (x : α), x ∈ s
⊢ (f * g).signAux3 hs = f.signAux3 hs * g.signAux3 hs ∧ Pairwise fun (x y : α) ↦ (swap x y).signAux3 hs = -1
have obtain : ∀ (n : ℕ) (e : α ≃ Fin n),
  (f * g).signAux3 hs = f.signAux3 hs * g.signAux3 hs ∧ Pairwise fun (x y : α) ↦ (swap x y).signAux3 hs = -1
Tactic: obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin α
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
f g : Perm α
s : Multiset α
hs : ∀ (x : α), x ∈ s
n : ℕ
e : α ≃ Fin n
⊢ (f * g).signAux3 hs = f.signAux3 hs * g.signAux3 hs ∧ Pairwise fun (x y : α) ↦ (swap x y).signAux3 hs = -1
have h : ∀ (l : List α) (hs : ∀ (x : α), x ∈ ⟦l⟧),
  (f * g).signAux3 hs = f.signAux3 hs * g.signAux3 hs ∧ Pairwise fun (x y : α) ↦ (swap x y).signAux3 hs = -1
Tactic: induction s using Quotient.inductionOn with | _ l => ?_
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
f g : Perm α
n : ℕ
e : α ≃ Fin n
l : List α
hs : ∀ (x : α), x ∈ ⟦l⟧
⊢ (f * g).signAux3 hs = f.signAux3 hs * g.signAux3 hs ∧ Pairwise fun (x y : α) ↦ (swap x y).signAux3 hs = -1
have h : signAux2 l (f * g) = signAux2 l f * signAux2 l g ∧ Pairwise fun (x y : α) ↦ signAux2 l (swap x y) = -1
Tactic: change
    signAux2 l (f * g) = signAux2 l f * signAux2 l g ∧
    Pairwise fun x y => signAux2 l (swap x y) = -1
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (hypothesis)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
f g : Perm α
n : ℕ
e : α ≃ Fin n
l : List α
hs : ∀ (x : α), x ∈ ⟦l⟧
⊢ signAux2 l (f * g) = signAux2 l f * signAux2 l g ∧ Pairwise fun (x y : α) ↦ signAux2 l (swap x y) = -1
have hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e
Tactic: have hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e :=
    Equiv.ext fun h => by simp [mul_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
f g : Perm α
n : ℕ
e : α ≃ Fin n
l : List α
hs : ∀ (x : α), x ∈ ⟦l⟧
hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e
⊢ signAux2 l (f * g) = signAux2 l f * signAux2 l g ∧ Pairwise fun (x y : α) ↦ signAux2 l (swap x y) = -1
have h : signAux2 l (f * g) = signAux2 l f * signAux2 l g
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
f g : Perm α
n : ℕ
e : α ≃ Fin n
l : List α
hs : ∀ (x : α), x ∈ ⟦l⟧
hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e
h : signAux2 l (f * g) = signAux2 l f * signAux2 l g
⊢ signAux2 l (f * g) = signAux2 l f * signAux2 l g ∧ Pairwise fun (x y : α) ↦ signAux2 l (swap x y) = -1
have h₁ : Pairwise fun (x y : α) ↦ signAux2 l (swap x y) = -1
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
f g : Perm α
n : ℕ
e : α ≃ Fin n
l : List α
hs : ∀ (x : α), x ∈ ⟦l⟧
hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e
⊢ signAux2 l (f * g) = signAux2 l f * signAux2 l g
have h : signAux ((e.symm.trans (f * g)).trans e) = signAux2 l f * signAux2 l g
Tactic: rw [← signAux_eq_signAux2 _ _ e fun _ _ => hs _, ←
      signAux_eq_signAux2 _ _ e fun _ _ => hs _, ← signAux_eq_signAux2 _ _ e fun _ _ => hs _,
      hfg, signAux_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
f g : Perm α
n : ℕ
e : α ≃ Fin n
l : List α
hs : ∀ (x : α), x ∈ ⟦l⟧
hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e
h : signAux ((e.symm.trans (f * g)).trans e) = signAux2 l f * signAux2 l g
⊢ signAux2 l (f * g) = signAux2 l f * signAux2 l g
have h₁ : signAux ((e.symm.trans (f * g)).trans e) = signAux ((e.symm.trans f).trans e) * signAux2 l g
Tactic: rw [← signAux_eq_signAux2 _ _ e fun _ _ => hs _, ←
      signAux_eq_signAux2 _ _ e fun _ _ => hs _, ← signAux_eq_signAux2 _ _ e fun _ _ => hs _,
      hfg, signAux_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
f g : Perm α
n : ℕ
e : α ≃ Fin n
l : List α
hs : ∀ (x : α), x ∈ ⟦l⟧
hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e
h : signAux ((e.symm.trans (f * g)).trans e) = signAux2 l f * signAux2 l g
h₁ : signAux ((e.symm.trans (f * g)).trans e) = signAux ((e.symm.trans f).trans e) * signAux2 l g
⊢ signAux2 l (f * g) = signAux2 l f * signAux2 l g
have h₂ : signAux ((e.symm.trans (f * g)).trans e) = signAux ((e.symm.trans f).trans e) * signAux ((e.symm.trans g).trans e)
Tactic: rw [← signAux_eq_signAux2 _ _ e fun _ _ => hs _, ←
      signAux_eq_signAux2 _ _ e fun _ _ => hs _, ← signAux_eq_signAux2 _ _ e fun _ _ => hs _,
      hfg, signAux_mul]