wlog error

Stream: mathlib4

[David Renshaw]

see https://github.com/leanprover-community/mathlib4/issues/5348

import Mathlib.Tactic.WLOG
import Mathlib.Data.Nat.Basic

example (x y : ℕ) : True := by
  let z := 10 -- works as expected if this line is commented out
  wlog hxy' : x < y with H
  · trivial
  · trivial

gives the error:

application type mismatch
  (let z := 10;
    fun hxy' ↦ True.intro)
    z
argument has type
  ℕ
but function has type
  x < y → True

[David Renshaw]

I'm going to try to debug this.

[David Renshaw]

If anyone has ideas about what might be going wrong, please let me know.

[Jireh Loreaux]

wlog is absorbing the let z := 10 into the context that it's generalizing.

[David Renshaw]

Hm... maybe we should filter out ldecls here: https://github.com/leanprover-community/mathlib4/blob/ee000bf3b049cd25914bfa67960159c9c51d2827/Mathlib/Tactic/WLOG.lean#L79

[Jireh Loreaux]

Seems reasonable. @Johan Commelin :up:

[Johan Commelin]

I don't think I'm equipped to debug/fix this issue

[Thomas Murrills]

revertedFVars is used for the later introNP, the tryClearMany, and the mkAppN; I do agree we ought to filter out the ldecls, but just for the mkAppN application, as they're still relevant for the introNP and tryClearMany usages. I'll try this and make a PR! :)

[Thomas Murrills]

!4#5362, once it passes CI