fix: wrapInstance: do not leak via un-reducible instances (#13441)

This PR ensures that if wrapInstance encounters an instance that cannot
be reduced to a constructor, the wrapping definition is left at
semireducible transparency to avoid leakage.

src/Lean/Meta/WrapInstance.lean

@@ -145,7 +145,6 @@ public partial def wrapInstance (inst expectedType : Expr) (compile : Bool := tr
           else
             let name ← mkAuxDeclName
             let wrapped ← mkAuxDefinition name expectedType inst (compile := false)
-            setReducibilityStatus name .implicitReducible
             if isMeta then modifyEnv (markMeta · name)
             if compile then
               compileDecls (logErrors := logCompileErrors) #[name]

tests/elab/inferInstanceAs.lean

@@ -46,7 +46,7 @@ instCD2._aux_1
 #guard_msgs in
 #print instCD2
 /--
-info: @[implicit_reducible] private def instCD2._aux_1 : C D2 :=
+info: private def instCD2._aux_1 : C D2 :=
 instCI2
 -/
 #guard_msgs in