fix: induction: do not register _ as binder in info tree

src/Lean/Elab/Tactic/Induction.lean

@@ -199,7 +199,7 @@ private def saveAltVarsInfo (altMVarId : MVarId) (altStx : Syntax) (fvarIds : Ar
     for fvarId in fvarIds do
       if !useNamesForExplicitOnly || (← getLocalDecl fvarId).binderInfo.isExplicit then
         if i < altVars.size then
-          Term.addLocalVarInfo altVars[i] (mkFVar fvarId)
+          Term.addTermInfo' (isBinder := altVars[i].isIdent) altVars[i] (mkFVar fvarId)
           i := i + 1
 
 /--

tests/lean/1196.lean

@@ -0,0 +1,9 @@
+inductive T: Type
+| mk: Nat -> T
+
+theorem T.zero_bad: T -> T
+:= by {
+  intro H;
+  induction H with
+  | mk _ => exact T.mk 0
+}