Law for type [[a]] -> ([a], [a])

If R1 and R2 are relations (say, R_i between A_i and B_i, with i in {1,2}), then lift{(,)}(R1,R2) is the "lifted" relations pairs, between A1 * A2 and B1 * B2, with * denoting the product (written (,) in Haskell).

In the lifed relation, two pairs (x1,x2) :: A1*A2 and (y1,y2) :: B1*B2 are related if and only if x1 R1 y1 and x2 R2 y2. In your case, R1 and R2 are functions map g, map g, so the lifting becomes a function as well: y1 = map g x1 && y2 = map g x2.

Hence, the generated

(f x, f (map (map g) x)) in lift{(,)}(map g,map g)

means:

fst (f (map (map g) x)) = map g (fst (f x))
AND
snd (f (map (map g) x)) = map g (snd (f x))

or, in other words:

f (map (map g) x) = (map g (fst (f x)), map g (snd (f x)))

which I wold write as, using Control.Arrow:

f (map (map g) x) = (map g *** map g) (f x)

or even, in pointfree style:

f . map (map g) = (map g *** map g) . f

This is no surprise, since your f can be written as

f :: F a -> G a
where F a = [[a]]
      G a = ([a], [a])

and F,G are functors (in Haskell we would need to use a newtype to define a functor instance, but I will omit that, since it's irrelevant). In such common case, the free theorem has a very nice form: for every g,

f . fmap_of_F g = fmap_of_G g . f

This is a very nice form, called naturality (f can be interpreted as a natural transformation in a suitable category). Note that the two fs above are actually instantiated on separate types, so to make types agree with the rest.

In your specific case, since F a = [[a]], it is the composition of the [] functor with itself, hence we (unsurprisingly) get fmap_of_F g = fmap_of_[] (fmap_of_[] g) = map (map g).

Instead, G a = ([a],[a]) is the composition of functors [] and H a = (a,a) (technically, diagonal functor composed with the product functor). We have fmap_of_H h = (h *** h) = (\x -> (h x, h x)), from which fmap_of_G g = fmap_of_H (fmap_of_[] g) = (map g *** map g).

Same thing as @chi's answer with less ceremony:

It doesn't matter if you change the as to bs before or after the function, you get the same thing (as long as you use an fmap-like-thing to do it).

For any f : a -> b,

    [[a]] ------------->   [[b]]
      |    (map.map) f       |
      |                      |
     foo                    foo
      |                      |
      v                      v
    ([a],[a]) ---------> ([b],[b])
              bimap f f

commutes.