Merge branch 'master' into defeq_perf2

src/Lean/Meta/ExprDefEq.lean

@@ -1872,7 +1872,7 @@ partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := withIncRecD
     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
 
-    Note that ew use `proj := .yesWithDeltaI` to ensure `whnfAtMostI` is used to reduce the projection structure.
+    Note that ew use `proj := .yesWithDeltaI` to ensure `whnfI` is used to reduce the projection structure.
     We added this refinement to address a performance issue in code such as
     ```
     let val : Test := bar c1 key

src/Lean/Meta/WHNF.lean

@@ -343,8 +343,8 @@ inductive ProjReductionKind where
   -/
   | yesWithDelta
   /--
-  Projections `s.i` are reduced at `whnfCore`, and `whnfAtMostI` is used at `s` during the process.
-  Recall that `whnfAtMostII` is like `whnf` but uses transparency at most `instances`.
+  Projections `s.i` are reduced at `whnfCore`, and `whnfI` is used at `s` during the process.
+  Recall that `whnfI` is like `whnf` but uses transparency `instances`.
   This option is stronger than `yes`, but weaker than `yesWithDelta`.
   We use this option to ensure we reduce projections to prevent expensive defeq checks when unifying TC operations.
   When unifying e.g. `(@Field.toNeg α inst1).1 =?= (@Field.toNeg α inst2).1`,
@@ -625,8 +625,7 @@ where
         | .no => return e
         | .yes => k (← go c)
         | .yesWithDelta => k (← whnf c)
-        -- Remark: If the current transparency setting is `reducible`, we should not increase it to `instances`
-        | .yesWithDeltaI => k (← whnfAtMostI c)
+        | .yesWithDeltaI => k (← whnfI c)
       | _ => unreachable!
 
 /--