refine BishopFin.count_eq_count_invimage_of_inv (Prod.map y.toFun y.toFun) (Prod.map y.inv.toFun y.inv.toFun) ?_ ?_
n : Nat
x y : Permutation n
⊢ (BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑x[↑t.fst] > ↑x[↑t.snd]) =
    BishopFin.count fun t => ↑y[↑t.fst] < ↑y[↑t.snd] ∧ ↑x[↑y[↑t.fst]] > ↑x[↑y[↑t.snd]]
case refine_1
n : Nat
x y : Permutation n
⊢ ∀ (b : Fin n × Fin n), Prod.map (toFun (inv y)) (toFun (inv y)) (Prod.map (toFun y) (toFun y) b) = b

case refine_2
n : Nat
x y : Permutation n
⊢ ∀ (a : Fin n × Fin n), Prod.map (toFun y) (toFun y) (Prod.map (toFun (inv y)) (toFun (inv y)) a) = a