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.

Author: nomeata

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

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