diff --git a/src/Lean/Meta/Match/MatcherApp/Transform.lean b/src/Lean/Meta/Match/MatcherApp/Transform.lean
index 93368b9abc..3c0995b5fe 100644
--- a/src/Lean/Meta/Match/MatcherApp/Transform.lean
+++ b/src/Lean/Meta/Match/MatcherApp/Transform.lean
@@ -222,7 +222,7 @@ def transform
     (addEqualities : Bool := false)
     (onParams : Expr → n Expr := pure)
     (onMotive : Array Expr → Expr → n Expr := fun _ e => pure e)
-    (onAlt : Expr → Expr → n Expr := fun _ e => pure e)
+    (onAlt : Nat → Expr → Expr → n Expr := fun _ _ e => pure e)
     (onRemaining : Array Expr → n (Array Expr) := pure) :
     n MatcherApp := do
 
@@ -294,12 +294,13 @@ def transform
     let aux2 := mkApp aux2 motive'
     let aux2 := mkAppN aux2 discrs'
     unless (← isTypeCorrect aux2) do
-      logError m!"failed to transform matcher, type error when constructing splitter motive:{indentExpr aux2}"
-      check aux2
+      mapError (f := (m!"failed to transform matcher, type error when constructing splitter motive:{indentExpr aux2}\n{indentD ·}")) do
+        check aux2
     let altTypes ← inferArgumentTypesN matcherApp.alts.size aux2
 
     let mut alts' := #[]
-    for alt in matcherApp.alts,
+    for altIdx in [:matcherApp.alts.size],
+        alt in matcherApp.alts,
         numParams in matcherApp.altNumParams,
         splitterNumParams in matchEqns.splitterAltNumParams,
         origAltType in origAltTypes,
@@ -313,7 +314,7 @@ def transform
             forallBoundedTelescope altType extraEqualities fun ys4 altType => do
               let alt ← try instantiateLambda alt (args ++ ys3)
                         catch _ => throwError "unexpected matcher application, insufficient number of parameters in alternative"
-              let alt' ← onAlt altType alt
+              let alt' ← onAlt altIdx altType alt
               mkLambdaFVars (ys ++ ys2 ++ ys3 ++ ys4) alt'
       alts' := alts'.push alt'
 
@@ -339,7 +340,8 @@ def transform
     let altTypes ← inferArgumentTypesN matcherApp.alts.size aux
 
     let mut alts' := #[]
-    for alt in matcherApp.alts,
+    for altIdx in [:matcherApp.alts.size],
+        alt in matcherApp.alts,
         numParams in matcherApp.altNumParams,
         altType in altTypes do
       let alt' ← forallBoundedTelescope altType numParams fun xs altType => do
@@ -348,7 +350,7 @@ def transform
           let names ← lambdaTelescope alt fun xs _ => xs.mapM (·.fvarId!.getUserName)
           withUserNames xs names do
             let alt ← instantiateLambda alt xs
-            let alt' ← onAlt altType alt
+            let alt' ← onAlt altIdx altType alt
             mkLambdaFVars (xs ++ ys4) alt'
       alts' := alts'.push alt'
 
@@ -422,7 +424,7 @@ def inferMatchType (matcherApp : MatcherApp) : MetaM MatcherApp := do
       }
       mkArrowN extraParams typeMatcherApp.toExpr
     )
-    (onAlt := fun expAltType alt => do
+    (onAlt := fun _altIdx expAltType alt => do
       let altType ← inferType alt
       let eq ← mkEq expAltType altType
       let proof ← mkFreshExprSyntheticOpaqueMVar eq
diff --git a/src/Lean/Meta/Tactic/FunInd.lean b/src/Lean/Meta/Tactic/FunInd.lean
index d90ee7f0f4..a3e46d3b60 100644
--- a/src/Lean/Meta/Tactic/FunInd.lean
+++ b/src/Lean/Meta/Tactic/FunInd.lean
@@ -203,8 +203,6 @@ something goes wrong, one still gets a useful induction principle, just maybe wi
 not fully simplified.
 -/
 
-set_option autoImplicit false
-
 namespace Lean.Tactic.FunInd
 
 open Lean Elab Meta
@@ -327,7 +325,7 @@ partial def foldAndCollect (oldIH newIH : FVarId) (isRecCall : Expr → Option E
             -- statement and the inferred alt types
             let dummyGoal := mkConst ``True []
             mkArrow eTypeAbst dummyGoal)
-          (onAlt := fun altType alt => do
+          (onAlt := fun _altIdx altType alt => do
             lambdaTelescope1 alt fun oldIH' alt => do
               forallBoundedTelescope altType (some 1) fun newIH' _goal' => do
                 let #[newIH'] := newIH' | unreachable!
@@ -345,7 +343,7 @@ partial def foldAndCollect (oldIH newIH : FVarId) (isRecCall : Expr → Option E
           (onMotive := fun _motiveArgs motiveBody => do
             let some (_extra, body) := motiveBody.arrow? | throwError "motive not an arrow"
             M.eval (foldAndCollect oldIH newIH isRecCall body))
-          (onAlt := fun altType alt => do
+          (onAlt := fun _altIdx altType alt => do
             lambdaTelescope1 alt fun oldIH' alt => do
             -- We don't have suitable newIH around here, but we don't care since
             -- we just want to fold calls. So lets create a fake one.
@@ -650,7 +648,7 @@ def rwFun (names : Array Name) (e : Expr) : MetaM Simp.Result := do
     else
       return { expr := e }
 
-def rwMatcher (e : Expr) : MetaM Simp.Result := do
+def rwMatcher (altIdx : Nat) (e : Expr) : MetaM Simp.Result := do
   if e.isAppOf ``PSum.casesOn || e.isAppOf ``PSigma.casesOn then
     let mut e := e
     while true do
@@ -664,10 +662,67 @@ def rwMatcher (e : Expr) : MetaM Simp.Result := do
           break
     return { expr := e }
   else
-    Split.simpMatch e
+    unless (← isMatcherApp e) do
+      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}"
+      return { expr := e }
+    let eqnThm := eqns[altIdx]!
+    try
+      withTraceNode `Meta.FunInd (pure m!"{exceptEmoji ·} rewriting with {.ofConstName eqnThm} in{indentExpr e}") do
+      let eqProof := mkAppN (mkConst eqnThm e.getAppFn.constLevels!) e.getAppArgs
+      let (hyps, _, eqType) ← forallMetaTelescope (← inferType eqProof)
+      trace[Meta.FunInd] "eqProof has type{indentExpr eqType}"
+      let proof := mkAppN eqProof hyps
+      let hyps := hyps.map (·.mvarId!)
+      let (isHeq, lhs, rhs) ← do
+        if let some (_, lhs, _, rhs) := eqType.heq? then pure (true, lhs, rhs) else
+        if let some (_, lhs, rhs) := eqType.eq? then pure (false, lhs, rhs) else
+        throwError m!"Type of {.ofConstName eqnThm} is not an equality"
+      if !(← isDefEq e lhs) then
+        throwError m!"Left-hand side {lhs} of {.ofConstName eqnThm} does not apply to {e}"
+      /-
+      Here we instantiate the hypotheses of the congruence equation theorem
+      There are two sets of hypotheses to instantiate:
+      - `Eq` or `HEq` that relate the discriminants to the patterns
+        Solving these should instantiate the pattern variables.
+      - Overlap hypotheses (`isEqnThmHypothesis`)
+      With more book keeping we could maybe do this very precisely, knowing exactly
+      which facts provided by the splitter should go where, but it's tedious.
+      So for now let's use heuristics and try `assumption` and `rfl`.
+      -/
+      for h in hyps do
+        unless (← h.isAssigned) do
+          let hType ← h.getType
+          if Simp.isEqnThmHypothesis hType then
+            -- Using unrestricted h.substVars here does not work well; it could
+            -- even introduce a dependency on the `oldIH` we want to eliminate
+            h.assumption <|> throwError "Failed to discharge {h}"
+          else if hType.isEq then
+            h.assumption <|> h.refl <|> throwError m!"Failed to resolve {h}"
+          else if hType.isHEq then
+            h.assumption <|> h.hrefl <|> throwError m!"Failed to resolve {h}"
+      let unassignedHyps ← hyps.filterM fun h => return !(← h.isAssigned)
+      unless unassignedHyps.isEmpty do
+        throwError m!"Not all hypotheses of {.ofConstName eqnThm} could be discharged: {unassignedHyps}"
+      let rhs ← instantiateMVars rhs
+      let proof ← instantiateMVars proof
+      let proof ← if isHeq then
+          try mkEqOfHEq proof
+          catch e => throwError m!"Could not un-HEq {proof}:{indentD e.toMessageData} "
+        else
+          pure proof
+      return {
+        expr := rhs
+        proof? := proof
+      }
+    catch ex =>
+      trace[Meta.FunInd] "Failed to apply {.ofConstName eqnThm}:{indentD ex.toMessageData}"
+      return { expr := e }
 
 /--
-
 Builds an expression of type `goal` by replicating the expression `e` into its tail-call-positions,
 where it calls `buildInductionCase`. Collects the cases of the final induction hypothesis
 as `MVars` as it goes.
@@ -767,13 +822,13 @@ partial def buildInductionBody (toErase toClear : Array FVarId) (goal : Expr)
         (addEqualities := true)
         (onParams := (foldAndCollect oldIH newIH isRecCall ·))
         (onMotive := fun xs _body => pure (absMotiveBody.beta (maskArray mask xs)))
-        (onAlt := fun expAltType alt => M2.branch do
+        (onAlt := fun altIdx expAltType alt => M2.branch do
           lambdaTelescope1 alt fun oldIH' alt => do
             forallBoundedTelescope expAltType (some 1) fun newIH' goal' => do
               let #[newIH'] := newIH' | unreachable!
               let toErase' := toErase ++ #[oldIH', newIH'.fvarId!]
               let toClear' := toClear ++ matcherApp.discrs.filterMap (·.fvarId?)
-              let alt' ← withRewrittenMotiveArg goal' rwMatcher fun goal'' => do
+              let alt' ← withRewrittenMotiveArg goal' (rwMatcher altIdx) fun goal'' => do
                 -- logInfo m!"rwMatcher after {matcherApp.matcherName} on{indentExpr goal'}\nyields{indentExpr goal''}"
                 buildInductionBody toErase' toClear' goal'' oldIH' newIH'.fvarId! isRecCall alt
               mkLambdaFVars #[newIH'] alt')
@@ -790,8 +845,8 @@ partial def buildInductionBody (toErase toClear : Array FVarId) (goal : Expr)
         (addEqualities := true)
         (onParams := (foldAndCollect oldIH newIH isRecCall ·))
         (onMotive := fun xs _body => pure (absMotiveBody.beta (maskArray mask xs)))
-        (onAlt := fun expAltType alt => M2.branch do
-          withRewrittenMotiveArg expAltType Split.simpMatch fun expAltType' =>
+        (onAlt := fun altIdx expAltType alt => M2.branch do
+          withRewrittenMotiveArg expAltType (rwMatcher altIdx) fun expAltType' =>
             buildInductionBody toErase toClear expAltType' oldIH newIH isRecCall alt)
       return matcherApp'.toExpr
 
diff --git a/tests/lean/run/funind_unfolding.lean b/tests/lean/run/funind_unfolding.lean
index 45aeaba6c5..0636d1b209 100644
--- a/tests/lean/run/funind_unfolding.lean
+++ b/tests/lean/run/funind_unfolding.lean
@@ -10,9 +10,10 @@ termination_by x => x
 info: fib.fun_cases_unfolding (motive : Nat → Nat → Prop) (case1 : motive 0 0) (case2 : motive 1 1)
   (case3 : ∀ (n : Nat), motive n.succ.succ (fib n + fib (n + 1))) (x✝ : Nat) : motive x✝ (fib x✝)
 -/
-#guard_msgs in
+#guard_msgs(pass trace, all) in
 #check fib.fun_cases_unfolding
 
+-- set_option trace.Meta.FunInd true in
 def ackermann : Nat → Nat → Nat
   | 0, m => m + 1
   | n+1, 0 => ackermann n 1
@@ -25,7 +26,7 @@ info: ackermann.fun_cases_unfolding (motive : Nat → Nat → Nat → Prop) (cas
   (case3 : ∀ (n m : Nat), motive n.succ m.succ (ackermann n (ackermann (n + 1) m))) (x✝ x✝¹ : Nat) :
   motive x✝ x✝¹ (ackermann x✝ x✝¹)
 -/
-#guard_msgs in
+#guard_msgs(pass trace, all) in
 #check ackermann.fun_cases_unfolding
 
 def fib' : Nat → Nat
@@ -39,7 +40,7 @@ info: fib'.fun_cases_unfolding (motive : Nat → Nat → Prop) (case1 : motive 0
   (case3 : ∀ (n : Nat), (n = 0 → False) → (n = 1 → False) → motive n (fib' (n - 1) + fib' (n - 2))) (x✝ : Nat) :
   motive x✝ (fib' x✝)
 -/
-#guard_msgs in
+#guard_msgs(pass trace, all) in
 #check fib'.fun_cases_unfolding
 
 def fib'' (n : Nat) : Nat :=
@@ -66,7 +67,7 @@ info: fib''.fun_cases_unfolding (motive : Nat → Nat → Prop) (case1 : ∀ (n
         ¬foo < 100 → motive n 0)
   (n : Nat) : motive n (fib'' n)
 -/
-#guard_msgs in
+#guard_msgs(pass trace, all) in
 #check fib''.fun_cases_unfolding
 
 -- set_option trace.Meta.FunInd true in
@@ -80,7 +81,7 @@ info: filter.fun_cases (motive : (Nat → Bool) → List Nat → Prop) (case1 :
   (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✝
 -/
-#guard_msgs in
+#guard_msgs(pass trace, all) in
 #check filter.fun_cases
 
 /--
@@ -90,7 +91,7 @@ info: filter.fun_cases_unfolding (motive : (Nat → Bool) → List Nat → List
   (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✝)
 -/
-#guard_msgs in
+#guard_msgs(pass trace, all) in
 #check filter.fun_cases_unfolding
 
 /--
@@ -98,7 +99,7 @@ info: filter.induct (p : Nat → Bool) (motive : List Nat → Prop) (case1 : mot
   (case2 : ∀ (x : Nat) (xs : List Nat), p x = true → motive xs → motive (x :: xs))
   (case3 : ∀ (x : Nat) (xs : List Nat), ¬p x = true → motive xs → motive (x :: xs)) (a✝ : List Nat) : motive a✝
 -/
-#guard_msgs in
+#guard_msgs(pass trace, all) in
 #check filter.induct
 
 /--
@@ -107,7 +108,7 @@ info: filter.induct_unfolding (p : Nat → Bool) (motive : List Nat → List Nat
   (case3 : ∀ (x : Nat) (xs : List Nat), ¬p x = true → motive xs (filter p xs) → motive (x :: xs) (filter p xs))
   (a✝ : List Nat) : motive a✝ (filter p a✝)
 -/
-#guard_msgs in
+#guard_msgs(pass trace, all) in
 #check filter.induct_unfolding
 
 theorem filter_const_false_is_nil :
@@ -141,7 +142,7 @@ info: map.fun_cases (motive : (Nat → Bool) → List Nat → Prop) (case1 : ∀
   (case2 : ∀ (f : Nat → Bool) (x : Nat) (xs : List Nat), motive f (x :: xs)) (f : Nat → Bool) (x✝ : List Nat) :
   motive f x✝
 -/
-#guard_msgs in
+#guard_msgs(pass trace, all) in
 #check map.fun_cases
 
 /--
@@ -150,14 +151,14 @@ info: map.fun_cases_unfolding (motive : (Nat → Bool) → List Nat → List Boo
   (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✝)
 -/
-#guard_msgs in
+#guard_msgs(pass trace, all) in
 #check map.fun_cases_unfolding
 
 /--
 info: map.induct (motive : List Nat → Prop) (case1 : motive [])
   (case2 : ∀ (x : Nat) (xs : List Nat), motive xs → motive (x :: xs)) (a✝ : List Nat) : motive a✝
 -/
-#guard_msgs in
+#guard_msgs(pass trace, all) in
 #check map.induct
 
 /--
@@ -165,11 +166,12 @@ info: map.induct_unfolding (f : Nat → Bool) (motive : List Nat → List Bool 
   (case2 : ∀ (x : Nat) (xs : List Nat), motive xs (map f xs) → motive (x :: xs) (f x :: map f xs)) (a✝ : List Nat) :
   motive a✝ (map f a✝)
 -/
-#guard_msgs in
+#guard_msgs(pass trace, all) in
 #check map.induct_unfolding
 
 namespace BinaryWF
 
+-- set_option trace.Meta.FunInd true in
 def map2 (f : Nat → Nat → Bool) : List Nat → List Nat → List Bool
   | x::xs, y::ys => f x y::map2 f xs ys
   | _, _ => []
@@ -187,7 +189,7 @@ info: BinaryWF.map2.induct_unfolding (f : Nat → Nat → Bool) (motive : List N
         motive x x_1 [])
   (a✝ a✝¹ : List Nat) : motive a✝ a✝¹ (map2 f a✝ a✝¹)
 -/
-#guard_msgs in
+#guard_msgs(pass trace, all) in
 #check map2.induct_unfolding
 
 end BinaryWF
@@ -209,7 +211,7 @@ info: BinaryStructural.map2.induct_unfolding (f : Nat → Nat → Bool) (motive
       (∀ (x_1 : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t = x_1 :: xs → x = y :: ys → False) → motive t x [])
   (a✝ a✝¹ : List Nat) : motive a✝ a✝¹ (map2 f a✝ a✝¹)
 -/
-#guard_msgs in
+#guard_msgs(pass trace, all) in
 #check map2.induct_unfolding
 
 end BinaryStructural
@@ -245,7 +247,7 @@ info: MutualWF.map2a.mutual_induct_unfolding (f : Nat → Nat → Bool) (motive1
         motive2 x x_1 []) :
   (∀ (a a_1 : List Nat), motive1 a a_1 (map2a f a a_1)) ∧ ∀ (a a_1 : List Nat), motive2 a a_1 (map2b f a a_1)
 -/
-#guard_msgs in
+#guard_msgs(pass trace, all) in
 #check map2a.mutual_induct_unfolding
 
 /--
@@ -266,7 +268,7 @@ info: MutualWF.map2a.induct_unfolding (f : Nat → Nat → Bool) (motive1 motive
         motive2 x x_1 [])
   (a✝ a✝¹ : List Nat) : motive1 a✝ a✝¹ (map2a f a✝ a✝¹)
 -/
-#guard_msgs in
+#guard_msgs(pass trace, all) in
 #check map2a.induct_unfolding
 
 end MutualWF
@@ -297,7 +299,7 @@ info: MutualStructural.map2a.induct (motive_1 motive_2 : List Nat → List Nat 
       (∀ (x_1 : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t = x_1 :: xs → x = y :: ys → False) → motive_2 t x)
   (a✝ a✝¹ : List Nat) : motive_1 a✝ a✝¹
 -/
-#guard_msgs in
+#guard_msgs(pass trace, all) in
 #check map2a.induct
 
 
@@ -320,7 +322,7 @@ info: MutualStructural.map2a.mutual_induct_unfolding (f : Nat → Nat → Bool)
         motive_2 t x (map2b f t x)) :
   (∀ (a a_1 : List Nat), motive_1 a a_1 (map2a f a a_1)) ∧ ∀ (a a_1 : List Nat), motive_2 a a_1 (map2b f a a_1)
 -/
-#guard_msgs in
+#guard_msgs(pass trace, all) in
 #check map2a.mutual_induct_unfolding
 
 
@@ -343,7 +345,7 @@ info: MutualStructural.map2a.induct_unfolding (f : Nat → Nat → Bool)
         motive_2 t x (map2b f t x))
   (a✝ a✝¹ : List Nat) : motive_1 a✝ a✝¹ (map2a f a✝ a✝¹)
 -/
-#guard_msgs in
+#guard_msgs(pass trace, all) in
 #check map2a.induct_unfolding
 
 end MutualStructural
@@ -391,7 +393,7 @@ info: siftDown.induct_unfolding (e : Nat) (motive : (a : Array Int) → Nat →
   (case3 : ∀ (a : Array Int) (root : Nat) (h : e ≤ a.size), ¬leftChild root < e → motive a root h a) (a : Array Int)
   (root : Nat) (h : e ≤ a.size) : motive a root h (siftDown a root e h)
 -/
-#guard_msgs in
+#guard_msgs(pass trace, all) in
 #check siftDown.induct_unfolding
 
 /--
@@ -413,7 +415,7 @@ info: siftDown.induct (e : Nat) (motive : (a : Array Int) → Nat → e ≤ a.si
   (case3 : ∀ (a : Array Int) (root : Nat) (h : e ≤ a.size), ¬leftChild root < e → motive a root h) (a : Array Int)
   (root : Nat) (h : e ≤ a.size) : motive a root h
 -/
-#guard_msgs in
+#guard_msgs(pass trace, all) in
 #check siftDown.induct
 
 -- Now something with have
@@ -429,14 +431,14 @@ info: withHave.induct_unfolding (motive : Nat → Bool → Prop) (case1 : 0 < 42
   (case2 : ∀ (x : Nat), 0 < x → ¬x = 42 → motive (x - 1) (withHave (x - 1)) → motive x (withHave (x - 1))) (n : Nat) :
   motive n (withHave n)
 -/
-#guard_msgs in
+#guard_msgs(pass trace, all) in
 #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)
 -/
-#guard_msgs in
+#guard_msgs(pass trace, all) in
 #check withHave.fun_cases_unfolding
 
 -- Structural Mutual recursion
@@ -466,7 +468,7 @@ info: Tree.size.induct_unfolding.{u_1} {α : Type u_1} (motive_1 : Tree α → N
       motive_1 t t.size → motive_2 ts (Tree.size_aux ts) → motive_2 (t :: ts) (t.size + Tree.size_aux ts))
   (a✝ : Tree α) : motive_1 a✝ a✝.size
 -/
-#guard_msgs in
+#guard_msgs(pass trace, all) in
 #check Tree.size.induct_unfolding
 
 /--
@@ -483,5 +485,55 @@ info: Tree.size_aux.induct_unfolding.{u_1} {α : Type u_1} (motive_1 : Tree α 
       motive_1 t t.size → motive_2 ts (Tree.size_aux ts) → motive_2 (t :: ts) (t.size + Tree.size_aux ts))
   (a✝ : List (Tree α)) : motive_2 a✝ (Tree.size_aux a✝)
 -/
-#guard_msgs in
+#guard_msgs(pass trace, all) in
 #check Tree.size_aux.induct_unfolding
+
+
+-- When the discriminants are duplicated, it is very easy for `FunInd` to be confused
+-- about how to instantiate the equality theorem. Maybe not relevant in practice for now?
+-- Maybe even impossible to solve.
+
+-- set_option trace.Meta.FunInd true in
+set_option linter.unusedVariables false in
+def duplicatedDiscriminant (n : Nat) : Bool :=
+  match h1 : n, h2 : n with
+  | 0, 0 => true
+  | a+1, 0 => false -- by simp_all
+  | 0, b+1 => false -- by simp_all
+  | a, b => true
+
+/--
+info: duplicatedDiscriminant.fun_cases_unfolding (motive : Nat → Bool → Prop) (case1 : 0 = 0 → motive 0 true)
+  (case2 :
+    ∀ (a : Nat),
+      a.succ = 0 →
+        motive 0
+          (match h1 : 0, h2 : 0 with
+          | 0, 0 => true
+          | a.succ, 0 => false
+          | 0, b.succ => false
+          | a, b => true))
+  (case3 :
+    ∀ (b : Nat),
+      0 = b.succ →
+        motive b.succ
+          (match h1 : b.succ, h2 : b.succ with
+          | 0, 0 => true
+          | a.succ, 0 => false
+          | 0, b_1.succ => false
+          | a, b_1 => true))
+  (case4 :
+    ∀ (b : Nat),
+      (b = 0 → b = 0 → False) →
+        (∀ (a : Nat), b = a.succ → b = 0 → False) →
+          (∀ (b_1 : Nat), b = 0 → b = b_1.succ → False) →
+            motive b
+              (match h1 : b, h2 : b with
+              | 0, 0 => true
+              | a.succ, 0 => false
+              | 0, b_1.succ => false
+              | a, b_1 => true))
+  (n : Nat) : motive n (duplicatedDiscriminant n)
+-/
+#guard_msgs(pass trace, all) in
+#check duplicatedDiscriminant.fun_cases_unfolding
diff --git a/tests/lean/run/issue8103.lean b/tests/lean/run/issue8103.lean
index 7ae159db86..c1b51eede9 100644
--- a/tests/lean/run/issue8103.lean
+++ b/tests/lean/run/issue8103.lean
@@ -1,3 +1,4 @@
+-- set_option trace.Meta.FunInd true in
 def foo (n m : Nat) (h : n < m) : Nat :=
   match m with
   | 0 => by contradiction -- This case should not show up in the principles below
@@ -10,7 +11,7 @@ info: foo.induct (motive : (n m : Nat) → n < m → Prop) (case1 : ∀ (m : Nat
   (case2 : ∀ (m n : Nat) (h : n + 1 < m + 1), n.succ < m.succ → motive n m ⋯ → motive n.succ m.succ h) (n m : Nat)
   (h : n < m) : motive n m h
 -/
-#guard_msgs in
+#guard_msgs(pass trace, all) in
 #check foo.induct
 
 /--
@@ -20,7 +21,7 @@ info: foo.induct_unfolding (motive : (n m : Nat) → n < m → Nat → Prop)
     ∀ (m n : Nat) (h : n + 1 < m + 1), n.succ < m.succ → motive n m ⋯ (foo n m ⋯) → motive n.succ m.succ h (foo n m ⋯))
   (n m : Nat) (h : n < m) : motive n m h (foo n m h)
 -/
-#guard_msgs in
+#guard_msgs(pass trace, all) in
 #check foo.induct_unfolding
 
 
@@ -30,7 +31,7 @@ info: foo.fun_cases (motive : (n m : Nat) → n < m → Prop)
   (case2 : ∀ (m n : Nat) (h : n + 1 < m + 1), n.succ < m + 1 → n.succ < m.succ → motive n.succ m.succ h) (n m : Nat)
   (h : n < m) : motive n m h
 -/
-#guard_msgs in
+#guard_msgs(pass trace, all) in
 #check foo.fun_cases
 
 def bar (n m : Nat) (h : n = m) : Nat :=
@@ -45,7 +46,7 @@ info: bar.induct (motive : (n m : Nat) → n = m → Prop) (case1 : ∀ (h : 0 =
   (case2 : ∀ (m n : Nat) (h : n + 1 = m + 1), m.succ = n.succ → motive n m ⋯ → motive n.succ m.succ h) (n m : Nat)
   (h : n = m) : motive n m h
 -/
-#guard_msgs in
+#guard_msgs(pass trace, all) in
 #check bar.induct
 
 /--
@@ -54,7 +55,7 @@ info: bar.induct_unfolding (motive : (n m : Nat) → n = m → Nat → Prop) (ca
     ∀ (m n : Nat) (h : n + 1 = m + 1), m.succ = n.succ → motive n m ⋯ (bar n m ⋯) → motive n.succ m.succ h (bar n m ⋯))
   (n m : Nat) (h : n = m) : motive n m h (bar n m h)
 -/
-#guard_msgs in
+#guard_msgs(pass trace, all) in
 #check bar.induct_unfolding
 
 /--
@@ -62,7 +63,7 @@ info: bar.fun_cases (motive : (n m : Nat) → n = m → Prop) (case1 : ∀ (h :
   (case2 : ∀ (m n : Nat) (h : n + 1 = m + 1), m.succ = m + 1 → m.succ = n.succ → motive n.succ m.succ h) (n m : Nat)
   (h : n = m) : motive n m h
 -/
-#guard_msgs in
+#guard_msgs(pass trace, all) in
 #check bar.fun_cases
 
 def baz (n : Nat) (h : n ≠ 0) : Nat :=
@@ -76,7 +77,7 @@ info: baz.induct (motive : (n : Nat) → n ≠ 0 → Prop) (case1 : ∀ (h : 0 +
   (case2 : ∀ (k : Nat) (h : k + 1 ≠ 0) (h_1 : ¬k = 0), motive k h_1 → motive k.succ h) (n : Nat) (h : n ≠ 0) :
   motive n h
 -/
-#guard_msgs in
+#guard_msgs(pass trace, all) in
 #check baz.induct
 
 /--
@@ -84,14 +85,14 @@ info: baz.induct_unfolding (motive : (n : Nat) → n ≠ 0 → Nat → Prop) (ca
   (case2 : ∀ (k : Nat) (h : k + 1 ≠ 0) (h_1 : ¬k = 0), motive k h_1 (baz k h_1) → motive k.succ h (baz k h_1)) (n : Nat)
   (h : n ≠ 0) : motive n h (baz n h)
 -/
-#guard_msgs in
+#guard_msgs(pass trace, all) in
 #check baz.induct_unfolding
 
 /--
 info: baz.fun_cases (motive : (n : Nat) → n ≠ 0 → Prop) (case1 : ∀ (h : 0 + 1 ≠ 0), Nat.succ 0 ≠ 0 → motive (Nat.succ 0) h)
   (case2 : ∀ (k : Nat) (h : k + 1 ≠ 0), ¬k = 0 → k.succ ≠ 0 → motive k.succ h) (n : Nat) (h : n ≠ 0) : motive n h
 -/
-#guard_msgs in
+#guard_msgs(pass trace, all) in
 #check baz.fun_cases
 
 
@@ -107,5 +108,5 @@ info: mean.fun_cases (motive : (n m : Nat) → n = m → Prop) (case1 : ∀ (h :
   (case2 : ∀ (m n : Nat) (h : n + 1 = m + 1), m.succ = m + 1 → m.succ = n.succ → motive n.succ m.succ h) (n m : Nat)
   (h : n = m) : motive n m h
 -/
-#guard_msgs in
+#guard_msgs(pass trace, all) in
 #check mean.fun_cases
diff --git a/tests/lean/run/issue8195.lean b/tests/lean/run/issue8195.lean
new file mode 100644
index 0000000000..50162aff92
--- /dev/null
+++ b/tests/lean/run/issue8195.lean
@@ -0,0 +1,106 @@
+import Lean
+
+-- set_option trace.Meta.FunInd true
+
+axiom testSorry : α
+
+def test (l : List Nat) : Nat :=
+  match l with
+  | [] => 0
+  | x :: l =>
+    match x == 3 with
+    | false => test l
+    | true => test l
+
+/--
+info: test.induct_unfolding (motive : List Nat → Nat → Prop) (case1 : motive [] 0)
+  (case2 : ∀ (x : Nat) (l : List Nat), (x == 3) = false → motive l (test l) → motive (x :: l) (test l))
+  (case3 : ∀ (x : Nat) (l : List Nat), (x == 3) = true → motive l (test l) → motive (x :: l) (test l)) (l : List Nat) :
+  motive l (test l)
+-/
+#guard_msgs in
+#check test.induct_unfolding
+
+opaque someFunction (x : Nat) (h : (x == 3) = false) : Nat
+opaque someOtherFunction (x : Nat) (h : (x == 3) = true) : Nat
+
+def deptest (l : List Nat) : Nat :=
+  match l with
+  | [] => 0
+  | x :: l =>
+    match h : x == 3 with
+    | false => deptest l + someFunction x h
+    | true => deptest l + someOtherFunction x h
+
+/--
+info: deptest.induct_unfolding (motive : List Nat → Nat → Prop) (case1 : motive [] 0)
+  (case2 :
+    ∀ (x : Nat) (l : List Nat) (h : (x == 3) = false),
+      motive l (deptest l) → motive (x :: l) (deptest l + someFunction x h))
+  (case3 :
+    ∀ (x : Nat) (l : List Nat) (h : (x == 3) = true),
+      motive l (deptest l) → motive (x :: l) (deptest l + someOtherFunction x h))
+  (l : List Nat) : motive l (deptest l)
+-/
+#guard_msgs in
+#check deptest.induct_unfolding
+
+-- This one doesn't work, the result type varies in the branches
+-- But we fail gracefully
+def depTestOddType (l : List Nat) :
+    match l with
+    | [] => Unit
+    | x :: _ =>
+      if x == 3 then
+        Unit
+      else
+        Nat
+  :=
+  match l with
+  | [] => ()
+  | x :: _ =>
+    (match h : x == 3 with
+    | false => someFunction x h
+    | true => () : if x == 3 then Unit else Nat)
+
+/--
+info: depTestOddType.fun_cases_unfolding
+  (motive :
+    (l : List Nat) →
+      (match l with
+        | [] => Unit
+        | x :: tail => if (x == 3) = true then Unit else Nat) →
+        Prop)
+  (case1 : motive [] ())
+  (case2 :
+    ∀ (x : Nat) (l : List Nat),
+      (x == 3) = false →
+        motive (x :: l)
+          (match h : x == 3 with
+          | false => someFunction x h
+          | true => ()))
+  (case3 :
+    ∀ (x : Nat) (l : List Nat),
+      (x == 3) = true →
+        motive (x :: l)
+          (match h : x == 3 with
+          | false => someFunction x h
+          | true => ()))
+  (l : List Nat) : motive l (depTestOddType l)
+-/
+#guard_msgs in
+#check depTestOddType.fun_cases_unfolding
+
+-- set_option trace.Meta.FunInd true in
+set_option linter.unusedVariables false in
+def testMe (n : Nat) : Bool :=
+  match _ : n - 2 with
+  | 0 => true
+  | 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)
+-/
+#guard_msgs in
+#check testMe.fun_cases_unfolding
diff --git a/tests/lean/run/issue8213.lean b/tests/lean/run/issue8213.lean
new file mode 100644
index 0000000000..1425f9440e
--- /dev/null
+++ b/tests/lean/run/issue8213.lean
@@ -0,0 +1,32 @@
+-- set_option trace.Meta.FunInd true
+
+def myTest {α}
+  (mmotive : (x : List α) → Sort v)
+  (x : List α)
+  (h_1 : (a : α) → (dc : List α) → x = a :: dc → mmotive (a :: dc))
+  (h_2 : (x' : List α) → x = x' → mmotive x') : mmotive x :=
+  match (generalizing := false) h : x with
+  | a :: dc => h_1 a dc h
+  | x' => h_2 x' h
+
+
+/--
+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
+    ⏎
+      Application type mismatch: In the appplication
+        motive mmotive x✝ h_1
+      the final argument
+        h_1
+      has type
+        (a : α) → (dc : List α) → x = a :: dc → mmotive (a :: dc) : Sort (imax (u_1 + 1) (u_1 + 1) v)
+      but is expected to have type
+        (a : α) → (dc : List α) → x✝ = a :: dc → mmotive (a :: dc) : Sort (imax (u_1 + 1) (u_1 + 1) v)
+---
+error: unknown identifier 'myTest.fun_cases'
+-/
+#guard_msgs in
+def foo := @myTest.fun_cases