awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
i j : Fin (n + 1)
ne : i ≠ j
lt : i < j
zero :
  ∀ (ne : i ≠ 0) (lt : i < 0),
    swap i 0 ∈ (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
succ :
  ∀ (j : Fin n)
    (ih :
      ∀ (ne : i ≠ j.castSucc) (lt : i < j.castSucc),
        swap i j.castSucc ∈
          (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1)))))
    (ne : i ≠ j.succ) (lt : i < j.succ),
    swap i j.succ ∈
      (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
⊢ swap i j ∈ (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))

Tactic:
induction j using Fin.induction with
  | zero => cases lt
  | succ j ih =>
    have mem : swap j.castSucc j.succ ∈ Submonoid.closure
      (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ) := Submonoid.subset_closure ⟨_, rfl⟩
    obtain rfl | lts := (Fin.le_castSucc_iff.mpr lt).eq_or_lt
    · exact mem
    rw [swap_comm, ← swap_mul_swap_mul_swap (y := Fin.castSucc j) lts.ne lt.ne]
    exact mul_mem (mul_mem mem <| ih lts.ne lts) mem

Premises used: Iff.mpr, LE.le.eq_or_lt, Equiv.swap_comm, Fin.le_castSucc_iff, rfl
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
motive : Perm α → Prop
f : Perm α
one : motive 1
mul_swap : ∀ (f : Perm α) (x y : α), x ≠ y → motive f → motive (f * swap x y)
⊢ motive f

Tactic:
inv_inv f ▸ swap_induction_on f⁻¹ one fun f => mul_swap f⁻¹

Premises used: Eq.rec, Equiv.Perm.swap_induction_on, Inv.inv, inv_inv
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
w x y_1 z_1 : α
hwx : w ≠ x
hyz_1 : y_1 ≠ z_1
y z : α
hyz : y ≠ z
hwz : w ≠ z
rw : swap w y * swap x z * swap w x * ((swap x z)⁻¹ * (swap w y)⁻¹) = swap y z
rw₁ : swap w y * swap x z * swap w x * (swap x z * (swap w y)⁻¹) = swap y z
rw₂ : swap w y * swap x z * swap w x * (swap x z * swap w y) = swap y z
rw₃ : swap w y * (swap x z * swap w x) * (swap x z * swap w y) = swap y z
rw₄ : swap w y * (swap x z * swap w x * (swap x z * swap w y)) = swap y z
rw₅ : swap w y * (swap x z * swap w x * swap x z * swap w y) = swap y z
rw₆ : swap w y * (swap z w * swap w y) = swap y z
rw₇ : swap w y * swap z w * swap w y = swap y z
rw₈ rw₉ : swap y z = swap y z
⊢ swap w y * swap x z * swap w x * (swap w y * swap x z)⁻¹ = swap y z

Tactic:
rw [mul_inv_rev, swap_inv, swap_inv, mul_assoc (swap w y), mul_assoc (swap w y), ←
        mul_assoc _ (swap x z), swap_mul_swap_mul_swap hwx hwz, ← mul_assoc,
        swap_mul_swap_mul_swap hwz.symm hyz.symm]

Premises used: mul_assoc, Equiv.swap, Ne.symm, Equiv.swap_inv, Equiv.swap_mul_swap_mul_swap, mul_inv_rev
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
w x y z : α
hwx : w ≠ x
hyz : y ≠ z
h : ∀ {y z : α}, y ≠ z → w ≠ z → swap w y * swap x z * swap w x * (swap w y * swap x z)⁻¹ = swap y z
hwz : w = z
rw : z ≠ y
⊢ w ≠ y

Tactic:
rw [hwz]
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
w x y z : α
hwx : w ≠ x
hyz : y ≠ z
h : ∀ {y z : α}, y ≠ z → w ≠ z → swap w y * swap x z * swap w x * (swap w y * swap x z)⁻¹ = swap y z
hwz : w = z
⊢ z ≠ y

Tactic:
hyz.symm

Premises used: Ne.symm
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
w x y z : α
hwx : w ≠ x
hyz : y ≠ z
h : ∀ {y z : α}, y ≠ z → w ≠ z → swap w y * swap x z * swap w x * (swap w y * swap x z)⁻¹ = swap y z
hwz : w = z
⊢ z ≠ y

Tactic:
exact hyz.symm

Premises used: Ne.symm
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
w x y z : α
hwx : w ≠ x
hyz : y ≠ z
h : ∀ {y z : α}, y ≠ z → w ≠ z → swap w y * swap x z * swap w x * (swap w y * swap x z)⁻¹ = swap y z
hwz : w = z
hwy : w ≠ y
rw : swap w z * swap x y * swap w x * (swap w z * swap x y)⁻¹ = swap z y
rw₁ rw₂ : swap z y = swap z y
⊢ swap w z * swap x y * swap w x * (swap w z * swap x y)⁻¹ = swap y z

Tactic:
rw [swap_comm y z, h hyz.symm hwy]

Premises used: Equiv.swap_comm, Ne.symm
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
a : (_ : Fin n) × Fin n
⊢ a ∈ finPairsLT n ↔ a.snd (β := fun (x : Fin n) ↦ Fin n) < a.fst (β := fun (x : Fin n) ↦ Fin n)

Tactic:
simp only [finPairsLT, Fin.lt_def, true_and, mem_attachFin, mem_range, mem_univ,
    mem_sigma]

Premises used: Finset.mem_univ, Finset.mem_sigma, Finset.mem_range, Fin.lt_def, Equiv.Perm.finPairsLT, Finset.mem_attachFin, true_and
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
rhs : 1
| Eq (α := ℤˣ)
    (∏ x ∈ finPairsLT n,
      if
          LE.le (α := Fin n) ((1 : (a : Fin n) → Fin n) (x.fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
            ((1 : (a : Fin n) → Fin n) (x.snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
        -1
      else 1)
    1

Tactic:
rhs
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
rw : ∏ _x ∈ finPairsLT n, 1
| 1

Tactic:
rw [← @Finset.prod_const_one _ _ (finPairsLT n)]

Premises used: Finset.prod_const_one
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
rw : ∏ _x ∈ finPairsLT n, 1
| Eq (α := ℤˣ)
    (∏ x ∈ finPairsLT n,
      if
          LE.le (α := Fin n) ((1 : (a : Fin n) → Fin n) (x.fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
            ((1 : (a : Fin n) → Fin n) (x.snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
        -1
      else 1)
    1

Tactic:
rhs; rw [← @Finset.prod_const_one _ _ (finPairsLT n)]

Premises used: Finset.prod_const_one
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
conv :
  Eq (α := ℤˣ)
    (∏ x ∈ finPairsLT n,
      if
          LE.le (α := Fin n) ((1 : (a : Fin n) → Fin n) (x.fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
            ((1 : (a : Fin n) → Fin n) (x.snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
        -1
      else 1)
    (∏ _x ∈ finPairsLT n, 1)
⊢ Eq (α := ℤˣ)
    (∏ x ∈ finPairsLT n,
      if
          LE.le (α := Fin n) ((1 : (a : Fin n) → Fin n) (x.fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
            ((1 : (a : Fin n) → Fin n) (x.snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
        -1
      else 1)
    1

Tactic:
conv => rhs; rw [← @Finset.prod_const_one _ _ (finPairsLT n)]

Premises used: Finset.prod_const_one
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
⊢ Eq (α := ℤˣ)
    (∏ x ∈ finPairsLT n,
      if
          LE.le (α := Fin n) ((1 : (a : Fin n) → Fin n) (x.fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
            ((1 : (a : Fin n) → Fin n) (x.snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
        -1
      else 1)
    (∏ _x ∈ finPairsLT n, 1)

Tactic:
Finset.prod_congr rfl fun a ha => if_neg (mem_finPairsLT.1 ha).not_ge

Premises used: Finset.prod_congr, Iff.mp, Equiv.Perm.mem_finPairsLT, LT.lt.not_ge, if_neg, rfl
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
⊢ Eq (α := ℤˣ)
    (∏ x ∈ finPairsLT n,
      if
          LE.le (α := Fin n) ((1 : (a : Fin n) → Fin n) (x.fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
            ((1 : (a : Fin n) → Fin n) (x.snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
        -1
      else 1)
    (∏ _x ∈ finPairsLT n, 1)

Tactic:
exact Finset.prod_congr rfl fun a ha => if_neg (mem_finPairsLT.1 ha).not_ge

Premises used: Finset.prod_congr, Iff.mp, Equiv.Perm.mem_finPairsLT, LT.lt.not_ge, if_neg, rfl
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
f : Perm (Fin n)
a₁ a₂ : Fin n
ha : Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂ ∈ (↑(finPairsLT n) : Set ((_ : Fin n) × Fin n))
b₁ b₂ : Fin n
hb : Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂ ∈ (↑(finPairsLT n) : Set ((_ : Fin n) × Fin n))
h :
  Eq (α := (_ : Fin n) × Fin n)
    (if LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) a₂ : Fin n) ((f : (a : Fin n) → Fin n) a₁ : Fin n) then
        Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) a₁) ((f : (a : Fin n) → Fin n) a₂)
      else Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) a₂) ((f : (a : Fin n) → Fin n) a₁) :
      (_ : Fin n) × Fin n)
    (if LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) b₂ : Fin n) ((f : (a : Fin n) → Fin n) b₁ : Fin n) then
        Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) b₁) ((f : (a : Fin n) → Fin n) b₂)
      else Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) b₂) ((f : (a : Fin n) → Fin n) b₁) :
      (_ : Fin n) × Fin n)
rw :
  ∀
    (ha :
      Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂) <
        Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂))
    (b₁ b₂ : Fin n)
    (hb :
      Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂) <
        Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂))
    (h :
      Eq (α := (_ : Fin n) × Fin n)
        (if LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) a₂ : Fin n) ((f : (a : Fin n) → Fin n) a₁ : Fin n) then
            Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) a₁) ((f : (a : Fin n) → Fin n) a₂)
          else Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) a₂) ((f : (a : Fin n) → Fin n) a₁) :
          (_ : Fin n) × Fin n)
        (if LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) b₂ : Fin n) ((f : (a : Fin n) → Fin n) b₁ : Fin n) then
            Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) b₁) ((f : (a : Fin n) → Fin n) b₂)
          else Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) b₂) ((f : (a : Fin n) → Fin n) b₁) :
          (_ : Fin n) × Fin n)),
    Eq (α := (_ : Fin n) × Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)
      (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂)
⊢ Eq (α := (_ : Fin n) × Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)
    (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂)

Tactic:
rw [Finset.mem_coe, mem_finPairsLT] at *

Premises used: Equiv.Perm.mem_finPairsLT, Finset.mem_coe
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
f : Perm (Fin n)
a₁ a₂ : Fin n
ha :
  Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂) <
    Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)
b₁ b₂ : Fin n
hb :
  Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂) <
    Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂)
h :
  Eq (α := (_ : Fin n) × Fin n)
    (if LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) a₂ : Fin n) ((f : (a : Fin n) → Fin n) a₁ : Fin n) then
        Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) a₁) ((f : (a : Fin n) → Fin n) a₂)
      else Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) a₂) ((f : (a : Fin n) → Fin n) a₁) :
      (_ : Fin n) × Fin n)
    (if LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) b₂ : Fin n) ((f : (a : Fin n) → Fin n) b₁ : Fin n) then
        Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) b₁) ((f : (a : Fin n) → Fin n) b₂)
      else Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) b₂) ((f : (a : Fin n) → Fin n) b₁) :
      (_ : Fin n) × Fin n)
⊢ ¬b₁ < b₂

Tactic:
have : ¬b₁ < b₂ := hb.le.not_gt
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
f : Perm (Fin n)
a₁ a₂ : Fin n
ha :
  Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂) <
    Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)
b₁ b₂ : Fin n
hb :
  Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂) <
    Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂)
this : ¬b₁ < b₂
h_1 : LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) a₂ : Fin n) ((f : (a : Fin n) → Fin n) a₁ : Fin n)
h_2 : LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) b₂ : Fin n) ((f : (a : Fin n) → Fin n) b₁ : Fin n)
h :
  Eq (α := (_ : Fin n) × Fin n)
    (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) a₁) ((f : (a : Fin n) → Fin n) a₂) :
      (_ : Fin n) × Fin n)
    (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) b₁) ((f : (a : Fin n) → Fin n) b₂) :
      (_ : Fin n) × Fin n)
⊢ Eq (α := (_ : Fin n) × Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)
    (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂)

Tactic:
simp_all only [not_lt, Sigma.mk.inj_iff, (Equiv.injective f).eq_iff, heq_eq_eq]

Premises used: Function.Injective.eq_iff, heq_eq_eq, not_lt, Sigma.mk.inj_iff, Equiv.injective
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
f : Perm (Fin n)
a₁ a₂ : Fin n
ha :
  Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂) <
    Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)
b₁ b₂ : Fin n
hb :
  Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂) <
    Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂)
this : ¬b₁ < b₂
h_1 : LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) a₂ : Fin n) ((f : (a : Fin n) → Fin n) a₁ : Fin n)
h_2 : ¬LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) b₂ : Fin n) ((f : (a : Fin n) → Fin n) b₁ : Fin n)
h :
  Eq (α := (_ : Fin n) × Fin n)
    (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) a₁) ((f : (a : Fin n) → Fin n) a₂) :
      (_ : Fin n) × Fin n)
    (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) b₂) ((f : (a : Fin n) → Fin n) b₁) :
      (_ : Fin n) × Fin n)
neg :
  ∀ (ha : b₁ < b₂) (hb : b₂ < b₁) (this : b₂ ≤ b₁),
    LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) b₁ : Fin n) ((f : (a : Fin n) → Fin n) b₂ : Fin n) →
      LE.le (α := Fin n) ((f : (a : Fin n) → Fin n) b₁ : Fin n) ((f : (a : Fin n) → Fin n) b₂ : Fin n) →
        ∀ (h : a₁ = b₂ ∧ a₂ = b₁), b₂ = b₁ ∧ b₁ = b₂
⊢ Eq (α := (_ : Fin n) × Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)
    (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂)

Tactic:
simp_all only [not_lt, Sigma.mk.inj_iff, (Equiv.injective f).eq_iff, heq_eq_eq]

Premises used: Function.Injective.eq_iff, heq_eq_eq, not_lt, Sigma.mk.inj_iff, Equiv.injective
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
f : Perm (Fin n)
a₁ a₂ : Fin n
ha :
  Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂) <
    Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)
b₁ b₂ : Fin n
hb :
  Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂) <
    Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂)
this : ¬b₁ < b₂
h_1 : ¬LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) a₂ : Fin n) ((f : (a : Fin n) → Fin n) a₁ : Fin n)
h_2 : LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) b₂ : Fin n) ((f : (a : Fin n) → Fin n) b₁ : Fin n)
h :
  Eq (α := (_ : Fin n) × Fin n)
    (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) a₂) ((f : (a : Fin n) → Fin n) a₁) :
      (_ : Fin n) × Fin n)
    (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) b₁) ((f : (a : Fin n) → Fin n) b₂) :
      (_ : Fin n) × Fin n)
pos :
  ∀ (ha : b₁ < b₂) (hb : b₂ < b₁) (this : b₂ ≤ b₁),
    LE.le (α := Fin n) ((f : (a : Fin n) → Fin n) b₂ : Fin n) ((f : (a : Fin n) → Fin n) b₁ : Fin n) →
      LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) b₂ : Fin n) ((f : (a : Fin n) → Fin n) b₁ : Fin n) →
        ∀ (h : a₂ = b₁ ∧ a₁ = b₂), b₂ = b₁ ∧ b₁ = b₂
⊢ Eq (α := (_ : Fin n) × Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)
    (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂)

Tactic:
simp_all only [not_lt, Sigma.mk.inj_iff, (Equiv.injective f).eq_iff, heq_eq_eq]

Premises used: Function.Injective.eq_iff, heq_eq_eq, not_lt, Sigma.mk.inj_iff, Equiv.injective
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
f : Perm (Fin n)
a₁ a₂ : Fin n
ha :
  Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂) <
    Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)
b₁ b₂ : Fin n
hb :
  Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂) <
    Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂)
this : ¬b₁ < b₂
h_1 : ¬LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) a₂ : Fin n) ((f : (a : Fin n) → Fin n) a₁ : Fin n)
h_2 : ¬LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) b₂ : Fin n) ((f : (a : Fin n) → Fin n) b₁ : Fin n)
h :
  Eq (α := (_ : Fin n) × Fin n)
    (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) a₂) ((f : (a : Fin n) → Fin n) a₁) :
      (_ : Fin n) × Fin n)
    (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) b₂) ((f : (a : Fin n) → Fin n) b₁) :
      (_ : Fin n) × Fin n)
⊢ Eq (α := (_ : Fin n) × Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)
    (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂)

Tactic:
simp_all only [not_lt, Sigma.mk.inj_iff, (Equiv.injective f).eq_iff, heq_eq_eq]

Premises used: Function.Injective.eq_iff, heq_eq_eq, not_lt, Sigma.mk.inj_iff, Equiv.injective
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
f : Perm (Fin n)
a₁ a₂ b₁ b₂ : Fin n
ha : b₁ < b₂
hb : b₂ < b₁
this : b₂ ≤ b₁
h_1 : LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) b₁ : Fin n) ((f : (a : Fin n) → Fin n) b₂ : Fin n)
h_2 : LE.le (α := Fin n) ((f : (a : Fin n) → Fin n) b₁ : Fin n) ((f : (a : Fin n) → Fin n) b₂ : Fin n)
h : a₁ = b₂ ∧ a₂ = b₁
⊢ b₂ = b₁ ∧ b₁ = b₂

Tactic:
absurd this (not_le.mpr ha)

Premises used: not_le, Iff.mpr, absurd
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
f : Perm (Fin n)
a₁ a₂ b₁ b₂ : Fin n
ha : b₁ < b₂
hb : b₂ < b₁
this : b₂ ≤ b₁
h_1 : LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) b₁ : Fin n) ((f : (a : Fin n) → Fin n) b₂ : Fin n)
h_2 : LE.le (α := Fin n) ((f : (a : Fin n) → Fin n) b₁ : Fin n) ((f : (a : Fin n) → Fin n) b₂ : Fin n)
h : a₁ = b₂ ∧ a₂ = b₁
⊢ b₂ = b₁ ∧ b₁ = b₂

Tactic:
exact absurd this (not_le.mpr ha)

Premises used: not_le, Iff.mpr, absurd
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
f : Perm (Fin n)
a₁ a₂ b₁ b₂ : Fin n
ha : b₁ < b₂
hb : b₂ < b₁
this : b₂ ≤ b₁
h_1 : LE.le (α := Fin n) ((f : (a : Fin n) → Fin n) b₂ : Fin n) ((f : (a : Fin n) → Fin n) b₁ : Fin n)
h_2 : LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) b₂ : Fin n) ((f : (a : Fin n) → Fin n) b₁ : Fin n)
h : a₂ = b₁ ∧ a₁ = b₂
⊢ b₂ = b₁ ∧ b₁ = b₂

Tactic:
absurd this (not_le.mpr ha)

Premises used: not_le, Iff.mpr, absurd
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
f : Perm (Fin n)
a₁ a₂ b₁ b₂ : Fin n
ha : b₁ < b₂
hb : b₂ < b₁
this : b₂ ≤ b₁
h_1 : LE.le (α := Fin n) ((f : (a : Fin n) → Fin n) b₂ : Fin n) ((f : (a : Fin n) → Fin n) b₁ : Fin n)
h_2 : LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) b₂ : Fin n) ((f : (a : Fin n) → Fin n) b₁ : Fin n)
h : a₂ = b₁ ∧ a₁ = b₂
⊢ b₂ = b₁ ∧ b₁ = b₂

Tactic:
exact absurd this (not_le.mpr ha)

Premises used: not_le, Iff.mpr, absurd
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
f : Perm (Fin n)
x : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂ ∈ finPairsLT n
hxa :
  LT.lt (α := Fin n) ((Equiv.symm f : (a : Fin n) → Fin n) a₂ : Fin n) ((Equiv.symm f : (a : Fin n) → Fin n) a₁ : Fin n)
⊢ f.signBijAux
      (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((Equiv.symm f : (a : Fin n) → Fin n) a₁)
        ((Equiv.symm f : (a : Fin n) → Fin n) a₂)) =
    Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂

Tactic:
simp [signBijAux, if_pos (mem_finPairsLT.1 ha)]

Premises used: if_pos, Iff.mp, Equiv.Perm.mem_finPairsLT, Equiv.Perm.signBijAux
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
f : Perm (Fin n)
x : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂ ∈ finPairsLT n
hxa :
  ¬LT.lt (α := Fin n) ((Equiv.symm f : (a : Fin n) → Fin n) a₂ : Fin n)
      ((Equiv.symm f : (a : Fin n) → Fin n) a₁ : Fin n)
h : Eq (α := Fin n) ((Equiv.symm f : (a : Fin n) → Fin n) a₁ : Fin n) ((Equiv.symm f : (a : Fin n) → Fin n) a₂ : Fin n)
⊢ False

Tactic:
simp [mem_finPairsLT, f⁻¹.injective h] at ha

Premises used: Inv.inv, Equiv.Perm.mem_finPairsLT, Equiv.injective
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
f : Perm (Fin n)
x : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂ ∈ finPairsLT n
hxa :
  ¬LT.lt (α := Fin n) ((Equiv.symm f : (a : Fin n) → Fin n) a₂ : Fin n)
      ((Equiv.symm f : (a : Fin n) → Fin n) a₁ : Fin n)
⊢ f.signBijAux
      (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((Equiv.symm f : (a : Fin n) → Fin n) a₂)
        ((Equiv.symm f : (a : Fin n) → Fin n) a₁)) =
    Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂

Tactic:
simp [signBijAux, if_neg (mem_finPairsLT.1 ha).le.not_gt]

Premises used: LT.lt.le, LE.le.not_gt, Iff.mp, Equiv.Perm.mem_finPairsLT, Equiv.Perm.signBijAux, if_neg
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
f : Perm (Fin n)
x : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂ ∈ finPairsLT n
pos :
  ∀
    (h :
      LT.lt (α := Fin n)
        ((f : (a : Fin n) → Fin n)
            (Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)) :
          Fin n)
        ((f : (a : Fin n) → Fin n)
            (Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)) :
          Fin n)),
    Sigma.mk (β := fun (x : Fin n) ↦ Fin n)
        ((f : (a : Fin n) → Fin n)
          (Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)))
        ((f : (a : Fin n) → Fin n)
          (Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂))) ∈
      finPairsLT n
neg :
  ∀
    (h :
      ¬LT.lt (α := Fin n)
          ((f : (a : Fin n) → Fin n)
              (Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)) :
            Fin n)
          ((f : (a : Fin n) → Fin n)
              (Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)) :
            Fin n)),
    Membership.mem (α := (_ : Fin n) × Fin n) (finPairsLT n)
      (Sigma.mk (β := fun (x : Fin n) ↦ Fin n)
          ((f : (a : Fin n) → Fin n)
            (Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)))
          ((f : (a : Fin n) → Fin n)
            (Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂))) :
        (_ : Fin n) × Fin n)
⊢ (if x :
        LT.lt (α := Fin n)
          ((f : (a : Fin n) → Fin n)
              (Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)) :
            Fin n)
          ((f : (a : Fin n) → Fin n)
              (Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)) :
            Fin n) then
      Sigma.mk (β := fun (x : Fin n) ↦ Fin n)
        ((f : (a : Fin n) → Fin n)
          (Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)))
        ((f : (a : Fin n) → Fin n)
          (Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)))
    else
      Sigma.mk (β := fun (x : Fin n) ↦ Fin n)
        ((f : (a : Fin n) → Fin n)
          (Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)))
        ((f : (a : Fin n) → Fin n)
          (Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)))) ∈
    finPairsLT n

Tactic:
split_ifs with h