From 008537abbd486f87aec2e1d4d4e6915e12a276f1 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Thu, 31 Oct 2024 19:04:36 +0100
Subject: [PATCH] fix: FunInd: unfold aux definitions more carefully (#5904)

fixes #5903
---
 src/Lean/Meta/Tactic/FunInd.lean | 10 +++++++---
 tests/lean/run/issue5903.lean    | 10 ++++++++++
 2 files changed, 17 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/run/issue5903.lean

diff --git a/src/Lean/Meta/Tactic/FunInd.lean b/src/Lean/Meta/Tactic/FunInd.lean
index 73e794381c14..b71b55c2d0c0 100644
--- a/src/Lean/Meta/Tactic/FunInd.lean
+++ b/src/Lean/Meta/Tactic/FunInd.lean
@@ -257,6 +257,7 @@ fails.
 partial def foldAndCollect (oldIH newIH : FVarId) (isRecCall : Expr → Option Expr) (e : Expr) : M Expr := do
   unless e.containsFVar oldIH do
     return e
+  withTraceNode `Meta.FunInd (pure m!"{exceptEmoji ·} foldAndCollect:{indentExpr e}") do
 
   let e' ← id do
     if let some (n, t, v, b) := e.letFun? then
@@ -319,10 +320,10 @@ partial def foldAndCollect (oldIH newIH : FVarId) (isRecCall : Expr → Option E
     if e.getAppArgs.any (·.isFVarOf oldIH) then
       -- Sometimes Fix.lean abstracts over oldIH in a proof definition.
       -- So beta-reduce that definition. We need to look through theorems here!
-      let e' ← withTransparency .all do whnf e
-      if e == e' then
+      if let some e' ← withTransparency .all do unfoldDefinition? e then
+        return ← foldAndCollect oldIH newIH isRecCall e'
+      else
         throwError "foldAndCollect: cannot reduce application of {e.getAppFn} in:{indentExpr e} "
-      return ← foldAndCollect oldIH newIH isRecCall e'
 
     match e with
     | .app e1 e2 =>
@@ -462,6 +463,7 @@ def M2.branch {α} (act : M2 α) : M2 α :=
 /-- Base case of `buildInductionBody`: Construct a case for the final induction hypthesis.  -/
 def buildInductionCase (oldIH newIH : FVarId) (isRecCall : Expr → Option Expr) (toClear : Array FVarId)
     (goal : Expr)  (e : Expr) : M2 Expr := do
+  withTraceNode `Meta.FunInd (pure m!"{exceptEmoji ·} buildInductionCase:{indentExpr e}") do
   let _e' ← foldAndCollect oldIH newIH isRecCall e
   let IHs : Array Expr ← M.ask
   let IHs ← deduplicateIHs IHs
@@ -518,6 +520,8 @@ as `MVars` as it goes.
 -/
 partial def buildInductionBody (toClear : Array FVarId) (goal : Expr)
     (oldIH newIH : FVarId) (isRecCall : Expr → Option Expr) (e : Expr) : M2 Expr := do
+  withTraceNode `Meta.FunInd
+    (pure m!"{exceptEmoji ·} buildInductionBody: {oldIH.name} → {newIH.name}:{indentExpr e}") do
 
   -- if-then-else cause case split:
   match_expr e with
diff --git a/tests/lean/run/issue5903.lean b/tests/lean/run/issue5903.lean
new file mode 100644
index 000000000000..4e8514876032
--- /dev/null
+++ b/tests/lean/run/issue5903.lean
@@ -0,0 +1,10 @@
+def foo (n : Nat) (_h : True) : Nat :=
+  n
+
+def bar : Nat → { _n : Nat // True }
+  | 0 => ⟨0, trivial⟩
+  | n + 1 =>
+      let r := bar n
+      ⟨foo r.1 r.2, trivial⟩
+
+def bar_induct := @bar.induct