Range guard on natural

[ldct]

I have two theorems about naturals that are both true. In true_example_without_guard, plausible admits the theorem, which is expected. However, in true_example_with_guard, it says that it gave up, which I did not expect, and the error message doesn't make sense to me. If I turn on set_option trace.plausible.discarded true I see that in the second example it actually tested many values of a so I expected it to admit the theorem.

import Mathlib

theorem true_example_without_guard (a : ℕ) : a ≤ 2^a := by
  plausible -- Unable to find a counter-example

theorem true_example_with_guard (a : ℕ) (ha : 4 ≤ a) : a^2 ≤ 2^a := by
  plausible -- Gave up after failing to generate values that fulfill the preconditions 4 times