From 3481f43130125ebbae42d49582c6096aeb842e76 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Thu, 15 May 2025 18:09:20 +0200
Subject: [PATCH] fix: FunInd: strip MData when creating the unfolding theorem
 (#8354)

This PR makes sure that when generating the unfolding functional
induction theorem, `mdata` does not get in the way.
---
 src/Lean/Meta/Tactic/FunInd.lean     |  9 +++++++--
 tests/lean/run/funind_unfolding.lean | 15 ++-------------
 tests/lean/run/grind_congrArg.lean   | 18 ------------------
 3 files changed, 9 insertions(+), 33 deletions(-)
 delete mode 100644 tests/lean/run/grind_congrArg.lean

diff --git a/src/Lean/Meta/Tactic/FunInd.lean b/src/Lean/Meta/Tactic/FunInd.lean
index 0ba795ab81..2a48b82b02 100644
--- a/src/Lean/Meta/Tactic/FunInd.lean
+++ b/src/Lean/Meta/Tactic/FunInd.lean
@@ -641,6 +641,9 @@ def rwLetWith (h : Expr) (e : Expr) : MetaM Simp.Result := do
       return { expr := e.letBody!.instantiate1 h }
   return { expr := e }
 
+def rwMData (e : Expr) : MetaM Simp.Result := do
+  return { expr := e.consumeMData }
+
 def rwHaveWith (h : Expr) (e : Expr) : MetaM Simp.Result := do
   if let some (_n, t, _v, b) := e.letFun? then
     if (← isDefEq t (← inferType h)) then
@@ -674,11 +677,12 @@ def rwMatcher (altIdx : Nat) (e : Expr) : MetaM Simp.Result := do
     return { expr := e }
   else
     unless (← isMatcherApp e) do
+      trace[Meta.FunInd] "Not a matcher application:{indentExpr e}"
       return { expr := e }
     let matcherDeclName := e.getAppFn.constName!
     let eqns ← Match.genMatchCongrEqns matcherDeclName
     unless altIdx < eqns.size do
-      trace[Tactic.FunInd] "When trying to reduce arm {altIdx}, only {eqns.size} equations for {.ofConstName matcherDeclName}"
+      trace[Meta.FunInd] "When trying to reduce arm {altIdx}, only {eqns.size} equations for {.ofConstName matcherDeclName}"
       return { expr := e }
     let eqnThm := eqns[altIdx]!
     try
@@ -865,7 +869,8 @@ partial def buildInductionBody (toErase toClear : Array FVarId) (goal : Expr)
 
   -- we look through mdata
   if e.isMData then
-    let b ← buildInductionBody toErase toClear goal oldIH newIH isRecCall e.mdataExpr!
+    let b ← withRewrittenMotiveArg goal (rwMData) fun goal' =>
+      buildInductionBody toErase toClear goal' oldIH newIH isRecCall e.mdataExpr!
     return e.updateMData! b
 
   if let .letE n t v b _ := e then
diff --git a/tests/lean/run/funind_unfolding.lean b/tests/lean/run/funind_unfolding.lean
index 0a35764e46..07acf2ee45 100644
--- a/tests/lean/run/funind_unfolding.lean
+++ b/tests/lean/run/funind_unfolding.lean
@@ -572,19 +572,8 @@ info: binaryWithMatch.induct_unfolding (motive : Nat → Nat → Nat → Prop)
   (case1 :
     ∀ (a b : Nat),
       decide (a < b) = true →
-        motive (a - 1) (b - 1) (binaryWithMatch (a - 1) (b - 1)) →
-          motive a b
-            (match h : decide (a < b) with
-            | true => 1 + binaryWithMatch (a - 1) (b - 1)
-            | false => 0))
-  (case2 :
-    ∀ (a b : Nat),
-      decide (a < b) = false →
-        motive a b
-          (match h : decide (a < b) with
-          | true => 1 + binaryWithMatch (a - 1) (b - 1)
-          | false => 0))
-  (a b : Nat) : motive a b (binaryWithMatch a b)
+        motive (a - 1) (b - 1) (binaryWithMatch (a - 1) (b - 1)) → motive a b (1 + binaryWithMatch (a - 1) (b - 1)))
+  (case2 : ∀ (a b : Nat), decide (a < b) = false → motive a b 0) (a b : Nat) : motive a b (binaryWithMatch a b)
 -/
 #guard_msgs in
 #check binaryWithMatch.induct_unfolding
diff --git a/tests/lean/run/grind_congrArg.lean b/tests/lean/run/grind_congrArg.lean
deleted file mode 100644
index 4f0ed54cba..0000000000
--- a/tests/lean/run/grind_congrArg.lean
+++ /dev/null
@@ -1,18 +0,0 @@
-set_option grind.warning false
-
-namespace Array
-
-private theorem getElem_qpartition_snd_of_hi_lt {n} (lt : α → α → Bool) (as : Vector α n) (lo hi : Nat)
-    (hlo : lo < n) (hhi : hi < n) (w : lo ≤ hi)
-    (k : Nat) (h : hi < k) (h' : k < n) : (qpartition as lt lo hi hlo hhi).2[k] = as[k] := sorry
-
-@[local grind] private theorem getElem_qsort_sort_of_hi_lt
-    {n} (lt : α → α → Bool) (as : Vector α n) (lo hi : Nat)
-    (hlo : lo < n) (hhi : hi < n) (w : lo ≤ hi)
-    (i : Nat) (h : hi < i) (h' : i < n) : (qsort.sort lt as lo hi hlo hhi)[i] = as[i] := by
-  fun_induction qsort.sort
-  case case1 a b =>
-    unfold qsort.sort
-    grind [getElem_qpartition_snd_of_hi_lt]
-  case case2 a b ih1 ih2 ih3 => sorry
-  case case3 => sorry