A strange case where proof search works only if there is a redundant `have` before

[ShreckYe]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• [X] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues
• [ ] Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries.
• [ ] Test your test case against the latest nightly release, for example on https://live.lean-lang.org/#project=lean-nightly (You can also use the settings there to switch to “Lean nightly”)

I have reduced this to a minimal test case as far as I can, but this is a strange case that's possibly related to the Mathlib definitions so I couldn't manage to remove the Mathlib dependency.

Description

See the code below and the comment inside:

import Mathlib

example (l : List ℝ) (l_sorted : l.Sorted (. ≤ .)) (l_nodup : l.Nodup) : True := by
  have l_sorted_lt : l.Sorted (. < .) := by
    have : True := trivial
    /-
    A strange issue here: the line below doesn't dependend on the `have` above,
    but without it, `hint`/`exact?` don't find the answer,
    and `apply?` reports "found a partial proof, but the corresponding tactic failed".
    -/
    exact List.Sorted.lt_of_le l_sorted l_nodup
  exact trivial

Context

no addtional context info

Steps to Reproduce

1. copy the code to a Lean project with the Mathlib dependency
2. replace exact List.Sorted.lt_of_le l_sorted l_nodup with hint/apply?/exact? and see that the exact proof is found
3. remove have : True := trivial above and see that hint/apply?/exact? can't find the proof correctly

Expected behavior: hint/apply?/exact? should find the proof correctly without the redundant have : True := trivial.

Actual behavior: They don't find the proof correctly.

Versions

Lean 4.22.0
Target: x86_64-unknown-linux-gnu

Additional Information

no addtional information

Impact

Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

[Rob23oba]

I suspect this has to do with meta-variables: A "no-op" dsimp also solves the problem:

import Mathlib

set_option says.verify true
example (l : List ℝ) (l_sorted : l.Sorted (. ≤ .)) (l_nodup : l.Nodup) : True := by
  have l_sorted_lt : l.Sorted (. < .) := by
    dsimp
    exact? says exact List.Sorted.lt_of_le l_sorted l_nodup
  exact trivial