α : 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
hxa : ↑f⁻¹ a₂ < ↑f⁻¹ a₁
⊢ { fst := a₁, snd := a₂ } =
    if ↑f (↑f⁻¹ a₂) < ↑f (↑f⁻¹ a₁) then { fst := ↑f (↑f⁻¹ a₁), snd := ↑f (↑f⁻¹ a₂) }
    else { fst := ↑f (↑f⁻¹ a₂), snd := ↑f (↑f⁻¹ a₁) }
α : 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
hxa : ↑f⁻¹ a₂ < ↑f⁻¹ a₁
⊢ { fst := a₁, snd := a₂ } = signBijAux f { fst := ↑f⁻¹ a₁, snd := ↑f⁻¹ a₂ }
dsimp [signBijAux]
no goals
α : 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
hxa : ↑f⁻¹ a₂ < ↑f⁻¹ a₁
⊢ { fst := a₁, snd := a₂ } =
    if ↑f (↑f⁻¹ a₂) < ↑f (↑f⁻¹ a₁) then { fst := ↑f (↑f⁻¹ a₁), snd := ↑f (↑f⁻¹ a₂) }
    else { fst := ↑f (↑f⁻¹ a₂), snd := ↑f (↑f⁻¹ a₁) }
rw [apply_inv_self, apply_inv_self, if_pos (mem_finPairsLT.1 ha)]
no goals
α : 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
hxa : ¬↑f⁻¹ a₂ < ↑f⁻¹ a₁
h : ↑f⁻¹ a₁ = ↑f⁻¹ a₂
⊢ False
simp [mem_finPairsLT, f⁻¹.injective h, lt_irrefl] at ha
α : 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
hxa : ¬↑f⁻¹ a₂ < ↑f⁻¹ a₁
⊢ { fst := a₁, snd := a₂ } =
    if ↑f (↑f⁻¹ a₁) < ↑f (↑f⁻¹ a₂) then { fst := ↑f (↑f⁻¹ a₂), snd := ↑f (↑f⁻¹ a₁) }
    else { fst := ↑f (↑f⁻¹ a₁), snd := ↑f (↑f⁻¹ a₂) }
α : 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
hxa : ¬↑f⁻¹ a₂ < ↑f⁻¹ a₁
⊢ { fst := a₁, snd := a₂ } = signBijAux f { fst := ↑f⁻¹ a₂, snd := ↑f⁻¹ a₁ }
dsimp [signBijAux]
no goals
α : 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
hxa : ¬↑f⁻¹ a₂ < ↑f⁻¹ a₁
⊢ { fst := a₁, snd := a₂ } =
    if ↑f (↑f⁻¹ a₁) < ↑f (↑f⁻¹ a₂) then { fst := ↑f (↑f⁻¹ a₂), snd := ↑f (↑f⁻¹ a₁) }
    else { fst := ↑f (↑f⁻¹ a₁), snd := ↑f (↑f⁻¹ a₂) }
rw [apply_inv_self, apply_inv_self, if_neg (mem_finPairsLT.1 ha).le.not_lt]