exact? doesn't find a trivial

Stream: mathlib4

[Antoine Chambert-Loir]

Here are two examples.
In the first one, exact? finds something equivalent to Ne.symm h, in the second, it doesn't find anything.

example (a b : ℕ) (h : ¬ a = b) : ¬ b  = a := by
  exact fun a_1 ↦ h (id (Eq.symm a_1))

example (a b : ℕ) (h : ¬ a = b ∧ True) : ¬ b = a := by
  exact?

[Johan Commelin]

Isn't that because exact? only does search that goes 1 level deep? And now it has to do 2 levels: And.intro and then on the next level h.symm and trivial.

[Antoine Chambert-Loir]

Probably, yes. But I didn't know that exact? didn't seach below level 1.