diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 8be94e99ebc8..14c0ae70d636 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Util.FindMVar
+import Lean.Util.CollectFVars
 import Lean.Parser.Term
 import Lean.Meta.KAbstract
 import Lean.Meta.Tactic.ElimInfo
@@ -711,6 +712,12 @@ structure Context where
   ```
   theorem Eq.subst' {α} {motive : α → Prop} {a b : α} (h : a = b) : motive a → motive b
   ```
+  For another example, the term `isEmptyElim (α := α)` is an underapplied eliminator, and it needs
+  argument `α` to be elaborated eagerly to create a type-correct motive.
+  ```
+  def isEmptyElim [IsEmpty α] {p : α → Sort _} (a : α) : p a := ...
+  example {α : Type _} [IsEmpty α] : id (α → False) := isEmptyElim (α := α)
+  ```
   -/
   extraArgsPos : Array Nat
 
@@ -724,8 +731,8 @@ structure State where
   namedArgs    : List NamedArg
   /-- User-provided arguments that still have to be processed. -/
   args         : List Arg
-  /-- Discriminants processed so far. -/
-  discrs       : Array Expr := #[]
+  /-- Discriminants (targets) processed so far. -/
+  discrs       : Array (Option Expr)
   /-- Instance implicit arguments collected so far. -/
   instMVars    : Array MVarId := #[]
   /-- Position of the next argument to be processed. We use it to decide whether the argument is the motive or a discriminant. -/
@@ -742,10 +749,7 @@ def mkMotive (discrs : Array Expr) (expectedType : Expr): MetaM Expr := do
     let motiveBody ← kabstract motive discr
     /- We use `transform (usedLetOnly := true)` to eliminate unnecessary let-expressions. -/
     let discrType ← transform (usedLetOnly := true) (← instantiateMVars (← inferType discr))
-    let motive := Lean.mkLambda (← mkFreshBinderName) BinderInfo.default discrType motiveBody
-    unless (← isTypeCorrect motive) do
-      throwError "failed to elaborate eliminator, motive is not type correct:{indentD motive}"
-    return motive
+    return Lean.mkLambda (← mkFreshBinderName) BinderInfo.default discrType motiveBody
 
 /-- If the eliminator is over-applied, we "revert" the extra arguments. -/
 def revertArgs (args : List Arg) (f : Expr) (expectedType : Expr) : TermElabM (Expr × Expr) :=
@@ -761,7 +765,7 @@ def revertArgs (args : List Arg) (f : Expr) (expectedType : Expr) : TermElabM (E
     return (mkApp f val, mkForall (← mkFreshBinderName) BinderInfo.default valType expectedTypeBody)
 
 /--
-Construct the resulting application after all discriminants have bee elaborated, and we have
+Construct the resulting application after all discriminants have been elaborated, and we have
 consumed as many given arguments as possible.
 -/
 def finalize : M Expr := do
@@ -769,29 +773,50 @@ def finalize : M Expr := do
     throwError "failed to elaborate eliminator, unused named arguments: {(← get).namedArgs.map (·.name)}"
   let some motive := (← get).motive?
     | throwError "failed to elaborate eliminator, insufficient number of arguments"
+  trace[Elab.app.elab_as_elim] "motive: {motive}"
   forallTelescope (← get).fType fun xs _ => do
+    trace[Elab.app.elab_as_elim] "xs: {xs}"
     let mut expectedType := (← read).expectedType
+    trace[Elab.app.elab_as_elim] "expectedType:{indentD expectedType}"
+    let throwInsufficient := do
+      throwError "failed to elaborate eliminator, insufficient number of arguments, expected type:{indentExpr expectedType}"
     let mut f := (← get).f
     if xs.size > 0 then
+      -- under-application, specialize the expected type using `xs`
       assert! (← get).args.isEmpty
-      try
-        expectedType ← instantiateForall expectedType xs
-      catch _ =>
-        throwError "failed to elaborate eliminator, insufficient number of arguments, expected type:{indentExpr expectedType}"
+      for x in xs do
+        let .forallE _ t b _ ← whnf expectedType | throwInsufficient
+        unless ← fullApproxDefEq <| isDefEq t (← inferType x) do
+          -- We can't assume that these binding domains were supposed to line up, so report insufficient arguments
+          throwInsufficient
+        expectedType := b.instantiate1 x
+      trace[Elab.app.elab_as_elim] "xs after specialization of expected type: {xs}"
     else
-      -- over-application, simulate `revert`
+      -- over-application, simulate `revert` while generalizing the values of these arguments in the expected type
       (f, expectedType) ← revertArgs (← get).args f expectedType
+      unless ← isTypeCorrect expectedType do
+        throwError "failed to elaborate eliminator, after generalizing over-applied arguments, expected type is type incorrect:{indentExpr expectedType}"
+    trace[Elab.app.elab_as_elim] "expectedType after processing:{indentD expectedType}"
     let result := mkAppN f xs
+    trace[Elab.app.elab_as_elim] "result:{indentD result}"
     let mut discrs := (← get).discrs
     let idx := (← get).idx
-    if (← get).discrs.size < (← read).elimInfo.targetsPos.size then
+    if discrs.any Option.isNone then
       for i in [idx:idx + xs.size], x in xs do
-        if (← read).elimInfo.targetsPos.contains i then
-          discrs := discrs.push x
-    let motiveVal ← mkMotive discrs expectedType
+        if let some tidx := (← read).elimInfo.targetsPos.indexOf? i then
+          discrs := discrs.set! tidx x
+    if let some idx := discrs.findIdx? Option.isNone then
+      -- This should not happen.
+      trace[Elab.app.elab_as_elim] "Internal error, missing target with index {idx}"
+      throwError "failed to elaborate eliminator, insufficient number of arguments"
+    trace[Elab.app.elab_as_elim] "discrs: {discrs.map Option.get!}"
+    let motiveVal ← mkMotive (discrs.map Option.get!) expectedType
+    unless (← isTypeCorrect motiveVal) do
+      throwError "failed to elaborate eliminator, motive is not type correct:{indentD motiveVal}"
     unless (← isDefEq motive motiveVal) do
       throwError "failed to elaborate eliminator, invalid motive{indentExpr motiveVal}"
     synthesizeAppInstMVars (← get).instMVars result
+    trace[Elab.app.elab_as_elim] "completed motive:{indentD motive}"
     let result ← mkLambdaFVars xs (← instantiateMVars result)
     return result
 
@@ -819,9 +844,9 @@ def getNextArg? (binderName : Name) (binderInfo : BinderInfo) : M (LOption Arg)
 def setMotive (motive : Expr) : M Unit :=
   modify fun s => { s with motive? := motive }
 
-/-- Push the given expression into the `discrs` field in the state. -/
-def addDiscr (discr : Expr) : M Unit :=
-  modify fun s => { s with discrs := s.discrs.push discr }
+/-- Push the given expression into the `discrs` field in the state, where `i` is which target it is for. -/
+def addDiscr (i : Nat) (discr : Expr) : M Unit :=
+  modify fun s => { s with discrs := s.discrs.set! i discr }
 
 /-- Elaborate the given argument with the given expected type. -/
 private def elabArg (arg : Arg) (argExpectedType : Expr) : M Expr := do
@@ -856,11 +881,11 @@ partial def main : M Expr := do
     let motive ← mkImplicitArg binderType binderInfo
     setMotive motive
     addArgAndContinue motive
-  else if (← read).elimInfo.targetsPos.contains idx then
+  else if let some tidx := (← read).elimInfo.targetsPos.indexOf? idx then
     match (← getNextArg? binderName binderInfo) with
-    | .some arg => let discr ← elabArg arg binderType; addDiscr discr; addArgAndContinue discr
+    | .some arg => let discr ← elabArg arg binderType; addDiscr tidx discr; addArgAndContinue discr
     | .undef => finalize
-    | .none => let discr ← mkImplicitArg binderType binderInfo; addDiscr discr; addArgAndContinue discr
+    | .none => let discr ← mkImplicitArg binderType binderInfo; addDiscr tidx discr; addArgAndContinue discr
   else match (← getNextArg? binderName binderInfo) with
     | .some (.stx stx) =>
       if (← read).extraArgsPos.contains idx then
@@ -922,10 +947,12 @@ def elabAppArgs (f : Expr) (namedArgs : Array NamedArg) (args : Array Arg)
     let expectedType ← instantiateMVars expectedType
     if expectedType.getAppFn.isMVar then throwError "failed to elaborate eliminator, expected type is not available"
     let extraArgsPos ← getElabAsElimExtraArgsPos elimInfo
+    trace[Elab.app.elab_as_elim] "extraArgsPos: {extraArgsPos}"
     ElabElim.main.run { elimInfo, expectedType, extraArgsPos } |>.run' {
       f, fType
       args := args.toList
       namedArgs := namedArgs.toList
+      discrs := mkArray elimInfo.targetsPos.size none
     }
   else
     ElabAppArgs.main.run { explicit, ellipsis, resultIsOutParamSupport } |>.run' {
@@ -955,19 +982,29 @@ where
 
   /--
   Collect extra argument positions that must be elaborated eagerly when using `elab_as_elim`.
-  The idea is that the contribute to motive inference. See comment at `ElamElim.Context.extraArgsPos`.
+  The idea is that they contribute to motive inference. See comment at `ElamElim.Context.extraArgsPos`.
   -/
   getElabAsElimExtraArgsPos (elimInfo : ElimInfo) : MetaM (Array Nat) := do
     forallTelescope elimInfo.elimType fun xs type => do
-      let resultArgs := type.getAppArgs
+      let targets := type.getAppArgs
+      /- Compute transitive closure of fvars appearing in the motive and the targets. -/
+      let initMotiveFVars : CollectFVars.State := targets.foldl (init := {}) collectFVars
+      let motiveFVars ← xs.size.foldRevM (init := initMotiveFVars) fun i s => do
+        let x := xs[i]!
+        if elimInfo.motivePos == i || elimInfo.targetsPos.contains i || s.fvarSet.contains x.fvarId! then
+          return collectFVars s (← inferType x)
+        else
+          return s
+      /- Collect the extra argument positions -/
       let mut extraArgsPos := #[]
       for i in [:xs.size] do
         let x := xs[i]!
-        unless elimInfo.targetsPos.contains i do
-          let xType ← inferType x
+        unless elimInfo.motivePos == i || elimInfo.targetsPos.contains i do
+          let xType ← x.fvarId!.getType
           /- We only consider "first-order" types because we can reliably "extract" information from them. -/
-          if isFirstOrder xType
-             && Option.isSome (xType.find? fun e => e.isFVar && resultArgs.contains e) then
+          if motiveFVars.fvarSet.contains x.fvarId!
+             || (isFirstOrder xType
+                 && Option.isSome (xType.find? fun e => e.isFVar && motiveFVars.fvarSet.contains e.fvarId!)) then
             extraArgsPos := extraArgsPos.push i
       return extraArgsPos
 
@@ -1528,5 +1565,6 @@ builtin_initialize
   registerTraceClass `Elab.app.args (inherited := true)
   registerTraceClass `Elab.app.propagateExpectedType (inherited := true)
   registerTraceClass `Elab.app.finalize (inherited := true)
+  registerTraceClass `Elab.app.elab_as_elim (inherited := true)
 
 end Lean.Elab.Term
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 41fac87cbbae..66e1194b60e8 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -12,19 +12,64 @@ import Lean.Language.Basic
 
 namespace Lean.Elab.Command
 
+/--
+A `Scope` records the part of the `CommandElabM` state that respects scoping,
+such as the data for `universe`, `open`, and `variable` declarations, the current namespace,
+and currently enabled options.
+The `CommandElabM` state contains a stack of scopes, and only the top `Scope`
+on the stack is read from or modified. There is always at least one `Scope` on the stack,
+even outside any `section` or `namespace`, and each new pushed `Scope`
+starts as a modified copy of the previous top scope.
+-/
 structure Scope where
+  /--
+  The component of the `namespace` or `section` that this scope is associated to.
+  For example, `section a.b.c` and `namespace a.b.c` each create three scopes with headers
+  named `a`, `b`, and `c`.
+  This is used for checking the `end` command. The "base scope" has `""` as its header.
+  -/
   header        : String
+  /--
+  The current state of all set options at this point in the scope. Note that this is the
+  full current set of options and does *not* simply contain the options set
+  while this scope has been active.
+  -/
   opts          : Options := {}
+  /-- The current namespace. The top-level namespace is represented by `Name.anonymous`. -/
   currNamespace : Name := Name.anonymous
+  /-- All currently `open`ed namespaces and names. -/
   openDecls     : List OpenDecl := []
+  /-- The current list of names for universe level variables to use for new declarations. This is managed by the `universe` command. -/
   levelNames    : List Name := []
-  /-- section variables -/
+  /--
+  The current list of binders to use for new declarations.
+  This is managed by the `variable` command.
+  Each binder is represented in `Syntax` form, and it is re-elaborated
+  within each command that uses this information.
+
+  This is also used by commands, such as `#check`, to create an initial local context,
+  even if they do not work with binders per se.
+  -/
   varDecls      : Array (TSyntax ``Parser.Term.bracketedBinder) := #[]
   /-- `include`d section variable names -/
   includedVars  : List Name := []
-  /-- Globally unique internal identifiers for the `varDecls` -/
+  /--
+  Globally unique internal identifiers for the `varDecls`.
+  There is one identifier per variable introduced by the binders
+  (recall that a binder such as `(a b c : Ty)` can produce more than one variable),
+  and each identifier is the user-provided variable name with a macro scope.
+  This is used by `TermElabM` in `Lean.Elab.Term.Context` to help with processing macros
+  that capture these variables.
+  -/
   varUIds       : Array Name := #[]
-  /-- noncomputable sections automatically add the `noncomputable` modifier to any declaration we cannot generate code for. -/
+  /--
+  If true (default: false), all declarations that fail to compile
+  automatically receive the `noncomputable` modifier.
+  A scope with this flag set is created by `noncomputable section`.
+
+  Recall that a new scope inherits all values from its parent scope,
+  so all sections and namespaces nested within a `noncomputable` section also have this flag set.
+  -/
   isNoncomputable : Bool := false
   deriving Inhabited
 
@@ -232,6 +277,7 @@ private def ioErrorToMessage (ctx : Context) (ref : Syntax) (err : IO.Error) : M
 instance : MonadLiftT IO CommandElabM where
   monadLift := liftIO
 
+/-- Return the current scope. -/
 def getScope : CommandElabM Scope := do pure (← get).scopes.head!
 
 instance : MonadResolveName CommandElabM where
@@ -614,6 +660,11 @@ Interrupt and abort exceptions are caught but not logged.
 private def liftAttrM {α} (x : AttrM α) : CommandElabM α := do
   liftCoreM x
 
+/--
+Return the stack of all currently active scopes:
+the base scope always comes last; new scopes are prepended in the front.
+In particular, the current scope is always the first element.
+-/
 def getScopes : CommandElabM (List Scope) := do
   pure (← get).scopes
 
diff --git a/src/Lean/Elab/PreDefinition/Main.lean b/src/Lean/Elab/PreDefinition/Main.lean
index 55763c83804e..426b3c147315 100644
--- a/src/Lean/Elab/PreDefinition/Main.lean
+++ b/src/Lean/Elab/PreDefinition/Main.lean
@@ -114,7 +114,7 @@ def checkTerminationByHints (preDefs : Array PreDefinition) : CoreM Unit := do
       if !structural && !preDefsWithout.isEmpty then
         let m := MessageData.andList (preDefsWithout.toList.map (m!"{·.declName}"))
         let doOrDoes := if preDefsWithout.size = 1 then "does" else "do"
-        logErrorAt termBy.ref (m!"Incomplete set of `termination_by` annotations:\n"++
+        logErrorAt termBy.ref (m!"incomplete set of `termination_by` annotations:\n"++
           m!"This function is mutually with {m}, which {doOrDoes} not have " ++
           m!"a `termination_by` clause.\n" ++
           m!"The present clause is ignored.")
diff --git a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
index 96f742b747cc..4bb591844fb7 100644
--- a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
@@ -5,11 +5,11 @@ Authors: Leonardo de Moura, Joachim Breitner
 -/
 prelude
 import Lean.Util.HasConstCache
+import Lean.Meta.PProdN
 import Lean.Meta.Match.MatcherApp.Transform
 import Lean.Elab.RecAppSyntax
 import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.Structural.Basic
-import Lean.Elab.PreDefinition.Structural.FunPacker
 import Lean.Elab.PreDefinition.Structural.RecArgInfo
 
 namespace Lean.Elab.Structural
@@ -21,11 +21,11 @@ private def throwToBelowFailed : MetaM α :=
 partial def searchPProd (e : Expr) (F : Expr) (k : Expr → Expr → MetaM α) : MetaM α := do
   match (← whnf e) with
   | .app (.app (.const `PProd _) d1) d2 =>
-        (do searchPProd d1 (← mkAppM ``PProd.fst #[F]) k)
-    <|> (do searchPProd d2 (← mkAppM `PProd.snd #[F]) k)
+        (do searchPProd d1 (.proj ``PProd 0 F) k)
+    <|> (do searchPProd d2 (.proj ``PProd 1 F) k)
   | .app (.app (.const `And _) d1) d2 =>
-        (do searchPProd d1 (← mkAppM `And.left #[F]) k)
-    <|> (do searchPProd d2 (← mkAppM `And.right #[F]) k)
+        (do searchPProd d1 (.proj `And 0 F) k)
+    <|> (do searchPProd d2 (.proj `And 1 F) k)
   | .const `PUnit _
   | .const `True _ => throwToBelowFailed
   | _ => k e F
@@ -85,7 +85,7 @@ private def withBelowDict [Inhabited α] (below : Expr) (numIndParams : Nat)
         return ((← mkFreshUserName `C), fun _ => pure t)
     withLocalDeclsD CDecls fun Cs => do
       -- We have to pack these canary motives like we packed the real motives
-      let packedCs ← positions.mapMwith packMotives motiveTypes Cs
+      let packedCs ← positions.mapMwith PProdN.packLambdas motiveTypes Cs
       let belowDict := mkAppN pre packedCs
       let belowDict := mkAppN belowDict finalArgs
       trace[Elab.definition.structural] "initial belowDict for {Cs}:{indentExpr belowDict}"
@@ -250,7 +250,7 @@ def mkBRecOnConst (recArgInfos : Array RecArgInfo) (positions : Positions)
   let brecOnAux := brecOnCons 0
   -- Infer the type of the packed motive arguments
   let packedMotiveTypes ← inferArgumentTypesN indGroup.numMotives brecOnAux
-  let packedMotives ← positions.mapMwith packMotives packedMotiveTypes motives
+  let packedMotives ← positions.mapMwith PProdN.packLambdas packedMotiveTypes motives
 
   return fun n => mkAppN (brecOnCons n) packedMotives
 
@@ -289,12 +289,11 @@ def mkBrecOnApp (positions : Positions) (fnIdx : Nat) (brecOnConst : Nat → Exp
     let brecOn := brecOnConst recArgInfo.indIdx
     let brecOn := mkAppN brecOn indexMajorArgs
     let packedFTypes ← inferArgumentTypesN positions.size brecOn
-    let packedFArgs ← positions.mapMwith packFArgs packedFTypes FArgs
+    let packedFArgs ← positions.mapMwith PProdN.mkLambdas packedFTypes FArgs
     let brecOn := mkAppN brecOn packedFArgs
     let some poss := positions.find? (·.contains fnIdx)
       | throwError "mkBrecOnApp: Could not find {fnIdx} in {positions}"
-    let brecOn ← if poss.size = 1 then pure brecOn else
-      mkPProdProjN (poss.getIdx? fnIdx).get! brecOn
+    let brecOn ← PProdN.proj poss.size (poss.getIdx? fnIdx).get! brecOn
     mkLambdaFVars ys (mkAppN brecOn otherArgs)
 
 end Lean.Elab.Structural
diff --git a/src/Lean/Elab/PreDefinition/Structural/FunPacker.lean b/src/Lean/Elab/PreDefinition/Structural/FunPacker.lean
deleted file mode 100644
index 7ef1262313b0..000000000000
--- a/src/Lean/Elab/PreDefinition/Structural/FunPacker.lean
+++ /dev/null
@@ -1,126 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joachim Breitner
--/
-prelude
-import Lean.Meta.InferType
-
-/-!
-This module contains the logic that packs the motives and FArgs of multiple functions into one,
-to allow structural mutual recursion where the number of functions is not exactly the same
-as the number of inductive data types in the mutual inductive group.
-
-The private helper functions related to `PProd` here should at some point be moved to their own
-module, so that they can be used elsewhere (e.g. `FunInd`), and possibly unified with the similar
-constructions for well-founded recursion (see `ArgsPacker` module).
--/
-
-namespace Lean.Elab.Structural
-open Meta
-
-private def mkPUnit : Level → Expr
-  | .zero => .const ``True []
-  | lvl   => .const ``PUnit [lvl]
-
-private def mkPProd (e1 e2 : Expr) : MetaM Expr := do
-  let lvl1 ← getLevel e1
-  let lvl2 ← getLevel e2
-  if lvl1 matches .zero && lvl2 matches .zero then
-    return mkApp2 (.const `And []) e1 e2
-  else
-    return mkApp2 (.const ``PProd [lvl1, lvl2]) e1 e2
-
-private def mkNProd (lvl : Level) (es : Array Expr) : MetaM Expr :=
-  es.foldrM (init := mkPUnit lvl) mkPProd
-
-private def mkPUnitMk : Level → Expr
-  | .zero => .const ``True.intro []
-  | lvl   => .const ``PUnit.unit [lvl]
-
-private def mkPProdMk (e1 e2 : Expr) : MetaM Expr := do
-  let t1 ← inferType e1
-  let t2 ← inferType e2
-  let lvl1 ← getLevel t1
-  let lvl2 ← getLevel t2
-  if lvl1 matches .zero && lvl2 matches .zero then
-    return mkApp4 (.const ``And.intro []) t1 t2 e1 e2
-  else
-    return mkApp4 (.const ``PProd.mk [lvl1, lvl2]) t1 t2 e1 e2
-
-private def mkNProdMk (lvl : Level) (es : Array Expr) : MetaM Expr :=
-  es.foldrM (init := mkPUnitMk lvl) mkPProdMk
-
-/-- `PProd.fst` or `And.left` (as projections) -/
-private def mkPProdFst (e : Expr) : MetaM Expr := do
-  let t ← whnf (← inferType e)
-  match_expr t with
-  | PProd _ _ => return .proj ``PProd 0 e
-  | And _ _ =>   return .proj ``And 0 e
-  | _ => throwError "Cannot project .1 out of{indentExpr e}\nof type{indentExpr t}"
-
-/-- `PProd.snd` or `And.right` (as projections) -/
-private def mkPProdSnd (e : Expr) : MetaM Expr := do
-  let t ← whnf (← inferType e)
-  match_expr t with
-  | PProd _ _ => return .proj ``PProd 1 e
-  | And _ _ =>   return .proj ``And 1 e
-  | _ => throwError "Cannot project .2 out of{indentExpr e}\nof type{indentExpr t}"
-
-/-- Given a proof of `P₁ ∧ … ∧ Pᵢ ∧ … ∧ Pₙ ∧ True`, return the proof of `Pᵢ` -/
-def mkPProdProjN (i : Nat) (e : Expr) : MetaM Expr := do
-  let mut value := e
-  for _ in [:i] do
-      value ← mkPProdSnd value
-  value ← mkPProdFst value
-  return value
-
-/--
-Combines motives from different functions that recurse on the same parameter type into a single
-function returning a `PProd` type.
-
-For example
-```
-packMotives (Nat → Sort u) #[(fun (n : Nat) => Nat), (fun (n : Nat) => Fin n -> Fin n )]
-```
-will return
-```
-fun (n : Nat) (PProd Nat (Fin n → Fin n))
-```
-
-It is the identity if `motives.size = 1`.
-
-It returns a dummy motive `(xs : ) → PUnit` or `(xs : … ) → True` if no motive is given.
-(this is the reason we need the expected type in the `motiveType` parameter).
-
--/
-def packMotives (motiveType : Expr) (motives : Array Expr) : MetaM Expr := do
-  if motives.size = 1 then
-    return motives[0]!
-  trace[Elab.definition.structural] "packing Motives\nexpected: {motiveType}\nmotives: {motives}"
-  forallTelescope motiveType fun xs sort => do
-    unless sort.isSort do
-      throwError "packMotives: Unexpected motiveType {motiveType}"
-    -- NB: Use beta, not instantiateLambda; when constructing the belowDict below
-    -- we pass `C`, a plain FVar, here
-    let motives := motives.map (·.beta xs)
-    let packedMotives ← mkNProd sort.sortLevel! motives
-    mkLambdaFVars xs packedMotives
-
-/--
-Combines the F-args from different functions that recurse on the same parameter type into a single
-function returning a `PProd` value. See `packMotives`
-
-It is the identity if `motives.size = 1`.
--/
-def packFArgs (FArgType : Expr) (FArgs : Array Expr) : MetaM Expr := do
-  if FArgs.size = 1 then
-    return FArgs[0]!
-  forallTelescope FArgType fun xs body => do
-    let lvl ← getLevel body
-    let FArgs := FArgs.map (·.beta xs)
-    let packedFArgs ← mkNProdMk lvl FArgs
-    mkLambdaFVars xs packedFArgs
-
-
-end Lean.Elab.Structural
diff --git a/src/Lean/Elab/PreDefinition/TerminationHint.lean b/src/Lean/Elab/PreDefinition/TerminationHint.lean
index 7a4a94d11e57..757d388d55a0 100644
--- a/src/Lean/Elab/PreDefinition/TerminationHint.lean
+++ b/src/Lean/Elab/PreDefinition/TerminationHint.lean
@@ -57,18 +57,18 @@ structure TerminationHints where
 
 def TerminationHints.none : TerminationHints := ⟨.missing, .none, .none, .none, 0⟩
 
-/-- Logs warnings when the `TerminationHints` are present.  -/
+/-- Logs warnings when the `TerminationHints` are unexpectedly present.  -/
 def TerminationHints.ensureNone (hints : TerminationHints) (reason : String) : CoreM Unit := do
   match hints.terminationBy??, hints.terminationBy?, hints.decreasingBy? with
   | .none, .none, .none => pure ()
   | .none, .none, .some dec_by =>
-    logErrorAt dec_by.ref m!"unused `decreasing_by`, function is {reason}"
+    logWarningAt dec_by.ref m!"unused `decreasing_by`, function is {reason}"
   | .some term_by?, .none, .none =>
-    logErrorAt term_by? m!"unused `termination_by?`, function is {reason}"
+    logWarningAt term_by? m!"unused `termination_by?`, function is {reason}"
   | .none, .some term_by, .none =>
-    logErrorAt term_by.ref m!"unused `termination_by`, function is {reason}"
+    logWarningAt term_by.ref m!"unused `termination_by`, function is {reason}"
   | _, _, _ =>
-    logErrorAt hints.ref m!"unused termination hints, function is {reason}"
+    logWarningAt hints.ref m!"unused termination hints, function is {reason}"
 
 /-- True if any form of termination hint is present. -/
 def TerminationHints.isNotNone (hints : TerminationHints) : Bool :=
diff --git a/src/Lean/Meta/AppBuilder.lean b/src/Lean/Meta/AppBuilder.lean
index 41a7ea2f1f1a..898b59abee51 100644
--- a/src/Lean/Meta/AppBuilder.lean
+++ b/src/Lean/Meta/AppBuilder.lean
@@ -665,27 +665,6 @@ def mkIffOfEq (h : Expr) : MetaM Expr := do
   else
     mkAppM ``Iff.of_eq #[h]
 
-/--
-Given proofs of `P₁`, …, `Pₙ`, returns a proof of `P₁ ∧ … ∧ Pₙ`.
-If `n = 0` returns a proof of `True`.
-If `n = 1` returns the proof of `P₁`.
--/
-def mkAndIntroN : Array Expr → MetaM Expr
-| #[] => return mkConst ``True.intro []
-| #[e] => return e
-| es => es.foldrM (start := es.size - 1) (fun a b => mkAppM ``And.intro #[a,b]) es.back
-
-
-/-- Given a proof of `P₁ ∧ … ∧ Pᵢ ∧ … ∧ Pₙ`, return the proof of `Pᵢ` -/
-def mkProjAndN (n i : Nat) (e : Expr) : Expr := Id.run do
-  let mut value := e
-  for _ in [:i] do
-      value := mkProj ``And 1 value
-  if i + 1 < n then
-      value := mkProj ``And 0 value
-  return value
-
-
 builtin_initialize do
   registerTraceClass `Meta.appBuilder
   registerTraceClass `Meta.appBuilder.result (inherited := true)
diff --git a/src/Lean/Meta/ArgsPacker.lean b/src/Lean/Meta/ArgsPacker.lean
index d871e97c972d..2b2b26d4711c 100644
--- a/src/Lean/Meta/ArgsPacker.lean
+++ b/src/Lean/Meta/ArgsPacker.lean
@@ -6,6 +6,7 @@ Authors: Joachim Breitner
 
 prelude
 import Lean.Meta.AppBuilder
+import Lean.Meta.PProdN
 import Lean.Meta.ArgsPacker.Basic
 
 /-!
@@ -518,7 +519,7 @@ def curry (argsPacker : ArgsPacker) (e : Expr) : MetaM Expr := do
   let mut es := #[]
   for i in [:argsPacker.numFuncs] do
     es := es.push (← argsPacker.curryProj e i)
-  mkAndIntroN es
+  PProdN.mk 0 es
 
 /--
 Given type `(a ⊗' b ⊕' c ⊗' d) → e`, brings `a → b → e` and `c → d → e`
@@ -533,7 +534,7 @@ where
   | [], acc => k acc
   | t::ts, acc => do
     let name := if argsPacker.numFuncs = 1 then name else .mkSimple s!"{name}{acc.size+1}"
-    withLocalDecl name .default t fun x => do
+    withLocalDeclD name t fun x => do
       go ts (acc.push x)
 
 /--
diff --git a/src/Lean/Meta/Constructions/BRecOn.lean b/src/Lean/Meta/Constructions/BRecOn.lean
index bee7244a54d3..52e4297d78fa 100644
--- a/src/Lean/Meta/Constructions/BRecOn.lean
+++ b/src/Lean/Meta/Constructions/BRecOn.lean
@@ -8,67 +8,18 @@ import Lean.Meta.InferType
 import Lean.AuxRecursor
 import Lean.AddDecl
 import Lean.Meta.CompletionName
+import Lean.Meta.PProdN
 
 namespace Lean
 open Meta
 
-section PProd
-
-/--!
-Helpers to construct types and values of `PProd` and project out of them, set up to use `And`
-instead of `PProd` if the universes allow. Maybe be extracted into a Utils module when useful
-elsewhere.
--/
-
-private def mkPUnit : Level → Expr
-  | .zero => .const ``True []
-  | lvl   => .const ``PUnit [lvl]
-
-private def mkPProd (e1 e2 : Expr) : MetaM Expr := do
-  let lvl1 ← getLevel e1
-  let lvl2 ← getLevel e2
-  if lvl1 matches .zero && lvl2 matches .zero then
-    return mkApp2 (.const `And []) e1 e2
-  else
-    return mkApp2 (.const ``PProd [lvl1, lvl2]) e1 e2
-
-private def mkNProd (lvl : Level) (es : Array Expr) : MetaM Expr :=
-  es.foldrM (init := mkPUnit lvl) mkPProd
-
-private def mkPUnitMk : Level → Expr
-  | .zero => .const ``True.intro []
-  | lvl   => .const ``PUnit.unit [lvl]
-
-private def mkPProdMk (e1 e2 : Expr) : MetaM Expr := do
-  let t1 ← inferType e1
-  let t2 ← inferType e2
-  let lvl1 ← getLevel t1
-  let lvl2 ← getLevel t2
-  if lvl1 matches .zero && lvl2 matches .zero then
-    return mkApp4 (.const ``And.intro []) t1 t2 e1 e2
-  else
-    return mkApp4 (.const ``PProd.mk [lvl1, lvl2]) t1 t2 e1 e2
-
-private def mkNProdMk (lvl : Level) (es : Array Expr) : MetaM Expr :=
-  es.foldrM (init := mkPUnitMk lvl) mkPProdMk
-
-/-- `PProd.fst` or `And.left` (as projections) -/
-private def mkPProdFst (e : Expr) : MetaM Expr := do
-  let t ← whnf (← inferType e)
-  match_expr t with
-  | PProd _ _ => return .proj ``PProd 0 e
-  | And _ _ =>   return .proj ``And 0 e
-  | _ => throwError "Cannot project .1 out of{indentExpr e}\nof type{indentExpr t}"
-
-/-- `PProd.snd` or `And.right` (as projections) -/
-private def mkPProdSnd (e : Expr) : MetaM Expr := do
-  let t ← whnf (← inferType e)
-  match_expr t with
-  | PProd _ _ => return .proj ``PProd 1 e
-  | And _ _ =>   return .proj ``And 1 e
-  | _ => throwError "Cannot project .2 out of{indentExpr e}\nof type{indentExpr t}"
-
-end PProd
+/-- Transforms `e : xᵢ → (t₁ ×' t₂)` into `(xᵢ → t₁) ×' (xᵢ → t₂) -/
+private def etaPProd (xs : Array Expr) (e : Expr) : MetaM Expr := do
+  if xs.isEmpty then return e
+  let r := mkAppN e xs
+  let r₁ ← mkLambdaFVars xs (← mkPProdFst r)
+  let r₂ ← mkLambdaFVars xs (← mkPProdSnd r)
+  mkPProdMk r₁ r₂
 
 /--
 If `minorType` is the type of a minor premies of a recursor, such as
@@ -91,7 +42,7 @@ private def buildBelowMinorPremise (rlvl : Level) (motives : Array Expr) (minorT
 where
   ibelow := rlvl matches .zero
   go (prods : Array Expr) : List Expr → MetaM Expr
-  | [] => mkNProd rlvl prods
+  | [] => PProdN.pack rlvl prods
   | arg::args => do
     let argType ← inferType arg
     forallTelescope argType fun arg_args arg_type => do
@@ -243,7 +194,7 @@ private def buildBRecOnMinorPremise (rlvl : Level) (motives : Array Expr)
   forallTelescope minorType fun minor_args minor_type => do
     let rec go (prods : Array Expr) : List Expr → MetaM Expr
       | [] => minor_type.withApp fun minor_type_fn minor_type_args => do
-          let b ← mkNProdMk rlvl prods
+          let b ← PProdN.mk rlvl prods
           let .some ⟨idx, _⟩ := motives.indexOf? minor_type_fn
             | throwError m!"Did not find {minor_type} in {motives}"
           mkPProdMk (mkAppN fs[idx]! (minor_type_args.push b)) b
@@ -256,14 +207,8 @@ private def buildBRecOnMinorPremise (rlvl : Level) (motives : Array Expr)
               let type' ← mkForallFVars arg_args
                 (← mkPProd arg_type (mkAppN belows[idx]! arg_type_args) )
               withLocalDeclD name type' fun arg' => do
-                if arg_args.isEmpty then
-                  mkLambdaFVars #[arg'] (← go (prods.push arg') args)
-                else
-                  let r := mkAppN arg' arg_args
-                  let r₁ ← mkLambdaFVars arg_args (← mkPProdFst r)
-                  let r₂ ← mkLambdaFVars arg_args (← mkPProdSnd r)
-                  let r ← mkPProdMk r₁ r₂
-                  mkLambdaFVars #[arg'] (← go (prods.push r) args)
+                let r ← etaPProd arg_args arg'
+                mkLambdaFVars #[arg'] (← go (prods.push r) args)
             else
               mkLambdaFVars #[arg] (← go prods args)
     go #[] minor_args.toList
diff --git a/src/Lean/Meta/PProdN.lean b/src/Lean/Meta/PProdN.lean
new file mode 100644
index 000000000000..fcde4d4a46fb
--- /dev/null
+++ b/src/Lean/Meta/PProdN.lean
@@ -0,0 +1,145 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joachim Breitner
+-/
+
+prelude
+import Lean.Meta.InferType
+
+/-!
+This module provides functios to pack and unpack values using nested `PProd` or `And`,
+as used in the `.below` construction, in the `.brecOn` construction for mutual recursion and
+and the `mutual_induct` construction.
+
+It uses `And` (equivalent to `PProd.{0}` when possible).
+
+The nesting is `t₁ ×' (t₂ ×' t₃)`, not `t₁ ×' (t₂ ×' (t₃ ×' PUnit))`. This is more readable,
+slightly shorter, and means that the packing is the identity if `n=1`, which we rely on in some
+places. It comes at the expense that hat projection needs to know `n`.
+
+Packing an empty list uses `True` or `PUnit` depending on the given `lvl`.
+
+Also see `Lean.Meta.ArgsPacker` for a similar module for `PSigma` and `PSum`, used by well-founded recursion.
+-/
+
+
+namespace Lean.Meta
+
+/-- Given types `t₁` and `t₂`, produces `t₁ ×' t₂` (or `t₁ ∧ t₂` if the universes allow) -/
+def mkPProd (e1 e2 : Expr) : MetaM Expr := do
+  let lvl1 ← getLevel e1
+  let lvl2 ← getLevel e2
+  if lvl1 matches .zero && lvl2 matches .zero then
+    return mkApp2 (.const `And []) e1 e2
+  else
+    return mkApp2 (.const ``PProd [lvl1, lvl2]) e1 e2
+
+/-- Given values of typs `t₁` and `t₂`, produces value of type `t₁ ×' t₂` (or `t₁ ∧ t₂` if the universes allow) -/
+def mkPProdMk (e1 e2 : Expr) : MetaM Expr := do
+  let t1 ← inferType e1
+  let t2 ← inferType e2
+  let lvl1 ← getLevel t1
+  let lvl2 ← getLevel t2
+  if lvl1 matches .zero && lvl2 matches .zero then
+    return mkApp4 (.const ``And.intro []) t1 t2 e1 e2
+  else
+    return mkApp4 (.const ``PProd.mk [lvl1, lvl2]) t1 t2 e1 e2
+
+/-- `PProd.fst` or `And.left` (using `.proj`) -/
+def mkPProdFst (e : Expr) : MetaM Expr := do
+  let t ← whnf (← inferType e)
+  match_expr t with
+  | PProd _ _ => return .proj ``PProd 0 e
+  | And _ _ => return .proj ``And 0 e
+  | _ => panic! "mkPProdFst: cannot handle{indentExpr e}\nof type{indentExpr t}"
+
+/-- `PProd.snd` or `And.right` (using `.proj`) -/
+def mkPProdSnd (e : Expr) : MetaM Expr := do
+  let t ← whnf (← inferType e)
+  match_expr t with
+  | PProd _ _ => return .proj ``PProd 1 e
+  | And _ _ => return .proj ``And 1 e
+  | _ => panic! "mkPProdSnd: cannot handle{indentExpr e}\nof type{indentExpr t}"
+
+
+
+namespace PProdN
+
+/-- Given types `tᵢ`, produces `t₁ ×' t₂ ×' t₃` -/
+def pack (lvl : Level) (xs : Array Expr) : MetaM Expr := do
+  if xs.size = 0 then
+    if lvl matches .zero then return .const ``True []
+                         else return .const ``PUnit [lvl]
+  let xBack := xs.back
+  xs.pop.foldrM mkPProd xBack
+
+/-- Given values `xᵢ` of type `tᵢ`, produces value of type `t₁ ×' t₂ ×' t₃` -/
+def mk (lvl : Level) (xs : Array Expr) : MetaM Expr := do
+  if xs.size = 0 then
+    if lvl matches .zero then return .const ``True.intro []
+                         else return .const ``PUnit.unit [lvl]
+  let xBack := xs.back
+  xs.pop.foldrM mkPProdMk xBack
+
+/-- Given a value of type `t₁ ×' … ×' tᵢ ×' … ×' tₙ`, return a value of type `tᵢ` -/
+def proj (n i : Nat) (e : Expr) : MetaM Expr := do
+  let mut value := e
+  for _ in [:i] do
+      value ← mkPProdSnd value
+  if i+1 < n then
+    mkPProdFst value
+  else
+    pure value
+
+
+
+/--
+Packs multiple type-forming lambda expressions taking the same parameters using `PProd`.
+
+The parameter `type` is the common type of the these expressions
+
+For example
+```
+packLambdas (Nat → Sort u) #[(fun (n : Nat) => Nat), (fun (n : Nat) => Fin n -> Fin n )]
+```
+will return
+```
+fun (n : Nat) => (Nat ×' (Fin n → Fin n))
+```
+
+It is the identity if `es.size = 1`.
+
+It returns a dummy motive `(xs : ) → PUnit` or `(xs : … ) → True` if no expressions are given.
+(this is the reason we need the expected type in the `type` parameter).
+
+-/
+def packLambdas (type : Expr) (es : Array Expr) : MetaM Expr := do
+  if es.size = 1 then
+    return es[0]!
+  forallTelescope type fun xs sort => do
+    assert! sort.isSort
+    -- NB: Use beta, not instantiateLambda; when constructing the belowDict below
+    -- we pass `C`, a plain FVar, here
+    let es' := es.map (·.beta xs)
+    let packed ← PProdN.pack sort.sortLevel! es'
+    mkLambdaFVars xs packed
+
+/--
+The value analogue to `PProdN.packLambdas`.
+
+It is the identity if `es.size = 1`.
+-/
+def mkLambdas (type : Expr) (es : Array Expr) : MetaM Expr := do
+  if es.size = 1 then
+    return es[0]!
+  forallTelescope type fun xs body => do
+    let lvl ← getLevel body
+    let es' := es.map (·.beta xs)
+    let packed ← PProdN.mk lvl es'
+    mkLambdaFVars xs packed
+
+
+end PProdN
+
+end Lean.Meta
diff --git a/src/Lean/Meta/Tactic/FunInd.lean b/src/Lean/Meta/Tactic/FunInd.lean
index e6eb1f96f52c..8cff7d5e0d41 100644
--- a/src/Lean/Meta/Tactic/FunInd.lean
+++ b/src/Lean/Meta/Tactic/FunInd.lean
@@ -12,8 +12,11 @@ import Lean.Meta.Tactic.Cleanup
 import Lean.Meta.Tactic.Subst
 import Lean.Meta.Injective -- for elimOptParam
 import Lean.Meta.ArgsPacker
+import Lean.Meta.PProdN
 import Lean.Elab.PreDefinition.WF.Eqns
 import Lean.Elab.PreDefinition.Structural.Eqns
+import Lean.Elab.PreDefinition.Structural.IndGroupInfo
+import Lean.Elab.PreDefinition.Structural.FindRecArg
 import Lean.Elab.Command
 import Lean.Meta.Tactic.ElimInfo
 
@@ -188,21 +191,6 @@ def removeLamda {n} [MonadLiftT MetaM n] [MonadError n] [MonadNameGenerator n] [
   let b := b.instantiate1 (.fvar x)
   k x b
 
-/-- `PProd.fst` or `And.left` -/
-def mkFst (e : Expr) : MetaM Expr := do
-  let t ← whnf (← inferType e)
-  match_expr t with
-  | PProd t₁ t₂ => return mkApp3 (.const ``PProd.fst t.getAppFn.constLevels!) t₁ t₂ e
-  | And t₁ t₂ => return mkApp3 (.const ``And.left []) t₁ t₂ e
-  | _ => throwError "Cannot project out of{indentExpr e}\nof type{indentExpr t}"
-
-/-- `PProd.snd` or `And.right` -/
-def mkSnd (e : Expr) : MetaM Expr := do
-  let t ← whnf (← inferType e)
-  match_expr t with
-  | PProd t₁ t₂ => return mkApp3 (.const ``PProd.snd t.getAppFn.constLevels!) t₁ t₂ e
-  | And t₁ t₂ => return mkApp3 (.const ``And.right []) t₁ t₂ e
-  | _ => throwError "Cannot project out of{indentExpr e}\nof type{indentExpr t}"
 
 /--
 A monad to help collecting inductive hypothesis.
@@ -310,7 +298,7 @@ partial def foldAndCollect (oldIH newIH : FVarId) (isRecCall : Expr → Option E
               forallBoundedTelescope altType (some 1) fun newIH' _goal' => do
                 let #[newIH'] := newIH' | unreachable!
                 let altIHs ← M.exec <| foldAndCollect oldIH' newIH'.fvarId! isRecCall alt
-                let altIH ← mkAndIntroN altIHs
+                let altIH ← PProdN.mk 0 altIHs
                 mkLambdaFVars #[newIH'] altIH)
           (onRemaining := fun _ => pure #[mkFVar newIH])
         let ihMatcherApp'' ← ihMatcherApp'.inferMatchType
@@ -328,11 +316,6 @@ partial def foldAndCollect (oldIH newIH : FVarId) (isRecCall : Expr → Option E
           (onRemaining := fun _ => pure #[])
         return matcherApp'.toExpr
 
-    -- These projections can be type changing, so re-infer their type arguments
-    match_expr e with
-    | PProd.fst _ _ e => mkFst (← foldAndCollect oldIH newIH isRecCall e)
-    | PProd.snd _ _ e => mkSnd (← foldAndCollect oldIH newIH isRecCall e)
-    | _ =>
 
     if e.getAppArgs.any (·.isFVarOf oldIH) then
       -- Sometimes Fix.lean abstracts over oldIH in a proof definition.
@@ -371,6 +354,10 @@ partial def foldAndCollect (oldIH newIH : FVarId) (isRecCall : Expr → Option E
     | .mdata m b =>
       pure <| .mdata m (← foldAndCollect oldIH newIH isRecCall b)
 
+    -- These projections can be type changing (to And), so re-infer their type arguments
+    | .proj ``PProd 0 e => mkPProdFst (← foldAndCollect oldIH newIH isRecCall e)
+    | .proj ``PProd 1 e => mkPProdSnd (← foldAndCollect oldIH newIH isRecCall e)
+
     | .proj t i e =>
       pure <| .proj t i (← foldAndCollect oldIH newIH isRecCall e)
 
@@ -417,14 +404,13 @@ def assertIHs (vals : Array Expr) (mvarid : MVarId) : MetaM MVarId := do
 
 
 /--
-Substitutes equations, but makes sure to only substitute variables introduced after the motive
-as the motive could depend on anything before, and `substVar` would happily drop equations
-about these fixed parameters.
+Substitutes equations, but makes sure to only substitute variables introduced after the motives
+(given by the index) as the motive could depend on anything before, and `substVar` would happily
+drop equations about these fixed parameters.
 -/
-def substVarAfter (mvarId : MVarId) (x : FVarId) : MetaM MVarId := do
+def substVarAfter (mvarId : MVarId) (index : Nat) : MetaM MVarId := do
   mvarId.withContext do
     let mut mvarId := mvarId
-    let index := (← x.getDecl).index
     for localDecl in (← getLCtx) do
       if localDecl.index > index then
         mvarId ← trySubstVar mvarId localDecl.fvarId
@@ -528,6 +514,20 @@ partial def buildInductionBody (toClear toPreserve : Array FVarId) (goal : Expr)
       mkLambdaFVars #[h] f'
     let u ← getLevel goal
     return mkApp5 (mkConst ``dite [u]) goal c' h' t' f'
+
+  | _ =>
+
+  -- we look in to `PProd.mk`, as it occurs in the mutual structural recursion construction
+  match_expr goal with
+  | And goal₁ goal₂ => match_expr e with
+    | PProd.mk _α _β e₁ e₂ =>
+      let e₁' ← buildInductionBody toClear toPreserve goal₁ oldIH newIH isRecCall e₁
+      let e₂' ← buildInductionBody toClear toPreserve goal₂ oldIH newIH isRecCall e₂
+      return mkApp4 (.const ``And.intro []) goal₁ goal₂ e₁' e₂'
+    | _ =>
+      throwError "Goal is PProd, but expression is:{indentExpr e}"
+  | True =>
+    return .const ``True.intro []
   | _ =>
 
   -- match and casesOn application cause case splitting
@@ -586,7 +586,7 @@ partial def buildInductionBody (toClear toPreserve : Array FVarId) (goal : Expr)
 /--
 Given an expression `e` with metavariables
 * collects all these meta-variables,
-* lifts them to the current context by reverting all local declarations up to `x`
+* lifts them to the current context by reverting all local declarations after index `index`
 * introducing a local variable for each of the meta variable
 * assigning that local variable to the mvar
 * and finally lambda-abstracting over these new local variables.
@@ -600,14 +600,18 @@ be used anymore.
 We are not using `mkLambdaFVars` on mvars directly, nor `abstractMVars`, as these at the moment
 do not handle delayed assignemnts correctly.
 -/
-def abstractIndependentMVars (mvars : Array MVarId) (x : FVarId) (e : Expr) : MetaM Expr := do
+def abstractIndependentMVars (mvars : Array MVarId) (index : Nat) (e : Expr) : MetaM Expr := do
+  trace[Meta.FunInd] "abstractIndependentMVars, to revert after {index}, original mvars: {mvars}"
   let mvars ← mvars.mapM fun mvar => do
-    let mvar ← substVarAfter mvar x
-    let (_, mvar) ← mvar.revertAfter x
-    pure mvar
+    let mvar ← substVarAfter mvar index
+    mvar.withContext do
+      let fvarIds := (← getLCtx).foldl (init := #[]) (start := index+1) fun fvarIds decl => fvarIds.push decl.fvarId
+      let (_, mvar) ← mvar.revert fvarIds
+      pure mvar
+  trace[Meta.FunInd] "abstractIndependentMVars, reverted mvars: {mvars}"
   let decls := mvars.mapIdx fun i mvar =>
-    (.mkSimple s!"case{i.val+1}", .default, (fun _ => mvar.getType))
-  Meta.withLocalDecls decls fun xs => do
+    (.mkSimple s!"case{i.val+1}", (fun _ => mvar.getType))
+  Meta.withLocalDeclsD decls fun xs => do
       for mvar in mvars, x in xs do
         mvar.assign x
       mkLambdaFVars xs (← instantiateMVars e)
@@ -662,7 +666,7 @@ def deriveUnaryInduction (name : Name) : MetaM Name := do
               mkLambdaFVars (targets.push genIH) (← mkLambdaFVars extraParams body')
         let e' := mkApp2 e' body' target
         let e' ← mkLambdaFVars #[target] e'
-        let e' ← abstractIndependentMVars mvars motive.fvarId! e'
+        let e' ← abstractIndependentMVars mvars (← motive.fvarId!.getDecl).index e'
         let e' ← mkLambdaFVars #[motive] e'
 
         -- We could pass (usedOnly := true) below, and get nicer induction principles that
@@ -690,6 +694,24 @@ def deriveUnaryInduction (name : Name) : MetaM Name := do
     { name := inductName, levelParams := us, type := eTyp, value := e' }
   return inductName
 
+/--
+Given `foo.mutual_induct`, defined `foo.induct`, `bar.induct` etc.
+Used for well-founded and structural recursion.
+-/
+def projectMutualInduct (names : Array Name) (mutualInduct : Name) : MetaM Unit := do
+  let ci ← getConstInfo mutualInduct
+  let levelParams := ci.levelParams
+
+  for name in names, idx in [:names.size] do
+    let inductName := .append name `induct
+    unless ← hasConst inductName do
+      let value ← forallTelescope ci.type fun xs _body => do
+        let value := .const ci.name (levelParams.map mkLevelParam)
+        let value := mkAppN value xs
+        let value ← PProdN.proj names.size idx value
+        mkLambdaFVars xs value
+      let type ← inferType value
+      addDecl <| Declaration.thmDecl { name := inductName, levelParams, type, value }
 
 /--
 In the type of `value`, reduces
@@ -794,22 +816,11 @@ def unpackMutualInduction (eqnInfo : WF.EqnInfo) (unaryInductName : Name) : Meta
     { name := inductName, levelParams := ci.levelParams, type, value }
   return inductName
 
+
 /-- Given `foo._unary.induct`, define `foo.mutual_induct` and then `foo.induct`, `bar.induct`, … -/
 def deriveUnpackedInduction (eqnInfo : WF.EqnInfo) (unaryInductName : Name): MetaM Unit := do
   let unpackedInductName ← unpackMutualInduction eqnInfo unaryInductName
-  let ci ← getConstInfo unpackedInductName
-  let levelParams := ci.levelParams
-
-  for name in eqnInfo.declNames, idx in [:eqnInfo.declNames.size] do
-    let inductName := .append name `induct
-    unless ← hasConst inductName do
-      let value ← forallTelescope ci.type fun xs _body => do
-        let value := .const ci.name (levelParams.map mkLevelParam)
-        let value := mkAppN value xs
-        let value := mkProjAndN eqnInfo.declNames.size idx value
-        mkLambdaFVars xs value
-      let type ← inferType value
-      addDecl <| Declaration.thmDecl { name := inductName, levelParams, type, value }
+  projectMutualInduct eqnInfo.declNames unpackedInductName
 
 def stripPProdProjs (e : Expr) : Expr :=
   match e with
@@ -817,93 +828,198 @@ def stripPProdProjs (e : Expr) : Expr :=
   | .proj ``And _ e' => stripPProdProjs e'
   | e => e
 
+def withLetDecls {α} (name : Name) (ts : Array Expr) (es : Array Expr) (k : Array Expr → MetaM α) : MetaM α := do
+  assert! es.size = ts.size
+  go 0 #[]
+where
+  go (i : Nat) (acc : Array Expr) := do
+    if h : i < es.size then
+      let n := if es.size = 1 then name else name.appendIndexAfter (i + 1)
+      withLetDecl n ts[i]! es[i] fun x => go (i+1) (acc.push x)
+    else
+      k acc
+
 /--
-Given a recursive definition `foo` defined via structural recursion, derive `foo.induct` for it. See
-module doc for details.
+Given a recursive definition `foo` defined via structural recursion, derive `foo.mutual_induct`,
+if needed, and `foo.induct` for all functions in the group.
+See module doc for details.
  -/
-def deriveStructuralInduction (name : Name) : MetaM Unit := do
-  let inductName := .append name `induct
-  if ← hasConst inductName then return
-
-  let info ← getConstInfoDefn name
-
-  let varNames ← forallTelescope info.type fun xs _ => xs.mapM (·.fvarId!.getUserName)
-
-  let e' ← lambdaTelescope info.value fun params body => (stripPProdProjs body).withApp fun f args => do
-    MatcherApp.withUserNames params varNames do
-      unless isBRecOnRecursor (← getEnv) f.constName! do
-        throwError "Body of strucually recursive function not as expected:{indentExpr body}"
-      -- Bail out on mutual or nested inductives
-      let .str indName _ := f.constName! | unreachable!
+def deriveInductionStructural (names : Array Name) (numFixed : Nat) : MetaM Unit := do
+  let infos ← names.mapM getConstInfoDefn
+  -- First open up the fixed parameters everywhere
+  let e' ← lambdaBoundedTelescope infos[0]!.value numFixed fun xs _ => do
+    -- Now look at the body of an arbitrary of the functions (they are essentially the same
+    -- up to the final projections)
+    let body ← instantiateLambda infos[0]!.value xs
+
+    lambdaTelescope body fun ys body => do
+      -- The body is of the form (brecOn … ).2.2.1 extra1 extra2 etc; ignore the
+      -- projection here
+      let f' := body.getAppFn
+      let body' := stripPProdProjs f'
+      let f := body'.getAppFn
+      let args := body'.getAppArgs ++ body.getAppArgs
+
+      let body := stripPProdProjs body
+      let .const brecOnName us := f |
+        throwError "{infos[0]!.name}: unexpected body:{indentExpr infos[0]!.value}"
+      unless isBRecOnRecursor (← getEnv) brecOnName do
+        throwError "{infos[0]!.name}: expected .brecOn application, found:{indentExpr body}"
+
+      let .str indName _ := brecOnName | unreachable!
       let indInfo ← getConstInfoInduct indName
-      if indInfo.numTypeFormers > 1 then
-        throwError "functional induction: cannot handle mutual or nested inductives"
-
-      let elimInfo ← getElimExprInfo f
-      let targets : Array Expr := elimInfo.targetsPos.map (args[·]!)
-      let body := args[elimInfo.motivePos + 1 + elimInfo.targetsPos.size]!
-      let extraArgs : Array Expr := args[elimInfo.motivePos + 1 + elimInfo.targetsPos.size + 1:]
-
-      let fixedParams := params.filter fun x => !(targets.contains x || extraArgs.contains x)
-      let varyingParams := params.filter fun x => targets.contains x || extraArgs.contains x
-      unless params == fixedParams ++ varyingParams do
-        throwError "functional induction: unexpected order of fixed and varying parameters:{indentExpr body}"
-      unless 1 ≤ f.constLevels!.length do
-        throwError "functional induction: unexpected recursor: {f} has no universe parameters"
-
-      let motiveType ← mkForallFVars varyingParams (.sort levelZero)
-      withLocalDecl `motive .default motiveType fun motive => do
-
-      let fn := mkAppN (.const name (info.levelParams.map mkLevelParam)) fixedParams
-      let isRecCall : Expr → Option Expr := fun e =>
-        if e.getAppNumArgs = varyingParams.size && e.getAppFn.isFVarOf motive.fvarId! then
-           mkAppN fn e.getAppArgs
-        else
-          none
-
-      -- Sometimes `brecOn` only supports eliminating to `Type u`, not `Sort `u`.
-      -- So just use `binductionOn` instead
-      let us := f.constLevels!.drop 1
-      let bInductionName := mkBInductionOnName indInfo.name
-      let value := mkAppN (.const bInductionName us) (args[:elimInfo.motivePos])
-      -- We may have to reorder the parameters for motive before passing it to brec
-      let brecMotive ← mkLambdaFVars targets
-        (← mkForallFVars extraArgs (mkAppN motive varyingParams))
-      let e' := mkAppN (mkApp value brecMotive) targets
-      check e'
-      let (body', mvars) ← M2.run do
-        forallTelescope (← inferType e').bindingDomain! fun xs goal => do
-          let arity := varyingParams.size + 1
-          if xs.size ≠ arity then
-            throwError "expected recursor argument to take {arity} parameters, got {xs}" else
-          let targets : Array Expr := xs[:targets.size]
-          let genIH := xs[targets.size]!
-          let extraParams := xs[targets.size+1:]
-          -- open body with the same arg
-          let body ← instantiateLambda body targets
-          removeLamda body fun oldIH body => do
-            let body ← instantiateLambda body extraParams
-            let body' ← buildInductionBody #[genIH.fvarId!] #[] goal oldIH genIH.fvarId! isRecCall body
-            if body'.containsFVar oldIH then
-              throwError m!"Did not fully eliminate {mkFVar oldIH} from induction principle body:{indentExpr body}"
-            mkLambdaFVars (targets.push genIH) (← mkLambdaFVars extraParams body')
-      let e' := mkApp e' body'
-      let e' := mkAppN e' extraArgs
-      let e' ← mkLambdaFVars varyingParams e'
-      let e' ← abstractIndependentMVars mvars motive.fvarId! e'
-      let e' ← mkLambdaFVars #[motive] e'
-
-      -- We could pass (usedOnly := true) below, and get nicer induction principles that
-      -- do do not mention odd unused parameters.
-      -- But the downside is that automatic instantiation of the principle (e.g. in a tactic
-      -- that derives them from an function application in the goal) is harder, as
-      -- one would have to infer or keep track of which parameters to pass.
-      -- So for now lets just keep them around.
-      let e' ← mkLambdaFVars (binderInfoForMVars := .default) fixedParams e'
-      instantiateMVars e'
+
+      -- we have a `.brecOn` application, so now figure out the length of the fixed prefix
+      -- we can use the recInfo for `.rec`, since `.brecOn` has a similar structure
+      let recInfo ← getConstInfoRec (mkRecName indName)
+      if args.size < recInfo.numParams + recInfo.numMotives + recInfo.numIndices + 1 + recInfo.numMotives then
+        throwError "insufficient arguments to .brecOn:{indentExpr body}"
+      let brecOnArgs    : Array Expr := args[:recInfo.numParams]
+      let _brecOnMotives : Array Expr := args[recInfo.numParams:recInfo.numParams + recInfo.numMotives]
+      let brecOnTargets : Array Expr := args[recInfo.numParams + recInfo.numMotives :
+        recInfo.numParams + recInfo.numMotives + recInfo.numIndices + 1]
+      let brecOnMinors  : Array Expr := args[recInfo.numParams + recInfo.numMotives + recInfo.numIndices + 1 :
+        recInfo.numParams + recInfo.numMotives + recInfo.numIndices + 1 + recInfo.numMotives]
+      let brecOnExtras  : Array Expr := args[ recInfo.numParams + recInfo.numMotives + recInfo.numIndices + 1 +
+        recInfo.numMotives:]
+      unless brecOnTargets.all (·.isFVar) do
+        throwError "the indices and major argument of the brecOn application are not variables:{indentExpr body}"
+      unless brecOnExtras.all (·.isFVar) do
+        throwError "the extra arguments to the the brecOn application are not variables:{indentExpr body}"
+      let lvl :: indLevels := us |throwError "Too few universe parameters in .brecOn application:{indentExpr body}"
+
+      let group : Structural.IndGroupInst := { Structural.IndGroupInfo.ofInductiveVal indInfo with
+        levels := indLevels, params := brecOnArgs }
+
+      -- We also need to know the number of indices of each type former, including the auxillary
+      -- type formers that do not have IndInfo. We can read it off the motives types of the recursor.
+      let numTargetss ← do
+        let aux := mkAppN (.const recInfo.name (0 :: group.levels)) group.params
+        let motives ← inferArgumentTypesN recInfo.numMotives aux
+        motives.mapM fun motive =>
+          forallTelescopeReducing motive fun xs _ => pure xs.size
+
+      let recArgInfos ← infos.mapM fun info => do
+        let some eqnInfo := Structural.eqnInfoExt.find? (← getEnv) info.name | throwError "{info.name} missing eqnInfo"
+        let value ← instantiateLambda info.value xs
+        let recArgInfo' ← lambdaTelescope value fun ys _ =>
+          Structural.getRecArgInfo info.name numFixed (xs ++ ys) eqnInfo.recArgPos
+        let #[recArgInfo] ← Structural.argsInGroup group xs value #[recArgInfo']
+          | throwError "Structural.argsInGroup did not return a recArgInfo"
+        pure recArgInfo
+
+      let positions : Structural.Positions := .groupAndSort (·.indIdx) recArgInfos (Array.range indInfo.numTypeFormers)
+
+      -- Below we'll need the types of the motive arguments (brecOn argument order)
+      let brecMotiveTypes ← inferArgumentTypesN recInfo.numMotives (group.brecOn true lvl 0)
+      trace[Meta.FunInd] m!"brecMotiveTypes: {brecMotiveTypes}"
+      assert! brecMotiveTypes.size = positions.size
+
+      -- Remove the varying parameters from the environment
+      withErasedFVars (ys.map (·.fvarId!)) do
+        -- The brecOnArgs, brecOnMotives and brecOnMinor should still be valid in this
+        -- context, and are the parts relevant for every function in the mutual group
+
+        -- Calculate the types of the induction motives (natural argument order) for each function
+        let motiveTypes ← infos.mapM fun info => do
+          lambdaTelescope (← instantiateLambda info.value xs) fun ys _ =>
+            mkForallFVars ys (.sort levelZero)
+        let motiveArities ← infos.mapM fun info => do
+          lambdaTelescope (← instantiateLambda info.value xs) fun ys _ => pure ys.size
+        let motiveDecls ← motiveTypes.mapIdxM fun ⟨i,_⟩ motiveType => do
+          let n := if infos.size = 1 then .mkSimple "motive"
+                                     else .mkSimple s!"motive_{i+1}"
+          pure (n, fun _ => pure motiveType)
+        withLocalDeclsD motiveDecls fun motives => do
+
+          -- Prepare the `isRecCall` that recognizes recursive calls
+          let fns := infos.map fun info =>
+            mkAppN (.const info.name (info.levelParams.map mkLevelParam)) xs
+          let isRecCall : Expr → Option Expr := fun e => do
+            if let .some i := motives.indexOf? e.getAppFn then
+              if e.getAppNumArgs = motiveArities[i]! then
+                return mkAppN fns[i]! e.getAppArgs
+            .none
+
+          -- Motives with parameters reordered, to put indices and major first
+          let brecMotives ← (Array.zip motives recArgInfos).mapM fun (motive, recArgInfo) => do
+            forallTelescope (← inferType motive) fun ys _ => do
+              let (indicesMajor, rest) := recArgInfo.pickIndicesMajor ys
+              mkLambdaFVars indicesMajor (← mkForallFVars rest (mkAppN motive ys))
+
+          -- We need to pack these motives according to the `positions` assignment.
+          let packedMotives ← positions.mapMwith PProdN.packLambdas brecMotiveTypes brecMotives
+          trace[Meta.FunInd] m!"packedMotives: {packedMotives}"
+
+          -- Now we can calcualte the expected types of the minor arguments
+          let minorTypes ← inferArgumentTypesN recInfo.numMotives <|
+            mkAppN (group.brecOn true lvl 0) (packedMotives ++ brecOnTargets)
+          trace[Meta.FunInd] m!"minorTypes: {minorTypes}"
+          -- So that we can transform them
+          let (minors', mvars) ← M2.run do
+            let mut minors' := #[]
+            for brecOnMinor in brecOnMinors, goal in minorTypes, numTargets in numTargetss do
+              let minor' ← forallTelescope goal fun xs goal => do
+                unless xs.size ≥ numTargets do
+                  throwError ".brecOn argument has too few parameters, expected at least {numTargets}: {xs}"
+                let targets : Array Expr := xs[:numTargets]
+                let genIH := xs[numTargets]!
+                let extraParams := xs[numTargets+1:]
+                -- open body with the same arg
+                let body ← instantiateLambda brecOnMinor targets
+                removeLamda body fun oldIH body => do
+                  trace[Meta.FunInd] "replacing {Expr.fvar oldIH} with {genIH}"
+                  let body ← instantiateLambda body extraParams
+                  let body' ← buildInductionBody #[genIH.fvarId!] #[] goal oldIH genIH.fvarId! isRecCall body
+                  if body'.containsFVar oldIH then
+                    throwError m!"Did not fully eliminate {mkFVar oldIH} from induction principle body:{indentExpr body}"
+                  mkLambdaFVars (targets.push genIH) (← mkLambdaFVars extraParams body')
+              minors' := minors'.push minor'
+            pure minors'
+          trace[Meta.FunInd] "processed minors: {minors'}"
+
+          -- Now assemble the mutual_induct theorem
+          -- Let-bind the transformed minors to avoid code duplication of possibly very large
+          -- terms when we have mutual induction.
+          let e' ← withLetDecls `minor minorTypes minors' fun minors' => do
+            let mut brecOnApps := #[]
+            for info in infos, recArgInfo in recArgInfos, idx in [:infos.size] do
+              -- Take care to pick the `ys` from the type, to get the variable names expected
+              -- by the user, but use the value arity
+              let arity ← lambdaTelescope (← instantiateLambda info.value xs) fun ys _ => pure ys.size
+              let e ← forallBoundedTelescope (← instantiateForall info.type xs) arity fun ys _ => do
+                let (indicesMajor, rest) := recArgInfo.pickIndicesMajor ys
+                -- Find where in the function packing we are (TODO: abstract out)
+                let some indIdx := positions.findIdx? (·.contains idx) | panic! "invalid positions"
+                let some pos := positions.find? (·.contains idx) | panic! "invalid positions"
+                let some packIdx := pos.findIdx? (· == idx) | panic! "invalid positions"
+                let e := group.brecOn true lvl indIdx -- unconditionally using binduction here
+                let e := mkAppN e packedMotives
+                let e := mkAppN e indicesMajor
+                let e := mkAppN e minors'
+                let e ← PProdN.proj pos.size packIdx e
+                let e := mkAppN e rest
+                let e ← mkLambdaFVars ys e
+                trace[Meta.FunInd] "assembled call for {info.name}: {e}"
+                pure e
+              brecOnApps := brecOnApps.push e
+            mkLetFVars minors' (← PProdN.mk 0 brecOnApps)
+          let e' ← abstractIndependentMVars mvars (← motives.back.fvarId!.getDecl).index e'
+          let e' ← mkLambdaFVars motives e'
+
+          -- We could pass (usedOnly := true) below, and get nicer induction principles that
+          -- do do not mention odd unused parameters.
+          -- But the downside is that automatic instantiation of the principle (e.g. in a tactic
+          -- that derives them from an function application in the goal) is harder, as
+          -- one would have to infer or keep track of which parameters to pass.
+          -- So for now lets just keep them around.
+          let e' ← mkLambdaFVars (binderInfoForMVars := .default) xs e'
+          let e' ← instantiateMVars e'
+          trace[Meta.FunInd] "complete body of mutual induction principle:{indentExpr e'}"
+          pure e'
 
   unless (← isTypeCorrect e') do
-    logError m!"failed to derive induction priciple:{indentExpr e'}"
+    logError m!"constructed induction principle is not type correct:{indentExpr e'}"
     check e'
 
   let eTyp ← inferType e'
@@ -911,25 +1027,33 @@ def deriveStructuralInduction (name : Name) : MetaM Unit := do
   -- logInfo m!"eTyp: {eTyp}"
   let params := (collectLevelParams {} eTyp).params
   -- Prune unused level parameters, preserving the original order
-  let us := info.levelParams.filter (params.contains ·)
+  let us := infos[0]!.levelParams.filter (params.contains ·)
+
+  let inductName :=
+    if names.size = 1 then
+      names[0]! ++ `induct
+    else
+      names[0]! ++ `mutual_induct
 
   addDecl <| Declaration.thmDecl
     { name := inductName, levelParams := us, type := eTyp, value := e' }
 
+  if names.size > 1 then
+    projectMutualInduct names inductName
+
 /--
 Given a recursively defined function `foo`, derives `foo.induct`. See the module doc for details.
 -/
 def deriveInduction (name : Name) : MetaM Unit := do
-  if let some eqnInfo := WF.eqnInfoExt.find? (← getEnv) name then
-    let unaryInductName ← deriveUnaryInduction eqnInfo.declNameNonRec
-    unless eqnInfo.declNameNonRec = name do
-      deriveUnpackedInduction eqnInfo unaryInductName
-  else if let some eqnInfo := Structural.eqnInfoExt.find? (← getEnv) name then
-    if eqnInfo.declNames.size > 1 then
-      throwError "Induction principles for mutually structurally recursive functions are not yet supported"
-    deriveStructuralInduction eqnInfo.declName
-  else
-    throwError "Cannot derive functional induction principle for {name}: Not defined by structural or well-founded recursion"
+  mapError (f := (m!"Cannot derive functional induction principle (please report this issue)\n{indentD ·}")) do
+    if let some eqnInfo := WF.eqnInfoExt.find? (← getEnv) name then
+      let unaryInductName ← deriveUnaryInduction eqnInfo.declNameNonRec
+      unless eqnInfo.declNameNonRec = name do
+        deriveUnpackedInduction eqnInfo unaryInductName
+    else if let some eqnInfo := Structural.eqnInfoExt.find? (← getEnv) name then
+      deriveInductionStructural eqnInfo.declNames eqnInfo.numFixed
+    else
+      throwError "{name} is not defined by structural or well-founded recursion"
 
 def isFunInductName (env : Environment) (name : Name) : Bool := Id.run do
   let .str p s := name | return false
@@ -942,6 +1066,9 @@ def isFunInductName (env : Environment) (name : Name) : Bool := Id.run do
     if let some eqnInfo := WF.eqnInfoExt.find? env p then
       if h : eqnInfo.declNames.size > 1 then
         return eqnInfo.declNames[0] = p
+    if let some eqnInfo := Structural.eqnInfoExt.find? env p then
+      if h : eqnInfo.declNames.size > 1 then
+        return eqnInfo.declNames[0] = p
     return false
   | _ => return false
 
diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index aab89fbf4203..a2ff8c914b05 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -269,7 +269,7 @@ corresponding `end <id>` or the end of the file.
   "namespace " >> checkColGt >> ident
 /--
 `end` closes a `section` or `namespace` scope. If the scope is named `<id>`, it has to be closed
-with `end <id>`.
+with `end <id>`. The `end` command is optional at the end of a file.
 -/
 @[builtin_command_parser] def «end»          := leading_parser
   "end" >> optional (ppSpace >> checkColGt >> ident)
diff --git a/src/Std/Data/DHashMap/Internal/List/Associative.lean b/src/Std/Data/DHashMap/Internal/List/Associative.lean
index 4b6e4eb4479a..0f7b29d5cf55 100644
--- a/src/Std/Data/DHashMap/Internal/List/Associative.lean
+++ b/src/Std/Data/DHashMap/Internal/List/Associative.lean
@@ -579,7 +579,7 @@ theorem getEntry?_replaceEntry_of_true [BEq α] [PartialEquivBEq α] {l : List (
 
 theorem getEntry?_replaceEntry [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a k : α}
     {v : β k} :
-    getEntry? a (replaceEntry k v l) = bif containsKey k l && k == a then some ⟨k, v⟩ else
+    getEntry? a (replaceEntry k v l) = if containsKey k l ∧ k == a then some ⟨k, v⟩ else
       getEntry? a l := by
   cases hl : containsKey k l
   · simp [getEntry?_replaceEntry_of_containsKey_eq_false hl]
@@ -632,13 +632,11 @@ theorem getValueCast?_replaceEntry [BEq α] [LawfulBEq α] {l : List ((a : α) 
 @[simp]
 theorem containsKey_replaceEntry [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a k : α}
     {v : β k} : containsKey a (replaceEntry k v l) = containsKey a l := by
-  cases h : containsKey k l && k == a
-  · rw [containsKey_eq_isSome_getEntry?, getEntry?_replaceEntry, h, cond_false,
-      containsKey_eq_isSome_getEntry?]
-  · rw [containsKey_eq_isSome_getEntry?, getEntry?_replaceEntry, h, cond_true, Option.isSome_some,
-      Eq.comm]
-    rw [Bool.and_eq_true] at h
-    exact containsKey_of_beq h.1 h.2
+  by_cases h : (getEntry? k l).isSome ∧ k == a
+  · simp only [containsKey_eq_isSome_getEntry?, getEntry?_replaceEntry, h, and_self, ↓reduceIte,
+      Option.isSome_some, Bool.true_eq]
+    rw [← getEntry?_congr h.2, h.1]
+  · simp [containsKey_eq_isSome_getEntry?, getEntry?_replaceEntry, h]
 
 /-- Internal implementation detail of the hash map -/
 def eraseKey [BEq α] (k : α) : List ((a : α) × β a) → List ((a : α) × β a)
@@ -681,7 +679,7 @@ theorem sublist_eraseKey [BEq α] {l : List ((a : α) × β a)} {k : α} :
     · simpa using Sublist.cons_right Sublist.refl
 
 theorem length_eraseKey [BEq α] {l : List ((a : α) × β a)} {k : α} :
-    (eraseKey k l).length = bif containsKey k l then l.length - 1 else l.length := by
+    (eraseKey k l).length = if containsKey k l then l.length - 1 else l.length := by
   induction l using assoc_induction
   · simp
   · next k' v' t ih =>
@@ -690,7 +688,7 @@ theorem length_eraseKey [BEq α] {l : List ((a : α) × β a)} {k : α} :
     · rw [cond_false, Bool.false_or, List.length_cons, ih]
       cases h : containsKey k t
       · simp
-      · simp only [cond_true, Nat.succ_eq_add_one, List.length_cons, Nat.add_sub_cancel]
+      · simp only [Nat.succ_eq_add_one, List.length_cons, Nat.add_sub_cancel, if_true]
         rw [Nat.sub_add_cancel]
         cases t
         · simp at h
@@ -855,7 +853,7 @@ theorem isEmpty_insertEntry [BEq α] {l : List ((a : α) × β a)} {k : α} {v :
   · rw [insertEntry_of_containsKey h, isEmpty_replaceEntry, isEmpty_eq_false_of_containsKey h]
 
 theorem length_insertEntry [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
-    (insertEntry k v l).length = bif containsKey k l then l.length else l.length + 1 := by
+    (insertEntry k v l).length = if containsKey k l then l.length else l.length + 1 := by
   simp [insertEntry, Bool.apply_cond List.length]
 
 theorem length_le_length_insertEntry [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
@@ -886,23 +884,23 @@ theorem getValue?_insertEntry_of_false [BEq α] [PartialEquivBEq α] {l : List (
   · rw [insertEntry_of_containsKey h', getValue?_replaceEntry_of_false h]
 
 theorem getValue?_insertEntry [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α}
-    {v : β} : getValue? a (insertEntry k v l) = bif k == a then some v else getValue? a l := by
+    {v : β} : getValue? a (insertEntry k v l) = if k == a then some v else getValue? a l := by
   cases h : k == a
   · simp [getValue?_insertEntry_of_false h, h]
   · simp [getValue?_insertEntry_of_beq h, h]
 
 theorem getValue?_insertEntry_self [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {k : α} {v : β} :
     getValue? k (insertEntry k v l) = some v := by
-  rw [getValue?_insertEntry, Bool.cond_pos BEq.refl]
+  simp [getValue?_insertEntry]
 
 end
 
 theorem getEntry?_insertEntry [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α}
     {v : β k} :
-    getEntry? a (insertEntry k v l) = bif k == a then some ⟨k, v⟩ else getEntry? a l := by
+    getEntry? a (insertEntry k v l) = if k == a then some ⟨k, v⟩ else getEntry? a l := by
   cases hl : containsKey k l
-  · rw [insertEntry_of_containsKey_eq_false hl, getEntry?_cons]
-  · rw [insertEntry_of_containsKey hl, getEntry?_replaceEntry, hl, Bool.true_and, BEq.comm]
+  · rw [insertEntry_of_containsKey_eq_false hl, getEntry?_cons, cond_eq_if]
+  · simp [insertEntry_of_containsKey hl, getEntry?_replaceEntry, hl]
 
 theorem getValueCast?_insertEntry [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
     {v : β k} : getValueCast? a (insertEntry k v l) =
@@ -938,21 +936,21 @@ theorem getValueCastD_insertEntry_self [BEq α] [LawfulBEq α] {l : List ((a : 
 
 theorem getValue!_insertEntry {β : Type v} [BEq α] [PartialEquivBEq α] [Inhabited β]
     {l : List ((_ : α) × β)} {k a : α} {v : β} :
-    getValue! a (insertEntry k v l) = bif k == a then v else getValue! a l := by
-  simp [getValue!_eq_getValue?, getValue?_insertEntry, Bool.apply_cond Option.get!]
+    getValue! a (insertEntry k v l) = if k == a then v else getValue! a l := by
+  simp [getValue!_eq_getValue?, getValue?_insertEntry, apply_ite Option.get!]
 
 theorem getValue!_insertEntry_self {β : Type v} [BEq α] [EquivBEq α] [Inhabited β]
     {l : List ((_ : α) × β)} {k : α} {v : β} : getValue! k (insertEntry k v l) = v := by
-  rw [getValue!_insertEntry, BEq.refl, cond_true]
+  simp [getValue!_insertEntry, BEq.refl]
 
 theorem getValueD_insertEntry {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)}
     {k a : α} {fallback v : β} : getValueD a (insertEntry k v l) fallback =
-      bif k == a then v else getValueD a l fallback := by
-  simp [getValueD_eq_getValue?, getValue?_insertEntry, Bool.apply_cond (fun x => Option.getD x fallback)]
+      if k == a then v else getValueD a l fallback := by
+  simp [getValueD_eq_getValue?, getValue?_insertEntry, apply_ite (fun x => Option.getD x fallback)]
 
 theorem getValueD_insertEntry_self {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)}
     {k : α} {fallback v : β} : getValueD k (insertEntry k v l) fallback = v := by
-  rw [getValueD_insertEntry, BEq.refl, cond_true]
+  simp [getValueD_insertEntry, BEq.refl]
 
 @[simp]
 theorem containsKey_insertEntry [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α}
@@ -991,7 +989,7 @@ theorem getValue_insertEntry {β : Type v} [BEq α] [PartialEquivBEq α] {l : Li
       if h' : k == a then v
       else getValue a l (containsKey_of_containsKey_insertEntry h (Bool.eq_false_iff.2 h')) := by
   rw [← Option.some_inj, ← getValue?_eq_some_getValue, apply_dite Option.some,
-    getValue?_insertEntry, cond_eq_if, ← dite_eq_ite]
+    getValue?_insertEntry, ← dite_eq_ite]
   simp only [← getValue?_eq_some_getValue]
 
 theorem getValue_insertEntry_self {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {k : α}
@@ -1020,7 +1018,7 @@ theorem isEmpty_insertEntryIfNew [BEq α] {l : List ((a : α) × β a)} {k : α}
 
 theorem getEntry?_insertEntryIfNew [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α}
     {v : β k} : getEntry? a (insertEntryIfNew k v l) =
-      bif k == a && !containsKey k l then some ⟨k, v⟩ else getEntry? a l := by
+      if k == a && !containsKey k l then some ⟨k, v⟩ else getEntry? a l := by
   cases h : containsKey k l
   · simp [insertEntryIfNew_of_containsKey_eq_false h, getEntry?_cons]
   · simp [insertEntryIfNew_of_containsKey h]
@@ -1036,18 +1034,22 @@ theorem getValueCast?_insertEntryIfNew [BEq α] [LawfulBEq α] {l : List ((a : 
 
 theorem getValue?_insertEntryIfNew {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)}
     {k a : α} {v : β} : getValue? a (insertEntryIfNew k v l) =
-      bif k == a && !containsKey k l then some v else getValue? a l := by
+      if k == a ∧ containsKey k l = false then some v else getValue? a l := by
   simp [getValue?_eq_getEntry?, getEntry?_insertEntryIfNew,
-      Bool.apply_cond (Option.map (fun (y : ((_ : α) × β)) => y.2))]
+      apply_ite (Option.map (fun (y : ((_ : α) × β)) => y.2))]
 
 theorem containsKey_insertEntryIfNew [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)}
     {k a : α} {v : β k} :
     containsKey a (insertEntryIfNew k v l) = ((k == a) || containsKey a l) := by
-  simp only [containsKey_eq_isSome_getEntry?, getEntry?_insertEntryIfNew, Bool.apply_cond Option.isSome,
-    Option.isSome_some, Bool.cond_true_left]
+  simp only [containsKey_eq_isSome_getEntry?, getEntry?_insertEntryIfNew, apply_ite Option.isSome,
+    Option.isSome_some, if_true_left]
+  simp only [Bool.and_eq_true, Bool.not_eq_true', Option.not_isSome, Option.isNone_iff_eq_none,
+    getEntry?_eq_none, Bool.if_true_left, Bool.decide_and, Bool.decide_eq_true,
+    Bool.decide_eq_false]
   cases h : k == a
   · simp
-  · rw [Bool.true_and, Bool.true_or, getEntry?_congr h, Bool.not_or_self]
+  · rw [containsKey_eq_isSome_getEntry?, getEntry?_congr h]
+    simp
 
 theorem containsKey_insertEntryIfNew_self [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k : α}
     {v : β k} : containsKey k (insertEntryIfNew k v l) := by
@@ -1085,7 +1087,7 @@ theorem getValue_insertEntryIfNew {β : Type v} [BEq α] [PartialEquivBEq α] {l
     if h' : k == a ∧ containsKey k l = false then v
     else getValue a l (containsKey_of_containsKey_insertEntryIfNew' h h') := by
   rw [← Option.some_inj, ← getValue?_eq_some_getValue, apply_dite Option.some,
-    getValue?_insertEntryIfNew, cond_eq_if, ← dite_eq_ite]
+    getValue?_insertEntryIfNew, ← dite_eq_ite]
   simp [← getValue?_eq_some_getValue]
 
 theorem getValueCast!_insertEntryIfNew [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
@@ -1096,8 +1098,8 @@ theorem getValueCast!_insertEntryIfNew [BEq α] [LawfulBEq α] {l : List ((a : 
 
 theorem getValue!_insertEntryIfNew {β : Type v} [BEq α] [PartialEquivBEq α] [Inhabited β]
     {l : List ((_ : α) × β)} {k a : α} {v : β} : getValue! a (insertEntryIfNew k v l) =
-      bif k == a && !containsKey k l then v else getValue! a l := by
-  simp [getValue!_eq_getValue?, getValue?_insertEntryIfNew, Bool.apply_cond Option.get!]
+      if k == a ∧ containsKey k l = false then v else getValue! a l := by
+  simp [getValue!_eq_getValue?, getValue?_insertEntryIfNew, apply_ite Option.get!]
 
 theorem getValueCastD_insertEntryIfNew [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
     {v : β k} {fallback : β a} : getValueCastD a (insertEntryIfNew k v l) fallback =
@@ -1108,12 +1110,12 @@ theorem getValueCastD_insertEntryIfNew [BEq α] [LawfulBEq α] {l : List ((a : 
 
 theorem getValueD_insertEntryIfNew {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)}
     {k a : α} {fallback v : β} : getValueD a (insertEntryIfNew k v l) fallback =
-      bif k == a && !containsKey k l then v else getValueD a l fallback := by
+      if k == a ∧ containsKey k l = false then v else getValueD a l fallback := by
   simp [getValueD_eq_getValue?, getValue?_insertEntryIfNew,
-    Bool.apply_cond (fun x => Option.getD x fallback)]
+    apply_ite (fun x => Option.getD x fallback)]
 
 theorem length_insertEntryIfNew [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
-    (insertEntryIfNew k v l).length = bif containsKey k l then l.length else l.length + 1 := by
+    (insertEntryIfNew k v l).length = if containsKey k l then l.length else l.length + 1 := by
   simp [insertEntryIfNew, Bool.apply_cond List.length]
 
 theorem length_le_length_insertEntryIfNew [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
@@ -1169,7 +1171,7 @@ theorem getEntry?_eraseKey_of_false [BEq α] [PartialEquivBEq α] {l : List ((a
 
 theorem getEntry?_eraseKey [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α}
     (hl : DistinctKeys l) :
-    getEntry? a (eraseKey k l) = bif k == a then none else getEntry? a l := by
+    getEntry? a (eraseKey k l) = if k == a then none else getEntry? a l := by
   cases h : k == a
   · simp [getEntry?_eraseKey_of_false h, h]
   · simp [getEntry?_eraseKey_of_beq hl h, h]
@@ -1222,8 +1224,8 @@ theorem getValue?_eraseKey_of_false [BEq α] [PartialEquivBEq α] {l : List ((_
 
 theorem getValue?_eraseKey [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α}
     (hl : DistinctKeys l) :
-    getValue? a (eraseKey k l) = bif k == a then none else getValue? a l := by
-  simp [getValue?_eq_getEntry?, getEntry?_eraseKey hl, Bool.apply_cond (Option.map _)]
+    getValue? a (eraseKey k l) = if k == a then none else getValue? a l := by
+  simp [getValue?_eq_getEntry?, getEntry?_eraseKey hl, apply_ite (Option.map _)]
 
 end
 
@@ -1241,25 +1243,25 @@ theorem containsKey_eraseKey_of_false [BEq α] [PartialEquivBEq α] {l : List ((
 
 theorem containsKey_eraseKey [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α}
     (hl : DistinctKeys l) : containsKey a (eraseKey k l) = (!(k == a) && containsKey a l) := by
-  simp [containsKey_eq_isSome_getEntry?, getEntry?_eraseKey hl, Bool.apply_cond]
+  simp [containsKey_eq_isSome_getEntry?, getEntry?_eraseKey hl, apply_ite]
 
 theorem getValueCast?_eraseKey [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
     (hl : DistinctKeys l) :
-    getValueCast? a (eraseKey k l) = bif k == a then none else getValueCast? a l := by
+    getValueCast? a (eraseKey k l) = if k == a then none else getValueCast? a l := by
   rw [getValueCast?_eq_getEntry?, Option.dmap_congr (getEntry?_eraseKey hl)]
-  rcases Bool.eq_false_or_eq_true (k == a) with h|h
-  · rw [Option.dmap_congr (Bool.cond_pos h), Option.dmap_none, Bool.cond_pos h]
-  · rw [Option.dmap_congr (Bool.cond_neg h), getValueCast?_eq_getEntry?]
-    exact (Bool.cond_neg h).symm
+  by_cases h : k == a
+  · rw [Option.dmap_congr (if_pos h), Option.dmap_none, if_pos h]
+  · rw [Option.dmap_congr (if_neg h), getValueCast?_eq_getEntry?]
+    exact (if_neg h).symm
 
 theorem getValueCast?_eraseKey_self [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α}
     (hl : DistinctKeys l) : getValueCast? k (eraseKey k l) = none := by
-  rw [getValueCast?_eraseKey hl, Bool.cond_pos BEq.refl]
+  rw [getValueCast?_eraseKey hl, if_pos BEq.refl]
 
 theorem getValueCast!_eraseKey [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
     [Inhabited (β a)] (hl : DistinctKeys l) :
-    getValueCast! a (eraseKey k l) = bif k == a then default else getValueCast! a l := by
-  simp [getValueCast!_eq_getValueCast?, getValueCast?_eraseKey hl, Bool.apply_cond Option.get!]
+    getValueCast! a (eraseKey k l) = if k == a then default else getValueCast! a l := by
+  simp [getValueCast!_eq_getValueCast?, getValueCast?_eraseKey hl, apply_ite Option.get!]
 
 theorem getValueCast!_eraseKey_self [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α}
     [Inhabited (β k)] (hl : DistinctKeys l) : getValueCast! k (eraseKey k l) = default := by
@@ -1267,9 +1269,9 @@ theorem getValueCast!_eraseKey_self [BEq α] [LawfulBEq α] {l : List ((a : α)
 
 theorem getValueCastD_eraseKey [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
     {fallback : β a} (hl : DistinctKeys l) : getValueCastD a (eraseKey k l) fallback =
-      bif k == a then fallback else getValueCastD a l fallback := by
+      if k == a then fallback else getValueCastD a l fallback := by
   simp [getValueCastD_eq_getValueCast?, getValueCast?_eraseKey hl,
-    Bool.apply_cond (fun x => Option.getD x fallback)]
+    apply_ite (fun x => Option.getD x fallback)]
 
 theorem getValueCastD_eraseKey_self [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α}
     {fallback : β k} (hl : DistinctKeys l) :
@@ -1278,8 +1280,8 @@ theorem getValueCastD_eraseKey_self [BEq α] [LawfulBEq α] {l : List ((a : α)
 
 theorem getValue!_eraseKey {β : Type v} [BEq α] [PartialEquivBEq α] [Inhabited β]
     {l : List ((_ : α) × β)} {k a : α} (hl : DistinctKeys l) :
-    getValue! a (eraseKey k l) = bif k == a then default else getValue! a l := by
-  simp [getValue!_eq_getValue?, getValue?_eraseKey hl, Bool.apply_cond Option.get!]
+    getValue! a (eraseKey k l) = if k == a then default else getValue! a l := by
+  simp [getValue!_eq_getValue?, getValue?_eraseKey hl, apply_ite Option.get!]
 
 theorem getValue!_eraseKey_self {β : Type v} [BEq α] [PartialEquivBEq α] [Inhabited β]
     {l : List ((_ : α) × β)} {k : α} (hl : DistinctKeys l) :
@@ -1288,8 +1290,8 @@ theorem getValue!_eraseKey_self {β : Type v} [BEq α] [PartialEquivBEq α] [Inh
 
 theorem getValueD_eraseKey {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)}
     {k a : α} {fallback : β} (hl : DistinctKeys l) : getValueD a (eraseKey k l) fallback =
-      bif k == a then fallback else getValueD a l fallback := by
-  simp [getValueD_eq_getValue?, getValue?_eraseKey hl, Bool.apply_cond (fun x => Option.getD x fallback)]
+      if k == a then fallback else getValueD a l fallback := by
+  simp [getValueD_eq_getValue?, getValue?_eraseKey hl, apply_ite (fun x => Option.getD x fallback)]
 
 theorem getValueD_eraseKey_self {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)}
     {k : α} {fallback : β} (hl : DistinctKeys l) :
@@ -1304,15 +1306,15 @@ theorem getValueCast_eraseKey [BEq α] [LawfulBEq α] {l : List ((a : α) × β
     (hl : DistinctKeys l) : getValueCast a (eraseKey k l) h =
       getValueCast a l (containsKey_of_containsKey_eraseKey hl h) := by
   rw [containsKey_eraseKey hl, Bool.and_eq_true, Bool.not_eq_true'] at h
-  rw [← Option.some_inj, ← getValueCast?_eq_some_getValueCast, getValueCast?_eraseKey hl, h.1,
-    cond_false, ← getValueCast?_eq_some_getValueCast]
+  rw [← Option.some_inj, ← getValueCast?_eq_some_getValueCast, getValueCast?_eraseKey hl, h.1]
+  simp [← getValueCast?_eq_some_getValueCast]
 
 theorem getValue_eraseKey {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)}
     {k a : α} {h} (hl : DistinctKeys l) :
     getValue a (eraseKey k l) h = getValue a l (containsKey_of_containsKey_eraseKey hl h) := by
   rw [containsKey_eraseKey hl, Bool.and_eq_true, Bool.not_eq_true'] at h
-  rw [← Option.some_inj, ← getValue?_eq_some_getValue, getValue?_eraseKey hl, h.1, cond_false,
-    ← getValue?_eq_some_getValue]
+  rw [← Option.some_inj, ← getValue?_eq_some_getValue, getValue?_eraseKey hl, h.1]
+  simp [← getValue?_eq_some_getValue]
 
 theorem getEntry?_of_perm [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {a : α}
     (hl : DistinctKeys l) (h : Perm l l') : getEntry? a l = getEntry? a l' := by
diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
index 3a9db521b268..10cee668c865 100644
--- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
@@ -146,7 +146,7 @@ theorem isEmpty_eq_size_eq_zero : m.1.isEmpty = (m.1.size == 0) := by
   simp [Raw.isEmpty]
 
 theorem size_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
-    (m.insert k v).1.size = bif m.contains k then m.1.size else m.1.size + 1 := by
+    (m.insert k v).1.size = if m.contains k then m.1.size else m.1.size + 1 := by
   simp_to_model using List.length_insertEntry
 
 theorem size_le_size_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
@@ -170,7 +170,7 @@ theorem contains_of_contains_erase [EquivBEq α] [LawfulHashable α] {k a : α}
   simp_to_model using List.containsKey_of_containsKey_eraseKey
 
 theorem size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
-    (m.erase k).1.size = bif m.contains k then m.1.size - 1 else m.1.size := by
+    (m.erase k).1.size = if m.contains k then m.1.size - 1 else m.1.size := by
   simp_to_model using List.length_eraseKey
 
 theorem size_erase_le [EquivBEq α] [LawfulHashable α] {k : α} :
@@ -216,7 +216,7 @@ theorem get?_eq_none [LawfulBEq α] {a : α} : m.contains a = false → m.get? a
   simp_to_model using List.getValueCast?_eq_none
 
 theorem get?_erase [LawfulBEq α] {k a : α} :
-    (m.erase k).get? a = bif k == a then none else m.get? a := by
+    (m.erase k).get? a = if k == a then none else m.get? a := by
   simp_to_model using List.getValueCast?_eraseKey
 
 theorem get?_erase_self [LawfulBEq α] {k : α} : (m.erase k).get? k = none := by
@@ -235,7 +235,7 @@ theorem get?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
   simp_to_model; empty
 
 theorem get?_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    get? (m.insert k v) a = bif k == a then some v else get? m a := by
+    get? (m.insert k v) a = if k == a then some v else get? m a := by
   simp_to_model using List.getValue?_insertEntry
 
 theorem get?_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
@@ -251,7 +251,7 @@ theorem get?_eq_none [EquivBEq α] [LawfulHashable α] {a : α} :
   simp_to_model using List.getValue?_eq_none.2
 
 theorem get?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
-    Const.get? (m.erase k) a = bif k == a then none else get? m a := by
+    Const.get? (m.erase k) a = if k == a then none else get? m a := by
   simp_to_model using List.getValue?_eraseKey
 
 theorem get?_erase_self [EquivBEq α] [LawfulHashable α] {k : α} :
@@ -341,7 +341,7 @@ theorem get!_eq_default [LawfulBEq α] {a : α} [Inhabited (β a)] :
   simp_to_model using List.getValueCast!_eq_default
 
 theorem get!_erase [LawfulBEq α] {k a : α} [Inhabited (β a)] :
-    (m.erase k).get! a = bif k == a then default else m.get! a := by
+    (m.erase k).get! a = if k == a then default else m.get! a := by
   simp_to_model using List.getValueCast!_eraseKey
 
 theorem get!_erase_self [LawfulBEq α] {k : α} [Inhabited (β k)] :
@@ -373,7 +373,7 @@ theorem get!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α
   simp_to_model; empty
 
 theorem get!_insert [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
-    get! (m.insert k v) a = bif k == a then v else get! m a := by
+    get! (m.insert k v) a = if k == a then v else get! m a := by
   simp_to_model using List.getValue!_insertEntry
 
 theorem get!_insert_self [EquivBEq α] [LawfulHashable α] [Inhabited β] {k : α} {v : β} :
@@ -385,7 +385,7 @@ theorem get!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α
   simp_to_model using List.getValue!_eq_default
 
 theorem get!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} :
-    get! (m.erase k) a = bif k == a then default else get! m a := by
+    get! (m.erase k) a = if k == a then default else get! m a := by
   simp_to_model using List.getValue!_eraseKey
 
 theorem get!_erase_self [EquivBEq α] [LawfulHashable α] [Inhabited β] {k : α} :
@@ -436,7 +436,7 @@ theorem getD_eq_fallback [LawfulBEq α] {a : α} {fallback : β a} :
   simp_to_model using List.getValueCastD_eq_fallback
 
 theorem getD_erase [LawfulBEq α] {k a : α} {fallback : β a} :
-    (m.erase k).getD a fallback = bif k == a then fallback else m.getD a fallback := by
+    (m.erase k).getD a fallback = if k == a then fallback else m.getD a fallback := by
   simp_to_model using List.getValueCastD_eraseKey
 
 theorem getD_erase_self [LawfulBEq α] {k : α} {fallback : β k} :
@@ -472,7 +472,7 @@ theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} {fallback : 
   simp_to_model; empty
 
 theorem getD_insert [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
-    getD (m.insert k v) a fallback = bif k == a then v else getD m a fallback := by
+    getD (m.insert k v) a fallback = if k == a then v else getD m a fallback := by
   simp_to_model using List.getValueD_insertEntry
 
 theorem getD_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {fallback v : β} :
@@ -484,7 +484,7 @@ theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] {a : α} {fallback :
   simp_to_model using List.getValueD_eq_fallback
 
 theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : β} :
-    getD (m.erase k) a fallback = bif k == a then fallback else getD m a fallback := by
+    getD (m.erase k) a fallback = if k == a then fallback else getD m a fallback := by
   simp_to_model using List.getValueD_eraseKey
 
 theorem getD_erase_self [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} :
@@ -540,7 +540,7 @@ theorem contains_of_contains_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a
   simp_to_model using List.containsKey_of_containsKey_insertEntryIfNew'
 
 theorem size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
-    (m.insertIfNew k v).1.size = bif m.contains k then m.1.size else m.1.size + 1 := by
+    (m.insertIfNew k v).1.size = if m.contains k then m.1.size else m.1.size + 1 := by
   simp_to_model using List.length_insertEntryIfNew
 
 theorem size_le_size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
@@ -576,7 +576,7 @@ namespace Const
 variable {β : Type v} (m : Raw₀ α (fun _ => β)) (h : m.1.WF)
 
 theorem get?_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    get? (m.insertIfNew k v) a = bif k == a && !m.contains k then some v else get? m a := by
+    get? (m.insertIfNew k v) a = if k == a ∧ m.contains k = false then some v else get? m a := by
   simp_to_model using List.getValue?_insertEntryIfNew
 
 theorem get_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
@@ -586,12 +586,12 @@ theorem get_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h
   simp_to_model using List.getValue_insertEntryIfNew
 
 theorem get!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
-    get! (m.insertIfNew k v) a = bif k == a && !m.contains k then v else get! m a := by
+    get! (m.insertIfNew k v) a = if k == a ∧ m.contains k = false then v else get! m a := by
   simp_to_model using List.getValue!_insertEntryIfNew
 
 theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
     getD (m.insertIfNew k v) a fallback =
-      bif k == a && !m.contains k then v else getD m a fallback := by
+      if k == a ∧ m.contains k = false then v else getD m a fallback := by
   simp_to_model using List.getValueD_insertEntryIfNew
 
 end Const
diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean
index 665871db313f..84e3dfac515c 100644
--- a/src/Std/Data/DHashMap/Internal/WF.lean
+++ b/src/Std/Data/DHashMap/Internal/WF.lean
@@ -472,7 +472,8 @@ theorem wfImp_eraseₘaux [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable 
   buckets_hash_self := isHashSelf_eraseₘaux m a h
   size_eq := by
     rw [(toListModel_eraseₘaux m a h).length_eq, eraseₘaux, length_eraseKey,
-      ← containsₘ_eq_containsKey h, h', cond_true, h.size_eq]
+      ← containsₘ_eq_containsKey h, h']
+    simp [h.size_eq]
   distinct := h.distinct.eraseKey.perm (toListModel_eraseₘaux m a h)
 
 theorem toListModel_perm_eraseKey_of_containsₘ_eq_false [BEq α] [Hashable α] [EquivBEq α]
diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean
index cf7661d8a083..f67c4c0e5ef3 100644
--- a/src/Std/Data/DHashMap/Lemmas.lean
+++ b/src/Std/Data/DHashMap/Lemmas.lean
@@ -102,7 +102,7 @@ theorem size_emptyc : (∅ : DHashMap α β).size = 0 :=
 theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) := rfl
 
 theorem size_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
-    (m.insert k v).size = bif m.contains k then m.size else m.size + 1 :=
+    (m.insert k v).size = if k ∈ m then m.size else m.size + 1 :=
   Raw₀.size_insert ⟨m.1, _⟩ m.2
 
 theorem size_le_size_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
@@ -140,7 +140,7 @@ theorem mem_of_mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} : a ∈ m.
   simp
 
 theorem size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
-    (m.erase k).size = bif m.contains k then m.size - 1 else m.size :=
+    (m.erase k).size = if k ∈ m then m.size - 1 else m.size :=
   Raw₀.size_erase _ m.2
 
 theorem size_erase_le [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).size ≤ m.size :=
@@ -194,7 +194,7 @@ theorem get?_eq_none [LawfulBEq α] {a : α} : ¬a ∈ m → m.get? a = none :=
   simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false
 
 theorem get?_erase [LawfulBEq α] {k a : α} :
-    (m.erase k).get? a = bif k == a then none else m.get? a :=
+    (m.erase k).get? a = if k == a then none else m.get? a :=
   Raw₀.get?_erase ⟨m.1, _⟩ m.2
 
 @[simp]
@@ -218,7 +218,7 @@ theorem get?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
   Raw₀.Const.get?_of_isEmpty ⟨m.1, _⟩ m.2
 
 theorem get?_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    get? (m.insert k v) a = bif k == a then some v else get? m a :=
+    get? (m.insert k v) a = if k == a then some v else get? m a :=
   Raw₀.Const.get?_insert ⟨m.1, _⟩ m.2
 
 @[simp]
@@ -238,7 +238,7 @@ theorem get?_eq_none [EquivBEq α] [LawfulHashable α] {a : α } : ¬a ∈ m →
   simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false
 
 theorem get?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
-    Const.get? (m.erase k) a = bif k == a then none else get? m a :=
+    Const.get? (m.erase k) a = if k == a then none else get? m a :=
   Raw₀.Const.get?_erase ⟨m.1, _⟩ m.2
 
 @[simp]
@@ -339,7 +339,7 @@ theorem get!_eq_default [LawfulBEq α] {a : α} [Inhabited (β a)] :
   simpa [mem_iff_contains] using get!_eq_default_of_contains_eq_false
 
 theorem get!_erase [LawfulBEq α] {k a : α} [Inhabited (β a)] :
-    (m.erase k).get! a = bif k == a then default else m.get! a :=
+    (m.erase k).get! a = if k == a then default else m.get! a :=
   Raw₀.get!_erase ⟨m.1, _⟩ m.2
 
 @[simp]
@@ -381,7 +381,7 @@ theorem get!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α
   Raw₀.Const.get!_of_isEmpty ⟨m.1, _⟩ m.2
 
 theorem get!_insert [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
-    get! (m.insert k v) a = bif k == a then v else get! m a :=
+    get! (m.insert k v) a = if k == a then v else get! m a :=
   Raw₀.Const.get!_insert ⟨m.1, _⟩ m.2
 
 @[simp]
@@ -398,7 +398,7 @@ theorem get!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α
   simpa [mem_iff_contains] using get!_eq_default_of_contains_eq_false
 
 theorem get!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} :
-    get! (m.erase k) a = bif k == a then default else get! m a :=
+    get! (m.erase k) a = if k == a then default else get! m a :=
   Raw₀.Const.get!_erase ⟨m.1, _⟩ m.2
 
 @[simp]
@@ -465,7 +465,7 @@ theorem getD_eq_fallback [LawfulBEq α] {a : α} {fallback : β a} :
   simpa [mem_iff_contains] using getD_eq_fallback_of_contains_eq_false
 
 theorem getD_erase [LawfulBEq α] {k a : α} {fallback : β a} :
-    (m.erase k).getD a fallback = bif k == a then fallback else m.getD a fallback :=
+    (m.erase k).getD a fallback = if k == a then fallback else m.getD a fallback :=
   Raw₀.getD_erase ⟨m.1, _⟩ m.2
 
 @[simp]
@@ -512,7 +512,7 @@ theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} {fallback : 
   Raw₀.Const.getD_of_isEmpty ⟨m.1, _⟩ m.2
 
 theorem getD_insert [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
-    getD (m.insert k v) a fallback = bif k == a then v else getD m a fallback :=
+    getD (m.insert k v) a fallback = if k == a then v else getD m a fallback :=
   Raw₀.Const.getD_insert ⟨m.1, _⟩ m.2
 
 @[simp]
@@ -529,7 +529,7 @@ theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] {a : α} {fallback :
   simpa [mem_iff_contains] using getD_eq_fallback_of_contains_eq_false
 
 theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : β} :
-    getD (m.erase k) a fallback = bif k == a then fallback else getD m a fallback :=
+    getD (m.erase k) a fallback = if k == a then fallback else getD m a fallback :=
   Raw₀.Const.getD_erase ⟨m.1, _⟩ m.2
 
 @[simp]
@@ -611,7 +611,7 @@ theorem mem_of_mem_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a : α} {v
   simpa [mem_iff_contains, -contains_insertIfNew] using contains_of_contains_insertIfNew'
 
 theorem size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
-    (m.insertIfNew k v).size = bif m.contains k then m.size else m.size + 1 :=
+    (m.insertIfNew k v).size = if k ∈ m then m.size else m.size + 1 :=
   Raw₀.size_insertIfNew ⟨m.1, _⟩ m.2
 
 theorem size_le_size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
@@ -647,8 +647,9 @@ namespace Const
 variable {β : Type v} {m : DHashMap α (fun _ => β)}
 
 theorem get?_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    get? (m.insertIfNew k v) a = bif k == a && !m.contains k then some v else get? m a :=
-  Raw₀.Const.get?_insertIfNew ⟨m.1, _⟩ m.2
+    get? (m.insertIfNew k v) a = if k == a ∧ ¬k ∈ m then some v else get? m a := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
+  exact Raw₀.Const.get?_insertIfNew ⟨m.1, _⟩ m.2
 
 theorem get_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
     get (m.insertIfNew k v) a h₁ =
@@ -657,13 +658,15 @@ theorem get_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h
   exact Raw₀.Const.get_insertIfNew ⟨m.1, _⟩ m.2
 
 theorem get!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
-    get! (m.insertIfNew k v) a = bif k == a && !m.contains k then v else get! m a :=
-  Raw₀.Const.get!_insertIfNew ⟨m.1, _⟩ m.2
+    get! (m.insertIfNew k v) a = if k == a ∧ ¬k ∈ m then v else get! m a := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
+  exact Raw₀.Const.get!_insertIfNew ⟨m.1, _⟩ m.2
 
 theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
     getD (m.insertIfNew k v) a fallback =
-      bif k == a && !m.contains k then v else getD m a fallback :=
-  Raw₀.Const.getD_insertIfNew ⟨m.1, _⟩ m.2
+      if k == a ∧ ¬k ∈ m then v else getD m a fallback := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
+  exact Raw₀.Const.getD_insertIfNew ⟨m.1, _⟩ m.2
 
 end Const
 
diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean
index 6f13f5d0bc63..2de44c87f657 100644
--- a/src/Std/Data/DHashMap/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/RawLemmas.lean
@@ -151,7 +151,8 @@ theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) := by
   simp [isEmpty]
 
 theorem size_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
-    (m.insert k v).size = bif m.contains k then m.size else m.size + 1 := by
+    (m.insert k v).size = if k ∈ m then m.size else m.size + 1 := by
+  simp only [mem_iff_contains]
   simp_to_raw using Raw₀.size_insert
 
 theorem size_le_size_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
@@ -190,7 +191,8 @@ theorem mem_of_mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} : a ∈ m.
   simpa [mem_iff_contains] using contains_of_contains_erase h
 
 theorem size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
-    (m.erase k).size = bif m.contains k then m.size - 1 else m.size := by
+    (m.erase k).size = if k ∈ m then m.size - 1 else m.size := by
+  simp only [mem_iff_contains]
   simp_to_raw using Raw₀.size_erase
 
 theorem size_erase_le [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).size ≤ m.size := by
@@ -244,7 +246,7 @@ theorem get?_eq_none [LawfulBEq α] {a : α} : ¬a ∈ m → m.get? a = none :=
   simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false h
 
 theorem get?_erase [LawfulBEq α] {k a : α} :
-    (m.erase k).get? a = bif k == a then none else m.get? a := by
+    (m.erase k).get? a = if k == a then none else m.get? a := by
   simp_to_raw using Raw₀.get?_erase
 
 @[simp]
@@ -268,7 +270,7 @@ theorem get?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
   simp_to_raw using Raw₀.Const.get?_of_isEmpty ⟨m, _⟩
 
 theorem get?_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    get? (m.insert k v) a = bif k == a then some v else get? m a := by
+    get? (m.insert k v) a = if k == a then some v else get? m a := by
   simp_to_raw using Raw₀.Const.get?_insert
 
 @[simp]
@@ -288,7 +290,7 @@ theorem get?_eq_none [EquivBEq α] [LawfulHashable α] {a : α} : ¬a ∈ m →
     simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false h
 
 theorem get?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
-    Const.get? (m.erase k) a = bif k == a then none else get? m a := by
+    Const.get? (m.erase k) a = if k == a then none else get? m a := by
   simp_to_raw using Raw₀.Const.get?_erase
 
 @[simp]
@@ -389,7 +391,7 @@ theorem get!_eq_default [LawfulBEq α] {a : α} [Inhabited (β a)] :
   simpa [mem_iff_contains] using get!_eq_default_of_contains_eq_false h
 
 theorem get!_erase [LawfulBEq α] {k a : α} [Inhabited (β a)] :
-    (m.erase k).get! a = bif k == a then default else m.get! a := by
+    (m.erase k).get! a = if k == a then default else m.get! a := by
   simp_to_raw using Raw₀.get!_erase
 
 @[simp]
@@ -430,7 +432,7 @@ theorem get!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α
   simp_to_raw using Raw₀.Const.get!_of_isEmpty ⟨m, _⟩
 
 theorem get!_insert [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
-    get! (m.insert k v) a = bif k == a then v else get! m a := by
+    get! (m.insert k v) a = if k == a then v else get! m a := by
   simp_to_raw using Raw₀.Const.get!_insert
 
 @[simp]
@@ -447,7 +449,7 @@ theorem get!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α
   simpa [mem_iff_contains] using get!_eq_default_of_contains_eq_false h
 
 theorem get!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} :
-    get! (m.erase k) a = bif k == a then default else get! m a := by
+    get! (m.erase k) a = if k == a then default else get! m a := by
   simp_to_raw using Raw₀.Const.get!_erase
 
 @[simp]
@@ -514,7 +516,7 @@ theorem getD_eq_fallback [LawfulBEq α] {a : α} {fallback : β a} :
   simpa [mem_iff_contains] using getD_eq_fallback_of_contains_eq_false h
 
 theorem getD_erase [LawfulBEq α] {k a : α} {fallback : β a} :
-    (m.erase k).getD a fallback = bif k == a then fallback else m.getD a fallback := by
+    (m.erase k).getD a fallback = if k == a then fallback else m.getD a fallback := by
   simp_to_raw using Raw₀.getD_erase
 
 @[simp]
@@ -560,7 +562,7 @@ theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} {fallback : 
   simp_to_raw using Raw₀.Const.getD_of_isEmpty ⟨m, _⟩
 
 theorem getD_insert [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
-    getD (m.insert k v) a fallback = bif k == a then v else getD m a fallback := by
+    getD (m.insert k v) a fallback = if k == a then v else getD m a fallback := by
   simp_to_raw using Raw₀.Const.getD_insert
 
 @[simp]
@@ -577,7 +579,7 @@ theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] {a : α} {fallback :
   simpa [mem_iff_contains] using getD_eq_fallback_of_contains_eq_false h
 
 theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : β} :
-    getD (m.erase k) a fallback = bif k == a then fallback else getD m a fallback := by
+    getD (m.erase k) a fallback = if k == a then fallback else getD m a fallback := by
   simp_to_raw using Raw₀.Const.getD_erase
 
 @[simp]
@@ -659,7 +661,8 @@ theorem mem_of_mem_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a : α} {v
   simpa [mem_iff_contains] using contains_of_contains_insertIfNew' h
 
 theorem size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
-    (m.insertIfNew k v).size = bif m.contains k then m.size else m.size + 1 := by
+    (m.insertIfNew k v).size = if k ∈ m then m.size else m.size + 1 := by
+  simp only [mem_iff_contains]
   simp_to_raw using Raw₀.size_insertIfNew
 
 theorem size_le_size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
@@ -698,7 +701,8 @@ namespace Const
 variable {β : Type v} {m : DHashMap.Raw α (fun _ => β)} (h : m.WF)
 
 theorem get?_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    get? (m.insertIfNew k v) a = bif k == a && !m.contains k then some v else get? m a := by
+    get? (m.insertIfNew k v) a = if k == a ∧ ¬k ∈ m then some v else get? m a := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
   simp_to_raw using Raw₀.Const.get?_insertIfNew
 
 theorem get_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
@@ -709,12 +713,14 @@ theorem get_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h
   simp_to_raw using Raw₀.Const.get_insertIfNew ⟨m, _⟩
 
 theorem get!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
-    get! (m.insertIfNew k v) a = bif k == a && !m.contains k then v else get! m a := by
+    get! (m.insertIfNew k v) a = if k == a ∧ ¬k ∈ m then v else get! m a := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
   simp_to_raw using Raw₀.Const.get!_insertIfNew
 
 theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
     getD (m.insertIfNew k v) a fallback =
-      bif k == a && !m.contains k then v else getD m a fallback := by
+      if k == a ∧ ¬k ∈ m then v else getD m a fallback := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
   simp_to_raw using Raw₀.Const.getD_insertIfNew
 
 end Const
diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean
index b271c7926321..88bd978a199f 100644
--- a/src/Std/Data/HashMap/Lemmas.lean
+++ b/src/Std/Data/HashMap/Lemmas.lean
@@ -110,7 +110,7 @@ theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) :=
   DHashMap.isEmpty_eq_size_eq_zero
 
 theorem size_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
-    (m.insert k v).size = bif m.contains k then m.size else m.size + 1 :=
+    (m.insert k v).size = if k ∈ m then m.size else m.size + 1 :=
   DHashMap.size_insert
 
 theorem size_le_size_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
@@ -148,7 +148,7 @@ theorem mem_of_mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} : a ∈ m.
   DHashMap.mem_of_mem_erase
 
 theorem size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
-    (m.erase k).size = bif m.contains k then m.size - 1 else m.size :=
+    (m.erase k).size = if k ∈ m then m.size - 1 else m.size :=
   DHashMap.size_erase
 
 theorem size_erase_le [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).size ≤ m.size :=
@@ -185,7 +185,7 @@ theorem getElem?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
   DHashMap.Const.get?_of_isEmpty
 
 theorem getElem?_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    (m.insert k v)[a]? = bif k == a then some v else m[a]? :=
+    (m.insert k v)[a]? = if k == a then some v else m[a]? :=
   DHashMap.Const.get?_insert
 
 @[simp]
@@ -205,7 +205,7 @@ theorem getElem?_eq_none [EquivBEq α] [LawfulHashable α] {a : α} : ¬a ∈ m
   DHashMap.Const.get?_eq_none
 
 theorem getElem?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
-    (m.erase k)[a]? = bif k == a then none else m[a]? :=
+    (m.erase k)[a]? = if k == a then none else m[a]? :=
   DHashMap.Const.get?_erase
 
 @[simp]
@@ -251,7 +251,7 @@ theorem getElem!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] {a
   DHashMap.Const.get!_of_isEmpty
 
 theorem getElem!_insert [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
-    (m.insert k v)[a]! = bif k == a then v else m[a]! :=
+    (m.insert k v)[a]! = if k == a then v else m[a]! :=
   DHashMap.Const.get!_insert
 
 @[simp]
@@ -268,7 +268,7 @@ theorem getElem!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited β] {a
   DHashMap.Const.get!_eq_default
 
 theorem getElem!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} :
-    (m.erase k)[a]! = bif k == a then default else m[a]! :=
+    (m.erase k)[a]! = if k == a then default else m[a]! :=
   DHashMap.Const.get!_erase
 
 @[simp]
@@ -310,7 +310,7 @@ theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} {fallback : 
   DHashMap.Const.getD_of_isEmpty
 
 theorem getD_insert [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
-    (m.insert k v).getD a fallback = bif k == a then v else m.getD a fallback :=
+    (m.insert k v).getD a fallback = if k == a then v else m.getD a fallback :=
   DHashMap.Const.getD_insert
 
 @[simp]
@@ -327,7 +327,7 @@ theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] {a : α} {fallback :
   DHashMap.Const.getD_eq_fallback
 
 theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : β} :
-    (m.erase k).getD a fallback = bif k == a then fallback else m.getD a fallback :=
+    (m.erase k).getD a fallback = if k == a then fallback else m.getD a fallback :=
   DHashMap.Const.getD_erase
 
 @[simp]
@@ -403,7 +403,7 @@ theorem mem_of_mem_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a : α} {v
   DHashMap.mem_of_mem_insertIfNew'
 
 theorem size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
-    (m.insertIfNew k v).size = bif m.contains k then m.size else m.size + 1 :=
+    (m.insertIfNew k v).size = if k ∈ m then m.size else m.size + 1 :=
   DHashMap.size_insertIfNew
 
 theorem size_le_size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
@@ -411,7 +411,7 @@ theorem size_le_size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v :
   DHashMap.size_le_size_insertIfNew
 
 theorem getElem?_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    (m.insertIfNew k v)[a]? = bif k == a && !m.contains k then some v else m[a]? :=
+    (m.insertIfNew k v)[a]? = if k == a ∧ ¬k ∈ m then some v else m[a]? :=
   DHashMap.Const.get?_insertIfNew
 
 theorem getElem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
@@ -420,12 +420,12 @@ theorem getElem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β
   DHashMap.Const.get_insertIfNew (h₁ := h₁)
 
 theorem getElem!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
-    (m.insertIfNew k v)[a]! = bif k == a && !m.contains k then v else m[a]! :=
+    (m.insertIfNew k v)[a]! = if k == a ∧ ¬k ∈ m then v else m[a]! :=
   DHashMap.Const.get!_insertIfNew
 
 theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
     (m.insertIfNew k v).getD a fallback =
-      bif k == a && !m.contains k then v else m.getD a fallback :=
+      if k == a ∧ ¬k ∈ m then v else m.getD a fallback :=
   DHashMap.Const.getD_insertIfNew
 
 @[simp]
diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean
index ae1e3e7140d6..c1da1187f2db 100644
--- a/src/Std/Data/HashMap/RawLemmas.lean
+++ b/src/Std/Data/HashMap/RawLemmas.lean
@@ -110,7 +110,7 @@ theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) :=
   DHashMap.Raw.isEmpty_eq_size_eq_zero
 
 theorem size_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
-    (m.insert k v).size = bif m.contains k then m.size else m.size + 1 :=
+    (m.insert k v).size = if k ∈ m then m.size else m.size + 1 :=
   DHashMap.Raw.size_insert h.out
 
 theorem size_le_size_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
@@ -148,7 +148,7 @@ theorem mem_of_mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} : a ∈ m.
   DHashMap.Raw.mem_of_mem_erase h.out
 
 theorem size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
-    (m.erase k).size = bif m.contains k then m.size - 1 else m.size :=
+    (m.erase k).size = if k ∈ m then m.size - 1 else m.size :=
   DHashMap.Raw.size_erase h.out
 
 theorem size_erase_le [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).size ≤ m.size :=
@@ -185,7 +185,7 @@ theorem getElem?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
   DHashMap.Raw.Const.get?_of_isEmpty h.out
 
 theorem getElem?_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    (m.insert k v)[a]? = bif k == a then some v else m[a]? :=
+    (m.insert k v)[a]? = if k == a then some v else m[a]? :=
   DHashMap.Raw.Const.get?_insert h.out
 
 @[simp]
@@ -205,7 +205,7 @@ theorem getElem?_eq_none [EquivBEq α] [LawfulHashable α] {a : α} : ¬a ∈ m
   DHashMap.Raw.Const.get?_eq_none h.out
 
 theorem getElem?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
-    (m.erase k)[a]? = bif k == a then none else m[a]? :=
+    (m.erase k)[a]? = if k == a then none else m[a]? :=
   DHashMap.Raw.Const.get?_erase h.out
 
 @[simp]
@@ -251,7 +251,7 @@ theorem getElem!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] {a
   DHashMap.Raw.Const.get!_of_isEmpty h.out
 
 theorem getElem!_insert [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
-    (m.insert k v)[a]! = bif k == a then v else m[a]! :=
+    (m.insert k v)[a]! = if k == a then v else m[a]! :=
   DHashMap.Raw.Const.get!_insert h.out
 
 @[simp]
@@ -268,7 +268,7 @@ theorem getElem!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited β] {a
   DHashMap.Raw.Const.get!_eq_default h.out
 
 theorem getElem!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} :
-    (m.erase k)[a]! = bif k == a then default else m[a]! :=
+    (m.erase k)[a]! = if k == a then default else m[a]! :=
   DHashMap.Raw.Const.get!_erase h.out
 
 @[simp]
@@ -309,7 +309,7 @@ theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} {fallback : 
   DHashMap.Raw.Const.getD_of_isEmpty h.out
 
 theorem getD_insert [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
-    (m.insert k v).getD a fallback = bif k == a then v else m.getD a fallback :=
+    (m.insert k v).getD a fallback = if k == a then v else m.getD a fallback :=
   DHashMap.Raw.Const.getD_insert h.out
 
 @[simp]
@@ -326,7 +326,7 @@ theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] {a : α} {fallback :
   DHashMap.Raw.Const.getD_eq_fallback h.out
 
 theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : β} :
-    (m.erase k).getD a fallback = bif k == a then fallback else m.getD a fallback :=
+    (m.erase k).getD a fallback = if k == a then fallback else m.getD a fallback :=
   DHashMap.Raw.Const.getD_erase h.out
 
 @[simp]
@@ -402,7 +402,7 @@ theorem mem_of_mem_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a : α} {v
   DHashMap.Raw.mem_of_mem_insertIfNew' h.out
 
 theorem size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
-    (m.insertIfNew k v).size = bif m.contains k then m.size else m.size + 1 :=
+    (m.insertIfNew k v).size = if k ∈ m then m.size else m.size + 1 :=
   DHashMap.Raw.size_insertIfNew h.out
 
 theorem size_le_size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
@@ -410,7 +410,7 @@ theorem size_le_size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v :
   DHashMap.Raw.size_le_size_insertIfNew h.out
 
 theorem getElem?_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    (m.insertIfNew k v)[a]? = bif k == a && !m.contains k then some v else m[a]? :=
+    (m.insertIfNew k v)[a]? = if k == a ∧ ¬k ∈ m then some v else m[a]? :=
   DHashMap.Raw.Const.get?_insertIfNew h.out
 
 theorem getElem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
@@ -419,12 +419,12 @@ theorem getElem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β
   DHashMap.Raw.Const.get_insertIfNew h.out (h₁ := h₁)
 
 theorem getElem!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
-    (m.insertIfNew k v)[a]! = bif k == a && !m.contains k then v else m[a]! :=
+    (m.insertIfNew k v)[a]! = if k == a ∧ ¬k ∈ m then v else m[a]! :=
   DHashMap.Raw.Const.get!_insertIfNew h.out
 
 theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
     (m.insertIfNew k v).getD a fallback =
-      bif k == a && !m.contains k then v else m.getD a fallback :=
+      if k == a ∧ ¬k ∈ m then v else m.getD a fallback :=
   DHashMap.Raw.Const.getD_insertIfNew h.out
 
 @[simp]
diff --git a/src/Std/Data/HashSet/Lemmas.lean b/src/Std/Data/HashSet/Lemmas.lean
index 01f8356e2ab1..bee599c20d2d 100644
--- a/src/Std/Data/HashSet/Lemmas.lean
+++ b/src/Std/Data/HashSet/Lemmas.lean
@@ -102,7 +102,7 @@ theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) :=
   HashMap.isEmpty_eq_size_eq_zero
 
 theorem size_insert [EquivBEq α] [LawfulHashable α] {k : α} :
-    (m.insert k).size = bif m.contains k then m.size else m.size + 1 :=
+    (m.insert k).size = if k ∈ m then m.size else m.size + 1 :=
   HashMap.size_insertIfNew
 
 theorem size_le_size_insert [EquivBEq α] [LawfulHashable α] {k : α} : m.size ≤ (m.insert k).size :=
@@ -139,7 +139,7 @@ theorem mem_of_mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} : a ∈ m.
   HashMap.mem_of_mem_erase
 
 theorem size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
-    (m.erase k).size = bif m.contains k then m.size - 1 else m.size :=
+    (m.erase k).size = if k ∈ m then m.size - 1 else m.size :=
   HashMap.size_erase
 
 theorem size_erase_le [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).size ≤ m.size :=
diff --git a/src/Std/Data/HashSet/RawLemmas.lean b/src/Std/Data/HashSet/RawLemmas.lean
index 2e35762ac629..8d76e59d00bf 100644
--- a/src/Std/Data/HashSet/RawLemmas.lean
+++ b/src/Std/Data/HashSet/RawLemmas.lean
@@ -103,7 +103,7 @@ theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) :=
   HashMap.Raw.isEmpty_eq_size_eq_zero
 
 theorem size_insert [EquivBEq α] [LawfulHashable α] {k : α} :
-    (m.insert k).size = bif m.contains k then m.size else m.size + 1 :=
+    (m.insert k).size = if k ∈ m then m.size else m.size + 1 :=
   HashMap.Raw.size_insertIfNew h.out
 
 theorem size_le_size_insert [EquivBEq α] [LawfulHashable α] {k : α} : m.size ≤ (m.insert k).size :=
@@ -140,7 +140,7 @@ theorem mem_of_mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} : a ∈ m.
   HashMap.Raw.mem_of_mem_erase h.out
 
 theorem size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
-    (m.erase k).size = bif m.contains k then m.size - 1 else m.size :=
+    (m.erase k).size = if k ∈ m then m.size - 1 else m.size :=
   HashMap.Raw.size_erase h.out
 
 theorem size_erase_le [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).size ≤ m.size :=
diff --git a/tests/lean/elabAsElim.lean b/tests/lean/elabAsElim.lean
deleted file mode 100644
index da254e3a58ff..000000000000
--- a/tests/lean/elabAsElim.lean
+++ /dev/null
@@ -1,98 +0,0 @@
-inductive Vec (α : Type u) : Nat → Type u
-  | nil : Vec α 0
-  | cons : α → Vec α n → Vec α (n+1)
-
-def f1 (xs : Vec α n) : Nat :=
-  Vec.casesOn xs 0 fun _ _ => 1
-
-def f2 (xs : Vec α n) : Nat :=
-  xs.casesOn 0 -- Error insufficient number of arguments
-
-def f3 (x : Nat) : Nat → (Nat → Nat) → Nat :=
-  x.casesOn
-
-def f4 (xs : List Nat) : xs ≠ [] → xs.length > 0 :=
-  xs.casesOn (by intros; contradiction) (by intros; simp_arith)
-
-def f5 (xs : List Nat) (h : xs ≠ []) : xs.length > 0 :=
-  xs.casesOn (by intros; contradiction) (by intros; simp_arith) h
-
-def f6 (x : Nat) :=
-  2 * x.casesOn 0 id
-
-example : f6 (x+1) = 2*x := rfl
-
-def f7 (xs : Vec α n) : Nat :=
-  xs.casesOn (a := 10) 0 -- Error unused named args
-
-def f8 (xs : List Nat) : xs ≠ [] → xs.length > 0 :=
-  @List.casesOn _ (fun xs => xs ≠ [] → xs.length > 0) xs (by dsimp; intros; contradiction) (by dsimp; intros; simp_arith)
-
-def f5' (xs : List Nat) (h : xs ≠ []) : xs.length > 0 :=
-  xs.casesOn (fun h => absurd rfl h) (fun _ _ _ => Nat.zero_lt_succ ..) h
-
-example (h₁ : a = b) (h₂ : b = c) : a = c :=
-  Eq.rec h₂ h₁.symm
-
-@[elab_as_elim] theorem subst {p : (b : α) → a = b → Prop} (h₁ : a = b) (h₂ : p a rfl) : p b h₁ := by
-  cases h₁
-  assumption
-
-example (h₁ : a = b) (h₂ : b = c) : a = c :=
-  subst h₁.symm h₂
-
-theorem not_or_not : (¬p ∨ ¬q) → ¬(p ∧ q) := λ h ⟨hp, hq⟩ =>
-  h.rec (λ h1 => h1 hp) (λ h2 => h2 hq)
-
-structure Point where
-  x : Nat
-
-theorem PointExt_lean4 (p : Point) : forall (q : Point) (h1 : Point.x p = Point.x q), p = q :=
-  Point.recOn p <|
-   fun z1 q => Point.recOn q $
-   fun z2 (hA : Point.x (Point.mk z1) = Point.x (Point.mk z2)) => congrArg Point.mk hA
-
-inductive pos_num : Type
-  | one  : pos_num
-  | bit1 : pos_num → pos_num
-  | bit0 : pos_num → pos_num
-
-inductive num : Type
-  | zero  : num
-  | pos   : pos_num → num
-
-inductive znum : Type
-  | zero : znum
-  | pos  : pos_num → znum
-  | neg  : pos_num → znum
-
-def pos_num.pred' : pos_num → num
-  | one    => .zero
-  | bit0 n => num.pos (num.casesOn (pred' n) one bit1)
-  | bit1 n => num.pos (bit0 n)
-
-protected def znum.bit1 : znum → znum
-  | zero    => pos .one
-  | pos n => pos (pos_num.bit1 n)
-  | neg n => neg (num.casesOn (pos_num.pred' n) .one pos_num.bit1)
-
-example (h : False) : a = c :=
-  h.rec
-
-example (h : False) : a = c :=
-  h.elim
-
-noncomputable def f : Nat → Nat :=
-  Nat.rec 0 (fun x _ => x)
-
-example : ∀ x, x ≥ 0 :=
-  Nat.rec (Nat.le_refl 0) (fun _ ih => Nat.le_succ_of_le ih)
-
-@[elab_as_elim]
-def Foo.induction {P : (α : Type) → Prop} (α : Type) : P α := sorry
-
-example {n : Type} {T : n} : T = T := Foo.induction n -- motive is not type correct
-
-example {n : Type} : {T : n} → T = T := Foo.induction n -- motive is not type correct
-
-example {n : Type} : {T : n} → T = T := @(Foo.induction n)
diff --git a/tests/lean/elabAsElim.lean.expected.out b/tests/lean/elabAsElim.lean.expected.out
deleted file mode 100644
index 07450ee1193e..000000000000
--- a/tests/lean/elabAsElim.lean.expected.out
+++ /dev/null
@@ -1,8 +0,0 @@
-elabAsElim.lean:9:2-9:14: error: failed to elaborate eliminator, insufficient number of arguments, expected type:
-  Nat
-elabAsElim.lean:26:2-26:24: error: failed to elaborate eliminator, unused named arguments: [a]
-elabAsElim.lean:92:4-92:17: warning: declaration uses 'sorry'
-elabAsElim.lean:94:38-94:53: error: failed to elaborate eliminator, motive is not type correct:
-  fun x => T = T
-elabAsElim.lean:96:40-96:55: error: failed to elaborate eliminator, motive is not type correct:
-  fun x => T✝ = T✝
diff --git a/tests/lean/run/elabAsElim.lean b/tests/lean/run/elabAsElim.lean
new file mode 100644
index 000000000000..b76607fcf5d1
--- /dev/null
+++ b/tests/lean/run/elabAsElim.lean
@@ -0,0 +1,177 @@
+/-!
+# Tests of elabAsElim elaborator and the `elab_as_elim` attribute
+-/
+
+-- For debugging:
+-- set_option trace.Elab.app.elab_as_elim true
+
+inductive Vec (α : Type u) : Nat → Type u
+  | nil : Vec α 0
+  | cons : α → Vec α n → Vec α (n+1)
+
+def f1 (xs : Vec α n) : Nat :=
+  Vec.casesOn xs 0 fun _ _ => 1
+
+/-! Under-applied eliminator, and expected type isn't a pi type. -/
+/--
+error: failed to elaborate eliminator, insufficient number of arguments, expected type:
+  Nat
+-/
+#guard_msgs in
+def f2 (xs : Vec α n) : Nat :=
+  xs.casesOn 0
+
+def f3 (x : Nat) : Nat → (Nat → Nat) → Nat :=
+  x.casesOn
+
+/-! Under-applied eliminator, expected type's binders do not unify with remaining arguments. -/
+/--
+error: failed to elaborate eliminator, insufficient number of arguments, expected type:
+  (Nat → Nat) → Nat → Nat
+-/
+#guard_msgs in
+def f3' (x : Nat) : (Nat → Nat) → Nat → Nat :=
+  x.casesOn
+
+def f4 (xs : List Nat) : xs ≠ [] → xs.length > 0 :=
+  xs.casesOn (by intros; contradiction) (by intros; simp_arith)
+
+def f5 (xs : List Nat) (h : xs ≠ []) : xs.length > 0 :=
+  xs.casesOn (by intros; contradiction) (by intros; simp_arith) h
+
+def f6 (x : Nat) :=
+  2 * x.casesOn 0 id
+
+example : f6 (x+1) = 2*x := rfl
+
+/-- error: failed to elaborate eliminator, unused named arguments: [a] -/
+#guard_msgs in
+def f7 (xs : Vec α n) : Nat :=
+  xs.casesOn (a := 10) 0
+
+def f8 (xs : List Nat) : xs ≠ [] → xs.length > 0 :=
+  @List.casesOn _ (fun xs => xs ≠ [] → xs.length > 0) xs (by dsimp; intros; contradiction) (by dsimp; intros; simp_arith)
+
+def f5' (xs : List Nat) (h : xs ≠ []) : xs.length > 0 :=
+  xs.casesOn (fun h => absurd rfl h) (fun _ _ _ => Nat.zero_lt_succ ..) h
+
+example (h₁ : a = b) (h₂ : b = c) : a = c :=
+  Eq.rec h₂ h₁.symm
+
+@[elab_as_elim] theorem subst {p : (b : α) → a = b → Prop} (h₁ : a = b) (h₂ : p a rfl) : p b h₁ := by
+  cases h₁
+  assumption
+
+example (h₁ : a = b) (h₂ : b = c) : a = c :=
+  subst h₁.symm h₂
+
+theorem not_or_not : (¬p ∨ ¬q) → ¬(p ∧ q) := λ h ⟨hp, hq⟩ =>
+  h.rec (λ h1 => h1 hp) (λ h2 => h2 hq)
+
+structure Point where
+  x : Nat
+
+theorem PointExt_lean4 (p : Point) : forall (q : Point) (h1 : Point.x p = Point.x q), p = q :=
+  Point.recOn p <|
+   fun z1 q => Point.recOn q $
+   fun z2 (hA : Point.x (Point.mk z1) = Point.x (Point.mk z2)) => congrArg Point.mk hA
+
+inductive pos_num : Type
+  | one  : pos_num
+  | bit1 : pos_num → pos_num
+  | bit0 : pos_num → pos_num
+
+inductive num : Type
+  | zero  : num
+  | pos   : pos_num → num
+
+inductive znum : Type
+  | zero : znum
+  | pos  : pos_num → znum
+  | neg  : pos_num → znum
+
+def pos_num.pred' : pos_num → num
+  | one    => .zero
+  | bit0 n => num.pos (num.casesOn (pred' n) one bit1)
+  | bit1 n => num.pos (bit0 n)
+
+protected def znum.bit1 : znum → znum
+  | zero    => pos .one
+  | pos n => pos (pos_num.bit1 n)
+  | neg n => neg (num.casesOn (pos_num.pred' n) .one pos_num.bit1)
+
+example (h : False) : a = c :=
+  h.rec
+
+example (h : False) : a = c :=
+  h.elim
+
+noncomputable def f : Nat → Nat :=
+  Nat.rec 0 (fun x _ => x)
+
+example : ∀ x, x ≥ 0 :=
+  Nat.rec (Nat.le_refl 0) (fun _ ih => Nat.le_succ_of_le ih)
+
+/-!
+Tests of `@[elab_as_elim]` when the motive is not type correct.
+-/
+
+@[elab_as_elim]
+def Foo.induction {P : (α : Type) → Prop} (α : Type) : P α := sorry
+
+/--
+error: failed to elaborate eliminator, motive is not type correct:
+  fun x => T = T
+-/
+#guard_msgs in
+example {n : Type} {T : n} : T = T := Foo.induction n
+
+/--
+error: failed to elaborate eliminator, motive is not type correct:
+  fun x => T✝ = T✝
+-/
+#guard_msgs in
+example {n : Type} : {T : n} → T = T := Foo.induction n
+
+example {n : Type} : (T : n) → T = T := Foo.induction n
+
+-- Disable implicit lambda
+example {n : Type} : {T : n} → T = T := @(Foo.induction n)
+
+/-!
+A "motive is not type correct" regression test.
+The `isEmptyElim` was failing due to being under-applied and the named `(α := α)` argument
+having postponed elaboration. This fix is that `α` now elaborates eagerly.
+-/
+
+class IsEmpty (α : Sort u) : Prop where
+  protected false : α → False
+
+@[elab_as_elim]
+def isEmptyElim [IsEmpty α] {p : α → Sort _} (a : α) : p a :=
+  (IsEmpty.false a).elim
+
+def Set (α : Type u) := α → Prop
+def Set.univ {α : Type _} : Set α := fun _ => True
+instance : Membership α (Set α) := ⟨fun x s => s x⟩
+def Set.pi {α : ι → Type _} (s : Set ι) (t : (i : ι) → Set (α i)) : Set ((i : ι) → α i) := fun f => ∀ i ∈ s, f i ∈ t i
+
+example {α : Type u} [IsEmpty α] {β : α → Type v} (x : (a : α) → β a) (s : (i : α) → Set (β i)) :
+    x ∈ Set.univ.pi s := isEmptyElim (α := α)
+
+-- Simplified version:
+example {α : Type _} [IsEmpty α] :
+  id (α → False) := isEmptyElim (α := α)
+
+/-!
+From mathlib, regression test. Need to eagerly elaborate the `n ≤ m` argument to deduce `m`
+before computing the motive.
+-/
+
+@[elab_as_elim]
+def leRecOn {C : Nat → Sort _} {n : Nat} : ∀ {m}, n ≤ m → (∀ {k}, C k → C (k + 1)) → C n → C m :=
+  sorry
+
+theorem leRecOn_self {C : Nat → Sort _} {n} {next : ∀ {k}, C k → C (k + 1)} (x : C n) :
+    (leRecOn n.le_refl next x : C n) = x :=
+  sorry
diff --git a/tests/lean/run/funind_structural_mutual.lean b/tests/lean/run/funind_structural_mutual.lean
new file mode 100644
index 000000000000..d364a4880787
--- /dev/null
+++ b/tests/lean/run/funind_structural_mutual.lean
@@ -0,0 +1,94 @@
+/-!
+A few tests for functional induction theorems generated from mutual recursive inductives.
+
+Some more tests are in `structuralMutual.lean` and `funind_structural`.
+-/
+
+set_option guard_msgs.diff true
+
+
+inductive Tree (α : Type u) : Type u where
+  | node : α → (Bool → List (Tree α)) → Tree α
+
+-- Recursion over nested inductive
+
+mutual
+def Tree.size : Tree α → Nat
+  | .node _ tsf => 1 + size_aux (tsf true) + size_aux (tsf false)
+termination_by structural t => t
+def Tree.size_aux : List (Tree α) → Nat
+  | [] => 0
+  | t :: ts => size t + size_aux ts
+end
+
+/--
+info: Tree.size.induct.{u_1} {α : Type u_1} (motive_1 : Tree α → Prop) (motive_2 : List (Tree α) → Prop)
+  (case1 :
+    ∀ (a : α) (tsf : Bool → List (Tree α)), motive_2 (tsf true) → motive_2 (tsf false) → motive_1 (Tree.node a tsf))
+  (case2 : motive_2 []) (case3 : ∀ (t : Tree α) (ts : List (Tree α)), motive_1 t → motive_2 ts → motive_2 (t :: ts)) :
+  ∀ (a : Tree α), motive_1 a
+-/
+#guard_msgs in
+#check Tree.size.induct
+
+
+-- Recursion over nested inductive, functions in the “wrong” order (auxillary first)
+
+mutual
+def Tree.size_aux' : List (Tree α) → Nat
+  | [] => 0
+  | t :: ts => size' t + size_aux' ts
+def Tree.size' : Tree α → Nat
+  | .node _ tsf => 1 + size_aux' (tsf true) + size_aux' (tsf false)
+termination_by structural t => t
+end
+
+/--
+info: Tree.size_aux'.mutual_induct.{u_1} {α : Type u_1} (motive_1 : List (Tree α) → Prop) (motive_2 : Tree α → Prop)
+  (case1 :
+    ∀ (a : α) (tsf : Bool → List (Tree α)), motive_1 (tsf true) → motive_1 (tsf false) → motive_2 (Tree.node a tsf))
+  (case2 : motive_1 []) (case3 : ∀ (t : Tree α) (ts : List (Tree α)), motive_2 t → motive_1 ts → motive_1 (t :: ts)) :
+  (∀ (a : List (Tree α)), motive_1 a) ∧ ∀ (a : Tree α), motive_2 a
+-/
+#guard_msgs in
+#check Tree.size_aux'.mutual_induct
+
+-- Similar, but with many packed functions
+mutual
+def Tree.size_aux1 : List (Tree α) → Nat
+  | [] => 0
+  | t :: ts => size2 t + size_aux2 ts
+def Tree.size1 : Tree α → Nat
+  | .node _ tsf => 1 + size_aux2 (tsf true) + size_aux3 (tsf false)
+termination_by structural t => t
+def Tree.size_aux2 : List (Tree α) → Nat
+  | [] => 0
+  | t :: ts => size3 t + size_aux3 ts
+def Tree.size2 : Tree α → Nat
+  | .node _ tsf => 1 + size_aux3 (tsf true) + size_aux1 (tsf false)
+def Tree.size_aux3 : List (Tree α) → Nat
+  | [] => 0
+  | t :: ts => size1 t + size_aux1 ts
+def Tree.size3 : Tree α → Nat
+  | .node _ tsf => 1 + size_aux1 (tsf true) + size_aux2 (tsf false)
+end
+
+/--
+info: Tree.size_aux1.mutual_induct.{u_1} {α : Type u_1} (motive_1 motive_2 motive_3 : List (Tree α) → Prop)
+  (motive_4 motive_5 motive_6 : Tree α → Prop)
+  (case1 :
+    ∀ (a : α) (tsf : Bool → List (Tree α)), motive_2 (tsf true) → motive_3 (tsf false) → motive_4 (Tree.node a tsf))
+  (case2 :
+    ∀ (a : α) (tsf : Bool → List (Tree α)), motive_1 (tsf true) → motive_2 (tsf false) → motive_5 (Tree.node a tsf))
+  (case3 :
+    ∀ (a : α) (tsf : Bool → List (Tree α)), motive_3 (tsf true) → motive_1 (tsf false) → motive_6 (Tree.node a tsf))
+  (case4 : motive_1 []) (case5 : ∀ (t : Tree α) (ts : List (Tree α)), motive_6 t → motive_2 ts → motive_1 (t :: ts))
+  (case6 : motive_2 []) (case7 : ∀ (t : Tree α) (ts : List (Tree α)), motive_5 t → motive_3 ts → motive_2 (t :: ts))
+  (case8 : motive_3 []) (case9 : ∀ (t : Tree α) (ts : List (Tree α)), motive_4 t → motive_1 ts → motive_3 (t :: ts)) :
+  (∀ (a : List (Tree α)), motive_1 a) ∧
+    (∀ (a : List (Tree α)), motive_2 a) ∧
+      (∀ (a : List (Tree α)), motive_3 a) ∧
+        (∀ (a : Tree α), motive_4 a) ∧ (∀ (a : Tree α), motive_5 a) ∧ ∀ (a : Tree α), motive_6 a
+-/
+#guard_msgs in
+#check Tree.size_aux1.mutual_induct
diff --git a/tests/lean/run/funind_tests.lean b/tests/lean/run/funind_tests.lean
index 06c594c0a4b7..98e421448675 100644
--- a/tests/lean/run/funind_tests.lean
+++ b/tests/lean/run/funind_tests.lean
@@ -634,6 +634,15 @@ info: Tree.Tree.map_forest.induct (f : Tree → Tree) (motive1 : Tree → Prop)
 #guard_msgs in
 #check Tree.map_forest.induct
 
+/--
+info: Tree.Tree.map.mutual_induct (f : Tree → Tree) (motive1 : Tree → Prop) (motive2 : List Tree → Prop)
+  (case1 : ∀ (ts : List Tree), motive2 ts → motive1 (Tree.node ts))
+  (case2 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive1 t) → motive2 ts) :
+  (∀ (a : Tree), motive1 a) ∧ ∀ (ts : List Tree), motive2 ts
+-/
+#guard_msgs in
+#check Tree.map.mutual_induct
+
 end Tree
 
 namespace DefaultArgument
diff --git a/tests/lean/run/letrecInProofs.lean b/tests/lean/run/letrecInProofs.lean
index 853b9f821a0e..8f8c0aa92e94 100644
--- a/tests/lean/run/letrecInProofs.lean
+++ b/tests/lean/run/letrecInProofs.lean
@@ -19,7 +19,7 @@ theorem Tree.acyclic (x t : Tree) : x = t → x ≮ t := by
       have ihl : x ≮ l → node s x ≠ l ∧ node s x ≮ l := right x s l
       have ihr : x ≮ r → node s x ≠ r ∧ node s x ≮ r := right x s r
       have hl : x ≠ l ∧ x ≮ l := h.1
-      have hr : x ≠ r ∧ x ≮ r := h.2.1
+      have hr : x ≠ r ∧ x ≮ r := h.2
       have ihl : node s x ≠ l ∧ node s x ≮ l := ihl hl.2
       have ihr : node s x ≠ r ∧ node s x ≮ r := ihr hr.2
       apply And.intro
@@ -31,7 +31,6 @@ theorem Tree.acyclic (x t : Tree) : x = t → x ≮ t := by
       focus
         apply And.intro
         apply ihl
-        apply And.intro _ trivial
         apply ihr
   let rec left (x t : Tree) (b : Tree) (h : x ≮ b) : node x t ≠ b ∧ node x t ≮ b := by
     match b, h with
@@ -42,7 +41,7 @@ theorem Tree.acyclic (x t : Tree) : x = t → x ≮ t := by
       have ihl : x ≮ l → node x t ≠ l ∧ node x t ≮ l := left x t l
       have ihr : x ≮ r → node x t ≠ r ∧ node x t ≮ r := left x t r
       have hl : x ≠ l ∧ x ≮ l := h.1
-      have hr : x ≠ r ∧ x ≮ r := h.2.1
+      have hr : x ≠ r ∧ x ≮ r := h.2
       have ihl : node x t ≠ l ∧ node x t ≮ l := ihl hl.2
       have ihr : node x t ≠ r ∧ node x t ≮ r := ihr hr.2
       apply And.intro
@@ -54,19 +53,17 @@ theorem Tree.acyclic (x t : Tree) : x = t → x ≮ t := by
       focus
         apply And.intro
         apply ihl
-        apply And.intro _ trivial
         apply ihr
   let rec aux : (x : Tree) → x ≮ x
     | leaf     => trivial
     | node l r => by
         have ih₁ : l ≮ l := aux l
         have ih₂ : r ≮ r := aux r
-        show (node l r ≠ l ∧ node l r ≮ l) ∧ (node l r ≠ r ∧ node l r ≮ r) ∧ True
+        show (node l r ≠ l ∧ node l r ≮ l) ∧ (node l r ≠ r ∧ node l r ≮ r)
         apply And.intro
         focus
           apply left
           assumption
-        apply And.intro _ trivial
         focus
           apply right
           assumption
@@ -78,7 +75,7 @@ open Tree
 
 theorem ex1 (x : Tree) : x ≠ node leaf (node x leaf) := by
   intro h
-  exact absurd rfl $ Tree.acyclic _ _ h |>.2.1.2.1.1
+  exact absurd rfl $ Tree.acyclic _ _ h |>.2.2.1.1
 
 theorem ex2 (x : Tree) : x ≠ node x leaf := by
   intro h
@@ -86,4 +83,4 @@ theorem ex2 (x : Tree) : x ≠ node x leaf := by
 
 theorem ex3 (x y : Tree) : x ≠ node y x := by
   intro h
-  exact absurd rfl $ Tree.acyclic _ _ h |>.2.1.1
+  exact absurd rfl $ Tree.acyclic _ _ h |>.2.1
diff --git a/tests/lean/run/nestedInductiveConstructions.lean b/tests/lean/run/nestedInductiveConstructions.lean
index 6b51c1067ea3..e1d1ab8c4197 100644
--- a/tests/lean/run/nestedInductiveConstructions.lean
+++ b/tests/lean/run/nestedInductiveConstructions.lean
@@ -12,11 +12,10 @@ inductive Tree where | node  : List Tree → Tree
 info: @[reducible] protected def Ex1.Tree.below.{u} : {motive_1 : Tree → Sort u} →
   {motive_2 : List.{0} Tree → Sort u} → Tree → Sort (max 1 u) :=
 fun {motive_1} {motive_2} t =>
-  Tree.rec.{(max 1 u) + 1}
-    (fun a a_ih => PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 a) a_ih) PUnit.{max 1 u}) PUnit.{max 1 u}
+  Tree.rec.{(max 1 u) + 1} (fun a a_ih => PProd.{u, max 1 u} (motive_2 a) a_ih) PUnit.{max 1 u}
     (fun head tail head_ih tail_ih =>
       PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_1 head) head_ih)
-        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 tail) tail_ih) PUnit.{max 1 u}))
+        (PProd.{u, max 1 u} (motive_2 tail) tail_ih))
     t
 -/
 #guard_msgs in
@@ -26,11 +25,10 @@ fun {motive_1} {motive_2} t =>
 info: @[reducible] protected def Ex1.Tree.below_1.{u} : {motive_1 : Tree → Sort u} →
   {motive_2 : List.{0} Tree → Sort u} → List.{0} Tree → Sort (max 1 u) :=
 fun {motive_1} {motive_2} t =>
-  Tree.rec_1.{(max 1 u) + 1}
-    (fun a a_ih => PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 a) a_ih) PUnit.{max 1 u}) PUnit.{max 1 u}
+  Tree.rec_1.{(max 1 u) + 1} (fun a a_ih => PProd.{u, max 1 u} (motive_2 a) a_ih) PUnit.{max 1 u}
     (fun head tail head_ih tail_ih =>
       PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_1 head) head_ih)
-        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 tail) tail_ih) PUnit.{max 1 u}))
+        (PProd.{u, max 1 u} (motive_2 tail) tail_ih))
     t
 -/
 #guard_msgs in
@@ -40,8 +38,8 @@ fun {motive_1} {motive_2} t =>
 info: @[reducible] protected def Ex1.Tree.ibelow_1 : {motive_1 : Tree → Prop} →
   {motive_2 : List.{0} Tree → Prop} → List.{0} Tree → Prop :=
 fun {motive_1} {motive_2} t =>
-  Tree.rec_1.{1} (fun a a_ih => And (And (motive_2 a) a_ih) True) True
-    (fun head tail head_ih tail_ih => And (And (motive_1 head) head_ih) (And (And (motive_2 tail) tail_ih) True)) t
+  Tree.rec_1.{1} (fun a a_ih => And (motive_2 a) a_ih) True
+    (fun head tail head_ih tail_ih => And (And (motive_1 head) head_ih) (And (motive_2 tail) tail_ih)) t
 -/
 #guard_msgs in
 #print Tree.ibelow_1
@@ -82,16 +80,15 @@ info: @[reducible] protected def Ex2.Tree.below.{u} : {motive_1 : Tree → Sort
 fun {motive_1} {motive_2} {motive_3} t =>
   Tree.rec.{(max 1 u) + 1}
     (fun a a_1 a_ih a_ih_1 =>
-      PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 a) a_ih)
-        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 a_1) a_ih_1) PUnit.{max 1 u}))
+      PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 a) a_ih) (PProd.{u, max 1 u} (motive_3 a_1) a_ih_1))
     PUnit.{max 1 u}
     (fun head tail head_ih tail_ih =>
       PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 head) head_ih)
-        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 tail) tail_ih) PUnit.{max 1 u}))
+        (PProd.{u, max 1 u} (motive_2 tail) tail_ih))
     PUnit.{max 1 u}
     (fun head tail head_ih tail_ih =>
       PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_1 head) head_ih)
-        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 tail) tail_ih) PUnit.{max 1 u}))
+        (PProd.{u, max 1 u} (motive_3 tail) tail_ih))
     t
 -/
 #guard_msgs in
@@ -104,16 +101,15 @@ info: @[reducible] protected def Ex2.Tree.below_1.{u} : {motive_1 : Tree → Sor
 fun {motive_1} {motive_2} {motive_3} t =>
   Tree.rec_1.{(max 1 u) + 1}
     (fun a a_1 a_ih a_ih_1 =>
-      PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 a) a_ih)
-        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 a_1) a_ih_1) PUnit.{max 1 u}))
+      PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 a) a_ih) (PProd.{u, max 1 u} (motive_3 a_1) a_ih_1))
     PUnit.{max 1 u}
     (fun head tail head_ih tail_ih =>
       PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 head) head_ih)
-        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 tail) tail_ih) PUnit.{max 1 u}))
+        (PProd.{u, max 1 u} (motive_2 tail) tail_ih))
     PUnit.{max 1 u}
     (fun head tail head_ih tail_ih =>
       PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_1 head) head_ih)
-        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 tail) tail_ih) PUnit.{max 1 u}))
+        (PProd.{u, max 1 u} (motive_3 tail) tail_ih))
     t
 -/
 #guard_msgs in
@@ -126,16 +122,15 @@ info: @[reducible] protected def Ex2.Tree.below_2.{u} : {motive_1 : Tree → Sor
 fun {motive_1} {motive_2} {motive_3} t =>
   Tree.rec_2.{(max 1 u) + 1}
     (fun a a_1 a_ih a_ih_1 =>
-      PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 a) a_ih)
-        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 a_1) a_ih_1) PUnit.{max 1 u}))
+      PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 a) a_ih) (PProd.{u, max 1 u} (motive_3 a_1) a_ih_1))
     PUnit.{max 1 u}
     (fun head tail head_ih tail_ih =>
       PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 head) head_ih)
-        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 tail) tail_ih) PUnit.{max 1 u}))
+        (PProd.{u, max 1 u} (motive_2 tail) tail_ih))
     PUnit.{max 1 u}
     (fun head tail head_ih tail_ih =>
       PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_1 head) head_ih)
-        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 tail) tail_ih) PUnit.{max 1 u}))
+        (PProd.{u, max 1 u} (motive_3 tail) tail_ih))
     t
 -/
 #guard_msgs in
@@ -169,12 +164,10 @@ inductive Tree : Type u where | node : List Tree → Tree
 info: @[reducible] protected def Ex3.Tree.below.{u_1, u} : {motive_1 : Tree.{u} → Sort u_1} →
   {motive_2 : List.{u} Tree.{u} → Sort u_1} → Tree.{u} → Sort (max 1 u_1) :=
 fun {motive_1} {motive_2} t =>
-  Tree.rec.{(max 1 u_1) + 1, u}
-    (fun a a_ih => PProd.{max 1 u_1, max 1 u_1} (PProd.{u_1, max 1 u_1} (motive_2 a) a_ih) PUnit.{max 1 u_1})
-    PUnit.{max 1 u_1}
+  Tree.rec.{(max 1 u_1) + 1, u} (fun a a_ih => PProd.{u_1, max 1 u_1} (motive_2 a) a_ih) PUnit.{max 1 u_1}
     (fun head tail head_ih tail_ih =>
       PProd.{max 1 u_1, max 1 u_1} (PProd.{u_1, max 1 u_1} (motive_1 head) head_ih)
-        (PProd.{max 1 u_1, max 1 u_1} (PProd.{u_1, max 1 u_1} (motive_2 tail) tail_ih) PUnit.{max 1 u_1}))
+        (PProd.{u_1, max 1 u_1} (motive_2 tail) tail_ih))
     t
 -/
 #guard_msgs in
@@ -184,12 +177,10 @@ fun {motive_1} {motive_2} t =>
 info: @[reducible] protected def Ex3.Tree.below_1.{u_1, u} : {motive_1 : Tree.{u} → Sort u_1} →
   {motive_2 : List.{u} Tree.{u} → Sort u_1} → List.{u} Tree.{u} → Sort (max 1 u_1) :=
 fun {motive_1} {motive_2} t =>
-  Tree.rec_1.{(max 1 u_1) + 1, u}
-    (fun a a_ih => PProd.{max 1 u_1, max 1 u_1} (PProd.{u_1, max 1 u_1} (motive_2 a) a_ih) PUnit.{max 1 u_1})
-    PUnit.{max 1 u_1}
+  Tree.rec_1.{(max 1 u_1) + 1, u} (fun a a_ih => PProd.{u_1, max 1 u_1} (motive_2 a) a_ih) PUnit.{max 1 u_1}
     (fun head tail head_ih tail_ih =>
       PProd.{max 1 u_1, max 1 u_1} (PProd.{u_1, max 1 u_1} (motive_1 head) head_ih)
-        (PProd.{max 1 u_1, max 1 u_1} (PProd.{u_1, max 1 u_1} (motive_2 tail) tail_ih) PUnit.{max 1 u_1}))
+        (PProd.{u_1, max 1 u_1} (motive_2 tail) tail_ih))
     t
 -/
 #guard_msgs in
diff --git a/tests/lean/run/structuralMutual.lean b/tests/lean/run/structuralMutual.lean
index abea5427e531..f3bdec673e17 100644
--- a/tests/lean/run/structuralMutual.lean
+++ b/tests/lean/run/structuralMutual.lean
@@ -1,5 +1,3 @@
-import Lean.Elab.Command
-
 set_option guard_msgs.diff true
 
 /-!
@@ -527,13 +525,13 @@ Too many possible combinations of parameters of type Nattish (or please indicate
 Could not find a decreasing measure.
 The arguments relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
-Call from ManyCombinations.f to ManyCombinations.g at 559:15-29:
+Call from ManyCombinations.f to ManyCombinations.g at 557:15-29:
    #1 #2 #3 #4
 #5  ?  ?  ?  ?
 #6  ?  =  ?  ?
 #7  ?  ?  =  ?
 #8  ?  ?  ?  =
-Call from ManyCombinations.g to ManyCombinations.f at 562:15-29:
+Call from ManyCombinations.g to ManyCombinations.f at 560:15-29:
    #5 #6 #7 #8
 #1  _  _  _  _
 #2  _  =  _  _
@@ -583,73 +581,55 @@ namespace FunIndTests
 -- out nicely
 
 /--
-error: Failed to realize constant A.size.induct:
-  Induction principles for mutually structurally recursive functions are not yet supported
----
-error: Failed to realize constant A.size.induct:
-  Induction principles for mutually structurally recursive functions are not yet supported
----
-error: unknown identifier 'A.size.induct'
+info: A.size.induct (motive_1 : A → Prop) (motive_2 : B → Prop) (case1 : ∀ (a : A), motive_1 a → motive_1 a.self)
+  (case2 : ∀ (b : B), motive_2 b → motive_1 (A.other b)) (case3 : motive_1 A.empty)
+  (case4 : ∀ (b : B), motive_2 b → motive_2 b.self) (case5 : ∀ (a : A), motive_1 a → motive_2 (B.other a))
+  (case6 : motive_2 B.empty) : ∀ (a : A), motive_1 a
 -/
 #guard_msgs in
 #check A.size.induct
 
 /--
-error: Failed to realize constant A.subs.induct:
-  Induction principles for mutually structurally recursive functions are not yet supported
----
-error: Failed to realize constant A.subs.induct:
-  Induction principles for mutually structurally recursive functions are not yet supported
----
-error: unknown identifier 'A.subs.induct'
+info: A.subs.induct (motive_1 : A → Prop) (motive_2 : B → Prop) (case1 : ∀ (a : A), motive_1 a → motive_1 a.self)
+  (case2 : ∀ (b : B), motive_2 b → motive_1 (A.other b)) (case3 : motive_1 A.empty)
+  (case4 : ∀ (b : B), motive_2 b → motive_2 b.self) (case5 : ∀ (a : A), motive_1 a → motive_2 (B.other a))
+  (case6 : motive_2 B.empty) (a : A) : motive_1 a
 -/
 #guard_msgs in
 #check A.subs.induct
 
 /--
-error: Failed to realize constant MutualIndNonMutualFun.A.self_size.induct:
-  functional induction: cannot handle mutual or nested inductives
----
-error: Failed to realize constant MutualIndNonMutualFun.A.self_size.induct:
-  functional induction: cannot handle mutual or nested inductives
----
-error: unknown identifier 'MutualIndNonMutualFun.A.self_size.induct'
+info: MutualIndNonMutualFun.A.self_size.induct (motive : MutualIndNonMutualFun.A → Prop)
+  (case1 : ∀ (a : MutualIndNonMutualFun.A), motive a → motive a.self)
+  (case2 : ∀ (a : MutualIndNonMutualFun.B), motive (MutualIndNonMutualFun.A.other a))
+  (case3 : motive MutualIndNonMutualFun.A.empty) : ∀ (a : MutualIndNonMutualFun.A), motive a
 -/
 #guard_msgs in
 #check MutualIndNonMutualFun.A.self_size.induct
 
 /--
-error: Failed to realize constant MutualIndNonMutualFun.A.self_size_with_param.induct:
-  functional induction: cannot handle mutual or nested inductives
----
-error: Failed to realize constant MutualIndNonMutualFun.A.self_size_with_param.induct:
-  functional induction: cannot handle mutual or nested inductives
----
-error: unknown identifier 'MutualIndNonMutualFun.A.self_size_with_param.induct'
+info: MutualIndNonMutualFun.A.self_size_with_param.induct (motive : Nat → MutualIndNonMutualFun.A → Prop)
+  (case1 : ∀ (n : Nat) (a : MutualIndNonMutualFun.A), motive n a → motive n a.self)
+  (case2 : ∀ (x : Nat) (a : MutualIndNonMutualFun.B), motive x (MutualIndNonMutualFun.A.other a))
+  (case3 : ∀ (x : Nat), motive x MutualIndNonMutualFun.A.empty) :
+  ∀ (a : Nat) (a_1 : MutualIndNonMutualFun.A), motive a a_1
 -/
 #guard_msgs in
 #check MutualIndNonMutualFun.A.self_size_with_param.induct
 
 /--
-error: Failed to realize constant A.hasNoBEmpty.induct:
-  Induction principles for mutually structurally recursive functions are not yet supported
----
-error: Failed to realize constant A.hasNoBEmpty.induct:
-  Induction principles for mutually structurally recursive functions are not yet supported
----
-error: unknown identifier 'A.hasNoBEmpty.induct'
+info: A.hasNoBEmpty.induct (motive_1 : A → Prop) (motive_2 : B → Prop) (case1 : ∀ (a : A), motive_1 a → motive_1 a.self)
+  (case2 : ∀ (b : B), motive_2 b → motive_1 (A.other b)) (case3 : motive_1 A.empty)
+  (case4 : ∀ (b : B), motive_2 b → motive_2 b.self) (case5 : ∀ (a : A), motive_1 a → motive_2 (B.other a))
+  (case6 : motive_2 B.empty) : ∀ (a : A), motive_1 a
 -/
 #guard_msgs in
 #check A.hasNoBEmpty.induct
 
 /--
-error: Failed to realize constant EvenOdd.isEven.induct:
-  Induction principles for mutually structurally recursive functions are not yet supported
----
-error: Failed to realize constant EvenOdd.isEven.induct:
-  Induction principles for mutually structurally recursive functions are not yet supported
----
-error: unknown identifier 'EvenOdd.isEven.induct'
+info: EvenOdd.isEven.induct (motive_1 motive_2 : Nat → Prop) (case1 : motive_1 0)
+  (case2 : ∀ (n : Nat), motive_2 n → motive_1 n.succ) (case3 : motive_2 0)
+  (case4 : ∀ (n : Nat), motive_1 n → motive_2 n.succ) : ∀ (a : Nat), motive_1 a
 -/
 #guard_msgs in
 #check EvenOdd.isEven.induct -- TODO: This error message can be improved
diff --git a/tests/lean/termination_by.lean.expected.out b/tests/lean/termination_by.lean.expected.out
index 41b7308ab95b..b438c7f68249 100644
--- a/tests/lean/termination_by.lean.expected.out
+++ b/tests/lean/termination_by.lean.expected.out
@@ -1,20 +1,20 @@
-termination_by.lean:9:2-9:18: error: unused `termination_by`, function is not recursive
-termination_by.lean:12:2-12:21: error: unused `decreasing_by`, function is not recursive
-termination_by.lean:15:2-16:21: error: unused termination hints, function is not recursive
-termination_by.lean:19:2-19:18: error: unused `termination_by`, function is partial
-termination_by.lean:22:2-22:21: error: unused `decreasing_by`, function is partial
-termination_by.lean:25:2-26:21: error: unused termination hints, function is partial
-termination_by.lean:29:0-29:16: error: unused `termination_by`, function is unsafe
-termination_by.lean:32:2-32:21: error: unused `decreasing_by`, function is unsafe
-termination_by.lean:35:2-36:21: error: unused termination hints, function is unsafe
-termination_by.lean:40:4-40:20: error: unused `termination_by`, function is not recursive
-termination_by.lean:44:4-44:20: error: unused `termination_by`, function is not recursive
-termination_by.lean:54:2-54:18: error: unused `termination_by`, function is not recursive
-termination_by.lean:62:2-62:23: error: Incomplete set of `termination_by` annotations:
+termination_by.lean:9:2-9:18: warning: unused `termination_by`, function is not recursive
+termination_by.lean:12:2-12:21: warning: unused `decreasing_by`, function is not recursive
+termination_by.lean:15:2-16:21: warning: unused termination hints, function is not recursive
+termination_by.lean:19:2-19:18: warning: unused `termination_by`, function is partial
+termination_by.lean:22:2-22:21: warning: unused `decreasing_by`, function is partial
+termination_by.lean:25:2-26:21: warning: unused termination hints, function is partial
+termination_by.lean:29:0-29:16: warning: unused `termination_by`, function is unsafe
+termination_by.lean:32:2-32:21: warning: unused `decreasing_by`, function is unsafe
+termination_by.lean:35:2-36:21: warning: unused termination hints, function is unsafe
+termination_by.lean:40:4-40:20: warning: unused `termination_by`, function is not recursive
+termination_by.lean:44:4-44:20: warning: unused `termination_by`, function is not recursive
+termination_by.lean:54:2-54:18: warning: unused `termination_by`, function is not recursive
+termination_by.lean:62:2-62:23: error: incomplete set of `termination_by` annotations:
 This function is mutually with isOdd, which does not have a `termination_by` clause.
 The present clause is ignored.
 Try this: termination_by x1 => x1
-termination_by.lean:79:2-79:27: error: Incomplete set of `termination_by` annotations:
+termination_by.lean:79:2-79:27: error: incomplete set of `termination_by` annotations:
 This function is mutually with Test.f, Test.h and Test.i, which do not have a `termination_by` clause.
 The present clause is ignored.
 termination_by.lean:101:2-101:27: error: Invalid `termination_by`; this function is mutually recursive with Test2.f, which is marked as `termination_by structural` so this one also needs to be marked `structural`.
diff --git a/tests/lean/unusedLet.lean.expected.out b/tests/lean/unusedLet.lean.expected.out
index c33c68f746c4..7408d3dcc9a7 100644
--- a/tests/lean/unusedLet.lean.expected.out
+++ b/tests/lean/unusedLet.lean.expected.out
@@ -8,5 +8,5 @@ fun x =>
       | 0 => fun x => 1
       | n.succ => fun x =>
         let y := 42;
-        2 * x.fst.fst)
+        2 * x.1.1)
       f