fix: oversight in isReadOnlyOrSyntheticOpaque (#4206)

### Explanation
In the case that `assignSyntheticOpaque := true` and the given
metavariable is `syntheticOpaque` and the depth of the metavariable is
not the current depth, `isReadOnlyOrSyntheticOpaque` returns false, even
though the metavariable is read-only because of being declared at a
smaller depth. This causes the metavariable to (wrongly) be able to be
instantiated by `isDefEq`.

This bug was found at the proof of
[RingHom.PropertyIsLocal.sourceAffineLocally_of_source_openCover](https://leanprover-community.github.io/mathlib4_docs/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.html#RingHom.PropertyIsLocal.sourceAffineLocally_of_source_openCover),
which involves a type class synthesis for `CommRing ?m.2404`, and the
synthesis manages to instantiate this metavariable into different
values, even though `synthInstance?` increases the metavariable depth.
This synthesis fails after 1 second.

I found the bug while modifying the instance synthesis code: the
modified code spent several minutes on this failed synthesis.

### Test
The problem can be verified with the test:
```
run_meta do
  let m ← mkFreshExprMVar (Expr.sort levelOne) MetavarKind.syntheticOpaque
  withAssignableSyntheticOpaque do
  withNewMCtxDepth do
  let eq ← isDefEq m (.const ``Nat [])
  Lean.logInfo m! "{eq}"
```
this unification used to succeed, giving `true`, and this fix makes it
return `false`.

### Impact on Mathlib

This fix causes a change in the behaviour of `congr`, `convert` and
friends, which breaks a couple of proofs in mathlib. Most of these are
fixed by supplying more arguments.

I fixed these proofs, and
[benched](http://speed.lean-fro.org/mathlib4/compare/b821bfd9-3769-4930-b77f-0adc6f9d218f/to/e7b27246-a3e6-496a-b552-ff4b45c7236e?hash2=4f3c460cc1668820c9af8418a87a23db44c7acab)
mathlib. The result is that most files are unaffected, but some files
are significantly improved. This is most prominent in
Mathlib.RingTheory.Jacobson, where the number of instructions has
decreased by 28%. The overall improvement is a 0.3% reduction in
instructions.

[Zulip
message](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Ways.20to.20speed.20up.20Mathlib/near/439218960)

src/Lean/Meta/Basic.lean

@@ -720,15 +720,18 @@ def isReadOnlyExprMVar (mvarId : MVarId) : MetaM Bool := do
   mvarId.isReadOnly
 
 /--
-Return true if `mvarId.isReadOnly` return true or if `mvarId` is a synthetic opaque metavariable.
+Returns true if `mvarId.isReadOnly` returns true or if `mvarId` is a synthetic opaque metavariable.
 
 Recall `isDefEq` will not assign a value to `mvarId` if `mvarId.isReadOnlyOrSyntheticOpaque`.
 -/
 def _root_.Lean.MVarId.isReadOnlyOrSyntheticOpaque (mvarId : MVarId) : MetaM Bool := do
   let mvarDecl ← mvarId.getDecl
-  match mvarDecl.kind with
-  | MetavarKind.syntheticOpaque => return !(← getConfig).assignSyntheticOpaque
-  | _ => return mvarDecl.depth != (← getMCtx).depth
+  if mvarDecl.depth != (← getMCtx).depth then
+    return true
+  else
+    match mvarDecl.kind with
+    | MetavarKind.syntheticOpaque => return !(← getConfig).assignSyntheticOpaque
+    | _ => return false
 
 @[deprecated MVarId.isReadOnlyOrSyntheticOpaque (since := "2022-07-15")]
 def isReadOnlyOrSyntheticOpaqueExprMVar (mvarId : MVarId) : MetaM Bool := do

tests/lean/syntheticOpaqueReadOnly.lean

@@ -0,0 +1,12 @@
+import Lean
+
+open Lean Meta
+
+-- In a new MCtx depth, metavariables should not be assignable by `isDefEq`.
+
+run_meta do
+  let m ← mkFreshExprMVar (Expr.sort levelOne) MetavarKind.syntheticOpaque
+  withAssignableSyntheticOpaque do
+  withNewMCtxDepth do
+  let eq ← isDefEq m (.const ``Nat [])
+  Lean.logInfo m! "{eq}"

tests/lean/syntheticOpaqueReadOnly.lean.expected.out

@@ -0,0 +1 @@
+false