fix: bug at elimOptParam (#3595)

`let_expr` uses `cleanupAnnotations` which consumes `optParam` type
annotations.

cc @nomeata

src/Lean/Meta/Injective.lean

@@ -26,8 +26,10 @@ private def mkAnd? (args : Array Expr) : Option Expr := Id.run do
 
 def elimOptParam (type : Expr) : CoreM Expr := do
   Core.transform type fun e =>
-    let_expr optParam _ a := e | return .continue
-    return TransformStep.visit a
+    if e.isAppOfArity ``optParam 2 then
+      return TransformStep.visit (e.getArg! 0)
+    else
+      return .continue
 
 private partial def mkInjectiveTheoremTypeCore? (ctorVal : ConstructorVal) (useEq : Bool) : MetaM (Option Expr) := do
   let us := ctorVal.levelParams.map mkLevelParam

tests/lean/run/elimOptParam.lean

@@ -0,0 +1,14 @@
+import Lean
+
+def f (x := 0) (y := 1) : Nat :=
+  x + y
+
+open Lean Meta
+
+/--
+info: Nat → Nat → Nat
+-/
+#guard_msgs in
+run_meta do
+  let info ← getConstInfo ``f
+  logInfo (← elimOptParam info.type)