fix: let_fun support in grind (#6531)

This PR fixes the support for `let_fun` in `grind`.

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

@@ -49,7 +49,7 @@ private def introNext (goal : Goal) (generation : Nat) : GrindM IntroResult := d
             -- `p` and `p'` are definitionally equal
             goal.mvarId.assign h
             return .newHyp fvarId { goal with mvarId := mvarIdNew }
-  else if target.isLet || target.isForall then
+  else if target.isLet || target.isForall || target.isLetFun then
     let (fvarId, mvarId) ← goal.mvarId.intro1P
     mvarId.withContext do
       let localDecl ← fvarId.getDecl
@@ -59,8 +59,8 @@ private def introNext (goal : Goal) (generation : Nat) : GrindM IntroResult := d
         return .newDepHyp { goal with mvarId }
       else
         let goal := { goal with mvarId }
-        if target.isLet then
-          let v := target.letValue!
+        if target.isLet || target.isLetFun then
+          let v := (← fvarId.getDecl).value
           let r ← simp v
           let x ← shareCommon (mkFVar fvarId)
           let goal ← GoalM.run' goal <| addNewEq x r.expr (← r.getProof) generation

tests/lean/run/grind_t1.lean

@@ -112,5 +112,24 @@ example (foo : Nat → Nat)
 
 end dite_propagator_test
 
+/--
+info: [grind.eqc] x = 2 * a
+[grind.eqc] y = x
+[grind.eqc] (y = 2 * a) = False
+[grind.eqc] (y = 2 * a) = True
+-/
+#guard_msgs (info) in
+set_option trace.grind.eqc true in
 example (a : Nat) : let x := a + a; y = x → y = a + a := by
   grind
+
+/--
+info: [grind.eqc] x = 2 * a
+[grind.eqc] y = x
+[grind.eqc] (y = 2 * a) = False
+[grind.eqc] (y = 2 * a) = True
+-/
+#guard_msgs (info) in
+set_option trace.grind.eqc true in
+example (a : Nat) : let_fun x := a + a; y = x → y = a + a := by
+  grind