test: failed to infer implicit target (#3189)

The `induction` tactic complains if implicit targets cannot be inferred,
let’s test that.

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

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'