diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 8be94e99ebc8..14c0ae70d636 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Util.FindMVar
+import Lean.Util.CollectFVars
 import Lean.Parser.Term
 import Lean.Meta.KAbstract
 import Lean.Meta.Tactic.ElimInfo
@@ -711,6 +712,12 @@ structure Context where
   ```
   theorem Eq.subst' {α} {motive : α → Prop} {a b : α} (h : a = b) : motive a → motive b
   ```
+  For another example, the term `isEmptyElim (α := α)` is an underapplied eliminator, and it needs
+  argument `α` to be elaborated eagerly to create a type-correct motive.
+  ```
+  def isEmptyElim [IsEmpty α] {p : α → Sort _} (a : α) : p a := ...
+  example {α : Type _} [IsEmpty α] : id (α → False) := isEmptyElim (α := α)
+  ```
   -/
   extraArgsPos : Array Nat
 
@@ -724,8 +731,8 @@ structure State where
   namedArgs    : List NamedArg
   /-- User-provided arguments that still have to be processed. -/
   args         : List Arg
-  /-- Discriminants processed so far. -/
-  discrs       : Array Expr := #[]
+  /-- Discriminants (targets) processed so far. -/
+  discrs       : Array (Option Expr)
   /-- Instance implicit arguments collected so far. -/
   instMVars    : Array MVarId := #[]
   /-- Position of the next argument to be processed. We use it to decide whether the argument is the motive or a discriminant. -/
@@ -742,10 +749,7 @@ def mkMotive (discrs : Array Expr) (expectedType : Expr): MetaM Expr := do
     let motiveBody ← kabstract motive discr
     /- We use `transform (usedLetOnly := true)` to eliminate unnecessary let-expressions. -/
     let discrType ← transform (usedLetOnly := true) (← instantiateMVars (← inferType discr))
-    let motive := Lean.mkLambda (← mkFreshBinderName) BinderInfo.default discrType motiveBody
-    unless (← isTypeCorrect motive) do
-      throwError "failed to elaborate eliminator, motive is not type correct:{indentD motive}"
-    return motive
+    return Lean.mkLambda (← mkFreshBinderName) BinderInfo.default discrType motiveBody
 
 /-- If the eliminator is over-applied, we "revert" the extra arguments. -/
 def revertArgs (args : List Arg) (f : Expr) (expectedType : Expr) : TermElabM (Expr × Expr) :=
@@ -761,7 +765,7 @@ def revertArgs (args : List Arg) (f : Expr) (expectedType : Expr) : TermElabM (E
     return (mkApp f val, mkForall (← mkFreshBinderName) BinderInfo.default valType expectedTypeBody)
 
 /--
-Construct the resulting application after all discriminants have bee elaborated, and we have
+Construct the resulting application after all discriminants have been elaborated, and we have
 consumed as many given arguments as possible.
 -/
 def finalize : M Expr := do
@@ -769,29 +773,50 @@ def finalize : M Expr := do
     throwError "failed to elaborate eliminator, unused named arguments: {(← get).namedArgs.map (·.name)}"
   let some motive := (← get).motive?
     | throwError "failed to elaborate eliminator, insufficient number of arguments"
+  trace[Elab.app.elab_as_elim] "motive: {motive}"
   forallTelescope (← get).fType fun xs _ => do
+    trace[Elab.app.elab_as_elim] "xs: {xs}"
     let mut expectedType := (← read).expectedType
+    trace[Elab.app.elab_as_elim] "expectedType:{indentD expectedType}"
+    let throwInsufficient := do
+      throwError "failed to elaborate eliminator, insufficient number of arguments, expected type:{indentExpr expectedType}"
     let mut f := (← get).f
     if xs.size > 0 then
+      -- under-application, specialize the expected type using `xs`
       assert! (← get).args.isEmpty
-      try
-        expectedType ← instantiateForall expectedType xs
-      catch _ =>
-        throwError "failed to elaborate eliminator, insufficient number of arguments, expected type:{indentExpr expectedType}"
+      for x in xs do
+        let .forallE _ t b _ ← whnf expectedType | throwInsufficient
+        unless ← fullApproxDefEq <| isDefEq t (← inferType x) do
+          -- We can't assume that these binding domains were supposed to line up, so report insufficient arguments
+          throwInsufficient
+        expectedType := b.instantiate1 x
+      trace[Elab.app.elab_as_elim] "xs after specialization of expected type: {xs}"
     else
-      -- over-application, simulate `revert`
+      -- over-application, simulate `revert` while generalizing the values of these arguments in the expected type
       (f, expectedType) ← revertArgs (← get).args f expectedType
+      unless ← isTypeCorrect expectedType do
+        throwError "failed to elaborate eliminator, after generalizing over-applied arguments, expected type is type incorrect:{indentExpr expectedType}"
+    trace[Elab.app.elab_as_elim] "expectedType after processing:{indentD expectedType}"
     let result := mkAppN f xs
+    trace[Elab.app.elab_as_elim] "result:{indentD result}"
     let mut discrs := (← get).discrs
     let idx := (← get).idx
-    if (← get).discrs.size < (← read).elimInfo.targetsPos.size then
+    if discrs.any Option.isNone then
       for i in [idx:idx + xs.size], x in xs do
-        if (← read).elimInfo.targetsPos.contains i then
-          discrs := discrs.push x
-    let motiveVal ← mkMotive discrs expectedType
+        if let some tidx := (← read).elimInfo.targetsPos.indexOf? i then
+          discrs := discrs.set! tidx x
+    if let some idx := discrs.findIdx? Option.isNone then
+      -- This should not happen.
+      trace[Elab.app.elab_as_elim] "Internal error, missing target with index {idx}"
+      throwError "failed to elaborate eliminator, insufficient number of arguments"
+    trace[Elab.app.elab_as_elim] "discrs: {discrs.map Option.get!}"
+    let motiveVal ← mkMotive (discrs.map Option.get!) expectedType
+    unless (← isTypeCorrect motiveVal) do
+      throwError "failed to elaborate eliminator, motive is not type correct:{indentD motiveVal}"
     unless (← isDefEq motive motiveVal) do
       throwError "failed to elaborate eliminator, invalid motive{indentExpr motiveVal}"
     synthesizeAppInstMVars (← get).instMVars result
+    trace[Elab.app.elab_as_elim] "completed motive:{indentD motive}"
     let result ← mkLambdaFVars xs (← instantiateMVars result)
     return result
 
@@ -819,9 +844,9 @@ def getNextArg? (binderName : Name) (binderInfo : BinderInfo) : M (LOption Arg)
 def setMotive (motive : Expr) : M Unit :=
   modify fun s => { s with motive? := motive }
 
-/-- Push the given expression into the `discrs` field in the state. -/
-def addDiscr (discr : Expr) : M Unit :=
-  modify fun s => { s with discrs := s.discrs.push discr }
+/-- Push the given expression into the `discrs` field in the state, where `i` is which target it is for. -/
+def addDiscr (i : Nat) (discr : Expr) : M Unit :=
+  modify fun s => { s with discrs := s.discrs.set! i discr }
 
 /-- Elaborate the given argument with the given expected type. -/
 private def elabArg (arg : Arg) (argExpectedType : Expr) : M Expr := do
@@ -856,11 +881,11 @@ partial def main : M Expr := do
     let motive ← mkImplicitArg binderType binderInfo
     setMotive motive
     addArgAndContinue motive
-  else if (← read).elimInfo.targetsPos.contains idx then
+  else if let some tidx := (← read).elimInfo.targetsPos.indexOf? idx then
     match (← getNextArg? binderName binderInfo) with
-    | .some arg => let discr ← elabArg arg binderType; addDiscr discr; addArgAndContinue discr
+    | .some arg => let discr ← elabArg arg binderType; addDiscr tidx discr; addArgAndContinue discr
     | .undef => finalize
-    | .none => let discr ← mkImplicitArg binderType binderInfo; addDiscr discr; addArgAndContinue discr
+    | .none => let discr ← mkImplicitArg binderType binderInfo; addDiscr tidx discr; addArgAndContinue discr
   else match (← getNextArg? binderName binderInfo) with
     | .some (.stx stx) =>
       if (← read).extraArgsPos.contains idx then
@@ -922,10 +947,12 @@ def elabAppArgs (f : Expr) (namedArgs : Array NamedArg) (args : Array Arg)
     let expectedType ← instantiateMVars expectedType
     if expectedType.getAppFn.isMVar then throwError "failed to elaborate eliminator, expected type is not available"
     let extraArgsPos ← getElabAsElimExtraArgsPos elimInfo
+    trace[Elab.app.elab_as_elim] "extraArgsPos: {extraArgsPos}"
     ElabElim.main.run { elimInfo, expectedType, extraArgsPos } |>.run' {
       f, fType
       args := args.toList
       namedArgs := namedArgs.toList
+      discrs := mkArray elimInfo.targetsPos.size none
     }
   else
     ElabAppArgs.main.run { explicit, ellipsis, resultIsOutParamSupport } |>.run' {
@@ -955,19 +982,29 @@ where
 
   /--
   Collect extra argument positions that must be elaborated eagerly when using `elab_as_elim`.
-  The idea is that the contribute to motive inference. See comment at `ElamElim.Context.extraArgsPos`.
+  The idea is that they contribute to motive inference. See comment at `ElamElim.Context.extraArgsPos`.
   -/
   getElabAsElimExtraArgsPos (elimInfo : ElimInfo) : MetaM (Array Nat) := do
     forallTelescope elimInfo.elimType fun xs type => do
-      let resultArgs := type.getAppArgs
+      let targets := type.getAppArgs
+      /- Compute transitive closure of fvars appearing in the motive and the targets. -/
+      let initMotiveFVars : CollectFVars.State := targets.foldl (init := {}) collectFVars
+      let motiveFVars ← xs.size.foldRevM (init := initMotiveFVars) fun i s => do
+        let x := xs[i]!
+        if elimInfo.motivePos == i || elimInfo.targetsPos.contains i || s.fvarSet.contains x.fvarId! then
+          return collectFVars s (← inferType x)
+        else
+          return s
+      /- Collect the extra argument positions -/
       let mut extraArgsPos := #[]
       for i in [:xs.size] do
         let x := xs[i]!
-        unless elimInfo.targetsPos.contains i do
-          let xType ← inferType x
+        unless elimInfo.motivePos == i || elimInfo.targetsPos.contains i do
+          let xType ← x.fvarId!.getType
           /- We only consider "first-order" types because we can reliably "extract" information from them. -/
-          if isFirstOrder xType
-             && Option.isSome (xType.find? fun e => e.isFVar && resultArgs.contains e) then
+          if motiveFVars.fvarSet.contains x.fvarId!
+             || (isFirstOrder xType
+                 && Option.isSome (xType.find? fun e => e.isFVar && motiveFVars.fvarSet.contains e.fvarId!)) then
             extraArgsPos := extraArgsPos.push i
       return extraArgsPos
 
@@ -1528,5 +1565,6 @@ builtin_initialize
   registerTraceClass `Elab.app.args (inherited := true)
   registerTraceClass `Elab.app.propagateExpectedType (inherited := true)
   registerTraceClass `Elab.app.finalize (inherited := true)
+  registerTraceClass `Elab.app.elab_as_elim (inherited := true)
 
 end Lean.Elab.Term
diff --git a/tests/lean/elabAsElim.lean b/tests/lean/elabAsElim.lean
deleted file mode 100644
index da254e3a58ff..000000000000
--- a/tests/lean/elabAsElim.lean
+++ /dev/null
@@ -1,98 +0,0 @@
-inductive Vec (α : Type u) : Nat → Type u
-  | nil : Vec α 0
-  | cons : α → Vec α n → Vec α (n+1)
-
-def f1 (xs : Vec α n) : Nat :=
-  Vec.casesOn xs 0 fun _ _ => 1
-
-def f2 (xs : Vec α n) : Nat :=
-  xs.casesOn 0 -- Error insufficient number of arguments
-
-def f3 (x : Nat) : Nat → (Nat → Nat) → Nat :=
-  x.casesOn
-
-def f4 (xs : List Nat) : xs ≠ [] → xs.length > 0 :=
-  xs.casesOn (by intros; contradiction) (by intros; simp_arith)
-
-def f5 (xs : List Nat) (h : xs ≠ []) : xs.length > 0 :=
-  xs.casesOn (by intros; contradiction) (by intros; simp_arith) h
-
-def f6 (x : Nat) :=
-  2 * x.casesOn 0 id
-
-example : f6 (x+1) = 2*x := rfl
-
-def f7 (xs : Vec α n) : Nat :=
-  xs.casesOn (a := 10) 0 -- Error unused named args
-
-def f8 (xs : List Nat) : xs ≠ [] → xs.length > 0 :=
-  @List.casesOn _ (fun xs => xs ≠ [] → xs.length > 0) xs (by dsimp; intros; contradiction) (by dsimp; intros; simp_arith)
-
-def f5' (xs : List Nat) (h : xs ≠ []) : xs.length > 0 :=
-  xs.casesOn (fun h => absurd rfl h) (fun _ _ _ => Nat.zero_lt_succ ..) h
-
-example (h₁ : a = b) (h₂ : b = c) : a = c :=
-  Eq.rec h₂ h₁.symm
-
-@[elab_as_elim] theorem subst {p : (b : α) → a = b → Prop} (h₁ : a = b) (h₂ : p a rfl) : p b h₁ := by
-  cases h₁
-  assumption
-
-example (h₁ : a = b) (h₂ : b = c) : a = c :=
-  subst h₁.symm h₂
-
-theorem not_or_not : (¬p ∨ ¬q) → ¬(p ∧ q) := λ h ⟨hp, hq⟩ =>
-  h.rec (λ h1 => h1 hp) (λ h2 => h2 hq)
-
-structure Point where
-  x : Nat
-
-theorem PointExt_lean4 (p : Point) : forall (q : Point) (h1 : Point.x p = Point.x q), p = q :=
-  Point.recOn p <|
-   fun z1 q => Point.recOn q $
-   fun z2 (hA : Point.x (Point.mk z1) = Point.x (Point.mk z2)) => congrArg Point.mk hA
-
-inductive pos_num : Type
-  | one  : pos_num
-  | bit1 : pos_num → pos_num
-  | bit0 : pos_num → pos_num
-
-inductive num : Type
-  | zero  : num
-  | pos   : pos_num → num
-
-inductive znum : Type
-  | zero : znum
-  | pos  : pos_num → znum
-  | neg  : pos_num → znum
-
-def pos_num.pred' : pos_num → num
-  | one    => .zero
-  | bit0 n => num.pos (num.casesOn (pred' n) one bit1)
-  | bit1 n => num.pos (bit0 n)
-
-protected def znum.bit1 : znum → znum
-  | zero    => pos .one
-  | pos n => pos (pos_num.bit1 n)
-  | neg n => neg (num.casesOn (pos_num.pred' n) .one pos_num.bit1)
-
-example (h : False) : a = c :=
-  h.rec
-
-example (h : False) : a = c :=
-  h.elim
-
-noncomputable def f : Nat → Nat :=
-  Nat.rec 0 (fun x _ => x)
-
-example : ∀ x, x ≥ 0 :=
-  Nat.rec (Nat.le_refl 0) (fun _ ih => Nat.le_succ_of_le ih)
-
-@[elab_as_elim]
-def Foo.induction {P : (α : Type) → Prop} (α : Type) : P α := sorry
-
-example {n : Type} {T : n} : T = T := Foo.induction n -- motive is not type correct
-
-example {n : Type} : {T : n} → T = T := Foo.induction n -- motive is not type correct
-
-example {n : Type} : {T : n} → T = T := @(Foo.induction n)
diff --git a/tests/lean/elabAsElim.lean.expected.out b/tests/lean/elabAsElim.lean.expected.out
deleted file mode 100644
index 07450ee1193e..000000000000
--- a/tests/lean/elabAsElim.lean.expected.out
+++ /dev/null
@@ -1,8 +0,0 @@
-elabAsElim.lean:9:2-9:14: error: failed to elaborate eliminator, insufficient number of arguments, expected type:
-  Nat
-elabAsElim.lean:26:2-26:24: error: failed to elaborate eliminator, unused named arguments: [a]
-elabAsElim.lean:92:4-92:17: warning: declaration uses 'sorry'
-elabAsElim.lean:94:38-94:53: error: failed to elaborate eliminator, motive is not type correct:
-  fun x => T = T
-elabAsElim.lean:96:40-96:55: error: failed to elaborate eliminator, motive is not type correct:
-  fun x => T✝ = T✝
diff --git a/tests/lean/run/elabAsElim.lean b/tests/lean/run/elabAsElim.lean
new file mode 100644
index 000000000000..b76607fcf5d1
--- /dev/null
+++ b/tests/lean/run/elabAsElim.lean
@@ -0,0 +1,177 @@
+/-!
+# Tests of elabAsElim elaborator and the `elab_as_elim` attribute
+-/
+
+-- For debugging:
+-- set_option trace.Elab.app.elab_as_elim true
+
+inductive Vec (α : Type u) : Nat → Type u
+  | nil : Vec α 0
+  | cons : α → Vec α n → Vec α (n+1)
+
+def f1 (xs : Vec α n) : Nat :=
+  Vec.casesOn xs 0 fun _ _ => 1
+
+/-! Under-applied eliminator, and expected type isn't a pi type. -/
+/--
+error: failed to elaborate eliminator, insufficient number of arguments, expected type:
+  Nat
+-/
+#guard_msgs in
+def f2 (xs : Vec α n) : Nat :=
+  xs.casesOn 0
+
+def f3 (x : Nat) : Nat → (Nat → Nat) → Nat :=
+  x.casesOn
+
+/-! Under-applied eliminator, expected type's binders do not unify with remaining arguments. -/
+/--
+error: failed to elaborate eliminator, insufficient number of arguments, expected type:
+  (Nat → Nat) → Nat → Nat
+-/
+#guard_msgs in
+def f3' (x : Nat) : (Nat → Nat) → Nat → Nat :=
+  x.casesOn
+
+def f4 (xs : List Nat) : xs ≠ [] → xs.length > 0 :=
+  xs.casesOn (by intros; contradiction) (by intros; simp_arith)
+
+def f5 (xs : List Nat) (h : xs ≠ []) : xs.length > 0 :=
+  xs.casesOn (by intros; contradiction) (by intros; simp_arith) h
+
+def f6 (x : Nat) :=
+  2 * x.casesOn 0 id
+
+example : f6 (x+1) = 2*x := rfl
+
+/-- error: failed to elaborate eliminator, unused named arguments: [a] -/
+#guard_msgs in
+def f7 (xs : Vec α n) : Nat :=
+  xs.casesOn (a := 10) 0
+
+def f8 (xs : List Nat) : xs ≠ [] → xs.length > 0 :=
+  @List.casesOn _ (fun xs => xs ≠ [] → xs.length > 0) xs (by dsimp; intros; contradiction) (by dsimp; intros; simp_arith)
+
+def f5' (xs : List Nat) (h : xs ≠ []) : xs.length > 0 :=
+  xs.casesOn (fun h => absurd rfl h) (fun _ _ _ => Nat.zero_lt_succ ..) h
+
+example (h₁ : a = b) (h₂ : b = c) : a = c :=
+  Eq.rec h₂ h₁.symm
+
+@[elab_as_elim] theorem subst {p : (b : α) → a = b → Prop} (h₁ : a = b) (h₂ : p a rfl) : p b h₁ := by
+  cases h₁
+  assumption
+
+example (h₁ : a = b) (h₂ : b = c) : a = c :=
+  subst h₁.symm h₂
+
+theorem not_or_not : (¬p ∨ ¬q) → ¬(p ∧ q) := λ h ⟨hp, hq⟩ =>
+  h.rec (λ h1 => h1 hp) (λ h2 => h2 hq)
+
+structure Point where
+  x : Nat
+
+theorem PointExt_lean4 (p : Point) : forall (q : Point) (h1 : Point.x p = Point.x q), p = q :=
+  Point.recOn p <|
+   fun z1 q => Point.recOn q $
+   fun z2 (hA : Point.x (Point.mk z1) = Point.x (Point.mk z2)) => congrArg Point.mk hA
+
+inductive pos_num : Type
+  | one  : pos_num
+  | bit1 : pos_num → pos_num
+  | bit0 : pos_num → pos_num
+
+inductive num : Type
+  | zero  : num
+  | pos   : pos_num → num
+
+inductive znum : Type
+  | zero : znum
+  | pos  : pos_num → znum
+  | neg  : pos_num → znum
+
+def pos_num.pred' : pos_num → num
+  | one    => .zero
+  | bit0 n => num.pos (num.casesOn (pred' n) one bit1)
+  | bit1 n => num.pos (bit0 n)
+
+protected def znum.bit1 : znum → znum
+  | zero    => pos .one
+  | pos n => pos (pos_num.bit1 n)
+  | neg n => neg (num.casesOn (pos_num.pred' n) .one pos_num.bit1)
+
+example (h : False) : a = c :=
+  h.rec
+
+example (h : False) : a = c :=
+  h.elim
+
+noncomputable def f : Nat → Nat :=
+  Nat.rec 0 (fun x _ => x)
+
+example : ∀ x, x ≥ 0 :=
+  Nat.rec (Nat.le_refl 0) (fun _ ih => Nat.le_succ_of_le ih)
+
+/-!
+Tests of `@[elab_as_elim]` when the motive is not type correct.
+-/
+
+@[elab_as_elim]
+def Foo.induction {P : (α : Type) → Prop} (α : Type) : P α := sorry
+
+/--
+error: failed to elaborate eliminator, motive is not type correct:
+  fun x => T = T
+-/
+#guard_msgs in
+example {n : Type} {T : n} : T = T := Foo.induction n
+
+/--
+error: failed to elaborate eliminator, motive is not type correct:
+  fun x => T✝ = T✝
+-/
+#guard_msgs in
+example {n : Type} : {T : n} → T = T := Foo.induction n
+
+example {n : Type} : (T : n) → T = T := Foo.induction n
+
+-- Disable implicit lambda
+example {n : Type} : {T : n} → T = T := @(Foo.induction n)
+
+/-!
+A "motive is not type correct" regression test.
+The `isEmptyElim` was failing due to being under-applied and the named `(α := α)` argument
+having postponed elaboration. This fix is that `α` now elaborates eagerly.
+-/
+
+class IsEmpty (α : Sort u) : Prop where
+  protected false : α → False
+
+@[elab_as_elim]
+def isEmptyElim [IsEmpty α] {p : α → Sort _} (a : α) : p a :=
+  (IsEmpty.false a).elim
+
+def Set (α : Type u) := α → Prop
+def Set.univ {α : Type _} : Set α := fun _ => True
+instance : Membership α (Set α) := ⟨fun x s => s x⟩
+def Set.pi {α : ι → Type _} (s : Set ι) (t : (i : ι) → Set (α i)) : Set ((i : ι) → α i) := fun f => ∀ i ∈ s, f i ∈ t i
+
+example {α : Type u} [IsEmpty α] {β : α → Type v} (x : (a : α) → β a) (s : (i : α) → Set (β i)) :
+    x ∈ Set.univ.pi s := isEmptyElim (α := α)
+
+-- Simplified version:
+example {α : Type _} [IsEmpty α] :
+  id (α → False) := isEmptyElim (α := α)
+
+/-!
+From mathlib, regression test. Need to eagerly elaborate the `n ≤ m` argument to deduce `m`
+before computing the motive.
+-/
+
+@[elab_as_elim]
+def leRecOn {C : Nat → Sort _} {n : Nat} : ∀ {m}, n ≤ m → (∀ {k}, C k → C (k + 1)) → C n → C m :=
+  sorry
+
+theorem leRecOn_self {C : Nat → Sort _} {n} {next : ∀ {k}, C k → C (k + 1)} (x : C n) :
+    (leRecOn n.le_refl next x : C n) = x :=
+  sorry