wlog with Unused Declarations

[dMaggot]

The following code

import Mathlib.Tactic.WLOG

theorem bugs: ∀ (a : Nat) (f : Nat → Nat), f a = 0 := by
  intros a f
  let f' : Nat → Nat := λ x ↦ (f x).succ
  -- have obv : ∀ x, (f x) + 1 = f' x := by simp [f']
  -- clear f'
  wlog h : a = 0
  sorry

gives an error:

8:2: 
tactic 'introN' failed, insufficient number of binders
a : Nat
f : Nat → Nat
h : a = 0
⊢ f a = 0

Uncommenting either of the commented lines fixes the problem so it seems to be related to the fact that the f' declaration is not used before the wlog tactic.

Tested with leanprover/lean4:v4.17.0-rc1 and 96a5ba5.

[dMaggot]

After much bisecting I found that the change that breaks this example was introduced between v14.0.0 and v15.0.0. Checking the diff it is very self-explanatory:

diff --git a/Mathlib/Tactic/WLOG.lean b/Mathlib/Tactic/WLOG.lean
index 461949d04a..cad9a19bf5 100644
--- a/Mathlib/Tactic/WLOG.lean
+++ b/Mathlib/Tactic/WLOG.lean
@@ -77,7 +77,8 @@ def _root_.Lean.MVarId.wlog (goal : MVarId) (h : Option Name) (P : Expr)
   let (revertedFVars, HType) ← liftMkBindingM fun ctx => (do
     let f ← collectForwardDeps lctx fvars
     let revertedFVars := filterOutImplementationDetails lctx (f.map Expr.fvarId!)
-    let HType ← withFreshCache do mkAuxMVarType lctx (revertedFVars.map Expr.fvar) .natural HSuffix
+    let HType ← withFreshCache do
+      mkAuxMVarType lctx (revertedFVars.map Expr.fvar) .natural HSuffix (usedLetOnly := true)
     return (revertedFVars, HType))
       { preserveOrder := false, mainModule := ctx.mainModule }
   /- Set up the goal which will suppose `h`; this begins as a goal with type H (hence HExpr), and h

Is this intentional then?