test: tracing and test case for #5347 (#5348)

not a fix, unfortunately, just recording the test.

src/Lean/Meta/Tactic/FunInd.lean

@@ -438,9 +438,11 @@ def buildInductionCase (oldIH newIH : FVarId) (isRecCall : Expr → Option Expr)
   let mvar ← mkFreshExprSyntheticOpaqueMVar goal (tag := `hyp)
   let mut mvarId := mvar.mvarId!
   mvarId ← assertIHs IHs mvarId
+  trace[Meta.FunInd] "Goal before cleanup:{mvarId}"
   for fvarId in toClear do
     mvarId ← mvarId.clear fvarId
   mvarId ← mvarId.cleanup (toPreserve := toPreserve)
+  trace[Meta.FunInd] "Goal after cleanup (toClear := {toClear.map mkFVar}) (toPreserve := {toPreserve.map mkFVar}):{mvarId}"
   modify (·.push mvarId)
   let mvar ← instantiateMVars mvar
   pure mvar

tests/lean/run/issue5347.lean

@@ -0,0 +1,19 @@
+def f (x: Nat): Option Nat :=
+  if x > 10 then some 0 else none
+
+def test (x: Nat): Nat :=
+  match f x, x with
+  | some k, _ => k
+  | none, 0 => 0
+  | none, n + 1 => test n
+
+-- set_option trace.Meta.FunInd true
+
+-- At the time of writing, the induction princpile misses the `f x = some k` assumptions:
+
+/--
+info: test.induct (motive : Nat → Prop) (case1 : ∀ (x : Nat), motive x) (case2 : motive 0)
+  (case3 : ∀ (n : Nat), motive n → motive n.succ) (x : Nat) : motive x
+-/
+#guard_msgs in
+#check test.induct