. apply BishopFin.count_congr; intro t
  rewrite [← and_assoc]
  apply and_congr_right
  intro ht
  rewrite [Nat.not_lt_eq, Nat.le_iff_lt_or_eq]
  apply or_iff_left
  intro hxyt
  have : t.1.1 = t.2.1 := (x*y).get_inj _ _ <| Fin.eq_of_val_eq hxyt
  exact Nat.lt_irrefl _ (this ▸ ht.1)
case refine_4
n : Nat
x y : Permutation n
this : ∀ (a b c d : Nat), a + b + (c + d) = a + c + (b + d)
⊢ (BishopFin.count fun a => (↑a.fst < ↑a.snd ∧ ↑y[↑a.fst] > ↑y[↑a.snd]) ∧ ¬↑(x * y)[↑a.fst] > ↑(x * y)[↑a.snd]) =
    BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd]
no goals