fix: defeq condition for projections

src/Lean/Meta/ExprDefEq.lean

@@ -1641,7 +1641,7 @@ private def isDefEqOnFailure (t s : Expr) : MetaM Bool := do
     tryUnificationHints t s <||> tryUnificationHints s t
 
 private def isDefEqProj : Expr → Expr → MetaM Bool
-  | Expr.proj _ i t, Expr.proj _ j s => pure (i == j) <&&> Meta.isExprDefEqAux t s
+  | Expr.proj m i t, Expr.proj n j s => pure (i == j && m == n) <&&> Meta.isExprDefEqAux t s
   | Expr.proj structName 0 s, v => isDefEqSingleton structName s v
   | v, Expr.proj structName 0 s => isDefEqSingleton structName s v
   | _, _ => pure false
@@ -1769,6 +1769,14 @@ partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := withIncRecD
   checkMaxHeartbeats "isDefEq"
   whenUndefDo (isDefEqQuick t s) do
   whenUndefDo (isDefEqProofIrrel t s) do
+  /-
+    We also reduce projections here to prevent expensive defeq checks when unifying TC operations.
+    When unifying e.g. `@Neg.neg α (@Field.toNeg α inst1) =?= @Neg.neg α (@Field.toNeg α inst2)`,
+    we only want to unify negation (and not all other field operations as well).
+    Unifying the field instances slowed down unification: https://github.com/leanprover/lean4/issues/1986
+    We used to *not* reduce projections here, to support unifying `(?a).1 =?= (x, y).1`.
+    NOTE: this still seems to work because we don't eagerly unfold projection definitions to primitive projections.
+  -/
   let t' ← whnfCore t
   let s' ← whnfCore s
   if t != t' || s != s' then