fix: .yesWithDeltaI behavior (#3816)

It should not increase the transparency level from `reducible` to
`instances`. See new test.

src/Lean/Meta/Basic.lean

@@ -1444,6 +1444,12 @@ def whnfD (e : Expr) : MetaM Expr :=
 def whnfI (e : Expr) : MetaM Expr :=
   withTransparency TransparencyMode.instances <| whnf e
 
+/-- `whnf` with at most instances transparency. -/
+def whnfAtMostI (e : Expr) : MetaM Expr := do
+  match (← getTransparency) with
+  | .all | .default => withTransparency TransparencyMode.instances <| whnf e
+  | _ => whnf e
+
 /--
   Mark declaration `declName` with the attribute `[inline]`.
   This method does not check whether the given declaration is a definition.

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 `whnfI` is used to reduce the projection structure.
+    Note that ew use `proj := .yesWithDeltaI` to ensure `whnfAtMostI` 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 `whnfI` is used at `s` during the process.
-  Recall that `whnfI` is like `whnf` but uses transparency `instances`.
+  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`.
   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,7 +625,8 @@ where
         | .no => return e
         | .yes => k (← go c)
         | .yesWithDelta => k (← whnf c)
-        | .yesWithDeltaI => k (← whnfI c)
+        -- Remark: If the current transparency setting is `reducible`, we should not increase it to `instances`
+        | .yesWithDeltaI => k (← whnfAtMostI c)
       | _ => unreachable!
 
 /--

tests/lean/run/simp_proj_transparency_issue.lean

@@ -0,0 +1,19 @@
+structure Foo where
+  x : Nat
+  y : Nat := 10
+
+@[instance]
+def f (x : Nat) : Foo :=
+  { x := x + x }
+
+@[instance]
+def g (x : Nat) : Foo :=
+  { x := x + x }
+
+opaque q : Nat → Prop
+
+example (h : q (f x).1) : q (g x).1 := by
+  -- Projections must not bump transparency setting from `reducible` to `instances`
+  -- Thus, the following tactic must fail
+  fail_if_success simp [h]
+  assumption