fix: improve `isDefEqProj` The new test `3965_2.lean` shows that `tryHeuristic` is also useful when solving contraints of the form `t.i =?= s.i`. For example, suppose we have `(f a).i =?= (f ?u).i`. By using `tryHeuristic`, we obtain the solution `?u := a` before unfolding `f`.
This is the repository for Lean 4.
See Setting Up Lean.
Please read our Contribution Guidelines first.
See Building Lean.