Lean `exact?` on Mathlib v4.35: what it misses and why to rewrite its suggestion
Tested on Mathlib v4.35.0. (1) It does not unfold plain defs: with def sq' (x : ℝ) := x * x, exact? fails on 0 ≤ sq' x ('could not close the goal'). After unfold sq' it finds mul_self_nonneg x. (2) exact? using h accepts only local hypotheses: using mul_self_nonneg errors with 'expected single reference to variable'. (3) Its pick is the first lemma that closes the goal, which is often not the idiomatic one. It suggested Left.mul_nonneg ha hb where mul_nonneg ha hb works. For 0 < a, 0 ≤ b ⊢ 0 ≤ a * b it gave (mul_nonneg_iff_of_pos_left ha).mpr hb instead of mul_nonneg ha.le hb. For h : a < b ⊢ a + 1 ≤ b on ℕ it gave Order.add_one_le_iff.mpr h, while plain h typechecks by defeq. So treat its output as a pointer, then replace it with the canonical lemma for stable proofs. (4) It does see through reducible defeq such as c + b + 0, where it found Nat.add_le_add_iff_left.mpr h. A file of 6 exact? calls took ~15 s wall, so remove them before committing.
Correction to (4), tested afterwards: 'reducible defeq' is wrong.
with_reducible exact Nat.add_le_add_iff_left.mpr hFAILS onc + a ≤ c + b + 0with a type mismatch. The suggestion is accepted becauseexactchecks at default transparency, wherec + b + 0unfolds toc + b. So exact? matches up to default defeq when it checks a candidate. (Also checked:mul_nonneg ha.le hbcompiles for the 0 < a case, as the note claims.)