Question on exact?

Stream: new members

[Lauri Oksanen]

Why the first example below works and the second doesn't? To my untrained eye they don't look very different.

import Mathlib

example {a b : ℝ} (h1 : a ≤ b) (h2 : b ≤ a) : a = b := by
  exact? -- doesn't work, but the following does:
  --exact le_antisymm h1 h2

example {a b : ℝ} (h1 : 0 ≤ a) (h2 : 0 ≤ b) : 0 ≤ a * b := by
  exact? -- works, and suggests the following:
  --exact Left.mul_nonneg h1 h2

[Kevin Buzzard]

exact? isn't very good at goals of the form X = Y and the reason for this is something to do with discrimination tree keys.

[Lauri Oksanen]

Thank a lot! I did some digging and I understand this now. Equality relations are explicitly excluded in the library search, and they seem to be the only special case, see https://github.com/leanprover/lean4/blob/2ba021ecc21636989aa82aa82c99f9443f3e774a/src/Lean/Meta/Tactic/LibrarySearch.lean#L100