. simp only [Prod.map, toFun_toFun_inv, implies_true]
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
no goals