fix: checkTargets check for duplicate target (#3171)

The `checkTargets` function introduced in 4a0f8bf2 as
```
  checkTargets (targets : Array Expr) : MetaM Unit := do
    let mut foundFVars : FVarIdSet := {}
    for target in targets do
      unless target.isFVar do
        throwError "index in target's type is not a variable (consider using the `cases` tactic instead){indentExpr target}"
      if foundFVars.contains target.fvarId! then
        throwError "target (or one of its indices) occurs more than once{indentExpr target}"
```
looks like it tries to check for duplicate indices, but it doesn’t
actually, as `foundFVars` is never written to.

This adds
```
      foundFVars := foundFVars.insert target.fvarId!
```
and a test case.

Maybe a linter that warns about `let mut` that are never writen to would
be useful?

src/Lean/Elab/Tactic/Induction.lean

@@ -571,6 +571,7 @@ where
         throwError "index in target's type is not a variable (consider using the `cases` tactic instead){indentExpr target}"
       if foundFVars.contains target.fvarId! then
         throwError "target (or one of its indices) occurs more than once{indentExpr target}"
+      foundFVars := foundFVars.insert target.fvarId!
 
 def elabCasesTargets (targets : Array Syntax) : TacticM (Array Expr × Array (Ident × FVarId)) :=
   withMainContext do

tests/lean/inductionGen.lean

@@ -66,3 +66,13 @@ theorem ex3 (a b : Expr α) (h : a = b) : eval (constProp a) = eval b := by
   induction a
   trace_state -- b's type must have been refined, `h` too
   repeat admit
+
+inductive Foo : Nat → Nat → Type where
+  | mk : Foo 1 2
+
+theorem ex4 (n m : Nat) (heq : n = m) (h : Foo n m) : False := by
+  induction h using Foo.rec
+  case mk => contradiction
+
+theorem ex5 (n : Nat) (h : Foo n n) : False := by
+  induction h using Foo.rec -- error, target repeated

tests/lean/inductionGen.lean.expected.out

@@ -41,3 +41,5 @@ a_ih✝ : ∀ (b : Expr ExprType.nat), a✝ = b → eval (constProp a✝) = eval
 b : Expr ExprType.nat
 h : Expr.add a✝¹ a✝ = b
 ⊢ eval (constProp (Expr.add a✝¹ a✝)) = eval b
+inductionGen.lean:78:2-78:27: error: target (or one of its indices) occurs more than once
+  n