fix: Sym.intro for have-declarations (#11851)

This PR fixes `Sym/Intro.lean` support for `have`-declarations.

src/Lean/Meta/Sym/Intro.lean

@@ -81,7 +81,12 @@ def introCore (goal : Goal) (max : Nat) (names : Array Name) : SymM (Array FVarI
       let type       ← instantiateRevS type fvars
       let value      ← instantiateRevS value fvars
       let fvarId     ← mkFreshFVarId
-      let lctx       := lctx.mkLetDecl fvarId (← mkName n i) type value nondep
+      /-
+      We have both dependent and non-dependent `let` expressions result in dependent `ldecl`s.
+      This is fine here since we never revert them in the Sym framework.
+      **Note**: If `type` is a proposition we could use a `cdecl`.
+      -/
+      let lctx       := lctx.mkLetDecl fvarId (← mkName n i) type value
       let fvar       ← Grind.mkFVarS fvarId
       let fvars      := fvars.push fvar
       let localInsts := updateLocalInsts localInsts fvar type

tests/lean/run/sym_intro.lean

@@ -19,11 +19,11 @@ trace: z✝² : Nat := 0
 x✝² y✝² : Nat
 z✝¹ : Nat := x✝² + y✝²
 y✝¹ : Nat := y✝² + 1
-this✝¹ : y✝¹ ≥ 0
+this✝¹ : y✝¹ ≥ 0 := Nat.zero_le y✝¹
 x✝¹ : Nat
 z✝ : Nat := x✝¹ + y✝¹
 y✝ : Nat := y✝¹ + 1
-this✝ : y✝ ≥ 0
+this✝ : y✝ ≥ 0 := Nat.zero_le y✝
 x✝ : Nat
 ⊢ True
 -/

tests/lean/run/sym_intro_have.lean

@@ -0,0 +1,29 @@
+import Lean.Meta.Tactic
+import Lean.Meta.Sym
+
+def f (x : Nat) :=
+  let y := x + 1
+  2*y
+
+open Lean Meta Sym
+/--
+info: x : Nat
+⊢ have y := x + 1;
+  x ≤ 2 * y
+---
+info: x : Nat
+y : Nat := x + 1
+⊢ x ≤ 2 * y
+-/
+#guard_msgs in
+run_meta SymM.run' do
+  withLocalDeclD `x Nat.mkType fun x => do
+  let m ← mkFreshExprMVar <| mkNatLE x (mkApp (mkConst ``f) x)
+  let mvarId := m.mvarId!
+  let mvarId ← unfoldTarget mvarId ``f
+  let mvarId ← mvarId.liftLets
+  let goal ← mkGoal mvarId
+  logInfo goal.mvarId
+  let (_, goal) ← intro goal `y
+  logInfo goal.mvarId
+  return ()