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>

.claude/commands/release.md

@@ -13,12 +13,54 @@ These comments explain the scripts' behavior, which repositories get special han
 ## Arguments
 - `version`: The version to release (e.g., v4.24.0)
 
+## Release Notes (Required for -rc1 releases)
+
+For first release candidates (`-rc1`), you must create release notes BEFORE the reference-manual toolchain bump PR can be merged.
+
+**Steps to create release notes:**
+
+1. Generate the release notes:
+   ```bash
+   cd /path/to/lean4
+   python3 script/release_notes.py --since <previous_version> > /tmp/release-notes-<version>.md
+   ```
+   Replace `<previous_version>` with the last stable release (e.g., `v4.27.0` when releasing `v4.28.0-rc1`).
+
+2. Review `/tmp/release-notes-<version>.md` for common issues:
+   - **Unterminated code blocks**: Look for code fences that aren't closed. Fetch original PR with `gh pr view <number>` to repair.
+   - **Truncated descriptions**: Some may end mid-sentence. Complete them from the original PR.
+   - **Markdown issues**: Other syntax problems that could cause parsing errors.
+
+3. Create the release notes file in the reference-manual repository:
+   - File path: `Manual/Releases/v<version>.lean` (e.g., `v4_28_0.lean`)
+   - Use Verso format with proper imports and `#doc (Manual)` block
+   - **Use `#` for headers, not `##`** (Verso uses level 1 for subsections)
+   - **Use plain ` ``` ` not ` ```lean `** (the latter executes code)
+   - **Wrap underscore identifiers in backticks**: `` `bv_decide` `` not `bv_decide`
+
+4. Update `Manual/Releases.lean`:
+   - Add import: `import Manual.Releases.«v4_28_0»`
+   - Add include: `{include 0 Manual.Releases.«v4_28_0»}`
+
+5. Build to verify: `lake build Manual.Releases.v4_28_0`
+
+6. Create a **separate PR** for release notes (not bundled with toolchain bump):
+   ```bash
+   git checkout -b v<version>-release-notes
+   gh pr create --title "doc: add v<version> release notes"
+   ```
+
+For subsequent RCs (`-rc2`, etc.) and stable releases, just update the version number in the existing release notes file title.
+
+See `doc/dev/release_checklist.md` section "Writing the release notes" for full details.
+
 ## Process
 
 1. Run `script/release_checklist.py {version}` to check the current status
 2. **CRITICAL: If preliminary lean4 checks fail, STOP immediately and alert the user**
-   - Check for: release branch exists, CMake version correct, tag exists, release page exists, release notes exist
+   - Check for: release branch exists, CMake version correct, tag exists, release page exists, release notes file exists
    - **IMPORTANT**: The release page is created AUTOMATICALLY by CI after pushing the tag - DO NOT create it manually
+   - **IMPORTANT**: For -rc1 releases, release notes must be created before proceeding
    - Do NOT create any PRs or proceed with repository updates if these checks fail
 3. Create a todo list tracking all repositories that need updates
 4. **CRITICAL RULE: You can ONLY run `release_steps.py` for a repository if `release_checklist.py` explicitly says to do so**

doc/dev/release_checklist.md

@@ -218,6 +218,11 @@ Please read https://leanprover-community.github.io/contribute/tags_and_branches.
 
 # Writing the release notes
 
+Release notes are only needed for the first release candidate (`-rc1`). For subsequent RCs and stable releases,
+just update the version number in the title of the existing release notes file.
+
+## Generating the release notes
+
 Release notes are automatically generated from the commit history, using `script/release_notes.py`.
 
 Run this as `script/release_notes.py --since v4.6.0`, where `v4.6.0` is the *previous* release version.
@@ -232,4 +237,93 @@ Some judgement is required here: ignore commits which look minor,
 but manually add items to the release notes for significant PRs that were rebase-merged.
 
 There can also be pre-written entries in `./releases_drafts`, which should be all incorporated in the release notes and then deleted from the branch.
+
+## Reviewing and fixing the generated markdown
+
+Before adding the release notes to the reference manual, carefully review the generated markdown for these common issues:
+
+1. **Unterminated code blocks**: PR descriptions sometimes have unclosed code fences. Look for code blocks
+   that don't have a closing ` ``` `. If found, fetch the original PR description with `gh pr view <number>`
+   and repair the code block with the complete content.
+
+2. **Truncated descriptions**: Some PR descriptions may end abruptly mid-sentence. Review these and complete
+   the descriptions based on the original PR.
+
+3. **Markdown syntax issues**: Check for other markdown problems that could cause parsing errors.
+
+## Creating the release notes file
+
+The release notes go in `Manual/Releases/v4_7_0.lean` in the reference-manual repository.
+
+The file structure must follow the Verso format:
+
+```lean
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: <Your Name>
+-/
+
+import VersoManual
+import Manual.Meta
+import Manual.Meta.Markdown
+
+open Manual
+open Verso.Genre
+open Verso.Genre.Manual
+open Verso.Genre.Manual.InlineLean
+
+#doc (Manual) "Lean 4.7.0-rc1 (YYYY-MM-DD)" =>
+%%%
+tag := "release-v4.7.0"
+file := "v4.7.0"
+%%%
+
+<release notes content here>
+```
+
+**Important formatting rules for Verso:**
+- Use `#` for section headers inside the document, not `##` (Verso uses header level 1 for subsections)
+- Use plain ` ``` ` for code blocks, not ` ```lean ` (the latter will cause Lean to execute the code)
+- Identifiers with underscores like `bv_decide` should be wrapped in backticks: `` `bv_decide` ``
+  (otherwise the underscore may be interpreted as markdown emphasis)
+
+## Updating Manual/Releases.lean
+
+After creating the release notes file, update `Manual/Releases.lean` to include it:
+
+1. Add the import near the top with other version imports:
+   ```lean
+   import Manual.Releases.«v4_7_0»
+   ```
+
+2. Add the include statement after the other includes:
+   ```lean
+   {include 0 Manual.Releases.«v4_7_0»}
+   ```
+
+## Building and verifying
+
+Build the release notes to check for errors:
+```bash
+lake build Manual.Releases.v4_7_0
+```
+
+Common errors and fixes:
+- "Wrong header nesting - got ## but expected at most #": Change `##` to `#`
+- "Tactic 'X' failed" or similar: Code is being executed; change ` ```lean ` to ` ``` `
+- "'_'" errors: Underscore in identifier being parsed as emphasis; wrap in backticks
+
+## Creating the PR
+
+Create a separate PR for the release notes (don't bundle with the toolchain bump PR):
+```bash
+git checkout -b v4.7.0-release-notes
+git add Manual/Releases/v4_7_0.lean Manual/Releases.lean
+git commit -m "doc: add v4.7.0 release notes"
+git push -u origin v4.7.0-release-notes
+gh pr create --title "doc: add v4.7.0 release notes" --body "This PR adds the release notes for Lean v4.7.0."
+```
+
+See `./releases_drafts/README.md` for more information about pre-written release note entries.
 See `./releases_drafts/README.md` for more information.

script/release_checklist.py

@@ -185,6 +185,30 @@ def get_release_notes(tag_name):
     except Exception:
         return None
 
+def check_release_notes_file_exists(toolchain, github_token):
+    """Check if the release notes file exists in the reference-manual repository.
+
+    For -rc1 releases, this checks that the release notes have been created.
+    For subsequent RCs and stable releases, release notes should already exist.
+
+    Returns tuple (exists: bool, is_rc1: bool) where is_rc1 indicates if this is
+    the first release candidate (when release notes need to be written).
+    """
+    # Determine the release notes file path
+    # e.g., v4.28.0-rc1 -> Manual/Releases/v4_28_0.lean
+    base_version = strip_rc_suffix(toolchain.lstrip('v'))  # "4.28.0"
+    file_name = f"v{base_version.replace('.', '_')}.lean"  # "v4_28_0.lean"
+    file_path = f"Manual/Releases/{file_name}"
+
+    is_rc1 = toolchain.endswith("-rc1")
+
+    repo_url = "https://github.com/leanprover/reference-manual"
+
+    # Check if the file exists on main branch
+    content = get_branch_content(repo_url, "main", file_path, github_token)
+
+    return (content is not None, is_rc1)
+
 def get_branch_content(repo_url, branch, file_path, github_token):
     api_url = repo_url.replace("https://github.com/", "https://api.github.com/repos/") + f"/contents/{file_path}?ref={branch}"
     headers = {'Authorization': f'token {github_token}'} if github_token else {}
@@ -714,6 +738,27 @@ def main():
     else:
         print(f"  ✅ Release notes page title looks good ('{actual_title}').")
 
+    # Check if release notes file exists in reference-manual repository
+    # For -rc1 releases, this is when release notes need to be written
+    # For subsequent RCs and stable releases, they should already exist
+    release_notes_exists, is_rc1 = check_release_notes_file_exists(toolchain, github_token)
+    base_version = strip_rc_suffix(toolchain.lstrip('v'))
+    release_notes_file = f"Manual/Releases/v{base_version.replace('.', '_')}.lean"
+
+    if not release_notes_exists:
+        if is_rc1:
+            print(f"  ❌ Release notes file not found: {release_notes_file}")
+            print(f"     This is an -rc1 release, so release notes need to be written.")
+            print(f"     Run `script/release_notes.py --since <previous_version>` to generate them.")
+            print(f"     See doc/dev/release_checklist.md section 'Writing the release notes' for details.")
+            lean4_success = False
+        else:
+            print(f"  ❌ Release notes file not found: {release_notes_file}")
+            print(f"     Release notes should have been created for -rc1. Check the reference-manual repository.")
+            lean4_success = False
+    else:
+        print(f"  ✅ Release notes file exists: {release_notes_file}")
+
     repo_status["lean4"] = lean4_success
 
     # If the release page doesn't exist, skip repository checks and master branch checks

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

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/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