∀ {r t : ℕ} {a b : Fin r × Fin t},
  (SimpleGraph.completeMultipartiteGraph (Function.const (Fin r) (Fin t))).Adj
      ((Equiv.sigmaEquivProd (Fin r) (Fin t)).symm a) ((Equiv.sigmaEquivProd (Fin r) (Fin t)).symm b) ↔
    (SimpleGraph.completeEquipartiteGraph r t).Adj a b