wlog tactic gives error application type mismatch

[dwrensha]

When I try this:

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

I get this error:

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

I suspect that the tactic logic is missing a withContext call or similar.

[dwrensha]

cc @thorimur