There are several non-trivial reasoning required when r is false. First observe that your while loop might terminate without seeing all elements of either a or b (but not both), when r is false.

In final assert it is reasoning over all elements of a and b. For us humans it is possible to connect various logical steps required to prove final assert. But for Dafny it is not still.

Let's change such that Dafny see through all elements of a and b

 while i < a.Length || j < b.Length
    invariant 0 <= i <= a.Length && 0 <= j <= b.Length
  {
    if i == a.Length {
      j := j + 1;
    }
    else if j == b.Length {
       i := i + 1;   
    }
    else if a[i] < b[j] {
      i := i + 1;
    } else if a[i] > b[j] {
      j := j + 1;
    } else {  
      return true;
    }
  }

Now it is complaining that loop might not terminate. Let's add decreases clause.

 while i < a.Length || j < b.Length
    decreases a.Length + b.Length - i - j
    invariant 0 <= i <= a.Length && 0 <= j <= b.Length

Still no luck. May be it needs loop invariant so that it can reason beyond loop statement. Let's add invariant which we believe is true.

while i < a.Length || j < b.Length
    decreases a.Length + b.Length - i - j
    invariant 0 <= i <= a.Length && 0 <= j <= b.Length
    invariant !(exists m, n:: 0 <= m < i && 0 <= n < j && a[m] == b[n])

Now using loop invariant it verifies method post condition but it has hard time reasoning through loop invariant. Establishing that requires some further steps which is along the line of invariant proof in this blog post. Have fun !