`Lean.Meta.Sym.Simp.toHave` reverses dependencies when reconstructing `have` telescopes

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Lean.Meta.Sym.Simp.toHave reverses dependencies when reconstructing have telescopes which, under the right circumstances, causes a kernel application type mismatch.

Context

When Lean.Meta.Sym.Simp.simpHave reconstructs a have telescope after simplification, it calls toHave. In toHave, dependencies are passed to Expr.betaRev in forward order (ys), but betaRev expects arguments in reversed order (revArgs).

As a result, any have binding whose value depends on two or more earlier bindings in the same telescope has its dependencies applied in reverse order, producing an ill-typed term that fails kernel type checking with an application type mismatch.

Steps to Reproduce

This self-contained reproduction requires no external dependencies or imports beyond Init:

def f (a : Nat) (b : Bool) : Nat := if b then a else 0

theorem test (y : Bool) :
    (have a := 1 + 1
     have b := y
     have c := f a b
     c = 0) := by
  sym =>
    simp
    sorry

Expected behavior: No error: (kernel) application type mismatch.

Actual behavior: We get the following error:

error: (kernel) application type mismatch
  f b
argument has type
  Bool
but function has type
  Nat → Bool → Nat

Versions

Tested on Lean 4.35.0-nightly-2026-08-17.

Additional Information

During simplification of have a := 1 + 1 to have a := 2, c := f a b is reconstructed as c := f b a. Because f has type Nat → Bool → Nat, b : Bool is passed where a : Nat is expected, causing the kernel to reject the proof term.

In Lean/Meta/Sym/Simp/Have.lean:255-258:

      let varPos := varDeps[i]
      let ys := varPos.map fun i => xs[i]!
      let type := consumeForallN t varPos.size
      let val ← share <| args[i].betaRev ys

1. varDeps[i] and ys are ordered forward (e.g. #[a, b]).
2. args[i] is fun a b => f a b.
3. args[i].betaRev #[a, b] reduces to f b a because betaRev treats its argument array as revArgs (i.e., args.reverse).

To fix this, one could pass ys.reverse to betaRev (or use betaS/beta I suppose):

-      let val ← share <| args[i].betaRev ys
+      let val ← share <| args[i].betaRev ys.reverse

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start in Lean/Meta/Sym/Simp/Have.lean at lines 255-258 and inspect how varDeps, ys, and betaRev order arguments during have-telescope reconstruction. Run the self-contained Init-only reproduction, then verify that simplification no longer produces the kernel application type mismatch.