Question: Unable to handle exact expressions that contain the product logarithm?

Let y＞1. It can be proved (maybe by hand) that the following four expressions are mathematically equivalent: 

assume(y > 1); # Assumption!
expr := [0, 0, 0, 0]: # Preallocation.
expr[1] := exp(y*LambertW(ln(y))):
expr[2] := (ln(y)/LambertW(ln(y)))^y:
expr[3] := eval(x^(x^x), x = exp(LambertW(ln(y)))):
expr[4] := eval(x^(x^x), x = ln(y)/LambertW(ln(y))):

But unfortunately, when I tried to simplify expr_i - expr_j (symbolically), I just got: 

seq(seq(ifelse(j <> i, [i, j, verify(expr[j], expr[i], equal)], NULL), j = 1 .. numelems(expr)), i = 1 .. numelems(expr)); # is(expr[j] = expr[i]) does not work as well.
 = 
   [1, 2, FAIL], [1, 3, FAIL], [1, 4, FAIL], [2, 1, FAIL], 

     [2, 3, FAIL], [2, 4, FAIL], [3, 1, FAIL], [3, 2, FAIL], 

     [3, 4, true], [4, 1, FAIL], [4, 2, FAIL], [4, 3, true]

In other words, Maple can only determine that expr[3] = expr[4].
One may check that, for example, 

MmaTranslator:-Mma:-Chop([seq](seq(evalhf(subs(y = log10(rand()), expr[i] - expr[j])), j = 1 .. numelems(expr)), i = 1 .. numelems(expr)), 2^(-26));
 = 
        [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]

However, the desired approach is simplifying them symbolically. Is there a way to do so in Maple?