exact? can suggest autogenerated proof_1 constants

[dwrensha]

This is a regression from mathlib's exact? which got removed on the v4.7.0 version bump.

In certain situations, Lean autogenerates constants with names like proof_1 or proof_2. These are not intended to be visible to the end user, but exact? can sometimes suggest them, shadowing more-canonical lemmas.

import Mathlib.Data.PNat.Basic

example (f : Nat → Nat) (a : Nat) (hae : f a = 0)
    (h : 0 < Nat.zero) : False := by
  exact?
-- Try this: exact PNat.caseStrongInductionOn.proof_1 h

If I comment out the mathlib import, then exact? gives me something more reasonable:

Try this: exact Nat.not_succ_le_zero 0 h

[dwrensha]

This is related to an old pull request: #2112. (I'm not sure whether that fix actually works for the current implementation of exact?.)

[dwrensha]

Here's an example that does not depend on any imports:

example (Person Topic : Type)
    (discusses : Person → Person → Topic)
    (discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1)
    (p1 : Person) :
    let Person' : Type := { p2 // p2 ≠ p1 }
    ∀ t1 : Topic,
    ∀ α : Person' → Prop,
    let Topic' : Type := { t2 // t2 ≠ t1 }
    ∀ p3 p4 : { x // α x },
    ∀ h10 : discusses ↑↑p3 ↑↑p4 ≠ t1,
    ∀ h11 : discusses ↑↑p4 ↑↑p3 ≠ t1,
    let s1 : Topic' := { val := discusses ↑↑p3 ↑↑p4, property := h10 }
    let s2 : Topic' := { val := discusses ↑↑p4 ↑↑p3, property := h11 }
    s1 = s2 := by
 intro Person' t1 α Topic' p3 p4 h10 h11 s1 s2
 exact?
-- Try this: exact Subtype.instDecidableEqSubtype.proof_1 (discusses p3.val.val p4.val.val) h10
--  (discusses p4.val.val p3.val.val) h11 (discussion_sym p3.val.val p4.val.val)

I don't expect exact? to ever return a proof_1 term like that.

(This example was extracted from this line of code in-the-wild.)

[joehendrix]

This was closed by #3769.