diff --git a/src/Lean/Elab/PreDefinition/FixedParams.lean b/src/Lean/Elab/PreDefinition/FixedParams.lean
index f93c27e419..dc359df977 100644
--- a/src/Lean/Elab/PreDefinition/FixedParams.lean
+++ b/src/Lean/Elab/PreDefinition/FixedParams.lean
@@ -172,20 +172,19 @@ end FixedParams
 
 open Lean Meta FixedParams
 
-def getParamRevDeps (preDefs : Array PreDefinition) : MetaM (Array (Array (Array Nat))) := do
-  preDefs.mapM fun preDef =>
-    lambdaTelescope preDef.value (cleanupAnnotations := true) fun xs _ => do
-      let mut revDeps := #[]
-      for h : i in [:xs.size] do
-        let mut deps := #[]
-        for h : j in [i+1:xs.size] do
-          if (← dependsOn (← inferType xs[j]) xs[i].fvarId!) then
-            deps := deps.push j
-        revDeps := revDeps.push deps
-      pure revDeps
+def getParamRevDeps (value : Expr) : MetaM (Array (Array Nat)) := do
+  lambdaTelescope value (cleanupAnnotations := true) fun xs _ => do
+    let mut revDeps := #[]
+    for h : i in [:xs.size] do
+      let mut deps := #[]
+      for h : j in [i+1:xs.size] do
+        if (← dependsOn (← inferType xs[j]) xs[i].fvarId!) then
+          deps := deps.push j
+      revDeps := revDeps.push deps
+    pure revDeps
 
 def getFixedParamsInfo (preDefs : Array PreDefinition) : MetaM FixedParams.Info := do
-  let revDeps ← getParamRevDeps preDefs
+  let revDeps ← preDefs.mapM (getParamRevDeps ·.value)
   let arities := revDeps.map (·.size)
   let ref ← IO.mkRef (Info.init revDeps)
 
diff --git a/src/Lean/Meta/Tactic/FunInd.lean b/src/Lean/Meta/Tactic/FunInd.lean
index 2a48b82b02..9de97b7001 100644
--- a/src/Lean/Meta/Tactic/FunInd.lean
+++ b/src/Lean/Meta/Tactic/FunInd.lean
@@ -551,6 +551,32 @@ def maskArray {α} (mask : Array Bool) (xs : Array α) : Array α := Id.run do
     if b then ys := ys.push x
   return ys
 
+/--
+Inverse of `maskArray`:
+```
+zipMaskedArray mask (maskArray (mask.map not) xs) (maskArray mask xs) == xs
+```
+-/
+def zipMaskedArray {α} (mask : Array Bool) (xs ys : Array α) : Array α := Id.run do
+  let mut i := 0
+  let mut j := 0
+  let mut zs := #[]
+  for b in mask do
+    if b then
+      if h : j < ys.size then
+        zs := zs.push ys[j]
+        j := j + 1
+      else
+        panic! "zipMaskedArray: not enough elements in ys"
+    else
+      if h : i < xs.size then
+        zs := zs.push xs[i]
+        i := i + 1
+      else
+        panic! "zipMaskedArray: not enough elements in xs"
+  return zs
+
+
 /--
 Applies `rw` to `goal`, passes the rewritten `goal'` to `k` (which should return an expression of
 type `goal'`), and wraps that using the proof from `rw`.
@@ -1478,6 +1504,55 @@ where doRealize inductName := do
     }
 
 
+/--
+Given an expression `fun x y z => body`, returns a bit mask of the functinon's arity length
+that has `true` whenver that parameter of the function appears as a scrutinee of a `match` in
+tail position. These are the parameters that are likely useful as targets of the motive
+of the functional cases theorem. All others become parameters or may be dropped.
+
+-/
+partial def refinedArguments (e : Expr) : MetaM (Array Bool) := do
+  let (_, mask) ← lambdaTelescope e fun xs body =>
+    let mask0 := Array.replicate xs.size false
+    go xs body |>.run mask0
+  let mut mask := mask
+  let revDeps ← getParamRevDeps e
+  assert! revDeps.size = mask.size
+  for i in [:mask.size] do
+    if mask[i]! then
+      for j in revDeps[i]! do
+          mask := mask.set! j true
+  pure mask
+where
+  -- NB: we process open terms here.
+  go (xs : Array Expr) (e : Expr) : StateT (Array Bool) MetaM Unit := do
+    let e := e.consumeMData
+
+    if e.isLambda then
+      -- Not strictly tail position, but simplifies the code below and should not make
+      -- a difference in practice
+      go xs e.bindingBody!
+    else if e.isLet then
+      go xs e.letBody!
+    else
+      e.withApp fun f args => do
+        if f.isConst then
+          if let some matchInfo ← getMatcherInfo? f.constName! then
+            for scrut in args[matchInfo.getFirstDiscrPos:matchInfo.getFirstAltPos] do
+              if let some i := xs.idxOf? scrut then
+                modify (·.set! i true)
+            for alt in args[matchInfo.getFirstAltPos:matchInfo.arity] do
+              go xs alt
+        if f.isConstOf ``letFun then
+          for arg in args[3:4] do
+            go xs arg
+        if f.isConstOf ``ite || f.isConstOf ``dite then
+          for arg in args[3:5] do
+            go xs arg
+        if f.isConstOf ``cond then
+          for arg in args[2:4] do
+            go xs arg
+
 /--
 For non-recursive (and recursive functions) functions we derive a “functional case splitting theorem”. This is very similar
 than the functional induction theorem. It splits the goal, but does not give you inductive hyptheses.
@@ -1503,34 +1578,44 @@ def deriveCases (unfolding : Bool) (name : Name) : MetaM Unit := do
         let some (_, _, rhs) := body.eq?
           | throwError "Type of {unfoldEqnName} not an equality: {body}"
         mkLambdaFVars xs rhs
-    let motiveType ← lambdaTelescope value fun xs _body => do
-      if unfolding then
-        withLocalDeclD `r (← instantiateForall info.type xs) fun r =>
-          mkForallFVars (xs.push r) (.sort 0)
-      else
-        mkForallFVars xs (.sort 0)
-    let motiveArity ← lambdaTelescope value fun xs _body => do
-      pure xs.size
-    let e' ← withLocalDeclD `motive motiveType fun motive => do
-      lambdaTelescope value fun xs body => do
-        let (e', mvars) ← M2.run do
-          let goal := mkAppN motive xs
-          let goal ← if unfolding then
-            pure <| mkApp goal (mkAppN (← mkConstWithLevelParams name) xs)
-          else
-            pure goal
-          withRewrittenMotiveArg goal (rwFun #[name]) fun goal => do
-            -- We bring an unused FVars into scope to pass as `oldIH` and `newIH`. These do not appear anywhere
-            -- so `buildInductionBody` should just do the right thing
-            withLocalDeclD `fakeIH (mkConst ``Unit) fun fakeIH =>
-              let isRecCall := fun _ => none
-              buildInductionBody #[fakeIH.fvarId!] #[] goal fakeIH.fvarId! fakeIH.fvarId! isRecCall body
-        let e' ← mkLambdaFVars xs e'
-        let e' ← abstractIndependentMVars mvars (← motive.fvarId!.getDecl).index e'
-        mkLambdaFVars #[motive] e'
+    let targetMask ← refinedArguments value
+    trace[Meta.FunInd] "targetMask: {targetMask}"
 
-    unless (← isTypeCorrect e') do
-      logError m!"constructed functional cases principle is not type correct:{indentExpr e'}"
+    let (paramsMask, e') ← lambdaTelescope value fun xs _ => do
+      let params := maskArray (targetMask.map not) xs
+      let targets := maskArray targetMask xs
+      let motiveType ←
+        if unfolding then
+          withLocalDeclD `r (← instantiateForall info.type xs) fun r =>
+            mkForallFVars (targets.push r) (.sort 0)
+        else
+          mkForallFVars targets (.sort 0)
+      -- Remove targets from local context, we want to bring them into scope after the motive
+      -- so that the index passed to `abstractIndependentMVars` works.
+      withErasedFVars (targets.map (·.fvarId!)) do
+        withLocalDeclD `motive motiveType fun motive => do
+          -- Bring targets freshly into scope again
+          forallBoundedTelescope motiveType targets.size fun targets _ => do
+            let (e', mvars) ← M2.run do
+              let args := zipMaskedArray targetMask params targets
+              let body := value.beta args
+              let goal := mkAppN motive targets
+              let goal ← if unfolding then
+                pure <| mkApp goal (mkAppN (← mkConstWithLevelParams name) args)
+              else
+                pure goal
+              withRewrittenMotiveArg goal (rwFun #[name]) fun goal => do
+                -- We bring an unused FVars into scope to pass as `oldIH` and `newIH`. These do not appear anywhere
+                -- so `buildInductionBody` should just do the right thing
+                withLocalDeclD `fakeIH (mkConst ``Unit) fun fakeIH =>
+                  let isRecCall := fun _ => none
+                  buildInductionBody #[fakeIH.fvarId!] #[] goal fakeIH.fvarId! fakeIH.fvarId! isRecCall body
+            let e' ← mkLambdaFVars targets e'
+            let e' ← abstractIndependentMVars mvars (← motive.fvarId!.getDecl).index e'
+            let e' ← mkLambdaFVars #[motive] e'
+            mkLambdaFVarsMasked params e'
+
+    mapError (f := (m!"constructed functional cases principle is not type correct:{indentExpr e'}\n{indentD ·}")) do
       check e'
 
     let eTyp ← inferType e'
@@ -1545,11 +1630,25 @@ def deriveCases (unfolding : Bool) (name : Name) : MetaM Unit := do
     addDecl <| Declaration.thmDecl
       { name := casesName, levelParams := us, type := eTyp, value := e' }
 
+    -- Calculate paramsKind from targetMask (length = arity) and paramsMask (length = params)
+    let mut paramKinds := #[]
+    let mut j := 0
+    for isTarget in targetMask do
+      if isTarget then
+        paramKinds := paramKinds.push .target
+      else
+        assert! j < paramsMask.size
+        if paramsMask[j]! then
+          paramKinds := paramKinds.push .param
+        else
+          paramKinds := paramKinds.push .dropped
+        j := j + 1
+
     setFunIndInfo {
       funName := name
       funIndName := casesName
       levelMask := usMask
-      params := .replicate motiveArity .target
+      params := paramKinds
     }
 
 /--
diff --git a/src/Std/Data/DTreeMap/Internal/Balancing.lean b/src/Std/Data/DTreeMap/Internal/Balancing.lean
index d79e7ba716..ae7d24c8c9 100644
--- a/src/Std/Data/DTreeMap/Internal/Balancing.lean
+++ b/src/Std/Data/DTreeMap/Internal/Balancing.lean
@@ -529,7 +529,8 @@ attribute [Std.Internal.tree_tac] and_true true_and and_self heq_eq_eq inner.inj
 theorem balance!_eq_balanceₘ {k v} {l r : Impl α β} (hlb : l.Balanced) (hrb : r.Balanced)
     (hlr : BalanceLErasePrecond l.size r.size ∨ BalanceLErasePrecond r.size l.size) :
     balance! k v l r = balanceₘ k v l r := by
-  cases k, v, l, r using balance!.fun_cases
+  set_option tactic.fun_induction.unfolding false in
+  fun_cases balance!
   all_goals dsimp only [balance!, balanceₘ]
   · rfl
   · split <;> simp_all [Std.Internal.tree_tac]
@@ -582,15 +583,13 @@ theorem balance!_eq_balanceₘ {k v} {l r : Impl α β} (hlb : l.Balanced) (hrb
     simp only [Std.Internal.tree_tac, Nat.add_right_cancel_iff] at *
     omega
   · exfalso
-    rename_i ls rs h rls _ _ _ _ _ _ _ _ _ _
     simp only [balanced_inner_iff, size_inner, size_leaf, balancedAtRoot_zero_iff'] at hrb
-    simp only [delta] at h
+    simp only [delta] at ‹delta * _ < _›
     have := hlb.one_le
     omega
   · exfalso
-    rename_i ls rs h _ _ _ _ _ _ _
     simp only [balanced_inner_iff, size_inner, size_leaf, balancedAtRoot_zero_iff] at hrb
-    simp only [delta] at h
+    simp only [delta] at ‹delta * _ < _›
     have := hlb.one_le
     omega
   · repeat simp_all only [Std.Internal.tree_tac, rotateR, dite_true, ite_true, dite_false]
@@ -602,15 +601,13 @@ theorem balance!_eq_balanceₘ {k v} {l r : Impl α β} (hlb : l.Balanced) (hrb
     simp only [Std.Internal.tree_tac, Nat.reduceMul] at *
     omega
   · exfalso
-    rename_i ls rs h rls _ _ _ _ _ _ _ _ _ _
     simp only [balanced_inner_iff, size_inner, size_leaf, balancedAtRoot_zero_iff'] at hlb
-    simp only [delta] at h
+    simp only [delta] at ‹delta * _ < _›
     have := hrb.one_le
     omega
   · exfalso
-    rename_i ls rs h _ _ _ _ _ _ _
     simp only [balanced_inner_iff, size_inner, size_leaf, balancedAtRoot_zero_iff] at hlb
-    simp only [delta] at h
+    simp only [delta] at ‹delta * _ < _›
     have := hrb.one_le
     omega
   · repeat simp only [Std.Internal.tree_tac, dite_true, dite_false, *] at *
@@ -654,6 +651,7 @@ theorem balanced_rotateL (k v l rs rk rv rl rr) (hl : l.Balanced)
     (hlr : BalanceLErasePrecond l.size rs ∨ BalanceLErasePrecond rs l.size)
     (hh : rs > delta * l.size) :
     (rotateL k v l rk rv rl rr : Impl α β).Balanced := by
+  set_option tactic.fun_induction.unfolding false in
   fun_cases rotateL k v l rk rv rl rr <;> dsimp only [rotateL]
   · split
     · next h =>
@@ -668,6 +666,7 @@ theorem balanced_rotateR (k v ls lk lv ll lr r) (hl : (Impl.inner ls lk lv ll lr
     (hr : r.Balanced) (hlr : BalanceLErasePrecond ls r.size ∨ BalanceLErasePrecond r.size ls)
     (hh : ls > delta * r.size) :
     (rotateR k v lk lv ll lr r : Impl α β).Balanced := by
+  set_option tactic.fun_induction.unfolding false in
   fun_cases rotateR k v lk lv ll lr r <;> dsimp only [rotateR]
   · split
     · next h =>
@@ -680,6 +679,7 @@ theorem balanced_rotateR (k v ls lk lv ll lr r) (hl : (Impl.inner ls lk lv ll lr
 
 theorem balanceL_eq_balanceLErase {k : α} {v : β k} {l r : Impl α β} {hlb hrb hlr} :
     balanceL k v l r hlb hrb hlr = balanceLErase k v l r hlb hrb hlr.erase := by
+  set_option tactic.fun_induction.unfolding false in
   fun_cases balanceL k v l r hlb hrb hlr
   all_goals dsimp only [balanceL, balanceLErase]
   split
@@ -697,7 +697,7 @@ theorem balanceLErase_eq_balanceL! {k : α} {v : β k} {l r : Impl α β} {hlb h
 theorem balanceL!_eq_balance! {k : α} {v : β k} {l r : Impl α β} (hlb : l.Balanced)
     (hrb : r.Balanced) (hlr : BalanceLErasePrecond l.size r.size) :
     balanceL! k v l r = balance! k v l r := by
-  cases k, v, l, r using balance!.fun_cases
+  fun_cases balance!
   all_goals dsimp only [balanceL!, balance!]
   all_goals try simp only [*]
   all_goals try dsimp only [dreduceDIte, dreduceIte]
@@ -708,6 +708,7 @@ theorem balanceL!_eq_balance! {k : α} {v : β k} {l r : Impl α β} (hlb : l.Ba
 
 theorem balanceR_eq_balanceRErase {k : α} {v : β k} {l r : Impl α β} {hlb hrb hlr} :
     balanceR k v l r hlb hrb hlr = balanceRErase k v l r hlb hrb hlr.erase := by
+  set_option tactic.fun_induction.unfolding false in
   fun_cases balanceR k v l r hlb hrb hlr
   all_goals dsimp only [balanceR, balanceRErase]
   split
@@ -725,7 +726,7 @@ theorem balanceRErase_eq_balanceR! {k : α} {v : β k} {l r : Impl α β} {hlb h
 theorem balanceR!_eq_balance! {k : α} {v : β k} {l r : Impl α β} (hlb : l.Balanced)
     (hrb : r.Balanced) (hlr : BalanceLErasePrecond r.size l.size) :
     balanceR! k v l r = balance! k v l r := by
-  cases k, v, l, r using balance!.fun_cases
+  fun_cases balance! k v l r
   all_goals dsimp only [balanceR!, balance!]
   all_goals try simp only [*]
   all_goals try dsimp only [dreduceDIte, dreduceIte]
@@ -736,6 +737,7 @@ theorem balanceR!_eq_balance! {k : α} {v : β k} {l r : Impl α β} (hlb : l.Ba
 
 theorem balance_eq_balance! {k : α} {v : β k} {l r : Impl α β} {hlb hrb hlr} :
     balance k v l r hlb hrb hlr = balance! k v l r := by
+  set_option tactic.fun_induction.unfolding false in
   fun_cases balance! k v l r
   all_goals dsimp only [balance, balance!]
   all_goals simp only [*]
diff --git a/src/Std/Data/DTreeMap/Internal/Model.lean b/src/Std/Data/DTreeMap/Internal/Model.lean
index 72d65b687e..838d106e34 100644
--- a/src/Std/Data/DTreeMap/Internal/Model.lean
+++ b/src/Std/Data/DTreeMap/Internal/Model.lean
@@ -674,19 +674,20 @@ theorem containsThenInsertIfNew!_snd_eq_insertIfNew! [Ord α] (t : Impl α β) (
 
 theorem insertMin_eq_insertMin! [Ord α] {a b} {t : Impl α β} (htb) :
     (t.insertMin a b htb).impl = t.insertMin! a b := by
-  cases a, b, t using insertMin!.fun_cases
+  fun_cases insertMin!
   · rfl
   · simp only [insertMin!, insertMin, balanceL_eq_balanceL!, insertMin_eq_insertMin! htb.left]
 
 theorem insertMax_eq_insertMax! [Ord α] {a b} {t : Impl α β} (htb) :
     (t.insertMax a b htb).impl = t.insertMax! a b := by
-  cases a, b, t using insertMax!.fun_cases
+  fun_cases insertMax!
   · rfl
   · simp only [insertMax!, insertMax, balanceR_eq_balanceR!, insertMax_eq_insertMax! htb.right]
 
 theorem link_eq_link! [Ord α] {k v} {l r : Impl α β} (hlb hrb) :
     (link k v l r hlb hrb).impl = link! k v l r := by
-  cases k, v, l, r using link!.fun_cases <;> rw [link, link!]
+  set_option tactic.fun_induction.unfolding false in
+  fun_cases link! <;> rw [link, link!]
   · rw [insertMin_eq_insertMin!]
   · rw [insertMax_eq_insertMax!]
   · split <;> simp only [balanceLErase_eq_balanceL!, link_eq_link! hlb hrb.left]
@@ -699,7 +700,8 @@ termination_by sizeOf l + sizeOf r
 
 theorem link2_eq_link2! [Ord α] {l r : Impl α β} (hlb hrb) :
     (link2 l r hlb hrb).impl = link2! l r := by
-  cases l, r using link2!.fun_cases <;> rw [link2!, link2]
+  set_option tactic.fun_induction.unfolding false in
+  fun_cases link2! <;> rw [link2!, link2]
   · split <;> simp only [balanceLErase_eq_balanceL!, link2_eq_link2! hlb hrb.left]
   · split <;> simp only [balanceRErase_eq_balanceR!, balanceLErase_eq_balanceL!,
       link2_eq_link2! hlb.right hrb, link2_eq_link2! hlb hrb.left]
diff --git a/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean
index fbe360bf90..d96e586172 100644
--- a/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean
@@ -167,7 +167,7 @@ theorem toListModel_insertMax [Ord α] {k v} {t : Impl α β} {h} :
 @[simp]
 theorem toListModel_link [Ord α] {k v} {l r : Impl α β} {hl hr} :
     (l.link k v r hl hr).impl.toListModel = l.toListModel ++ ⟨k, v⟩ :: r.toListModel := by
-  cases k, v, l, r, hl, hr using link.fun_cases <;> simp [link] <;> split <;> (try simp; done)
+  fun_cases link <;> simp [link] <;> split <;> (try simp; done)
   all_goals
     simp only [toListModel_balanceLErase, toListModel_balanceRErase]
     rw [toListModel_link]
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index 79a0e58edd..f4d5f7ddae 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// please update stage0
+
 namespace lean {
 options get_default_options() {
     options opts;
diff --git a/tests/lean/run/fun_cases.lean b/tests/lean/run/fun_cases.lean
index 570265ccf8..1de0946b18 100644
--- a/tests/lean/run/fun_cases.lean
+++ b/tests/lean/run/fun_cases.lean
@@ -1,32 +1,26 @@
 /--
-info: Option.map.fun_cases.{u_1, u_2} (motive : {α : Type u_1} → {β : Type u_2} → (α → β) → Option α → Prop)
-  (case1 : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (x : α), motive f (some x))
-  (case2 : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), motive f none) {α : Type u_1} {β : Type u_2} (f : α → β)
-  (x✝ : Option α) : motive f x✝
+info: Option.map.fun_cases.{u_1} {α : Type u_1} (motive : Option α → Prop) (case1 : ∀ (x : α), motive (some x))
+  (case2 : motive none) (x✝ : Option α) : motive x✝
 -/
-#guard_msgs in
+#guard_msgs(pass trace, all) in
 #check Option.map.fun_cases
 
 example (x : Option Nat) (f : Nat → Nat) : (x.map f).isSome = x.isSome := by
-  cases f, x using Option.map.fun_cases
+  cases x using Option.map.fun_cases
   case case1 x => simp
   case case2 =>   simp
 
 /--
-info: List.map.fun_cases.{u, v} (motive : {α : Type u} → {β : Type v} → (α → β) → List α → Prop)
-  (case1 : ∀ {α : Type u} {β : Type v} (f : α → β), motive f [])
-  (case2 : ∀ {α : Type u} {β : Type v} (f : α → β) (a : α) (as : List α), motive f (a :: as)) {α : Type u} {β : Type v}
-  (f : α → β) (x✝ : List α) : motive f x✝
+info: List.map.fun_cases.{u} {α : Type u} (motive : List α → Prop) (case1 : motive [])
+  (case2 : ∀ (a : α) (as : List α), motive (a :: as)) (x✝ : List α) : motive x✝
 -/
 #guard_msgs in
 #check List.map.fun_cases
 
 /--
-info: List.find?.fun_cases.{u} (motive : {α : Type u} → (α → Bool) → List α → Prop)
-  (case1 : ∀ {α : Type u} (p : α → Bool), motive p [])
-  (case2 : ∀ {α : Type u} (p : α → Bool) (a : α) (as : List α), p a = true → motive p (a :: as))
-  (case3 : ∀ {α : Type u} (p : α → Bool) (a : α) (as : List α), p a = false → motive p (a :: as)) {α : Type u}
-  (p : α → Bool) (x✝ : List α) : motive p x✝
+info: List.find?.fun_cases.{u} {α : Type u} (p : α → Bool) (motive : List α → Prop) (case1 : motive [])
+  (case2 : ∀ (a : α) (as : List α), p a = true → motive (a :: as))
+  (case3 : ∀ (a : α) (as : List α), p a = false → motive (a :: as)) (x✝ : List α) : motive x✝
 -/
 #guard_msgs in
 #check List.find?.fun_cases
@@ -41,8 +35,8 @@ def areTheseTargetsUnchanged (x y : Nat) : Bool :=
     false
 
 /--
-info: areTheseTargetsUnchanged.fun_cases (motive : Nat → Nat → Prop) (case1 : ∀ (y : Nat), motive y y)
-  (case2 : ∀ (x y : Nat), ¬x = y → motive x y) (x y : Nat) : motive x y
+info: areTheseTargetsUnchanged.fun_cases (x y : Nat) (motive : Prop) (case1 : x = y → motive) (case2 : ¬x = y → motive) :
+  motive
 -/
 #guard_msgs in
 #check areTheseTargetsUnchanged.fun_cases
diff --git a/tests/lean/run/funind_unfolding.lean b/tests/lean/run/funind_unfolding.lean
index 07acf2ee45..c149c1c74a 100644
--- a/tests/lean/run/funind_unfolding.lean
+++ b/tests/lean/run/funind_unfolding.lean
@@ -54,18 +54,16 @@ def fib'' (n : Nat) : Nat :=
       0
 
 /--
-info: fib''.fun_cases_unfolding (motive : Nat → Nat → Prop) (case1 : ∀ (n : Nat), n < 2 → motive n n)
+info: fib''.fun_cases_unfolding (n : Nat) (motive : Nat → Prop) (case1 : n < 2 → motive n)
   (case2 :
-    ∀ (n : Nat),
-      ¬n < 2 →
-        let foo := n - 2;
-        foo < 100 → motive n (fib'' (n - 1) + fib'' foo))
+    ¬n < 2 →
+      let foo := n - 2;
+      foo < 100 → motive (fib'' (n - 1) + fib'' foo))
   (case3 :
-    ∀ (n : Nat),
-      ¬n < 2 →
-        let foo := n - 2;
-        ¬foo < 100 → motive n 0)
-  (n : Nat) : motive n (fib'' n)
+    ¬n < 2 →
+      let foo := n - 2;
+      ¬foo < 100 → motive 0) :
+  motive (fib'' n)
 -/
 #guard_msgs(pass trace, all) in
 #check fib''.fun_cases_unfolding
@@ -76,20 +74,18 @@ def filter (p : Nat → Bool) : List Nat → List Nat
   | x::xs => if p x then x::filter p xs else filter p xs
 
 /--
-info: filter.fun_cases (motive : (Nat → Bool) → List Nat → Prop) (case1 : ∀ (p : Nat → Bool), motive p [])
-  (case2 : ∀ (p : Nat → Bool) (x : Nat) (xs : List Nat), p x = true → motive p (x :: xs))
-  (case3 : ∀ (p : Nat → Bool) (x : Nat) (xs : List Nat), ¬p x = true → motive p (x :: xs)) (p : Nat → Bool)
-  (x✝ : List Nat) : motive p x✝
+info: filter.fun_cases (p : Nat → Bool) (motive : List Nat → Prop) (case1 : motive [])
+  (case2 : ∀ (x : Nat) (xs : List Nat), p x = true → motive (x :: xs))
+  (case3 : ∀ (x : Nat) (xs : List Nat), ¬p x = true → motive (x :: xs)) (x✝ : List Nat) : motive x✝
 -/
 #guard_msgs(pass trace, all) in
 #check filter.fun_cases
 
 /--
-info: filter.fun_cases_unfolding (motive : (Nat → Bool) → List Nat → List Nat → Prop)
-  (case1 : ∀ (p : Nat → Bool), motive p [] [])
-  (case2 : ∀ (p : Nat → Bool) (x : Nat) (xs : List Nat), p x = true → motive p (x :: xs) (x :: filter p xs))
-  (case3 : ∀ (p : Nat → Bool) (x : Nat) (xs : List Nat), ¬p x = true → motive p (x :: xs) (filter p xs))
-  (p : Nat → Bool) (x✝ : List Nat) : motive p x✝ (filter p x✝)
+info: filter.fun_cases_unfolding (p : Nat → Bool) (motive : List Nat → List Nat → Prop) (case1 : motive [] [])
+  (case2 : ∀ (x : Nat) (xs : List Nat), p x = true → motive (x :: xs) (x :: filter p xs))
+  (case3 : ∀ (x : Nat) (xs : List Nat), ¬p x = true → motive (x :: xs) (filter p xs)) (x✝ : List Nat) :
+  motive x✝ (filter p x✝)
 -/
 #guard_msgs(pass trace, all) in
 #check filter.fun_cases_unfolding
@@ -138,18 +134,15 @@ def map (f : Nat → Bool) : List Nat → List Bool
 termination_by x => x
 
 /--
-info: map.fun_cases (motive : (Nat → Bool) → List Nat → Prop) (case1 : ∀ (f : Nat → Bool), motive f [])
-  (case2 : ∀ (f : Nat → Bool) (x : Nat) (xs : List Nat), motive f (x :: xs)) (f : Nat → Bool) (x✝ : List Nat) :
-  motive f x✝
+info: map.fun_cases (motive : List Nat → Prop) (case1 : motive []) (case2 : ∀ (x : Nat) (xs : List Nat), motive (x :: xs))
+  (x✝ : List Nat) : motive x✝
 -/
 #guard_msgs(pass trace, all) in
 #check map.fun_cases
 
 /--
-info: map.fun_cases_unfolding (motive : (Nat → Bool) → List Nat → List Bool → Prop)
-  (case1 : ∀ (f : Nat → Bool), motive f [] [])
-  (case2 : ∀ (f : Nat → Bool) (x : Nat) (xs : List Nat), motive f (x :: xs) (f x :: map f xs)) (f : Nat → Bool)
-  (x✝ : List Nat) : motive f x✝ (map f x✝)
+info: map.fun_cases_unfolding (f : Nat → Bool) (motive : List Nat → List Bool → Prop) (case1 : motive [] [])
+  (case2 : ∀ (x : Nat) (xs : List Nat), motive (x :: xs) (f x :: map f xs)) (x✝ : List Nat) : motive x✝ (map f x✝)
 -/
 #guard_msgs(pass trace, all) in
 #check map.fun_cases_unfolding
@@ -435,8 +428,8 @@ info: withHave.induct_unfolding (motive : Nat → Bool → Prop) (case1 : 0 < 42
 #check withHave.induct_unfolding
 
 /--
-info: withHave.fun_cases_unfolding (motive : Nat → Bool → Prop) (case1 : 0 < 42 → motive 42 true)
-  (case2 : ∀ (n : Nat), 0 < n → ¬n = 42 → motive n (withHave (n - 1))) (n : Nat) : motive n (withHave n)
+info: withHave.fun_cases_unfolding (n : Nat) (motive : Bool → Prop) (case1 : 0 < n → n = 42 → motive true)
+  (case2 : 0 < n → ¬n = 42 → motive (withHave (n - 1))) : motive (withHave n)
 -/
 #guard_msgs(pass trace, all) in
 #check withHave.fun_cases_unfolding
diff --git a/tests/lean/run/issue8195.lean b/tests/lean/run/issue8195.lean
index 50162aff92..7d8be75315 100644
--- a/tests/lean/run/issue8195.lean
+++ b/tests/lean/run/issue8195.lean
@@ -99,8 +99,8 @@ def testMe (n : Nat) : Bool :=
   | m => false
 
 /--
-info: testMe.fun_cases_unfolding (motive : Nat → Bool → Prop) (case1 : ∀ (n : Nat), n - 2 = 0 → motive n true)
-  (case2 : ∀ (n : Nat), (n - 2 = 0 → False) → motive n false) (n : Nat) : motive n (testMe n)
+info: testMe.fun_cases_unfolding (n : Nat) (motive : Bool → Prop) (case1 : n - 2 = 0 → motive true)
+  (case2 : (n - 2 = 0 → False) → motive false) : motive (testMe n)
 -/
 #guard_msgs in
 #check testMe.fun_cases_unfolding
diff --git a/tests/lean/run/issue8213.lean b/tests/lean/run/issue8213.lean
index de42de10f7..325509928b 100644
--- a/tests/lean/run/issue8213.lean
+++ b/tests/lean/run/issue8213.lean
@@ -15,10 +15,10 @@ error: Failed to realize constant myTest.fun_cases:
   Cannot derive functional cases principle (please report this issue)
   ⏎
     failed to transform matcher, type error when constructing new pre-splitter motive:
-      @myTest.match_1 _fvar.28 (fun x => @_fvar.27 _fvar.28 _fvar.29 x _fvar.31 _fvar.32) _fvar.30
+      @myTest.match_1 _fvar.27 (fun x => @_fvar.32 x _fvar.34 _fvar.35) _fvar.33
     ⏎
       Application type mismatch: In the application
-        motive mmotive x✝ h_1
+        motive x✝ h_1
       the argument
         h_1
       has type
diff --git a/tests/lean/run/issue8293.lean b/tests/lean/run/issue8293.lean
index a17ca596fa..1219def87b 100644
--- a/tests/lean/run/issue8293.lean
+++ b/tests/lean/run/issue8293.lean
@@ -10,22 +10,22 @@ def test (f : Unit → MyVec α n) : Nat :=
   | .cons _ _ => 421
 
 /--
-info: test.fun_cases_unfolding.{u_1} (motive : {α : Type u_1} → {n : Nat} → (Unit → MyVec α n) → Nat → Prop)
+info: test.fun_cases_unfolding.{u_1} {α : Type u_1} (motive : {n : Nat} → (Unit → MyVec α n) → Nat → Prop)
   (case1 :
-    ∀ {α : Type u_1} (f : Unit → MyVec α 0),
+    ∀ (f : Unit → MyVec α 0),
       f () = MyVec.nil →
         motive f
           (match 0, f (), f with
           | .(0), MyVec.nil, f => 52
           | .(n + 1), MyVec.cons a a_1, f => 421))
   (case2 :
-    ∀ {α : Type u_1} (n : Nat) (a : α) (a_1 : MyVec α n) (f : Unit → MyVec α (n + 1)),
+    ∀ (n : Nat) (a : α) (a_1 : MyVec α n) (f : Unit → MyVec α (n + 1)),
       f () = MyVec.cons a a_1 →
         motive f
           (match n + 1, f (), f with
           | .(0), MyVec.nil, f => 52
           | .(n + 1), MyVec.cons a a_2, f => 421))
-  {α : Type u_1} {n : Nat} (f : Unit → MyVec α n) : motive f (test f)
+  {n : Nat} (f : Unit → MyVec α n) : motive f (test f)
 -/
 #guard_msgs(pass trace, all) in
 #check test.fun_cases_unfolding
@@ -36,22 +36,22 @@ def alsoTest (f : Unit → MyVec α n) : Nat :=
   | .cons _ _ => 421
 
 /--
-info: alsoTest.fun_cases_unfolding.{u_1} (motive : {α : Type u_1} → {n : Nat} → (Unit → MyVec α n) → Nat → Prop)
+info: alsoTest.fun_cases_unfolding.{u_1} {α : Type u_1} (motive : {n : Nat} → (Unit → MyVec α n) → Nat → Prop)
   (case1 :
-    ∀ {α : Type u_1} (f : Unit → MyVec α 0),
+    ∀ (f : Unit → MyVec α 0),
       f () = MyVec.nil →
         motive f
           (match h : 0, h : f (), f with
           | .(0), MyVec.nil, f_1 => 52
           | .(n + 1), MyVec.cons a a_1, f_1 => 421))
   (case2 :
-    ∀ {α : Type u_1} (n : Nat) (a : α) (a_1 : MyVec α n) (f : Unit → MyVec α (n + 1)),
+    ∀ (n : Nat) (a : α) (a_1 : MyVec α n) (f : Unit → MyVec α (n + 1)),
       f () = MyVec.cons a a_1 →
         motive f
           (match h : n + 1, h : f (), f with
           | .(0), MyVec.nil, f_1 => 52
           | .(n_1 + 1), MyVec.cons a a_2, f_1 => 421))
-  {α : Type u_1} {n : Nat} (f : Unit → MyVec α n) : motive f (alsoTest f)
+  {n : Nat} (f : Unit → MyVec α n) : motive f (alsoTest f)
 -/
 #guard_msgs(pass trace, all) in
 #check alsoTest.fun_cases_unfolding