diff --git a/src/Init/Lean/Elab/App.lean b/src/Init/Lean/Elab/App.lean
index a31baa4f67..6e3b287193 100644
--- a/src/Init/Lean/Elab/App.lean
+++ b/src/Init/Lean/Elab/App.lean
@@ -98,9 +98,6 @@ structure ElabAppArgsCtx :=
 (typeMVars     : Array MVarId := #[]) -- metavariables for implicit arguments of the form `{α : Sort u}` that have already been processed
 (foundExplicit : Bool := false)       -- true if an explicit argument has already been processed
 
-private def isAutoOrOptParam (type : Expr) : Bool :=
-type.getOptParamDefault?.isSome || type.getAutoParamTactic?.isSome
-
 /- Auxiliary function for retrieving the resulting type of a function application.
    See `propagateExpectedType`. -/
 private partial def getForallBody : Nat → Array NamedArg → Expr → Option Expr
@@ -112,7 +109,7 @@ private partial def getForallBody : Nat → Array NamedArg → Expr → Option E
       getForallBody i namedArgs b
     else if i > 0 then
       getForallBody (i-1) namedArgs b
-    else if isAutoOrOptParam d then
+    else if d.isAutoParam || d.isOptParam then
       getForallBody i namedArgs b
     else
       some type
diff --git a/src/Init/Lean/Expr.lean b/src/Init/Lean/Expr.lean
index d49d471354..a5ef75052b 100644
--- a/src/Init/Lean/Expr.lean
+++ b/src/Init/Lean/Expr.lean
@@ -739,6 +739,12 @@ if e.isAppOfArity `autoParam 2 then
 else
   none
 
+def isOptParam (e : Expr) : Bool :=
+e.isAppOfArity `optParam 2
+
+def isAutoParam (e : Expr) : Bool :=
+e.isAppOfArity `autoParam 2
+
 @[specialize] private partial def hasAnyFVarAux (p : FVarId → Bool) : Expr → Bool
 | e => if !e.hasFVar then false else
   match e with