α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : { fst := a₁, snd := a₂ } ∈ finPairsLT n
⊢ (if x : ↑f { fst := a₁, snd := a₂ }.snd < ↑f { fst := a₁, snd := a₂ }.fst then
      { fst := ↑f { fst := a₁, snd := a₂ }.fst, snd := ↑f { fst := a₁, snd := a₂ }.snd }
    else { fst := ↑f { fst := a₁, snd := a₂ }.snd, snd := ↑f { fst := a₁, snd := a₂ }.fst }) ∈
    finPairsLT n
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : { fst := a₁, snd := a₂ } ∈ finPairsLT n
⊢ signBijAux f { fst := a₁, snd := a₂ } ∈ finPairsLT n
unfold signBijAux
case inl
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : { fst := a₁, snd := a₂ } ∈ finPairsLT n
h : ↑f { fst := a₁, snd := a₂ }.snd < ↑f { fst := a₁, snd := a₂ }.fst
⊢ { fst := ↑f { fst := a₁, snd := a₂ }.fst, snd := ↑f { fst := a₁, snd := a₂ }.snd } ∈ finPairsLT n

case inr
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : { fst := a₁, snd := a₂ } ∈ finPairsLT n
h : ¬↑f { fst := a₁, snd := a₂ }.snd < ↑f { fst := a₁, snd := a₂ }.fst
⊢ { fst := ↑f { fst := a₁, snd := a₂ }.snd, snd := ↑f { fst := a₁, snd := a₂ }.fst } ∈ finPairsLT n
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : { fst := a₁, snd := a₂ } ∈ finPairsLT n
⊢ (if x : ↑f { fst := a₁, snd := a₂ }.snd < ↑f { fst := a₁, snd := a₂ }.fst then
      { fst := ↑f { fst := a₁, snd := a₂ }.fst, snd := ↑f { fst := a₁, snd := a₂ }.snd }
    else { fst := ↑f { fst := a₁, snd := a₂ }.snd, snd := ↑f { fst := a₁, snd := a₂ }.fst }) ∈
    finPairsLT n
split_ifs with h
no goals
case inl
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : { fst := a₁, snd := a₂ } ∈ finPairsLT n
h : ↑f { fst := a₁, snd := a₂ }.snd < ↑f { fst := a₁, snd := a₂ }.fst
⊢ { fst := ↑f { fst := a₁, snd := a₂ }.fst, snd := ↑f { fst := a₁, snd := a₂ }.snd } ∈ finPairsLT n
exact mem_finPairsLT.2 h
no goals
case inr
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : { fst := a₁, snd := a₂ } ∈ finPairsLT n
h : ¬↑f { fst := a₁, snd := a₂ }.snd < ↑f { fst := a₁, snd := a₂ }.fst
⊢ { fst := ↑f { fst := a₁, snd := a₂ }.snd, snd := ↑f { fst := a₁, snd := a₂ }.fst } ∈ finPairsLT n
exact mem_finPairsLT.2
  ((le_of_not_gt h).lt_of_ne fun h => (mem_finPairsLT.1 ha).ne (f.injective h.symm))