diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 5b45bdeb1f..8537925cd8 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -155,7 +155,7 @@ private def addNewArg (argName : Name) (arg : Expr) : M Unit := do
   Recall that, `Arg` may be wrapping an already elaborated `Expr`. -/
 private def elabAndAddNewArg (argName : Name) (arg : Arg) : M Unit := do
   let s ← get
-  let expectedType ← getArgExpectedType
+  let expectedType := (← getArgExpectedType).consumeAutoOptParam
   match arg with
   | Arg.expr val =>
     let arg ← ensureArgType s.f val expectedType
@@ -386,7 +386,6 @@ mutual
         | Except.ok tacticSyntax =>
           -- TODO(Leo): does this work correctly for tactic sequences?
           let tacticBlock ← `(by $tacticSyntax)
-          let argType     := argType.getArg! 0 -- `autoParam type := by tactic` ==> `type`
           let argNew := Arg.stx tacticBlock
           propagateExpectedType argNew
           elabAndAddNewArg argName argNew