fix: induction MetaM tactic

The major premise may be a let-declaration.

closes #983

src/Lean/Meta/Tactic/Induction.lean

@@ -196,7 +196,11 @@ def induction (mvarId : MVarId) (majorFVarId : FVarId) (recursorName : Name) (gi
             let recursor ← addRecParams mvarId majorTypeArgs recursorInfo.paramsPos recursor
             -- Compute motive
             let motive := target
-            let motive ← if recursorInfo.depElim then mkLambdaFVars #[major] motive else pure motive
+            let motive ←
+              if recursorInfo.depElim then
+                pure <| mkLambda `x BinderInfo.default (← inferType major) (← abstract motive #[major])
+              else
+                pure motive
             let motive ← mkLambdaFVars indices motive
             let recursor := mkApp recursor motive
             finalize mvarId givenNames recursorInfo reverted major indices baseSubst recursor

tests/lean/run/983.lean

@@ -0,0 +1,29 @@
+import Lean
+
+-- The `cases` tactic does not use `Lean.Meta.cases` under the hood,
+-- so it is unaffected by this issue. We define a tactic
+-- `mcases` that delegates to `Lean.Meta.cases`.
+syntax (name := mcases) "mcases" ident : tactic
+
+namespace Lean.Elab.Tactic
+
+@[tactic mcases]
+def evalMcases : Tactic
+| `(tactic| mcases $hyp) => do
+  let hyp ← getFVarId hyp
+  liftMetaTactic fun goal => do
+    let goals ← Lean.Meta.cases goal hyp
+    return goals.map (·.mvarId) |>.toList
+| _ => unreachable!
+
+end Lean.Elab.Tactic
+
+example : True := by
+  let h : ∃ n, n = 0 := ⟨0, rfl⟩
+  mcases h
+  sorry -- sorry
+
+example : True := by
+  have h : ∃ n, n = 0 := ⟨0, rfl⟩
+  mcases h
+  apply True.intro