leanprover-community · github-actions · Jun 23, 2025 · Jun 18, 2025 · Jun 18, 2025 · Jun 18, 2025
diff --git a/Mathlib/Algebra/Lie/Weights/Chain.lean b/Mathlib/Algebra/Lie/Weights/Chain.lean
@@ -228,13 +228,15 @@ lemma exists_forall_mem_corootSpace_smul_add_eq_zero
     ← LieSubmodule.toEnd_restrict_eq_toEnd]
   -- The lines below illustrate the cost of treating `LieSubmodule` as both a
   -- `Submodule` and a `LieSubmodule` simultaneously.
+  #adaptation_note /-- 2025-06-18 (lean4#8804).
+    The `erw` causes a kernel timeout if there is no `subst`. -/
+  subst a b N
   erw [LinearMap.trace_eq_sum_trace_restrict_of_eq_biSup _ h₁ h₂ (genWeightSpaceChain M α χ p q) h₃]
-  simp_rw [N, LieSubmodule.toEnd_restrict_eq_toEnd]
-  dsimp [N]
+  simp_rw [LieSubmodule.toEnd_restrict_eq_toEnd]
   convert_to _ =
     ∑ k ∈ Finset.Ioo p q, (LinearMap.trace R { x // x ∈ (genWeightSpace M (k • α + χ)) })
       ((toEnd R { x // x ∈ H } { x // x ∈ genWeightSpace M (k • α + χ) }) x)
-  simp_rw [a, b, trace_toEnd_genWeightSpace, Pi.add_apply, Pi.smul_apply, smul_add,
+  simp_rw [trace_toEnd_genWeightSpace, Pi.add_apply, Pi.smul_apply, smul_add,
     ← smul_assoc, Finset.sum_add_distrib, ← Finset.sum_smul, natCast_zsmul]
 
 end IsCartanSubalgebra

diff --git a/Mathlib/NumberTheory/Cyclotomic/Rat.lean b/Mathlib/NumberTheory/Cyclotomic/Rat.lean
@@ -181,7 +181,7 @@ lemma coe_toInteger {k : ℕ} [NeZero k] (hζ : IsPrimitiveRoot ζ k) : hζ.toIn
 /-- `𝓞 K ⧸ Ideal.span {ζ - 1}` is finite. -/
 lemma finite_quotient_toInteger_sub_one [NumberField K] {k : ℕ} (hk : 1 < k)
     (hζ : IsPrimitiveRoot ζ k) :
-    have : NeZero k := NeZero.of_gt hk
+    haveI : NeZero k := NeZero.of_gt hk
     Finite (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1}) := by
   refine Ideal.finiteQuotientOfFreeOfNeBot _ (fun h ↦ ?_)
   simp only [Ideal.span_singleton_eq_bot, sub_eq_zero] at h

diff --git a/Mathlib/Tactic/Explode.lean b/Mathlib/Tactic/Explode.lean
@@ -109,7 +109,7 @@ partial def explodeCore (e : Expr) (depth : Nat) (entries : Entries) (start : Bo
   | .letE varName varType val body _ => do
     trace[explode] ".letE"
     let varType := varType.cleanupAnnotations
-    Meta.withLocalDeclD varName varType fun var => do
+    Meta.withLetDecl varName varType val fun var => do
       let (valEntry?, entries) ← explodeCore val depth entries
       -- Add a synonym so that the substituted fvars refer to `valEntry?`
       let entries := valEntry?.map (entries.addSynonym var) |>.getD entries

diff --git a/Mathlib/Tactic/FunProp/Core.lean b/Mathlib/Tactic/FunProp/Core.lean
@@ -638,7 +638,7 @@ mutual
         letTelescope e fun xs b => do
           let .some r ← funProp b
             | return none
-          cacheResult e {proof := ← mkLambdaFVars xs r.proof }
+          cacheResult e {proof := ← mkLambdaFVars (generalizeNondepLet := false) xs r.proof }
       | .forallE .. =>
         forallTelescope e fun xs b => do
           let .some r ← funProp b
@@ -663,9 +663,7 @@ mutual
 
     -- if function starts with let bindings move them the top of `e` and try again
     if f.isLet then
-      return ← letTelescope f fun xs b => do
-        let e' := e.setArg funPropDecl.funArgId b
-        funProp (← mkLambdaFVars xs e')
+      return ← funProp (← mapLetTelescope f fun _ b => pure <| e.setArg funPropDecl.funArgId b)
 
     match ← getFunctionData? f (← unfoldNamePred) with
     | .letE f =>

diff --git a/Mathlib/Tactic/FunProp/FunctionData.lean b/Mathlib/Tactic/FunProp/FunctionData.lean
@@ -6,6 +6,7 @@ Authors: Tomáš Skřivan
 import Qq
 
 import Mathlib.Tactic.FunProp.Mor
+import Mathlib.Tactic.FunProp.ToBatteries
 
 /-!
 ## `funProp` data structure holding information about a function

diff --git a/Mathlib/Tactic/FunProp/Mor.lean b/Mathlib/Tactic/FunProp/Mor.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Tomáš Skřivan
 -/
 import Mathlib.Data.FunLike.Basic
-import Mathlib.Tactic.FunProp.ToBatteries
 
 /-!
 ## `funProp` Meta programming functions like in Lean.Expr.* but for working with bundled morphisms.
@@ -73,8 +72,7 @@ partial def whnfPred (e : Expr) (pred : Expr → MetaM Bool) :
       if (← getConfig).zeta then
         return (coe.app f).app x
       else
-        return ← letTelescope f fun xs f' =>
-          mkLambdaFVars xs ((coe.app f').app x)
+        return ← mapLetTelescope f fun _ f' => pure ((coe.app f').app x)
 
     if (← pred e) then
         match (← unfoldDefinition? e) with

diff --git a/Mathlib/Tactic/FunProp/ToBatteries.lean b/Mathlib/Tactic/FunProp/ToBatteries.lean
@@ -32,19 +32,6 @@ def isOrderedSubsetOf {α} [Inhabited α] [DecidableEq α] (a b : Array α) : Bo
   else
     return false
 
-private def letTelescopeImpl {α} (e : Expr) (k : Array Expr → Expr → MetaM α) :
-    MetaM α :=
-  lambdaLetTelescope e fun xs b ↦ do
-    if let .some i ← xs.findIdxM? (fun x ↦ do pure !(← x.fvarId!.isLetVar)) then
-      k xs[0:i] (← mkLambdaFVars xs[i:] b)
-    else
-      k xs b
-
-/-- Telescope consuming only let bindings -/
-def letTelescope {α n} [MonadControlT MetaM n] [Monad n] (e : Expr)
-    (k : Array Expr → Expr → n α) : n α :=
-  map2MetaM (fun k => letTelescopeImpl e k) k
-
 /--
 Swaps bvars indices `i` and `j`
 
@@ -134,7 +121,7 @@ private def betaThroughLetAux (f : Expr) (args : List Expr) : Expr :=
   match f, args with
   | f, [] => f
   | .lam _ _ b _, a :: as => (betaThroughLetAux (b.instantiate1 a) as)
-  | .letE n t v b _, args => .letE n t v (betaThroughLetAux b args) false
+  | .letE n t v b nondep, args => .letE n t v (betaThroughLetAux b args) nondep
   | .mdata _ b, args => betaThroughLetAux b args
   | f, args => mkAppN f args.toArray
 

diff --git a/Mathlib/Tactic/GeneralizeProofs.lean b/Mathlib/Tactic/GeneralizeProofs.lean
@@ -257,10 +257,10 @@ where
                 else
                   pure none
               mkLambdaFVars #[x] (← visit (b.instantiate1 x) ty'?)
-          | .letE n t v b _ =>
+          | .letE n t v b nondep =>
             let t' ← visit t none
-            withLetDecl n t' (← visit v t') fun x ↦ MAbs.withLocal x do
-              mkLetFVars #[x] (← visit (b.instantiate1 x) ty?)
+            mapLetDecl n t' (← visit v t') (nondep := nondep) fun x ↦ MAbs.withLocal x do
+              visit (b.instantiate1 x) ty?
           | .app .. =>
             e.withApp fun f args ↦ do
               let f' ← visit f none
@@ -419,10 +419,10 @@ where
               -- Make this prop available as a proof
               MGen.insertFVar t' (.fvar fvar')
             go g' (i + 1) (hs ++ hs')
-        | .letE n t v b _ =>
+        | .letE n t v b nondep =>
           withGeneralizedProofs t none fun hs' pfs' t' => do
             withGeneralizedProofs v t' fun hs'' pfs'' v' => do
-              let tgt' := Expr.letE n t' v' b false
+              let tgt' := Expr.letE n t' v' b nondep
               let g' ← mkFreshExprSyntheticOpaqueMVar tgt' tag
               g.assign <| mkAppN (← mkLambdaFVars (hs' ++ hs'') g') (pfs' ++ pfs'')
               let (fvar', g') ← g'.mvarId!.intro1P

diff --git a/MathlibTest/GeneralizeProofs.lean b/MathlibTest/GeneralizeProofs.lean
@@ -189,3 +189,27 @@ example (P : True → Sort*) (p : True → P (by decide)) : True := by
   exact h
 
 end
+
+/-!
+Extracting proofs from under let bindings
+-/
+/--
+trace: pf✝ : ∀ (n : ℕ), 0 < n + 1
+⊢ have n := 0;
+  ↑⟨0, ⋯⟩ = 0
+-/
+#guard_msgs in
+example : have n := 0; (⟨0, id (by simp)⟩ : Fin (n + 1)).val = 0 := by
+  generalize_proofs
+  trace_state
+  rfl
+/--
+trace: pf✝ : ∀ (n : ℕ), 0 < n + 1
+⊢ have n := 0;
+  ↑⟨0, ⋯⟩ = 0
+-/
+#guard_msgs in
+example : have n := 0; (⟨0, id (by simp)⟩ : Fin (n + 1)).val = 0 := by
+  generalize_proofs
+  trace_state
+  rfl
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -45,30 +45,30 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c37af3a23d5798c560bce190bfd779710eaff1e1",
+   "rev": "6cdec09fae4b82592981036609ee73b2eeb9fc05",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing",
+   "inputRev": "lean-pr-testing-8804",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e1d2994e0acdee2f0c03c9d84d28a5df34aa0020",
+   "rev": "7f4c286cc750fcff5be4edae3bb21e26adcc4697",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "lean-pr-testing-8804",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "481cbb4065fba7ba938c217c41f1a28b55207e2f",
+   "rev": "d621ddb1069644388fd880d3f8c44e0fef638a96",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing",
+   "inputRev": "lean-pr-testing-8804",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",

diff --git a/lakefile.lean b/lakefile.lean
@@ -6,9 +6,9 @@ open Lake DSL
 ## Mathlib dependencies on upstream projects
 -/
 
-require "leanprover-community" / "batteries" @ git "nightly-testing"
-require "leanprover-community" / "Qq" @ git "master"
-require "leanprover-community" / "aesop" @ git "nightly-testing"
+require "leanprover-community" / "batteries" @ git "lean-pr-testing-8804"
+require "leanprover-community" / "Qq" @ git "lean-pr-testing-8804"
+require "leanprover-community" / "aesop" @ git "lean-pr-testing-8804"
 require "leanprover-community" / "proofwidgets" @ git "v0.0.63-pre" -- ProofWidgets should always be pinned to a specific version
   with NameMap.empty.insert `errorOnBuild
     "ProofWidgets not up-to-date. \

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2025-06-18
+leanprover/lean4-pr-releases:pr-release-8804-0b63061
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:nightly-2025-06-18
		leanprover/lean4-pr-releases:pr-release-8804-0b63061