∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] {L : Sublattice α} {M : Sublattice β}
  {N : Sublattice (α × β)}, N ≤ L.prod M ↔ N ≤ Sublattice.comap LatticeHom.fst L ∧ N ≤ Sublattice.comap LatticeHom.snd M