doc: document release notes process and add guard check

This PR documents the release notes writing process in detail and adds a guard
check to release_checklist.py to ensure release notes are created for -rc1
releases before proceeding with downstream repository updates.

Changes:
- doc/dev/release_checklist.md: Expanded "Writing the release notes" section
  with detailed steps for generating, reviewing, and formatting release notes
  in Verso format
- script/release_checklist.py: Added check_release_notes_file_exists() to
  verify the release notes file exists in reference-manual repository
- .claude/commands/release.md: Added "Release Notes" section explaining the
  process for creating release notes during -rc1 releases

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

.github/workflows/build-template.yml

@@ -66,10 +66,16 @@ jobs:
           brew install ccache tree zstd coreutils gmp libuv
         if: runner.os == 'macOS'
       - name: Checkout
+        if: (!endsWith(matrix.os, '-with-cache'))
         uses: actions/checkout@v6
         with:
           # the default is to use a virtual merge commit between the PR and master: just use the PR
           ref: ${{ github.event.pull_request.head.sha }}
+      - name: Namespace Checkout
+        if: endsWith(matrix.os, '-with-cache')
+        uses: namespacelabs/nscloud-checkout-action@v8
+        with:
+          ref: ${{ github.event.pull_request.head.sha }}
       - name: Open Nix shell once
         run: true
         if: runner.os == 'Linux'

script/release_repos.yml

@@ -14,6 +14,13 @@ repositories:
     bump-branch: true
     dependencies: []
 
+  - name: verso
+    url: https://github.com/leanprover/verso
+    toolchain-tag: true
+    stable-branch: false
+    branch: main
+    dependencies: []
+
   - name: lean4checker
     url: https://github.com/leanprover/lean4checker
     toolchain-tag: true
@@ -35,14 +42,6 @@ repositories:
     branch: main
     dependencies: []
 
-  - name: verso
-    url: https://github.com/leanprover/verso
-    toolchain-tag: true
-    stable-branch: false
-    branch: main
-    dependencies:
-      - plausible
-
   - name: import-graph
     url: https://github.com/leanprover-community/import-graph
     toolchain-tag: true

src/CMakeLists.txt

@@ -11,8 +11,8 @@ include(ExternalProject)
 project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4)
 set(LEAN_VERSION_MINOR 28)
-set(LEAN_VERSION_PATCH 1)
-set(LEAN_VERSION_IS_RELEASE 1)  # This number is 1 in the release revision, and 0 otherwise.
+set(LEAN_VERSION_PATCH 0)
+set(LEAN_VERSION_IS_RELEASE 0)  # This number is 1 in the release revision, and 0 otherwise.
 set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")
 set(LEAN_VERSION_STRING "${LEAN_VERSION_MAJOR}.${LEAN_VERSION_MINOR}.${LEAN_VERSION_PATCH}")
 if (LEAN_SPECIAL_VERSION_DESC)

src/Init/SimpLemmas.lean

@@ -44,6 +44,61 @@ theorem implies_congr_left {p₁ p₂ : Sort u} {q : Sort v} (h : p₁ = p₂) :
 theorem implies_congr_right {p : Sort u} {q₁ q₂ : Sort v} (h : q₁ = q₂) : (p → q₁) = (p → q₂) :=
   h ▸ rfl
 
+namespace Lean
+/--
+`Arrow α β` is definitionally equal to `α → β`, but represented as a function
+application rather than `Expr.forallE`.
+
+This representation is useful for proof automation that builds nested implications
+like `pₙ → ... → p₂ → p₁`. With `Expr.forallE`, each nesting level introduces a
+binder that bumps de Bruijn indices in subterms, destroying sharing even with
+hash-consing. For example, if `p₁` contains `#20`, then at depth 2 it becomes `#21`,
+at depth 3 it becomes `#22`, etc., causing quadratic proof growth.
+
+With `arrow`, both arguments are explicit (not under binders), so subterms remain
+identical across nesting levels and can be shared, yielding linear-sized proofs.
+-/
+def Arrow (α : Sort u) (β : Sort v) : Sort (imax u v) := α → β
+
+theorem arrow_congr {p₁ p₂ : Sort u} {q₁ q₂ : Sort v} (h₁ : p₁ = p₂) (h₂ : q₁ = q₂) : Arrow p₁ q₁ = Arrow p₂ q₂ :=
+  h₁ ▸ h₂ ▸ rfl
+
+theorem arrow_congr_left {p₁ p₂ : Sort u} {q : Sort v} (h : p₁ = p₂) : Arrow p₁ q = Arrow p₂ q :=
+  h ▸ rfl
+
+theorem arrow_congr_right {p : Sort u} {q₁ q₂ : Sort v} (h : q₁ = q₂) : Arrow p q₁ = Arrow p q₂ :=
+  h ▸ rfl
+
+theorem true_arrow (p : Prop) : Arrow True p = p := by
+  simp [Arrow]; constructor
+  next => intro h; exact h .intro
+  next => intros; assumption
+
+theorem true_arrow_congr_left (p q : Prop) : p = True → Arrow p q = q := by
+  intros; subst p; apply true_arrow
+
+theorem true_arrow_congr_right (q q' : Prop) : q = q' → Arrow True q = q' := by
+  intros; subst q; apply true_arrow
+
+theorem true_arrow_congr (p q q' : Prop) : p = True → q = q' → Arrow p q = q' := by
+  intros; subst p q; apply true_arrow
+
+theorem false_arrow (p : Prop) : Arrow False p = True := by
+  simp [Arrow]; constructor
+  next => intros; exact .intro
+  next => intros; contradiction
+
+theorem false_arrow_congr (p q : Prop) : p = False → Arrow p q = True := by
+  intros; subst p; apply false_arrow
+
+theorem arrow_true (α : Sort u) : Arrow α True = True := by
+  simp [Arrow]; constructor <;> intros <;> exact .intro
+
+theorem arrow_true_congr (α : Sort u) (p : Prop) : p = True → Arrow α p = True := by
+  intros; subst p; apply arrow_true
+
+end Lean
+
 theorem iff_congr {p₁ p₂ q₁ q₂ : Prop} (h₁ : p₁ ↔ p₂) (h₂ : q₁ ↔ q₂) : (p₁ ↔ q₁) ↔ (p₂ ↔ q₂) :=
   Iff.of_eq (propext h₁ ▸ propext h₂ ▸ rfl)
 

src/Lean/Meta/Sym/Simp.lean

@@ -22,3 +22,4 @@ public import Lean.Meta.Sym.Simp.EvalGround
 public import Lean.Meta.Sym.Simp.Discharger
 public import Lean.Meta.Sym.Simp.ControlFlow
 public import Lean.Meta.Sym.Simp.Goal
+public import Lean.Meta.Sym.Simp.Telescope

src/Lean/Meta/Sym/Simp/ControlFlow.lean

@@ -27,16 +27,16 @@ def simpIte : Simproc := fun e => do
     let_expr f@ite α c _ a b := e | return .rfl
     match (← simp c) with
     | .rfl _ =>
-      if isSameExpr c (← getTrueExpr) then
+      if (← isTrueExpr c) then
         return .step a <| mkApp3 (mkConst ``ite_true f.constLevels!) α a b
-      else if isSameExpr c (← getFalseExpr) then
+      else if (← isFalseExpr  c) then
         return .step b <| mkApp3 (mkConst ``ite_false f.constLevels!) α a b
       else
         return .rfl (done := true)
     | .step c' h _ =>
-      if isSameExpr c' (← getTrueExpr) then
+      if (← isTrueExpr c') then
         return .step a <| mkApp (e.replaceFn ``ite_cond_eq_true) h
-      else if isSameExpr c' (← getFalseExpr) then
+      else if (← isFalseExpr c') then
         return .step b <| mkApp (e.replaceFn ``ite_cond_eq_false) h
       else
         let .some inst' ← trySynthInstance (mkApp (mkConst ``Decidable) c') | return .rfl
@@ -56,20 +56,20 @@ def simpDIte : Simproc := fun e => do
     let_expr f@dite α c _ a b := e | return .rfl
     match (← simp c) with
     | .rfl _ =>
-      if isSameExpr c (← getTrueExpr) then
+      if (← isTrueExpr c) then
         let a' ← share <| a.betaRev #[mkConst ``True.intro]
         return .step a' <| mkApp3 (mkConst ``dite_true f.constLevels!) α a b
-      else if isSameExpr c (← getFalseExpr) then
+      else if (← isFalseExpr c) then
         let b' ← share <| b.betaRev #[mkConst ``not_false]
         return .step b' <| mkApp3 (mkConst ``dite_false f.constLevels!) α a b
       else
         return .rfl (done := true)
     | .step c' h _ =>
-      if isSameExpr c' (← getTrueExpr) then
+      if (← isTrueExpr c') then
         let h' ← shareCommon <| mkOfEqTrueCore c h
         let a ← share <| a.betaRev #[h']
         return .step a <| mkApp (e.replaceFn ``dite_cond_eq_true) h
-      else if isSameExpr c' (← getFalseExpr) then
+      else if (← isFalseExpr c') then
         let h' ← shareCommon <| mkOfEqFalseCore c h
         let b ← share <| b.betaRev #[h']
         return .step b <| mkApp (e.replaceFn ``dite_cond_eq_false) h

src/Lean/Meta/Sym/Simp/Forall.lean

@@ -7,6 +7,8 @@ module
 prelude
 public import Lean.Meta.Sym.Simp.SimpM
 import Lean.Meta.Sym.AlphaShareBuilder
+import Lean.Meta.Sym.InferType
+import Lean.Meta.Sym.Simp.Result
 namespace Lean.Meta.Sym.Simp
 
 /--
@@ -25,7 +27,7 @@ The proof uses the approach used in `mkFunextFor` followed by an `Eq.ndrec`.
 def mkForallCongrFor (xs : Array Expr) : MetaM Expr := do
   let prop := mkSort 0
   let type ← mkForallFVars xs prop
-  let w ← getLevel type
+  let w ← Meta.getLevel type
   withLocalDeclD `p type fun p =>
   withLocalDeclD `q type fun q => do
   let eq := mkApp3 (mkConst ``Eq [1]) prop (mkAppN p xs) (mkAppN q xs)
@@ -53,6 +55,119 @@ def mkForallCongrFor (xs : Array Expr) : MetaM Expr := do
 
 open Internal
 
+structure ArrowInfo where
+  binderName : Name
+  binderInfo : BinderInfo
+  u          : Level
+  v          : Level
+
+structure ToArrowResult where
+  arrow : Expr
+  infos : List ArrowInfo
+  v     : Level
+
+def toArrow (e : Expr) : SymM ToArrowResult := do
+  if let .forallE n α β bi := e then
+    if !β.hasLooseBVars then
+      let { arrow, infos, v } ← toArrow β
+      let u ← getLevel α
+      let arrow ← mkAppS₂ (← mkConstS ``Arrow [u, v]) α arrow
+      let info := { binderName := n, binderInfo := bi, u, v }
+      return { arrow, v := mkLevelIMax' u v, infos := info :: infos }
+  return { arrow := e, infos := [], v := (← getLevel e) }
+
+def toForall (e : Expr) (infos : List ArrowInfo) : SymM Expr := do
+  let { binderName, binderInfo, .. } :: infos := infos | return e
+  let_expr Arrow α β := e | return e
+  mkForallS binderName binderInfo α (← toForall β infos)
+
+/--
+Recursively simplifies an `Arrow` telescope, applying telescope-specific simplifications:
+
+- **False hypothesis**: `False → q` simplifies to `True` (via `false_arrow`)
+- **True hypothesis**: `True → q` simplifies to `q` (via `true_arrow`)
+- **True conclusion**: `p → True` simplifies to `True` (via `arrow_true`)
+
+The first two are applicable only if  `q` is in `Prop` (checked via `info.v.isZero`).
+
+Returns the simplified result paired with the remaining `ArrowInfo` list. When a telescope
+collapses (e.g., to `True`), the returned `infos` list is empty, signaling to `toForall`
+that no reconstruction is needed.
+-/
+partial def simpArrows (e : Expr) (infos : List ArrowInfo) (simpBody : Simproc) : SimpM (Result × List ArrowInfo) := do
+  match infos with
+  | [] => return ((← simpBody e), [])
+  | info :: infos' =>
+    let_expr f@Arrow p q := e | return ((← simpBody e), infos)
+    let p_r ← simp p
+    if (← isFalseExpr (p_r.getResultExpr p)) && info.v.isZero then
+      match p_r with
+      | .rfl _ => return (.step (← getTrueExpr) (mkApp (mkConst ``false_arrow) q), [])
+      | .step _ h _ => return (.step (← getTrueExpr) (mkApp3 (mkConst ``false_arrow_congr) p q h), [])
+    let (q_r, infos') ← simpArrows q infos' simpBody
+    if (← isTrueExpr (q_r.getResultExpr q)) then
+      match q_r with
+      | .rfl _ => return (.step (← getTrueExpr) (mkApp (mkConst ``arrow_true [info.u]) p), [])
+      | .step _ h _ => return (.step (← getTrueExpr) (mkApp3 (mkConst ``arrow_true_congr [info.u]) p q h), [])
+    match p_r, q_r with
+    | .rfl _, .rfl _ =>
+      if (← isTrueExpr p) && info.v.isZero then
+        return (.step q (mkApp (mkConst ``true_arrow) q), infos')
+      else
+        return (.rfl, infos)
+    | .step p' h _, .rfl _ =>
+      if (← isTrueExpr p') && info.v.isZero then
+        return (.step q (mkApp3 (mkConst ``true_arrow_congr_left) p q h), infos')
+      else
+        let e' ← mkAppS₂ f p' q
+        return (.step e' <| mkApp4 (mkConst ``arrow_congr_left f.constLevels!) p p' q h, info :: infos')
+    | .rfl _, .step q' h _ =>
+      if (← isTrueExpr p) && info.v.isZero then
+        return (.step q' (mkApp3 (mkConst ``true_arrow_congr_right) q q' h), infos')
+      else
+        let e' ← mkAppS₂ f p q'
+        return (.step e' <| mkApp4 (mkConst ``arrow_congr_right f.constLevels!) p q q' h, info :: infos')
+    | .step p' h₁ _, .step q' h₂ _ =>
+      if (← isTrueExpr p') && info.v.isZero then
+        return (.step q' (mkApp5 (mkConst ``true_arrow_congr) p q q' h₁ h₂), infos')
+      else
+        let e' ← mkAppS₂ f p' q'
+        return (.step e' <| mkApp6 (mkConst ``arrow_congr f.constLevels!) p p' q q' h₁ h₂, info :: infos')
+
+/--
+Simplifies a telescope of non-dependent arrows `p₁ → p₂ → ... → pₙ → q` by:
+1. Converting to `Arrow p₁ (Arrow p₂ (... (Arrow pₙ q)))` (see `toArrow`)
+2. Simplifying each `pᵢ` and `q` (see `simpArrows`)
+3. Converting back to `→` form (see `toForall`)
+
+Using `Arrow` (a definitional wrapper around `→`) avoids the quadratic proof growth that
+occurs with `Expr.forallE`. With `forallE`, each nesting level bumps de Bruijn indices in
+subterms, destroying sharing. For example, if each `pᵢ` contains a free variable `x`, the
+de Bruijn representation of `x` differs at each depth, preventing hash-consing from
+recognizing them as identical.
+
+With `Arrow`, both arguments are explicit (not under binders), so subterms remain identical
+across nesting levels and can be shared, yielding linear-sized proofs.
+
+**Tradeoff**: This function simplifies each `pᵢ` and `q` individually, but misses
+simplifications that depend on the arrow structure itself. For example, `q → p → p`
+won't be simplified to `True` (when `p : Prop`) because the simplifier does not have
+a chance to apply `post` methods to the intermediate arrow `p → p`.
+
+Thus, this is a simproc that is meant to be used as a pre-method and marks the
+result as fully simplified to prevent `simpArrow` from being applied.
+-/
+public def simpArrowTelescope (simpBody : Simproc := simp) : Simproc := fun e => do
+  unless e.isArrow do return .rfl -- not applicable
+  let { arrow, infos, v } ← toArrow e
+  let (.step arrow' h _, infos) ← simpArrows arrow infos simpBody | return .rfl (done := true)
+  let e' ← toForall arrow' infos
+  let α := mkSort v
+  let v1 := v.succ
+  let h := mkApp6 (mkConst ``Eq.trans [v1]) α e arrow arrow' (mkApp2 (mkConst ``Eq.refl [v1]) α arrow) h
+  let h := mkApp6 (mkConst ``Eq.trans [v1]) α e arrow' e' h (mkApp2 (mkConst ``Eq.refl [v1]) α e')
+  return .step e' h (done := true)
+
 public def simpArrow (e : Expr) : SimpM Result := do
   let p := e.bindingDomain!
   let q := e.bindingBody!
@@ -75,7 +190,7 @@ public def simpArrow (e : Expr) : SimpM Result := do
     let e' ← e.updateForallS! p' q'
     return .step e' <| mkApp6 (mkConst ``implies_congr [u, v]) p p' q q' h₁ h₂
 
-public def simpForall (e : Expr) : SimpM Result := do
+public def simpForall' (simpArrow : Simproc) (simpBody : Simproc) (e : Expr) : SimpM Result := do
   if e.isArrow then
     simpArrow e
   else if (← isProp e) then
@@ -86,7 +201,7 @@ public def simpForall (e : Expr) : SimpM Result := do
     return .rfl
 where
   main (xs : Array Expr) (b : Expr) : SimpM Result := do
-    match (← simp b) with
+    match (← simpBody b) with
     | .rfl _ => return .rfl
     | .step b' h _ =>
       let h ← mkLambdaFVars xs h
@@ -101,4 +216,7 @@ where
     | .forallE _ _ b _ => if b.hasLooseBVar 0 then getForallTelescopeSize b (n+1) else n
     | _ => n
 
+public def simpForall : Simproc :=
+  simpForall' simpArrow simp
+
 end Lean.Meta.Sym.Simp

src/Lean/Meta/Sym/Simp/Have.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Sym.Simp.SimpM
-import Lean.Meta.Sym.Simp.Lambda
+public import Lean.Meta.Sym.Simp.Lambda
 import Lean.Meta.Sym.AlphaShareBuilder
 import Lean.Meta.Sym.InstantiateS
 import Lean.Meta.Sym.ReplaceS
@@ -316,7 +316,8 @@ For each application `f a`:
 - If only `a` changed: use `congrArg : a = a' → f a = f a'`
 - If neither changed: return `.rfl`
 -/
-def simpBetaApp (e : Expr) (fType : Expr) (fnUnivs argUnivs : Array Level) : SimpM Result := do
+def simpBetaApp (e : Expr) (fType : Expr) (fnUnivs argUnivs : Array Level)
+    (simpBody : Simproc) : SimpM Result := do
   return (← go e 0).1
 where
   go (e : Expr) (i : Nat) : SimpM (Result × Expr) := do
@@ -339,7 +340,7 @@ where
           let h := mkApp6 (← mkCongrPrefix ``congr fType i) f f' a a' hf ha
           pure <| .step e' h
       return (r, fType.bindingBody!)
-    | .lam .. => return (← simpLambda e, fType)
+    | .lam .. => return (← simpBody e, fType)
     | _ => unreachable!
 
   mkCongrPrefix (declName : Name) (fType : Expr) (i : Nat) : SymM Expr := do
@@ -375,12 +376,12 @@ e₃ = e₄    (by rfl, definitional equality from toHave)
 e₁ = e₄    (by transitivity)
 ```
 -/
-def simpHaveCore (e : Expr) : SimpM SimpHaveResult := do
+def simpHaveCore (e : Expr) (simpBody : Simproc) : SimpM SimpHaveResult := do
   let e₁ := e
   let r ← toBetaApp e₁
   let e₂ := r.e
   let { fnUnivs, argUnivs } ← getUnivs r.fType
-  match (← simpBetaApp e₂ r.fType fnUnivs argUnivs) with
+  match (← simpBetaApp e₂ r.fType fnUnivs argUnivs simpBody) with
   | .rfl _ => return { result := .rfl, α := r.α, u := r.u }
   | .step e₃ h _ =>
     let h₁ := mkApp6 (mkConst ``Eq.trans [r.u]) r.α e₁ e₂ e₃ r.h h
@@ -397,8 +398,8 @@ Simplify a `have`-telescope.
 This is the main entry point for `have`-telescope simplification in `Sym.simp`.
 See module documentation for the algorithm overview.
 -/
-public def simpHave (e : Expr) : SimpM Result := do
-  return (← simpHaveCore e).result
+public def simpHave (e : Expr) (simpBody : Simproc) : SimpM Result := do
+  return (← simpHaveCore e simpBody).result
 
 /--
 Simplify a `have`-telescope and eliminate unused bindings.
@@ -406,8 +407,8 @@ Simplify a `have`-telescope and eliminate unused bindings.
 This combines simplification with dead variable elimination in a single pass,
 avoiding quadratic behavior from multiple passes.
 -/
-public def simpHaveAndZetaUnused (e₁ : Expr) : SimpM Result := do
-  let r ← simpHaveCore e₁
+public def simpHaveAndZetaUnused (e₁ : Expr) (simpBody : Simproc) : SimpM Result := do
+  let r ← simpHaveCore e₁ simpBody
   match r.result with
   | .rfl _ =>
     let e₂ ← zetaUnused e₁
@@ -425,7 +426,7 @@ public def simpHaveAndZetaUnused (e₁ : Expr) : SimpM Result := do
         (mkApp2 (mkConst ``Eq.refl [r.u]) r.α e₃)
       return .step e₃ h
 
-public def simpLet (e : Expr) : SimpM Result := do
+public def simpLet' (simpBody : Simproc) (e : Expr) : SimpM Result := do
   if !e.letNondep! then
     /-
     **Note**: We don't do anything if it is a dependent `let`.
@@ -433,6 +434,9 @@ public def simpLet (e : Expr) : SimpM Result := do
     -/
     return .rfl
   else
-    simpHaveAndZetaUnused e
+    simpHaveAndZetaUnused e simpBody
+
+public def simpLet : Simproc :=
+  simpLet' simpLambda
 
 end Lean.Meta.Sym.Simp

src/Lean/Meta/Sym/Simp/Lambda.lean

@@ -46,12 +46,12 @@ def mkFunextFor (xs : Array Expr) (β : Expr) : MetaM Expr := do
   let result ← mkLambdaFVars #[f, g, h] result
   return result
 
-public def simpLambda (e : Expr) : SimpM Result := do
+public def simpLambda' (simpBody : Simproc) (e : Expr) : SimpM Result := do
   lambdaTelescope e fun xs b => withoutModifyingCacheIfNotWellBehaved do
     main xs (← shareCommon b)
 where
   main (xs : Array Expr) (b : Expr) : SimpM Result := do
-    match (← simp b) with
+    match (← simpBody b) with
     | .rfl _ => return .rfl
     | .step b' h _ =>
       let h ← mkLambdaFVars xs h
@@ -69,4 +69,7 @@ where
       modify fun s => { s with funext := s.funext.insert { expr := key } h }
       return h
 
+public def simpLambda : Simproc :=
+  simpLambda' simp
+
 end Lean.Meta.Sym.Simp

src/Lean/Meta/Sym/Simp/Result.lean

@@ -26,4 +26,8 @@ public def Result.markAsDone : Result → Result
   | .rfl _ => .rfl true
   | .step e h _ => .step e h true
 
+public def Result.getResultExpr : Expr → Result → Expr
+  | e, .rfl _ => e
+  | _, .step e _ _ => e
+
 end Lean.Meta.Sym.Simp

src/Lean/Meta/Sym/Simp/Telescope.lean

@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Sym.Simp.SimpM
+import Lean.Meta.Sym.Simp.Have
+import Lean.Meta.Sym.Simp.Forall
+namespace Lean.Meta.Sym.Simp
+/--
+Simplify telescope binders (`have`-expression values, and arrow hypotheses)
+but not the final body. This simproc is useful to simplify target before
+introducing.
+-/
+public partial def simpTelescope : Simproc := fun e => do
+  match e with
+  | .letE .. =>
+    simpLet' (simpLambda' simpTelescope) e
+  | .forallE .. =>
+    simpForall' (simpArrow := simpArrowTelescope simpTelescope) (simpBody := simpLambda' simpTelescope) e
+  | _ => return .rfl
+
+end Lean.Meta.Sym.Simp

src/Lean/Meta/Sym/SymM.lean

@@ -157,8 +157,12 @@ def getSharedExprs : SymM SharedExprs :=
 
 /-- Returns the internalized `True` constant.  -/
 def getTrueExpr : SymM Expr := return (← getSharedExprs).trueExpr
+/-- Returns `true` if `e` is the internalized `True` expression.  -/
+def isTrueExpr (e : Expr) : SymM Bool := return isSameExpr e (← getTrueExpr)
 /-- Returns the internalized `False` constant.  -/
 def getFalseExpr : SymM Expr := return (← getSharedExprs).falseExpr
+/-- Returns `true` if `e` is the internalized `False` expression.  -/
+def isFalseExpr (e : Expr) : SymM Bool := return isSameExpr e (← getFalseExpr)
 /-- Returns the internalized `Bool.true`.  -/
 def getBoolTrueExpr : SymM Expr := return (← getSharedExprs).btrueExpr
 /-- Returns the internalized `Bool.false`.  -/

src/Lean/Meta/Tactic/Grind/Types.lean

@@ -162,7 +162,7 @@ structure Context where
   extensions   : ExtensionStateArray := #[]
   debug        : Bool -- Cached `grind.debug (← getOptions)`
 
-export Sym (getTrueExpr getFalseExpr getBoolTrueExpr getBoolFalseExpr getNatZeroExpr getOrderingEqExpr getIntExpr)
+export Sym (getTrueExpr getFalseExpr getBoolTrueExpr getBoolFalseExpr getNatZeroExpr getOrderingEqExpr getIntExpr isTrueExpr isFalseExpr)
 
 /-- Key for the congruence theorem cache. -/
 structure CongrTheoremCacheKey where
@@ -379,14 +379,6 @@ Abstracts nested proofs in `e`. This is a preprocessing step performed before in
 def abstractNestedProofs (e : Expr) : GrindM Expr :=
   Meta.abstractNestedProofs e
 
-/-- Returns `true` if `e` is the internalized `True` expression.  -/
-def isTrueExpr (e : Expr) : GrindM Bool :=
-  return isSameExpr e (← getTrueExpr)
-
-/-- Returns `true` if `e` is the internalized `False` expression.  -/
-def isFalseExpr (e : Expr) : GrindM Bool :=
-  return isSameExpr e (← getFalseExpr)
-
 /--
 Creates a congruence theorem for a `f`-applications with `numArgs` arguments.
 -/
@@ -1115,11 +1107,11 @@ def getGeneration (e : Expr) : GoalM Nat :=
 
 /-- Returns `true` if `e` is in the equivalence class of `True`. -/
 def isEqTrue (e : Expr) : GoalM Bool := do
-  return isSameExpr (← getENode e).root (← getTrueExpr)
+  return (← isTrueExpr (← getENode e).root)
 
 /-- Returns `true` if `e` is in the equivalence class of `False`. -/
 def isEqFalse (e : Expr) : GoalM Bool := do
-  return isSameExpr (← getENode e).root (← getFalseExpr)
+  return (← isFalseExpr (← getENode e).root)
 
 /-- Returns `true` if `e` is in the equivalence class of `Bool.true`. -/
 def isEqBoolTrue (e : Expr) : GoalM Bool := do

src/include/lean/lean.h

@@ -324,55 +324,6 @@ LEAN_EXPORT LEAN_NORETURN void lean_internal_panic(char const * msg);
 LEAN_EXPORT LEAN_NORETURN void lean_internal_panic_out_of_memory(void);
 LEAN_EXPORT LEAN_NORETURN void lean_internal_panic_unreachable(void);
 LEAN_EXPORT LEAN_NORETURN void lean_internal_panic_rc_overflow(void);
-LEAN_EXPORT LEAN_NORETURN void lean_internal_panic_overflow(void);
-
-static inline bool lean_usize_mul_would_overflow(size_t a, size_t b) {
-#if defined(__GNUC__) || defined(__clang__)
-    size_t r;
-    return __builtin_mul_overflow(a, b, &r);
-#else
-    return a != 0 && b > SIZE_MAX / a;
-#endif
-}
-
-static inline bool lean_usize_add_would_overflow(size_t a, size_t b) {
-#if defined(__GNUC__) || defined(__clang__)
-    size_t r;
-    return __builtin_add_overflow(a, b, &r);
-#else
-    return a > SIZE_MAX - b;
-#endif
-}
-
-static inline size_t lean_usize_mul_checked(size_t a, size_t b) {
-#if defined(__GNUC__) || defined(__clang__)
-    size_t r;
-    if (LEAN_UNLIKELY(__builtin_mul_overflow(a, b, &r))) {
-        lean_internal_panic_overflow();
-    }
-    return r;
-#else
-    if (a != 0 && b > SIZE_MAX / a) {
-        lean_internal_panic_overflow();
-    }
-    return a * b;
-#endif
-}
-
-static inline size_t lean_usize_add_checked(size_t a, size_t b) {
-#if defined(__GNUC__) || defined(__clang__)
-    size_t r;
-    if (LEAN_UNLIKELY(__builtin_add_overflow(a, b, &r))) {
-        lean_internal_panic_overflow();
-    }
-    return r;
-#else
-    if (a > SIZE_MAX - b) {
-        lean_internal_panic_overflow();
-    }
-    return a + b;
-#endif
-}
 
 static inline size_t lean_align(size_t v, size_t a) {
     return (v / a)*a + a * (v % a != 0);
@@ -658,7 +609,7 @@ static inline uint8_t * lean_ctor_scalar_cptr(lean_object * o) {
 
 static inline lean_object * lean_alloc_ctor(unsigned tag, unsigned num_objs, unsigned scalar_sz) {
     assert(tag <= LeanMaxCtorTag && num_objs < LEAN_MAX_CTOR_FIELDS && scalar_sz < LEAN_MAX_CTOR_SCALARS_SIZE);
-    lean_object * o = lean_alloc_ctor_memory(lean_usize_add_checked(lean_usize_add_checked(sizeof(lean_ctor_object), lean_usize_mul_checked(sizeof(void*), num_objs)), scalar_sz));
+    lean_object * o = lean_alloc_ctor_memory(sizeof(lean_ctor_object) + sizeof(void*)*num_objs + scalar_sz);
     lean_set_st_header(o, tag, num_objs);
     return o;
 }
@@ -764,7 +715,7 @@ static inline lean_object ** lean_closure_arg_cptr(lean_object * o) { return lea
 static inline lean_obj_res lean_alloc_closure(void * fun, unsigned arity, unsigned num_fixed) {
     assert(arity > 0);
     assert(num_fixed < arity);
-    lean_closure_object * o = (lean_closure_object*)lean_alloc_object(lean_usize_add_checked(sizeof(lean_closure_object), lean_usize_mul_checked(sizeof(void*), num_fixed)));
+    lean_closure_object * o = (lean_closure_object*)lean_alloc_object(sizeof(lean_closure_object) + sizeof(void*)*num_fixed);
     lean_set_st_header((lean_object*)o, LeanClosure, 0);
     o->m_fun = fun;
     o->m_arity = arity;
@@ -810,7 +761,7 @@ LEAN_EXPORT lean_object* lean_apply_m(lean_object* f, unsigned n, lean_object**
 
 /* Arrays of objects (low level API) */
 static inline lean_obj_res lean_alloc_array(size_t size, size_t capacity) {
-    lean_array_object * o = (lean_array_object*)lean_alloc_object(lean_usize_add_checked(sizeof(lean_array_object), lean_usize_mul_checked(sizeof(void*), capacity)));
+    lean_array_object * o = (lean_array_object*)lean_alloc_object(sizeof(lean_array_object) + sizeof(void*)*capacity);
     lean_set_st_header((lean_object*)o, LeanArray, 0);
     o->m_size = size;
     o->m_capacity = capacity;
@@ -983,18 +934,8 @@ LEAN_EXPORT lean_object * lean_mk_array(lean_obj_arg n, lean_obj_arg v);
 
 /* Array of scalars */
 
-static inline bool lean_alloc_sarray_would_overflow(unsigned elem_size, size_t capacity) {
-    if (lean_usize_mul_would_overflow(elem_size, capacity)) {
-        return true;
-    }
-    if (lean_usize_add_would_overflow(sizeof(lean_sarray_object), elem_size * capacity)) {
-        return true;
-    }
-    return false;
-}
-
 static inline lean_obj_res lean_alloc_sarray(unsigned elem_size, size_t size, size_t capacity) {
-    lean_sarray_object * o = (lean_sarray_object*)lean_alloc_object(lean_usize_add_checked(sizeof(lean_sarray_object), lean_usize_mul_checked(elem_size, capacity)));
+    lean_sarray_object * o = (lean_sarray_object*)lean_alloc_object(sizeof(lean_sarray_object) + elem_size*capacity);
     lean_set_st_header((lean_object*)o, LeanScalarArray, elem_size);
     o->m_size = size;
     o->m_capacity = capacity;
@@ -1149,7 +1090,7 @@ static inline lean_obj_res lean_float_array_set(lean_obj_arg a, b_lean_obj_arg i
 /* Strings */
 
 static inline lean_obj_res lean_alloc_string(size_t size, size_t capacity, size_t len) {
-    lean_string_object * o = (lean_string_object*)lean_alloc_object(lean_usize_add_checked(sizeof(lean_string_object), capacity));
+    lean_string_object * o = (lean_string_object*)lean_alloc_object(sizeof(lean_string_object) + capacity);
     lean_set_st_header((lean_object*)o, LeanString, 0);
     o->m_size = size;
     o->m_capacity = capacity;

src/runtime/compact.cpp

@@ -143,7 +143,7 @@ object * object_compactor::copy_object(object * o) {
 void object_compactor::insert_sarray(object * o) {
     size_t sz        = lean_sarray_size(o);
     unsigned elem_sz = lean_sarray_elem_size(o);
-    size_t obj_sz = lean_usize_add_checked(sizeof(lean_sarray_object), lean_usize_mul_checked(elem_sz, sz));
+    size_t obj_sz = sizeof(lean_sarray_object) + elem_sz*sz;
     lean_sarray_object * new_o = (lean_sarray_object*)alloc(obj_sz);
     lean_set_non_heap_header_for_big((lean_object*)new_o, LeanScalarArray, elem_sz);
     new_o->m_size     = sz;
@@ -155,7 +155,7 @@ void object_compactor::insert_sarray(object * o) {
 void object_compactor::insert_string(object * o) {
     size_t sz        = lean_string_size(o);
     size_t len       = lean_string_len(o);
-    size_t obj_sz = lean_usize_add_checked(sizeof(lean_string_object), sz);
+    size_t obj_sz = sizeof(lean_string_object) + sz;
     lean_string_object * new_o = (lean_string_object*)alloc(obj_sz);
     lean_set_non_heap_header_for_big((lean_object*)new_o, LeanString, 0);
     new_o->m_size     = sz;
@@ -214,7 +214,7 @@ bool object_compactor::insert_array(object * o) {
     }
     if (missing_children)
         return false;
-    size_t obj_sz = lean_usize_add_checked(sizeof(lean_array_object), lean_usize_mul_checked(sizeof(void*), sz));
+    size_t obj_sz = sizeof(lean_array_object) + sizeof(void*)*sz;
     lean_array_object * new_o = (lean_array_object*)alloc(obj_sz);
     lean_set_non_heap_header_for_big((lean_object*)new_o, LeanArray, 0);
     new_o->m_size     = sz;
@@ -274,8 +274,8 @@ bool object_compactor::insert_promise(object * o) {
 void object_compactor::insert_mpz(object * o) {
 #ifdef LEAN_USE_GMP
     size_t nlimbs = mpz_size(to_mpz(o)->m_value.m_val);
-    size_t data_sz = lean_usize_mul_checked(sizeof(mp_limb_t), nlimbs);
-    size_t sz = lean_usize_add_checked(sizeof(mpz_object), data_sz);
+    size_t data_sz = sizeof(mp_limb_t) * nlimbs;
+    size_t sz = sizeof(mpz_object) + data_sz;
     mpz_object * new_o = (mpz_object *)alloc(sz);
     memcpy(new_o, to_mpz(o), sizeof(mpz_object));
     lean_set_non_heap_header((lean_object*)new_o, sz, LeanMPZ, 0);
@@ -287,8 +287,8 @@ void object_compactor::insert_mpz(object * o) {
     m._mp_alloc = nlimbs;
     save(o, (lean_object*)new_o);
 #else
-    size_t data_sz = lean_usize_mul_checked(sizeof(mpn_digit), to_mpz(o)->m_value.m_size);
-    size_t sz      = lean_usize_add_checked(sizeof(mpz_object), data_sz);
+    size_t data_sz = sizeof(mpn_digit) * to_mpz(o)->m_value.m_size;
+    size_t sz      = sizeof(mpz_object) + data_sz;
     mpz_object * new_o = (mpz_object *)alloc(sz);
     // Manually copy the `mpz_object` to ensure `mpz` struct padding is left as
     // zero as prepared by `object_compactor::alloc`. `memcpy` would copy the

src/runtime/io.cpp

@@ -583,9 +583,6 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_truncate(b_obj_arg h) {
 /* Handle.read : (@& Handle) → USize → IO ByteArray */
 extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_read(b_obj_arg h, usize nbytes) {
     FILE * fp = io_get_handle(h);
-    if (lean_alloc_sarray_would_overflow(1, nbytes)) {
-        return io_result_mk_error(decode_io_error(ENOMEM, NULL));
-    }
     obj_res res = lean_alloc_sarray(1, 0, nbytes);
     usize n = std::fread(lean_sarray_cptr(res), 1, nbytes, fp);
     if (n > 0) {
@@ -864,9 +861,6 @@ extern "C" LEAN_EXPORT obj_res lean_io_get_random_bytes (size_t nbytes) {
     }
 #endif
 
-    if (lean_alloc_sarray_would_overflow(1, nbytes)) {
-        return io_result_mk_error(decode_io_error(ENOMEM, NULL));
-    }
     obj_res res = lean_alloc_sarray(1, 0, nbytes);
     size_t remain = nbytes;
     uint8_t *dst = lean_sarray_cptr(res);

src/runtime/mpz.cpp

@@ -340,7 +340,7 @@ static void mpz_dealloc(void *ptr, size_t size) {
 
 void mpz::allocate(size_t s) {
     m_size   = s;
-    m_digits = static_cast<mpn_digit*>(mpz_alloc(lean_usize_mul_checked(s, sizeof(mpn_digit))));
+    m_digits = static_cast<mpn_digit*>(mpz_alloc(s * sizeof(mpn_digit)));
 }
 
 void mpz::init() {
@@ -409,8 +409,8 @@ void mpz::init_int64(int64 v) {
 void mpz::init_mpz(mpz const & v) {
     m_sign   = v.m_sign;
     m_size   = v.m_size;
-    m_digits = static_cast<mpn_digit*>(mpz_alloc(lean_usize_mul_checked(m_size, sizeof(mpn_digit))));
-    memcpy(m_digits, v.m_digits, lean_usize_mul_checked(m_size, sizeof(mpn_digit)));
+    m_digits = static_cast<mpn_digit*>(mpz_alloc(m_size * sizeof(mpn_digit)));
+    memcpy(m_digits, v.m_digits, m_size * sizeof(mpn_digit));
 }
 
 mpz::mpz() {

src/runtime/object.cpp

@@ -99,10 +99,6 @@ extern "C" LEAN_EXPORT void lean_internal_panic_rc_overflow() {
     lean_internal_panic("reference counter overflowed");
 }
 
-extern "C" LEAN_EXPORT void lean_internal_panic_overflow() {
-    lean_internal_panic("integer overflow in runtime computation");
-}
-
 bool g_exit_on_panic = false;
 bool g_panic_messages = true;
 

src/runtime/uv/tcp.cpp

@@ -182,9 +182,6 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_send(b_obj_arg socket, obj_arg d
     }
 
     // Allocate buffer array for uv_write
-    if (lean_usize_mul_would_overflow(array_len, sizeof(uv_buf_t))) {
-        return lean_io_result_mk_error(decode_io_error(ENOMEM, nullptr));
-    }
     uv_buf_t* bufs = (uv_buf_t*)malloc(array_len * sizeof(uv_buf_t));
 
     for (size_t i = 0; i < array_len; i++) {

src/runtime/uv/udp.cpp

@@ -140,9 +140,6 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_send(b_obj_arg socket, obj_arg d
         return lean_io_result_mk_ok(promise);
     }
 
-    if (lean_usize_mul_would_overflow(array_len, sizeof(uv_buf_t))) {
-        return lean_io_result_mk_error(decode_io_error(ENOMEM, nullptr));
-    }
     uv_buf_t* bufs = (uv_buf_t*)malloc(array_len * sizeof(uv_buf_t));
 
     for (size_t i = 0; i < array_len; i++) {

tests/bench/sym/simp_4.lean

@@ -1,7 +1,5 @@
 import Lean
 open Lean Meta
-opaque f : Nat → Nat
-
 namespace SimpBench
 /-!
 ## `SymM` Simplifier benchmarks
@@ -24,15 +22,18 @@ def checkWithKernel (r : Sym.Simp.Result) : MetaM Float := do
     let endTime ← IO.monoNanosNow
     return (endTime - startTime).toFloat / 1000000.0
 
-def mkSimpMethods : MetaM Sym.Simp.Methods := do
+def mkSimpMethods (arrowTelescope : Bool) : MetaM Sym.Simp.Methods := do
   let thms : Sym.Simp.Theorems := {}
   let thms := thms.insert (← Sym.Simp.mkTheoremFromDecl ``Nat.zero_add)
   let thms := thms.insert (← Sym.Simp.mkTheoremFromDecl ``Nat.add_zero)
-  return { post := thms.rewrite }
+  if arrowTelescope then
+    return { pre := Sym.Simp.simpArrowTelescope, post := thms.rewrite }
+  else
+    return { post := thms.rewrite }
 
-def simp (e : Expr) : MetaM (Sym.Simp.Result × Float) := Sym.SymM.run do
+def simp (e : Expr) (arrowTelescope : Bool) : MetaM (Sym.Simp.Result × Float) := Sym.SymM.run do
   let e ← Grind.shareCommon e
-  let methods ← mkSimpMethods
+  let methods ← mkSimpMethods arrowTelescope
   let startTime ← IO.monoNanosNow
   let r ← Sym.simp e methods { maxSteps := 100000000 }
   let endTime ← IO.monoNanosNow
@@ -44,11 +45,11 @@ def simp (e : Expr) : MetaM (Sym.Simp.Result × Float) := Sym.SymM.run do
   --   logInfo e'; logInfo h
   return (r, timeMs)
 
-def ppExample (e : Expr) (info := false) : MetaM Unit := do
+def ppExample (e : Expr) (arrowTelescope : Bool) (info := false) : MetaM Unit := do
   IO.println "Example:"
   IO.println (← ppExpr e)
   IO.println "====>"
-  match (← simp e).1 with
+  match (← simp e arrowTelescope).1 with
   | .rfl _ => IO.println "<no change>"
   | .step e' h _ =>
     IO.println (← ppExpr e')
@@ -59,8 +60,8 @@ def ppExample (e : Expr) (info := false) : MetaM Unit := do
       IO.println (← ppExpr h)
   IO.println ""
 
-def benchSimp (name : String) (e : Expr) (check := false) : MetaM Unit := do
-  let (r, timeMs) ← simp e
+def benchSimp (name : String) (e : Expr) (arrowTelescope : Bool) (check := false) : MetaM Unit := do
+  let (r, timeMs) ← simp e arrowTelescope
   let proofSize ← getProofSize r
   if check then
     let kMs ← checkWithKernel r
@@ -87,11 +88,16 @@ def mkForallBench (n : Nat) (useImplies : Bool) : MetaM Expr :=
           go n (mkApp2 (mkConst ``implies) (mkNatEq xs[n]! (mkNatAdd (mkNatLit 0) xs[n]!)) e)
         else
           go n (← mkArrow (mkNatEq xs[n]! (mkNatAdd (mkNatLit 0) xs[n]!)) e)
-    go n (mkConst ``True)
+    go n (mkConst ``False)
 
-def benchForall (n : Nat) (useImplies : Bool) (check := false) : MetaM Unit := do
-  let e ← mkForallBench n useImplies
-  benchSimp s!"forall_{n}" e check
+inductive Kind where
+  | implies
+  | arrowTelescope
+  | arrow
+
+def benchForall (n : Nat) (kind : Kind) (check := false) : MetaM Unit := do
+  let e ← mkForallBench n (kind matches .implies)
+  benchSimp s!"forall_{n}" e (kind matches .arrowTelescope) check
 
 set_option maxRecDepth 100000
 
@@ -102,17 +108,24 @@ def runAllBenchmarks : MetaM Unit := do
 
   IO.println ""
   IO.println "--- Benchmark 1: Forall Telescope block using arrows in the body ---"
-  ppExample (← mkForallBench 5 false)
+  ppExample (← mkForallBench 5 false) false
 
   for n in [10, 20, 30, 40, 50, 60, 70, 80, 90, 100, 110, 120, 130, 140, 150, 160, 170, 180, 190, 200, 300, 400] do
-    benchForall n false (n < 500)
+    benchForall n .arrow (n < 500)
 
   IO.println ""
-  IO.println "--- Benchmark 1: Forall Telescope block using `implies` in the body ---"
-  ppExample (← mkForallBench 5 true)
+  IO.println "--- Benchmark 2: Forall Telescope block using arrow telescope in the body ---"
+  ppExample (← mkForallBench 5 false) true
 
   for n in [10, 20, 30, 40, 50, 60, 70, 80, 90, 100, 110, 120, 130, 140, 150, 160, 170, 180, 190, 200, 300, 400] do
-    benchForall n true (n < 500)
+    benchForall n .arrowTelescope (n < 500)
+
+  IO.println ""
+  IO.println "--- Benchmark 3: Forall Telescope block using `implies` in the body ---"
+  ppExample (← mkForallBench 5 true) false
+
+  for n in [10, 20, 30, 40, 50, 60, 70, 80, 90, 100, 110, 120, 130, 140, 150, 160, 170, 180, 190, 200, 300, 400] do
+    benchForall n .implies (n < 500)
 
 #eval runAllBenchmarks
 

tests/compiler/file_read_overflow.lean

@@ -1,14 +0,0 @@
-/-!
-This issue is a minimal reproducer for #13388 which now throws an out of memory error.
--/
-
-def main : IO UInt32 := do
-  let (h, _) ← IO.FS.createTempFile
-  let n : USize := (0 : USize) - (1 : USize)
-  try
-    discard <| h.read n
-    return 1
-  catch e =>
-    match e with
-    | .resourceExhausted .. => return 0
-    | _ => return 1

tests/lean/run/sym_simp_4.lean

@@ -0,0 +1,96 @@
+import Lean
+open Lean Meta Elab Tactic
+
+elab "sym_simp" "[" declNames:ident,* "]" : tactic => do
+  let rewrite ← Sym.mkSimprocFor (← declNames.getElems.mapM fun s => realizeGlobalConstNoOverload s.raw) Sym.Simp.dischargeSimpSelf
+  let methods : Sym.Simp.Methods := {
+    pre  := Sym.Simp.simpControl.andThen Sym.Simp.simpArrowTelescope
+    post := Sym.Simp.evalGround.andThen rewrite
+  }
+  liftMetaTactic1 fun mvarId => Sym.SymM.run do
+    let mvarId ← Sym.preprocessMVar mvarId
+    (← Sym.simpGoal mvarId methods).toOption
+
+example : (if true then a else b) = a := by
+  sym_simp []
+
+example : (if True then a else b) = a := by
+  sym_simp []
+
+example : (if False then a else b) = b := by
+  sym_simp []
+
+/--
+trace: α✝ : Sort u_1
+x : α✝
+p q : Prop
+h : p → q
+⊢ p → q
+-/
+#guard_msgs in
+example (p q : Prop) (h : p → q) : True → p → x = x → q := by
+  sym_simp []
+  trace_state
+  exact h
+
+example (p q : Prop) : q → p → True := by
+  sym_simp []
+
+example (p q : Prop) : q → p → x = x := by
+  sym_simp []
+
+example (q : Prop) : q → x ≠ x → True := by
+  sym_simp []
+
+example (α : Type) (p : Prop) : α → p → x = x := by
+  sym_simp []
+
+example (q : Prop) (α : Type) (p : Prop) : q → α → p → x = x := by
+  sym_simp []
+
+example (α β : Type) (p q : Prop) : q → β → p → α → True := by
+  sym_simp []
+
+/--
+trace: α✝ : Sort ?u.1893
+x : α✝
+α : Type
+p : Prop
+h : α → p → True → α
+⊢ α → p → True → α
+-/
+#guard_msgs in
+example (α : Type) (p : Prop) (h : α → p → True → α) : α → p → x = x → α := by
+  sym_simp []
+  trace_state
+  exact h
+
+set_option linter.unusedVariables false
+
+/--
+trace: α✝ : Sort u_1
+x : α✝
+α : Type
+q : Prop
+h : False
+⊢ ∀ (a b : α), q
+-/
+#guard_msgs in
+example (α : Type) (q : Prop) (h : False) : (a : α) → x = x → (b : α) → True → q := by
+  sym_simp []
+  trace_state
+  cases h
+
+/--
+trace: α✝ : Sort u_1
+x : α✝
+α : Type
+p q : Prop
+h : False
+⊢ ∀ (a : α) {b : α}, q
+-/
+#guard_msgs in
+example (α : Type) (p q : Prop) (h : False) : (a : α) → x = x → {b : α} → True → (q ∧ True) := by
+  sym_simp [and_true]
+  trace_state
+  cases h

tests/lean/run/sym_simp_5.lean

@@ -0,0 +1,33 @@
+import Lean
+open Lean Meta Elab Tactic
+
+elab "sym_simp" "[" declNames:ident,* "]" : tactic => do
+  let rewrite ← Sym.mkSimprocFor (← declNames.getElems.mapM fun s => realizeGlobalConstNoOverload s.raw) Sym.Simp.dischargeSimpSelf
+  let methods : Sym.Simp.Methods := {
+    pre  := Sym.Simp.simpTelescope
+    post := Sym.Simp.evalGround.andThen rewrite
+  }
+  liftMetaTactic1 fun mvarId => Sym.SymM.run do
+    let mvarId ← Sym.preprocessMVar mvarId
+    (← Sym.simpGoal mvarId methods).toOption
+
+set_option warn.sorry false
+
+/-!
+Recall that `simpTelescope` does not simplify the body of a telescope.
+This is why `0 + x = 0 + id x` is not simplified in the following example.
+-/
+/--
+trace: p q : Prop
+⊢ q →
+    ∀ (x : Nat),
+      p →
+        have x := x;
+        have y := x;
+        x = y → 0 + x = 0 + id x
+-/
+#guard_msgs in
+example (p q : Prop) : q → ∀ x : Nat, p ∧ True → have x := 0 + x; have y := x; True → x = 0 + 0 + id y → 0 + x = 0 + id x := by
+  sym_simp [and_true, Nat.zero_add, id_eq]
+  trace_state
+  admit