perf: cache for isDefEqI in Sym

This PR caches `isDefEqI` results in `Sym`. During symbolic
computation (e.g., VC generators), we find the same instances over and over again.

Performance numbers before/after fr the benchmark
`tests/bench/mvcgen/sym/vcgen_deep_add_sub_cancel.lean`.

| Benchmark | Before (ms) | After (ms) | Speedup |
|-----------|------------|------------|---------|
| goal_100  | 192.1      | 134.1      | 30%     |
| goal_200  | 325.6      | 225.4      | 31%     |
| goal_300  | 490.2      | 333.5      | 32%     |
| goal_400  | 655.6      | 441.9      | 33%     |
| goal_500  | 861.9      | 553.1      | 36%     |
| goal_600  | 1060.6     | 664.5      | 37%     |
| goal_700  | 1166.8     | 818.7      | 30%     |
| goal_800  | 1393.3     | 919.0      | 34%     |
| goal_900  | 1524.2     | 1025.0     | 33%     |
| goal_1000 | 1663.1     | 1141.9     | 31%     |

The time does not include the kernel type checking time. The
optimization does not affect it.

src/Lean/Meta/Sym/SymM.lean

@@ -131,6 +131,8 @@ structure State where
   -/
   getLevel : PHashMap ExprPtr Level := {}
   congrInfo : PHashMap ExprPtr CongrInfo := {}
+  /-- Cache for `isDefEqI` results -/
+  defEqI : PHashMap (ExprPtr × ExprPtr) Bool := {}
   debug : Bool := false
 
 abbrev SymM := ReaderT Context <| StateRefT State MetaM
@@ -219,4 +221,13 @@ abbrev share (e : Expr) : SymM Expr :=
 @[inline] def isDebugEnabled : SymM Bool :=
   return (← get).debug
 
+/-- Similar to `Meta.isDefEqI`, but the result is cache using pointer equality. -/
+def isDefEqI (s t : Expr) : SymM Bool := do
+  let key := (⟨s⟩, ⟨t⟩)
+  if let some result := (← get).defEqI.find? key then
+    return result
+  let result ← Meta.isDefEqI s t
+  modify fun s => { s with defEqI := s.defEqI.insert key result }
+  return result
+
 end Lean.Meta.Sym