α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝¹ x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : { fst := a₁, snd := a₂ } ∈ finPairsLT n
b₁ b₂ : Fin n
hb : { fst := b₁, snd := b₂ } ∈ finPairsLT n
h :
  (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 }) =
    if x : ↑f { fst := b₁, snd := b₂ }.snd < ↑f { fst := b₁, snd := b₂ }.fst then
      { fst := ↑f { fst := b₁, snd := b₂ }.fst, snd := ↑f { fst := b₁, snd := b₂ }.snd }
    else { fst := ↑f { fst := b₁, snd := b₂ }.snd, snd := ↑f { fst := b₁, snd := b₂ }.fst }
⊢ { fst := a₁, snd := a₂ } = { fst := b₁, snd := b₂ }
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝¹ x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : { fst := a₁, snd := a₂ } ∈ finPairsLT n
b₁ b₂ : Fin n
hb : { fst := b₁, snd := b₂ } ∈ finPairsLT n
h : signBijAux f { fst := a₁, snd := a₂ } = signBijAux f { fst := b₁, snd := b₂ }
⊢ { fst := a₁, snd := a₂ } = { fst := b₁, snd := b₂ }
unfold signBijAux at h
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝¹ x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : { fst := a₁, snd := a₂ }.snd < { fst := a₁, snd := a₂ }.fst
b₁ b₂ : Fin n
hb : { fst := b₁, snd := b₂ }.snd < { fst := b₁, snd := b₂ }.fst
h :
  (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 }) =
    if x : ↑f { fst := b₁, snd := b₂ }.snd < ↑f { fst := b₁, snd := b₂ }.fst then
      { fst := ↑f { fst := b₁, snd := b₂ }.fst, snd := ↑f { fst := b₁, snd := b₂ }.snd }
    else { fst := ↑f { fst := b₁, snd := b₂ }.snd, snd := ↑f { fst := b₁, snd := b₂ }.fst }
⊢ { fst := a₁, snd := a₂ } = { fst := b₁, snd := b₂ }
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝¹ x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : { fst := a₁, snd := a₂ } ∈ finPairsLT n
b₁ b₂ : Fin n
hb : { fst := b₁, snd := b₂ } ∈ finPairsLT n
h :
  (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 }) =
    if x : ↑f { fst := b₁, snd := b₂ }.snd < ↑f { fst := b₁, snd := b₂ }.fst then
      { fst := ↑f { fst := b₁, snd := b₂ }.fst, snd := ↑f { fst := b₁, snd := b₂ }.snd }
    else { fst := ↑f { fst := b₁, snd := b₂ }.snd, snd := ↑f { fst := b₁, snd := b₂ }.fst }
⊢ { fst := a₁, snd := a₂ } = { fst := b₁, snd := b₂ }
rw [mem_finPairsLT] at *
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝¹ x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : { fst := a₁, snd := a₂ }.snd < { fst := a₁, snd := a₂ }.fst
b₁ b₂ : Fin n
hb : { fst := b₁, snd := b₂ }.snd < { fst := b₁, snd := b₂ }.fst
h :
  (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 }) =
    if x : ↑f { fst := b₁, snd := b₂ }.snd < ↑f { fst := b₁, snd := b₂ }.fst then
      { fst := ↑f { fst := b₁, snd := b₂ }.fst, snd := ↑f { fst := b₁, snd := b₂ }.snd }
    else { fst := ↑f { fst := b₁, snd := b₂ }.snd, snd := ↑f { fst := b₁, snd := b₂ }.fst }
this : ¬b₁ < b₂
⊢ { fst := a₁, snd := a₂ } = { fst := b₁, snd := b₂ }
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝¹ x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : { fst := a₁, snd := a₂ }.snd < { fst := a₁, snd := a₂ }.fst
b₁ b₂ : Fin n
hb : { fst := b₁, snd := b₂ }.snd < { fst := b₁, snd := b₂ }.fst
h :
  (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 }) =
    if x : ↑f { fst := b₁, snd := b₂ }.snd < ↑f { fst := b₁, snd := b₂ }.fst then
      { fst := ↑f { fst := b₁, snd := b₂ }.fst, snd := ↑f { fst := b₁, snd := b₂ }.snd }
    else { fst := ↑f { fst := b₁, snd := b₂ }.snd, snd := ↑f { fst := b₁, snd := b₂ }.fst }
⊢ { fst := a₁, snd := a₂ } = { fst := b₁, snd := b₂ }
have : ¬b₁ < b₂ := hb.le.not_lt
case inl.inr
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝¹ x✝ : (_ : Fin n) × Fin n
a₁ a₂ b₁ b₂ : Fin n
ha : b₁ < b₂
hb : b₂ < b₁
this : b₂ ≤ b₁
h✝¹ : ↑f b₁ < ↑f b₂
h✝ : ↑f b₁ ≤ ↑f b₂
h : a₁ = b₂ ∧ a₂ = b₁
⊢ b₂ = b₁ ∧ b₁ = b₂

case inr.inl
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝¹ x✝ : (_ : Fin n) × Fin n
a₁ a₂ b₁ b₂ : Fin n
ha : b₁ < b₂
hb : b₂ < b₁
this : b₂ ≤ b₁
h✝¹ : ↑f b₂ ≤ ↑f b₁
h✝ : ↑f b₂ < ↑f b₁
h : a₂ = b₁ ∧ a₁ = b₂
⊢ b₂ = b₁ ∧ b₁ = b₂
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝¹ x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : { fst := a₁, snd := a₂ }.snd < { fst := a₁, snd := a₂ }.fst
b₁ b₂ : Fin n
hb : { fst := b₁, snd := b₂ }.snd < { fst := b₁, snd := b₂ }.fst
h :
  (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 }) =
    if x : ↑f { fst := b₁, snd := b₂ }.snd < ↑f { fst := b₁, snd := b₂ }.fst then
      { fst := ↑f { fst := b₁, snd := b₂ }.fst, snd := ↑f { fst := b₁, snd := b₂ }.snd }
    else { fst := ↑f { fst := b₁, snd := b₂ }.snd, snd := ↑f { fst := b₁, snd := b₂ }.fst }
this : ¬b₁ < b₂
⊢ { fst := a₁, snd := a₂ } = { fst := b₁, snd := b₂ }
split_ifs at h <;>
simp_all [(Equiv.injective f).eq_iff, eq_self_iff_true, and_self_iff, heq_iff_eq]
case inr.inl
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝¹ x✝ : (_ : Fin n) × Fin n
a₁ a₂ b₁ b₂ : Fin n
ha : b₁ < b₂
hb : b₂ < b₁
this : b₂ ≤ b₁
h✝¹ : ↑f b₂ ≤ ↑f b₁
h✝ : ↑f b₂ < ↑f b₁
h : a₂ = b₁ ∧ a₁ = b₂
⊢ b₂ = b₁ ∧ b₁ = b₂
case inl.inr
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝¹ x✝ : (_ : Fin n) × Fin n
a₁ a₂ b₁ b₂ : Fin n
ha : b₁ < b₂
hb : b₂ < b₁
this : b₂ ≤ b₁
h✝¹ : ↑f b₁ < ↑f b₂
h✝ : ↑f b₁ ≤ ↑f b₂
h : a₁ = b₂ ∧ a₂ = b₁
⊢ b₂ = b₁ ∧ b₁ = b₂

case inr.inl
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝¹ x✝ : (_ : Fin n) × Fin n
a₁ a₂ b₁ b₂ : Fin n
ha : b₁ < b₂
hb : b₂ < b₁
this : b₂ ≤ b₁
h✝¹ : ↑f b₂ ≤ ↑f b₁
h✝ : ↑f b₂ < ↑f b₁
h : a₂ = b₁ ∧ a₁ = b₂
⊢ b₂ = b₁ ∧ b₁ = b₂
. exact absurd this (not_le.mpr ha)
no goals
case inr.inl
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝¹ x✝ : (_ : Fin n) × Fin n
a₁ a₂ b₁ b₂ : Fin n
ha : b₁ < b₂
hb : b₂ < b₁
this : b₂ ≤ b₁
h✝¹ : ↑f b₂ ≤ ↑f b₁
h✝ : ↑f b₂ < ↑f b₁
h : a₂ = b₁ ∧ a₁ = b₂
⊢ b₂ = b₁ ∧ b₁ = b₂
. exact absurd this (not_le.mpr ha)
no goals
case inl.inr
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝¹ x✝ : (_ : Fin n) × Fin n
a₁ a₂ b₁ b₂ : Fin n
ha : b₁ < b₂
hb : b₂ < b₁
this : b₂ ≤ b₁
h✝¹ : ↑f b₁ < ↑f b₂
h✝ : ↑f b₁ ≤ ↑f b₂
h : a₁ = b₂ ∧ a₂ = b₁
⊢ b₂ = b₁ ∧ b₁ = b₂
exact absurd this (not_le.mpr ha)
no goals
case inr.inl
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝¹ x✝ : (_ : Fin n) × Fin n
a₁ a₂ b₁ b₂ : Fin n
ha : b₁ < b₂
hb : b₂ < b₁
this : b₂ ≤ b₁
h✝¹ : ↑f b₂ ≤ ↑f b₁
h✝ : ↑f b₂ < ↑f b₁
h : a₂ = b₁ ∧ a₁ = b₂
⊢ b₂ = b₁ ∧ b₁ = b₂
exact absurd this (not_le.mpr ha)