WLOG bug?

Stream: lean4

[Nir Paz]

In the second example, wlog fails with the error message "tactic 'introN' failed, insufficient number of binders". This doesn't happen on a version of mathlib from a few months ago.

import Mathlib

example : True := by
  wlog obv : True -- works
  · sorry
  sorry

example : True := by
  let x : ℕ := 0
  wlog obv : True -- tactic 'introN' failed, insufficient number of binders
  · sorry
  sorry

[Yury G. Kudryashov]

Can you git bisect the bad commit, please?

[Yury G. Kudryashov]

Running it myself.

[Yury G. Kudryashov]

The offending commit is #19675

[Nir Paz]

Sorry it takes me a few minutes per commit just to get the cache

[Yury G. Kudryashov]

That's why I minimized imports first and didn't get the cache.

[Yury G. Kudryashov]

This PR adds (usedLetOnly := true) to mkAuxMVarType call. If I change it to (usedLetOnly := false), then this test works. @Kim Morrison Is it the correct fix or should we do something else?

[Kim Morrison]

Sorry, missed this until now. Yes, this seems fine to change.