diff --git a/tests/lean/indimpltarget.lean b/tests/lean/indimpltarget.lean
new file mode 100644
index 0000000000..3008fd14a1
--- /dev/null
+++ b/tests/lean/indimpltarget.lean
@@ -0,0 +1,30 @@
+namespace Ex1
+
+theorem elim_with_implicit_target (motive : Nat → Nat → Prop) (case1  : ∀ m n, motive m n) (n : Nat) {m : Nat} : motive m n := case1 _ _
+
+example (n m : Nat) : n ≤ m := by
+  induction n using elim_with_implicit_target
+  case case1 => sorry
+
+end Ex1
+
+namespace Ex2
+
+theorem elim_with_implicit_target (motive : Nat → Nat → Prop) (case1  : ∀ m n, motive m n) {n : Nat} (m : Nat) : motive m n := case1 _ _
+
+example (n m : Nat) : n ≤ m := by
+  induction m using elim_with_implicit_target
+  case case1 => sorry
+
+end Ex2
+
+namespace Ex3
+
+-- this one should work
+theorem elim_with_implicit_target (motive : (n : Nat) → Fin n → Prop) (case1  : ∀ m n, motive m n) {n : Nat} (m : Fin n) : motive n m := case1 _ _
+
+example (n : Nat) (m : Fin n) : n ≤ m := by
+  induction m using elim_with_implicit_target
+  case case1 => sorry
+
+end Ex3
diff --git a/tests/lean/indimpltarget.lean.expected.out b/tests/lean/indimpltarget.lean.expected.out
new file mode 100644
index 0000000000..797357e144
--- /dev/null
+++ b/tests/lean/indimpltarget.lean.expected.out
@@ -0,0 +1,5 @@
+indimpltarget.lean:6:2-6:45: error: failed to infer implicit target, it contains unresolved metavariables
+  ?m
+indimpltarget.lean:16:2-16:45: error: failed to infer implicit target, it contains unresolved metavariables
+  ?m
+indimpltarget.lean:26:0-26:7: warning: declaration uses 'sorry'