diff --git a/src/Lean/Meta/Injective.lean b/src/Lean/Meta/Injective.lean
index c1d1aaa82f..95e4dad4b7 100644
--- a/src/Lean/Meta/Injective.lean
+++ b/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
diff --git a/tests/lean/run/elimOptParam.lean b/tests/lean/run/elimOptParam.lean
new file mode 100644
index 0000000000..b0a99ae657
--- /dev/null
+++ b/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)