apply BishopFin.count_congr
case refine_3
n : Nat
x y : Permutation n
this✝ : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
swap : Fin n × Fin n → Fin n × Fin n := fun t => (t.snd, t.fst)
this : ∀ (t : Fin n × Fin n), swap (swap t) = t
⊢ (BishopFin.count fun x_1 =>
      (↑y[↑x_1.snd] < ↑y[↑x_1.fst] ∧ ↑(x * y)[↑x_1.snd] > ↑(x * y)[↑x_1.fst]) ∧ ¬↑x_1.snd < ↑x_1.fst) =
    BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd]
case refine_3.h
n : Nat
x y : Permutation n
this✝ : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
swap : Fin n × Fin n → Fin n × Fin n := fun t => (t.snd, t.fst)
this : ∀ (t : Fin n × Fin n), swap (swap t) = t
⊢ ∀ (a : Fin n × Fin n),
    (↑y[↑a.snd] < ↑y[↑a.fst] ∧ ↑(x * y)[↑a.snd] > ↑(x * y)[↑a.fst]) ∧ ¬↑a.snd < ↑a.fst ↔
      ↑a.fst < ↑a.snd ∧ ↑y[↑a.fst] > ↑y[↑a.snd] ∧ ↑(x * y)[↑a.fst] < ↑(x * y)[↑a.snd]