chore: adaptations for nightly-2024-11-21 (#19331)

Co-authored-by: Kyle Miller <[email protected]> Co-authored-by: JovanGerb <[email protected]> Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Johan Commelin <[email protected]>
leanprover-community · Nov 21, 2024 · 77813d7 · 77813d7
1 parent f1ce937
commit 77813d7
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 4 deletions.
diff --git 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

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -65,10 +65,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9b9f4d0406d00baaae62d1a717b5aa854a2ae51d",
+   "rev": "b3935d53ce8dad5665af7ac41f06f0f6de4d942f",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing",
+   "inputRev": "lean-pr-testing-6128",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-11-20
+leanprover/lean4:nightly-2024-11-21
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:nightly-2024-11-20
		leanprover/lean4:nightly-2024-11-21