fix: wlog: don't supply let vars to mkAppN (#5362)

`wlog` was erroneously supplying all reverted fvars to `mkAppN`, instead of just supplying the ones which weren't ldecls. This fixes #5348.

Mathlib/Tactic/WLOG.lean

@@ -100,8 +100,10 @@ def _root_.Lean.MVarId.wlog (goal : MVarId) (h : Option Name) (P : Expr)
   let (⟨easyGoal, hyp⟩, ⟨reductionGoal, negHyp⟩) ←
     reductionGoal.byCases P <| if inaccessible then `_ else h
   easyGoal.withContext do
+    -- Exclude ldecls from the `mkAppN` arguments
+    let HArgFVarIds ← revertedFVars.filterM (notM ·.isLetVar)
     let HApp ← instantiateMVars <|
-      mkAppN (.fvar HFVarId) (revertedFVars.map .fvar) |>.app (.fvar hyp)
+      mkAppN (.fvar HFVarId) (HArgFVarIds.map .fvar) |>.app (.fvar hyp)
     ensureHasNoMVars HApp
     easyGoal.assign HApp
   return ⟨reductionGoal, (HFVarId, negHyp), hGoal, hFVar, revertedFVars⟩

test/wlog.lean

@@ -71,3 +71,10 @@ example {x y : ℕ} : True := by
     guard_hyp h : x ≤ y
     guard_target =ₛ True
     trivial
+
+-- Handle ldecls properly:
+example (x y : ℕ) : True := by
+  let z := 0
+  wlog hxy' : z ≤ y with H
+  · trivial
+  · trivial