awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
a₂ : Fin (n + 2)
ha₂ :
  Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 0 a₂ ∉ {Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 1 0}
ha₁ : a₂ < 0
⊢ Eq (α := ℤˣ)
    (if
        LE.le (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) 0 : Fin (n + 2))
          ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) a₂ : Fin (n + 2)) then
      -1
    else 1)
    1

Tactic:
absurd a₂.zero_le ha₁.not_ge

Premises used: Fin.zero_le, absurd, LT.lt.not_ge
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
a₂ : Fin (n + 2)
ha₂ :
  Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 0 a₂ ∉ {Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 1 0}
ha₁ : a₂ < 0
⊢ Eq (α := ℤˣ)
    (if
        LE.le (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) 0 : Fin (n + 2))
          ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) a₂ : Fin (n + 2)) then
      -1
    else 1)
    1

Tactic:
exact absurd a₂.zero_le ha₁.not_ge

Premises used: Fin.zero_le, absurd, LT.lt.not_ge
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ :
  Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) a₁ a₂ ∉ {Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 1 0}
ha₁ : a₂ < a₁
H : 0 < a₁
inr :
  ∀
    (ha₂ :
      Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) a₁ 0 ∉
        {Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 1 0})
    (ha₁ : 0 < a₁),
    Eq (α := ℤˣ)
      (if
          LE.le (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) a₁ : Fin (n + 2))
            ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) 0 : Fin (n + 2)) then
        -1
      else 1)
      1
inr₁ :
  ∀ (H' : 0 < a₂),
    Eq (α := ℤˣ)
      (if
          LE.le (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) a₁ : Fin (n + 2))
            ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) a₂ : Fin (n + 2)) then
        -1
      else 1)
      1
⊢ Eq (α := ℤˣ)
    (if
        LE.le (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) a₁ : Fin (n + 2))
          ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) a₂ : Fin (n + 2)) then
      -1
    else 1)
    1

Tactic:
rcases a₂.zero_le.eq_or_lt with (rfl | H')

Premises used: LE.le.eq_or_lt, Fin.zero_le, rfl
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₂ :
  Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) a₁ 0 ∉ {Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 1 0}
ha₁ : 0 < a₁
⊢ ¬a₁ = 1

Tactic:
simp only [and_true, heq_iff_eq, mem_singleton, Sigma.mk.inj_iff] at ha₂

Premises used: Finset.mem_singleton, and_true, heq_iff_eq, Sigma.mk.inj_iff
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₁ : 0 < a₁
ha₂ : ¬a₁ = 1
⊢ 1 < a₁

Tactic:
have : 1 < a₁ := lt_of_le_of_ne' (Nat.succ_le_of_lt ha₁) ha₂
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₁ : 0 < a₁
ha₂ : ¬a₁ = 1
this : 1 < a₁
⊢ Eq (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) 0) 1

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₁ : 0 < a₁
ha₂ : ¬a₁ = 1
this : 1 < a₁
⊢ Eq (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) 0) 1

Tactic:
have h01 : Equiv.swap (0 : Fin (n + 2)) 1 0 = 1 := by simp
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₁ : 0 < a₁
ha₂ : ¬a₁ = 1
this : 1 < a₁
h01 : Eq (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) 0) 1
inr : Eq (α := ℤˣ) (if a₁ ≤ (swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) 0 then -1 else 1) 1
inr₁ : Eq (α := ℤˣ) (if a₁ ≤ 1 then -1 else 1) 1
inr₂ inr₃ : Eq (α := ℤˣ) 1 1
⊢ Eq (α := ℤˣ)
    (if
        LE.le (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) a₁ : Fin (n + 2))
          ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) 0 : Fin (n + 2)) then
      -1
    else 1)
    1

Tactic:
rw [swap_apply_of_ne_of_ne (ne_of_gt H) ha₂, h01, if_neg this.not_ge]

Premises used: ne_of_gt, Equiv.swap_apply_of_ne_of_ne, LT.lt.not_ge, if_neg
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ :
  Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) a₁ a₂ ∉ {Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 1 0}
ha₁ : a₂ < a₁
H : 0 < a₁
H' : 0 < a₂
⊢ 1 ≤ a₂

Tactic:
have le : 1 ≤ a₂ := Nat.succ_le_of_lt H'
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ :
  Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) a₁ a₂ ∉ {Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 1 0}
ha₁ : a₂ < a₁
H : 0 < a₁
H' : 0 < a₂
le : 1 ≤ a₂
⊢ 1 < a₁

Tactic:
have lt : 1 < a₁ := le.trans_lt ha₁
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ :
  Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) a₁ a₂ ∉ {Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 1 0}
ha₁ : a₂ < a₁
H : 0 < a₁
H' : 0 < a₂
le : 1 ≤ a₂
lt : 1 < a₁
⊢ Eq (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) 1) 0

Tactic:
simp only [swap_apply_right]

Premises used: Equiv.swap_apply_right
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ :
  Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) a₁ a₂ ∉ {Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 1 0}
ha₁ : a₂ < a₁
H : 0 < a₁
H' : 0 < a₂
le : 1 ≤ a₂
lt : 1 < a₁
⊢ Eq (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) 1) 0

Tactic:
have h01 : Equiv.swap (0 : Fin (n + 2)) 1 1 = 0 := by simp only [swap_apply_right]
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ :
  Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) a₁ a₂ ∉ {Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 1 0}
ha₁ : a₂ < a₁
H : 0 < a₁
H' : 0 < a₂
le : 1 ≤ a₂
lt : 1 < a₁
h01 : Eq (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) 1) 0
inr :
  ∀
    (ha₂ :
      Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) a₁ 1 ∉
        {Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 1 0})
    (ha₁ : 1 < a₁) (H' : LT.lt (α := Fin (n + 2)) 0 1) (le : LE.le (α := Fin (n + 2)) 1 1),
    Eq (α := ℤˣ)
      (if
          LE.le (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) a₁ : Fin (n + 2))
            ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) 1 : Fin (n + 2)) then
        -1
      else 1)
      1
inr₁ :
  ∀ (lt' : 1 < a₂),
    Eq (α := ℤˣ)
      (if
          LE.le (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) a₁ : Fin (n + 2))
            ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) a₂ : Fin (n + 2)) then
        -1
      else 1)
      1
⊢ Eq (α := ℤˣ)
    (if
        LE.le (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) a₁ : Fin (n + 2))
          ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) a₂ : Fin (n + 2)) then
      -1
    else 1)
    1

Tactic:
rcases le.eq_or_lt with (rfl | lt')

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
lt : 1 < a₁
h01 : Eq (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) 1) 0
ha₂ :
  Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) a₁ 1 ∉ {Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 1 0}
ha₁ : 1 < a₁
H' : LT.lt (α := Fin (n + 2)) 0 1
le : LE.le (α := Fin (n + 2)) 1 1
inr : Eq (α := ℤˣ) (if a₁ ≤ (swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) 1 then -1 else 1) 1
inr₁ : Eq (α := ℤˣ) (if a₁ ≤ 0 then -1 else 1) 1
inr₂ inr₃ : Eq (α := ℤˣ) 1 1
⊢ Eq (α := ℤˣ)
    (if
        LE.le (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) a₁ : Fin (n + 2))
          ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) 1 : Fin (n + 2)) then
      -1
    else 1)
    1

Tactic:
rw [swap_apply_of_ne_of_ne H.ne' lt.ne', h01, if_neg H.not_ge]

Premises used: Equiv.swap_apply_of_ne_of_ne, LT.lt.ne', LT.lt.not_ge, if_neg
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ :
  Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) a₁ a₂ ∉ {Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 1 0}
ha₁ : a₂ < a₁
H : 0 < a₁
H' : 0 < a₂
le : 1 ≤ a₂
lt : 1 < a₁
h01 : Eq (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) 1) 0
lt' : 1 < a₂
inr : Eq (α := ℤˣ) (if a₁ ≤ (swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) a₂ then -1 else 1) 1
inr₁ : Eq (α := ℤˣ) (if a₁ ≤ a₂ then -1 else 1) 1
inr₂ inr₃ : Eq (α := ℤˣ) 1 1
⊢ Eq (α := ℤˣ)
    (if
        LE.le (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) a₁ : Fin (n + 2))
          ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) a₂ : Fin (n + 2)) then
      -1
    else 1)
    1

Tactic:
rw [swap_apply_of_ne_of_ne (ne_of_gt H) (ne_of_gt lt),
          swap_apply_of_ne_of_ne (ne_of_gt H') (ne_of_gt lt'), if_neg ha₁.not_ge]

Premises used: ne_of_gt, Equiv.swap_apply_of_ne_of_ne, LT.lt.not_ge, if_neg
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
n : ℕ
hn : 2 ≤ n
⊢ LT.lt (α := ℕ) 0 2

Tactic:
decide
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
n : ℕ
hn : 2 ≤ n
⊢ LT.lt (α := ℕ) 1 2

Tactic:
decide
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
hn : 2 ≤ n
zero : ∀ (hn : LE.le (α := ℕ) 2 0), (swap (⟨0, ⋯⟩ : Fin 0) (⟨1, ⋯⟩ : Fin 0)).signAux = -1
succ :
  ∀ (hn : 2 ≤ HAdd.hAdd (α := ℕ) 0 1),
    (swap (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1))).signAux = -1
succ₁ : ∀ (n : ℕ) (hn : 2 ≤ n + 1 + 1), (swap (⟨0, ⋯⟩ : Fin (n + 1 + 1)) (⟨1, ⋯⟩ : Fin (n + 1 + 1))).signAux = -1
⊢ (swap (⟨0, ⋯⟩ : Fin n) (⟨1, ⋯⟩ : Fin n)).signAux = -1

Tactic:
rcases n with (_ | _ | n)
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
hn : LE.le (α := ℕ) 2 0
⊢ (swap (⟨0, ⋯⟩ : Fin 0) (⟨1, ⋯⟩ : Fin 0)).signAux = -1

Tactic:
norm_num at hn
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
hn : 2 ≤ HAdd.hAdd (α := ℕ) 0 1
⊢ (swap (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1))).signAux = -1

Tactic:
norm_num at hn
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
hn : 2 ≤ n + 1 + 1
⊢ (swap (⟨0, ⋯⟩ : Fin (n + 1 + 1)) (⟨1, ⋯⟩ : Fin (n + 1 + 1))).signAux = -1

Tactic:
signAux_swap_zero_one' n

Premises used: Fin.ofNat, Nat.mod, _private.0.Equiv.Perm.signAux_swap_zero_one', ite
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
hn : 2 ≤ n + 1 + 1
⊢ (swap (⟨0, ⋯⟩ : Fin (n + 1 + 1)) (⟨1, ⋯⟩ : Fin (n + 1 + 1))).signAux = -1

Tactic:
exact signAux_swap_zero_one' n

Premises used: _private.0.Equiv.Perm.signAux_swap_zero_one'
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
x y : Fin 0
_hxy : x ≠ y
⊢ (swap x y).signAux = -1

Tactic:
Fin.elim0 x

Premises used: Fin.elim0
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
x y : Fin 0
_hxy : x ≠ y
⊢ (swap x y).signAux = -1

Tactic:
exact Fin.elim0 x

Premises used: Fin.elim0
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
x y : Fin 1
⊢ ∀ (_hxy : ¬x = y),
    Eq (α := ℤˣ)
      (∏ x_1 ∈ finPairsLT 1,
        if
            (if x_1.fst (β := fun (x : Fin 1) ↦ Fin 1) = x then y
              else if x_1.fst (β := fun (x : Fin 1) ↦ Fin 1) = y then x else x_1.fst (β := fun (x : Fin 1) ↦ Fin 1)) ≤
              if x_1.snd (β := fun (x : Fin 1) ↦ Fin 1) = x then y
              else if x_1.snd (β := fun (x : Fin 1) ↦ Fin 1) = y then x else x_1.snd (β := fun (x : Fin 1) ↦ Fin 1) then
          -1
        else 1)
      (-1)

Tactic:
simp only [eq_iff_true_of_subsingleton, not_true, ite_true, le_refl, prod_const,
               IsEmpty.forall_iff]

Premises used: le_refl, ite_true, Finset.prod_const, not_true, eq_iff_true_of_subsingleton, IsEmpty.forall_iff
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
x y : Fin (n + 2)
hxy : x ≠ y
⊢ 2 ≤ n + 2

Tactic:
le_add_self

Premises used: le_add_self
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
x y : Fin (n + 2)
hxy : x ≠ y
⊢ 2 ≤ n + 2

Tactic:
exact le_add_self

Premises used: le_add_self
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
x y : Fin (n + 2)
hxy : x ≠ y
⊢ 2 ≤ n + 2

Tactic:
have h2n : 2 ≤ n + 2 := by exact le_add_self
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
x y : Fin (n + 2)
hxy : x ≠ y
h2n : 2 ≤ n + 2
rw : IsConj (swap x y).signAux (swap (⟨0, ⋯⟩ : Fin (n + 2)) (⟨1, ⋯⟩ : Fin (n + 2))).signAux
⊢ (swap x y).signAux = -1

Tactic:
rw [← isConj_iff_eq, ← signAux_swap_zero_one h2n]

Premises used: _private.0.Equiv.Perm.signAux_swap_zero_one, isConj_iff_eq
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
x y : Fin (n + 2)
hxy : x ≠ y
h2n : 2 ≤ n + 2
⊢ (⟨0, ⋯⟩ : Fin (n + 2)) ≠ ⟨1, ⋯⟩

Tactic:
of_decide_eq_true rfl

Premises used: of_decide_eq_true, rfl
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
x y : Fin (n + 2)
hxy : x ≠ y
h2n : 2 ≤ n + 2
⊢ (⟨0, ⋯⟩ : Fin (n + 2)) ≠ ⟨1, ⋯⟩

Tactic:
exact of_decide_eq_true rfl

Premises used: of_decide_eq_true
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
x y : Fin (n + 2)
hxy : x ≠ y
h2n : 2 ≤ n + 2
⊢ IsConj (swap x y).signAux (swap (⟨0, ⋯⟩ : Fin (n + 2)) (⟨1, ⋯⟩ : Fin (n + 2))).signAux

Tactic:
exact (MonoidHom.mk' signAux signAux_mul).map_isConj
      (isConj_swap hxy (by exact of_decide_eq_true rfl))

Premises used: MonoidHom.mk', Equiv.Perm.signAux, Equiv.Perm.isConj_swap, MonoidHom.map_isConj, Equiv.Perm.signAux_mul
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
n : ℕ
f : Perm α
e : α ≃ Fin n
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → Membership.mem (γ := List α) [] x
⊢ f = 1

Tactic:
have : f = 1 := Equiv.ext fun y => Classical.not_not.1 (mt (h y) List.not_mem_nil)
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
n : ℕ
f : Perm α
e : α ≃ Fin n
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → Membership.mem (γ := List α) [] x
this : f = 1
rw : signAux (Equiv.trans (e.symm.trans 1) e) = signAux2.{u} (α := α) [] 1
rw₁ : signAux ((e.symm.trans (Equiv.refl α)).trans e) = signAux2 [] (Equiv.refl α)
rw₂ : signAux (e.symm.trans e) = signAux2 [] (Equiv.refl α)
rw₃ : signAux (n := n) (Equiv.refl (Fin n)) = signAux2 [] (Equiv.refl α)
rw₄ : signAux (n := n) 1 = signAux2 [] (Equiv.refl α)
rw₅ : 1 = signAux2 [] (Equiv.refl α)
rw₆ rw₇ : Eq (α := ℤˣ) 1 1
⊢ signAux ((e.symm.trans f).trans e) = signAux2 [] f

Tactic:
rw [this, one_def, Equiv.trans_refl, Equiv.symm_trans_self, ← one_def, signAux_one, signAux2]

Premises used: Equiv.Perm.signAux2, Equiv.Perm.one_def, Equiv.Perm.signAux_one, Equiv.trans_refl, Equiv.symm_trans_self
-- Module: Mathlib.GroupTheory.Perm.Sign
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
pos :
  ∀ (hfx : x = (f : (a : α) → α) x),
    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)
neg :
  ∀ (hfx : ¬x = (f : (a : α) → α) x),
    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)
⊢ 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)

Tactic:
by_cases hfx : x = f x

Premises used: DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Sign
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
pos : signAux ((e.symm.trans f).trans e) = signAux2 l f
⊢ 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)

Tactic:
rw [if_pos hfx]

Premises used: if_pos
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h_1 : ∀ (x_1 : α), (f : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : x = (f : (a : α) → α) x
y : α
hy : (f : (a : α) → α) y ≠ y
h : y = x
⊢ False

Tactic:
simp [h, hfx.symm] at hy

Premises used: Eq.symm
-- Module: Mathlib.GroupTheory.Perm.Sign
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
⊢ signAux ((e.symm.trans f).trans e) = signAux2 l f

Tactic:
exact
        signAux_eq_signAux2 l f _ fun y (hy : f y ≠ y) =>
          List.mem_of_ne_of_mem (fun h : y = x => by simp [h, hfx.symm] at hy) (h y hy)

Premises used: List.mem_of_ne_of_mem
-- Module: Mathlib.GroupTheory.Perm.Sign
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
⊢ ∀ (y : α), (swap x ((f : (a : α) → α) x) * f : (a : α) → α) y ≠ y → y ∈ l

Tactic:
have hy : ∀ y : α, (swap x (f x) * f) y ≠ y → y ∈ l := fun y hy =>
        have : f y ≠ y ∧ y ≠ x := ne_and_ne_of_swap_mul_apply_ne_self hy
        List.mem_of_ne_of_mem this.2 (h _ this.1)
-- Module: Mathlib.GroupTheory.Perm.Sign
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
H :
  ∀ (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) :
        ℕ)
⊢ (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:
ext
-- Module: Mathlib.GroupTheory.Perm.Sign
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
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) :
      ℕ)
⊢ (↑(((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) :
      ℕ)

Tactic:
rw [← Equiv.symm_trans_swap_trans, mul_def, Equiv.symm_trans_swap_trans, mul_def]

Premises used: Equiv.Perm.mul_def, Equiv.symm_trans_swap_trans
-- Module: Mathlib.GroupTheory.Perm.Sign
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
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) :
      ℕ)
⊢ (↑(((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 [trans_apply]

Premises used: Equiv.trans_apply
-- Module: Mathlib.GroupTheory.Perm.Sign
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
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) :
      ℕ)
⊢ (↑((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]

Premises used: Equiv.trans_apply
-- Module: Mathlib.GroupTheory.Perm.Sign
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
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) :
      ℕ)
⊢ (↑((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]

Premises used: Equiv.trans_apply
-- Module: Mathlib.GroupTheory.Perm.Sign
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
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)) :
      ℕ)
⊢ (↑((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]

Premises used: Equiv.trans_apply
-- Module: Mathlib.GroupTheory.Perm.Sign
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
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))) :
      ℕ)
⊢ (↑((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]

Premises used: Equiv.trans_apply