feat: some missing Array grind annotations

src/Init/Data/Dyadic/Basic.lean

@@ -440,11 +440,11 @@ theorem toDyadic_mkRat (a : Int) (b : Nat) (prec : Int) :
   cases prec
   · simp only [Rat.toDyadic, Int.ofNat_eq_natCast, Int.toNat_natCast, Int.toNat_neg_natCast,
       shiftLeft_zero, Int.natCast_mul]
-    rw [Int.mul_comm d, ← Int.ediv_ediv_of_nonneg (by simp), ← Int.shiftLeft_mul,
+    rw [Int.mul_comm d, ← Int.ediv_ediv (by simp), ← Int.shiftLeft_mul,
       Int.mul_ediv_cancel _ (by simpa using hm)]
   · simp only [Rat.toDyadic, Int.natCast_shiftLeft, Int.negSucc_eq, ← Int.natCast_add_one,
       Int.toNat_neg_natCast, Int.shiftLeft_zero, Int.neg_neg, Int.toNat_natCast, Int.natCast_mul]
-    rw [Int.mul_comm d, ← Int.mul_shiftLeft, ← Int.ediv_ediv_of_nonneg (by simp),
+    rw [Int.mul_comm d, ← Int.mul_shiftLeft, ← Int.ediv_ediv (by simp),
       Int.mul_ediv_cancel _ (by simpa using hm)]
 
 theorem toDyadic_eq_ofIntWithPrec (x : Rat) (prec : Int) :
@@ -472,7 +472,7 @@ theorem toRat_toDyadic (x : Rat) (prec : Int) :
       Rat.den_ofNat, Nat.one_pow, Nat.mul_one]
     split
     · simp_all
-    · rw [Int.ediv_ediv_of_nonneg (Int.natCast_nonneg _)]
+    · rw [Int.ediv_ediv (Int.natCast_nonneg _)]
       congr 1
       rw [Int.natCast_ediv, Int.mul_ediv_cancel']
       rw [Int.natCast_dvd_natCast]
@@ -495,7 +495,7 @@ theorem toRat_toDyadic (x : Rat) (prec : Int) :
     simp only [this, Int.mul_one]
     split
     · simp_all
-    · rw [Int.ediv_ediv_of_nonneg (Int.natCast_nonneg _)]
+    · rw [Int.ediv_ediv (Int.natCast_nonneg _)]
       congr 1
       rw [Int.natCast_ediv, Int.mul_ediv_cancel']
       · simp

src/Init/Data/Int/DivMod.lean

@@ -9,4 +9,3 @@ prelude
 public import Init.Data.Int.DivMod.Basic
 public import Init.Data.Int.DivMod.Bootstrap
 public import Init.Data.Int.DivMod.Lemmas
-public import Init.Data.Int.DivMod.Pow

src/Init/Data/Int/DivMod/Lemmas.lean

@@ -145,12 +145,6 @@ theorem dvd_of_mul_dvd_mul_left {a m n : Int} (ha : a ≠ 0) (h : a * m ∣ a *
 theorem dvd_of_mul_dvd_mul_right {a m n : Int} (ha : a ≠ 0) (h : m * a ∣ n * a) : m ∣ n :=
   dvd_of_mul_dvd_mul_left ha (by simpa [Int.mul_comm] using h)
 
-theorem dvd_mul_of_dvd_right {a b c : Int} (h : a ∣ c) : a ∣ b * c :=
-  Int.dvd_trans h (Int.dvd_mul_left b c)
-
-theorem dvd_mul_of_dvd_left {a b c : Int} (h : a ∣ b) : a ∣ b * c :=
-  Int.dvd_trans h (Int.dvd_mul_right b c)
-
 @[norm_cast] theorem natCast_dvd_natCast {m n : Nat} : (↑m : Int) ∣ ↑n ↔ m ∣ n where
   mp := by
     rintro ⟨a, h⟩
@@ -1235,7 +1229,7 @@ private theorem ediv_ediv_of_pos {x y z : Int} (hy : 0 < y) (hz : 0 < z) :
   · rw [Int.mul_comm y, ← Int.mul_assoc, ← Int.add_mul, Int.mul_comm _ z]
     exact Int.lt_mul_of_ediv_lt hy (Int.lt_mul_ediv_self_add hz)
 
-theorem ediv_ediv_of_nonneg {x y z : Int} (hy : 0 ≤ y) : x / y / z = x / (y * z) := by
+theorem ediv_ediv {x y z : Int} (hy : 0 ≤ y) : x / y / z = x / (y * z) := by
   rcases y with (_ | a) | a
   · simp
   · rcases z with (_ | b) | b
@@ -1244,21 +1238,6 @@ theorem ediv_ediv_of_nonneg {x y z : Int} (hy : 0 ≤ y) : x / y / z = x / (y *
     · simp [Int.negSucc_eq, Int.mul_neg, ediv_ediv_of_pos]
   · simp at hy
 
-theorem ediv_ediv {x y z : Int} : x / y / z = x / (y * z) - if y < 0 ∧ ¬ z ∣ x / y then z.sign else 0 := by
-  rcases y with y | y
-  · rw [ediv_ediv_of_nonneg (by simp), if_neg (by simp; omega)]
-    simp
-  · rw [Int.negSucc_eq, Int.ediv_neg, Int.neg_mul, Int.ediv_neg, Int.neg_ediv, ediv_ediv_of_nonneg (by omega)]
-    simp
-
-theorem ediv_mul {x y z : Int} : x / (y * z) = x / y / z + if y < 0 ∧ ¬ z ∣ x / y then z.sign else 0 := by
-  have := ediv_ediv (x := x) (y := y) (z := z)
-  omega
-
-theorem ediv_mul_of_nonneg {x y z : Int} (hy : 0 ≤ y) : x / (y * z) = x / y / z := by
-  have := ediv_ediv_of_nonneg (x := x) (y := y) (z := z) hy
-  omega
-
 /-! ### tdiv -/
 
 -- `tdiv` analogues of `ediv` lemmas from `Bootstrap.lean`

src/Init/Data/Int/DivMod/Pow.lean

@@ -1,35 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison
--/
-module
-prelude
-public import Init.Data.Int.DivMod.Lemmas
-public import Init.Data.Int.Pow
-
-/-!
-# Lemmas about divisibility of powers
--/
-
-namespace Int
-
-theorem dvd_pow {a b : Int} {n : Nat} (hab : b ∣ a) : b ^ n ∣ a ^ n := by
-  rcases hab with ⟨c, rfl⟩
-  rw [Int.mul_pow]
-  exact Int.dvd_mul_right (b ^ n) (c ^ n)
-
-theorem ediv_pow {a b : Int} {n : Nat} (hab : b ∣ a) :
-    (a / b) ^ n = a ^ n / b ^ n := by
-  obtain ⟨c, rfl⟩ := hab
-  by_cases b = 0
-  · by_cases n = 0 <;> simp [*, Int.zero_pow]
-  · simp [Int.mul_pow, Int.pow_ne_zero, *]
-
-theorem tdiv_pow {a b : Int} {n : Nat} (hab : b ∣ a) :
-    (a.tdiv b) ^ n = (a ^ n).tdiv (b ^ n) := by
-  rw [Int.tdiv_eq_ediv_of_dvd hab, ediv_pow hab, Int.tdiv_eq_ediv_of_dvd (dvd_pow hab)]
-
-theorem fdiv_pow {a b : Int} {n : Nat} (hab : b ∣ a) :
-    (a.fdiv b) ^ n = (a ^ n).fdiv (b ^ n) := by
-  rw [Int.fdiv_eq_ediv_of_dvd hab, ediv_pow hab, Int.fdiv_eq_ediv_of_dvd (dvd_pow hab)]

src/Init/Data/Int/Lemmas.lean

@@ -552,7 +552,7 @@ protected theorem mul_eq_zero {a b : Int} : a * b = 0 ↔ a = 0 ∨ b = 0 := by
   exact match a, b, h with
   | .ofNat 0, _, _ => by simp
   | _, .ofNat 0, _ => by simp
-  | .ofNat (_+1), .negSucc _, h => by cases h
+  | .ofNat (a+1), .negSucc b, h => by cases h
 
 protected theorem mul_ne_zero {a b : Int} (a0 : a ≠ 0) (b0 : b ≠ 0) : a * b ≠ 0 :=
   Or.rec a0 b0 ∘ Int.mul_eq_zero.mp

src/Init/Data/Int/Pow.lean

@@ -32,13 +32,6 @@ protected theorem zero_pow {n : Nat} (h : n ≠ 0) : (0 : Int) ^ n = 0 := by
 protected theorem one_pow {n : Nat} : (1 : Int) ^ n = 1 := by
   induction n with simp_all [Int.pow_succ]
 
-protected theorem mul_pow {a b : Int} {n : Nat} : (a * b) ^ n = a ^ n * b ^ n := by
-  induction n with
-  | zero => simp
-  | succ n ih =>
-    rw [Int.pow_succ, Int.pow_succ, Int.pow_succ, ih, Int.mul_assoc, Int.mul_assoc,
-      Int.mul_left_comm (b^n)]
-
 protected theorem pow_pos {n : Int} {m : Nat} : 0 < n → 0 < n ^ m := by
   induction m with
   | zero => simp

src/Lean/Compiler/LCNF/Util.lean

@@ -9,7 +9,6 @@ prelude
 public import Init.Data.FloatArray.Basic
 public import Lean.CoreM
 public import Lean.Util.Recognizers
-import Lean.Meta.Basic
 
 public section
 

src/Lean/Elab/MutualDef.lean

@@ -1322,9 +1322,6 @@ where
           if !(← isProp header.type) then
             return false
         return true))) do
-    -- Never export private decls from theorem bodies to make sure they stay irrelevant for rebuilds
-    withOptions (fun opts =>
-      if headers.any (·.kind.isTheorem) then ResolveName.backward.privateInPublic.set opts false else opts) do
     let headers := headers.map fun header =>
       { header with modifiers.attrs := header.modifiers.attrs.filter (!·.name ∈ [`expose, `no_expose]) }
     let values ← try

src/Lean/Elab/Structure.lean

@@ -10,7 +10,6 @@ public import Lean.Meta.Structure
 public import Lean.Elab.MutualInductive
 import Lean.Linter.Basic
 import Lean.DocString
-import Lean.DocString.Extension
 
 public section
 
@@ -662,8 +661,8 @@ private partial def withStructField (view : StructView) (sourceStructNames : Lis
     let mut declName := view.declName ++ fieldName
     if inSubobject?.isNone then
       declName ← applyVisibility (← toModifiers fieldInfo) declName
-      -- Create a link to the parent field's docstring
-      addInheritedDocString declName fieldInfo.projFn
+      -- No need to validate links because this docstring was already added to the environment previously
+      addDocStringCore' declName (← findDocString? (← getEnv) fieldInfo.projFn)
       addDeclarationRangesFromSyntax declName (← getRef)
     checkNotAlreadyDeclared declName
     withLocalDecl fieldName fieldInfo.binderInfo (← reduceFieldProjs fieldType) fun fieldFVar => do

src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/TypeAnalysis.lean

@@ -71,7 +71,7 @@ def isSupportedMatch (declName : Name) : MetaM (Option MatchKind) := do
       Where we have as many arms as constructors but the last arm is a default.
       -/
 
-      if let some kind ← trySimpleEnum inductiveInfo xs numCtors motive then
+      if let some kind ← trySimpleEnum defnInfo inductiveInfo xs numCtors motive then
         return kind
 
     if xs.size > 2 then
@@ -97,11 +97,12 @@ def isSupportedMatch (declName : Name) : MetaM (Option MatchKind) := do
 
       if !defaultOk then return none
 
+      if !(← verifyEnumWithDefault defnInfo inductiveInfo handledCtors) then return none
       return some <| .enumWithDefault inductiveInfo handledCtors
     else
       return none
 where
-  trySimpleEnum (inductiveInfo : InductiveVal) (xs : Array Expr)
+  trySimpleEnum (defnInfo : DefinitionVal) (inductiveInfo : InductiveVal) (xs : Array Expr)
       (numCtors : Nat) (motive : Expr) : MetaM (Option MatchKind) := do
     -- Check that all parameters are `h_n EnumInductive.ctor`
     let mut handledCtors := Array.mkEmpty numCtors
@@ -112,8 +113,66 @@ where
       let .ctorInfo ctorInfo ← getConstInfo c | return none
       handledCtors := handledCtors.push ctorInfo
 
+    if !(← verifySimpleEnum defnInfo inductiveInfo handledCtors) then return none
+
     return some <| .simpleEnum inductiveInfo handledCtors
 
+  verifySimpleCasesOnApp (inductiveInfo : InductiveVal) (fn : Expr) (args : Array Expr)
+      (params : Array Expr) : MetaM Bool := do
+    -- Body is an application of `EnumInductive.casesOn`
+    if !fn.isConstOf (mkCasesOnName inductiveInfo.name) then return false
+    if args.size != inductiveInfo.numCtors + 2 then return false
+    -- first argument is `(fun x => motive x)`
+    let firstArgOk ← lambdaTelescope args[0]! fun args body => do
+      if args.size != 1 then return false
+      let arg := args[0]!
+      let .app fn arg' := body | return false
+      return fn == params[0]! && arg == arg'
+
+    if !firstArgOk then return false
+
+    -- second argument is discr
+    return args[1]! == params[1]!
+
+  verifySimpleEnum (defnInfo : DefinitionVal) (inductiveInfo : InductiveVal)
+      (ctors : Array ConstructorVal) : MetaM Bool := do
+    lambdaTelescope defnInfo.value fun params body =>
+      body.withApp fun fn args => do
+        if !(← verifySimpleCasesOnApp inductiveInfo fn args params) then return false
+
+        -- remaining arguments are of the form `(h_n Unit.unit)`
+        for i in *...inductiveInfo.numCtors do
+          let .app fn (.const ``Unit.unit []) := args[i + 2]! | return false
+          let some (_, .app _ (.const relevantCtor ..)) := (← inferType fn).arrow? | unreachable!
+          let some ctorIdx := ctors.findIdx? (·.name == relevantCtor) | unreachable!
+          if fn != params[ctorIdx + 2]! then return false
+
+        return true
+
+  verifyEnumWithDefault (defnInfo : DefinitionVal) (inductiveInfo : InductiveVal)
+      (ctors : Array ConstructorVal) : MetaM Bool := do
+    lambdaTelescope defnInfo.value fun params body =>
+      body.withApp fun fn args => do
+        if !(← verifySimpleCasesOnApp inductiveInfo fn args params) then return false
+
+        /-
+        Remaining arguments are of the form:
+        - `(h_n Unit.unit)` if the constructor is handled explicitly
+        - `(h_n InductiveEnum.ctor)` if the constructor is handled as part of the default case
+        -/
+        for i in *...inductiveInfo.numCtors do
+          let .app fn (.const argName ..) := args[i + 2]! | return false
+          if argName == ``Unit.unit then
+            let some (_, .app _ (.const relevantCtor ..)) := (← inferType fn).arrow? | unreachable!
+            let some ctorIdx := ctors.findIdx? (·.name == relevantCtor) | unreachable!
+            if fn != params[ctorIdx + 2]! then return false
+          else
+            let .ctorInfo ctorInfo ← getConstInfo argName | return false
+            if ctorInfo.cidx != i then return false
+            if fn != params[params.size - 1]! then return false
+
+        return true
+
 def builtinTypes : Array Name :=
   #[``BitVec, ``Bool,
     ``UInt8, ``UInt16, ``UInt32, ``UInt64, ``USize,

src/Lean/Elab/Tactic/Grind/Main.lean

@@ -11,7 +11,6 @@ public import Lean.Elab.Command
 public import Lean.Elab.Tactic.Config
 public import Lean.LibrarySuggestions.Basic
 import Lean.Meta.Tactic.Grind.SimpUtil
-import Lean.Meta.Tactic.Grind.Util
 import Lean.Meta.Tactic.Grind.EMatchTheoremParam
 import Lean.Elab.Tactic.Grind.Basic
 import Lean.Elab.Tactic.Grind.Param
@@ -151,21 +150,32 @@ def grind
     return {}
   mvarId.withContext do
     let params ← mkGrindParams config only ps mvarId
-    Grind.withProtectedMCtx config.abstractProof mvarId fun mvarId' => do
-      let finalize (result : Grind.Result) : TacticM Grind.Trace := do
-        if result.hasFailed then
-          throwError "`grind` failed\n{← result.toMessageData}"
-        return result.trace
-      if let some seq := seq? then
-        let (result, _) ← Grind.GrindTacticM.runAtGoal mvarId' params do
-          Grind.evalGrindTactic seq
-          -- **Note**: We are returning only the first goal that could not be solved.
-          let goal? := if let goal :: _ := (← get).goals then some goal else none
-          Grind.liftGrindM <| Grind.mkResult params goal?
-        finalize result
+    let type ← mvarId.getType
+    let mvar' ← mkFreshExprSyntheticOpaqueMVar type
+    let finalize (result : Grind.Result) : TacticM Grind.Trace := do
+      if result.hasFailed then
+        throwError "`grind` failed\n{← result.toMessageData}"
+      trace[grind.debug.proof] "{← instantiateMVars mvar'}"
+      -- `grind` proofs are often big, if `abstractProof` is true, we create an auxiliary theorem.
+      let e ← if !config.abstractProof then
+        instantiateMVarsProfiling mvar'
+      else if (← isProp type) then
+        mkAuxTheorem type (← instantiateMVarsProfiling mvar') (zetaDelta := true)
       else
-        let result ← Grind.main mvarId' params
-        finalize result
+        let auxName ← Term.mkAuxName `grind
+        mkAuxDefinition auxName type (← instantiateMVarsProfiling mvar') (zetaDelta := true)
+      mvarId.assign e
+      return result.trace
+    if let some seq := seq? then
+      let (result, _) ← Grind.GrindTacticM.runAtGoal mvar'.mvarId! params do
+        Grind.evalGrindTactic seq
+        -- **Note**: We are returning only the first goal that could not be solved.
+        let goal? := if let goal :: _ := (← get).goals then some goal else none
+        Grind.liftGrindM <| Grind.mkResult params goal?
+      finalize result
+    else
+      let result ← Grind.main mvar'.mvarId! params
+      finalize result
 
 def evalGrindCore
     (ref : Syntax)
@@ -263,8 +273,7 @@ private def elabGrindConfig' (config : TSyntax ``Lean.Parser.Tactic.optConfig) (
   let params := if let some params := params? then params.getElems else #[]
   let mvarId ← getMainGoal
   let params ← mkGrindParams config only params mvarId
-  Grind.withProtectedMCtx config.abstractProof mvarId fun mvarId' =>
-    discard <| Grind.GrindTacticM.runAtGoal mvarId' params do
+  discard <| Grind.GrindTacticM.runAtGoal mvarId params do
     let finish ← Grind.mkFinishAction
     let goal :: _ ← Grind.getGoals
       | let tac ← `(tactic| grind only)

src/Lean/Elab/Tactic/RCases.lean

@@ -323,7 +323,7 @@ partial def rcasesCore (g : MVarId) (fs : FVarSubst) (clears : Array FVarId) (e
           let (v, g) ← g.intro x
           let (varsOut, g) ← g.introNP vars.size
           let fs' := (vars.zip varsOut).foldl (init := fs) fun fs (v, w) => fs.insert v (mkFVar w)
-          pure ([(n, ps)], #[{mvarId := g, fields := #[mkFVar v], subst := fs', ctorName := n }])
+          pure ([(n, ps)], #[⟨⟨g, #[mkFVar v], fs'⟩, n⟩])
       | ConstantInfo.inductInfo info, _ => do
         let (altVarNames, r) ← processConstructors pat.ref info.numParams #[] info.ctors pat.asAlts
         (r, ·) <$> g.cases e.fvarId! altVarNames (useNatCasesAuxOn := true)

src/Lean/LibrarySuggestions/Basic.lean

@@ -417,16 +417,7 @@ open Lean.Elab.Tactic in
 @[builtin_tactic Lean.Parser.Tactic.suggestions] def evalSuggestions : Tactic := fun _ =>
   liftMetaTactic1 fun mvarId => do
     let suggestions ← select mvarId
-    let mut msg : MessageData := "Library suggestions:"
-    -- Check if all scores are 1.0
-    let allScoresOne := suggestions.all (·.score == 1.0)
-    for s in suggestions do
-      msg := msg ++ Format.line ++ "  " ++ MessageData.ofConstName s.name
-      if !allScoresOne then
-        msg := msg ++ m!" (score: {s.score})"
-      if let some flag := s.flag then
-        msg := msg ++ m!" [{flag}]"
-    logInfo msg
+    logInfo m!"Library suggestions: {suggestions.map (·.name)}"
     return mvarId
 
 end Lean.LibrarySuggestions

src/Lean/Meta/Match/Match.lean

@@ -17,22 +17,15 @@ public section
 
 namespace Lean.Meta.Match
 
-register_builtin_option backwards.match.sparseCases : Bool := {
-  defValue := true
-  descr := "if true (the default), generate and use sparse case constructs when splitting inductive
-    types. In some cases this will prevent Lean from noticing that a match statement is complete
-    because it performs less case-splitting for the unreachable case. In this case, give explicit
-    patterns to perform the deeper split with `by contradiction` as the right-hand side.
-     ,"
-}
-
 register_builtin_option backwards.match.rowMajor : Bool := {
   defValue := true
+  group := "bootstrap"
   descr := "If true (the default), match compilation will split the discrimnants based \
     on position of the first constructor pattern in the first alternative. If false, \
     it splits them from left to right, which can lead to unnecessary code bloat."
 }
 
+
 private def mkIncorrectNumberOfPatternsMsg [ToMessageData α]
     (discrepancyKind : String) (expected actual : Nat) (pats : List α) :=
   let patternsMsg := MessageData.joinSep (pats.map toMessageData) ", "
@@ -169,12 +162,6 @@ private def hasArrayLitPattern (p : Problem) : Bool :=
     | .arrayLit .. :: _ => true
     | _                 => false
 
-private def hasVarOrInaccessiblePattern (p : Problem) : Bool :=
-  p.alts.any fun alt => match alt.patterns with
-    | .inaccessible _ :: _ => true
-    | .var _ :: _          => true
-    | _                    => false
-
 private def isVariableTransition (p : Problem) : Bool :=
   p.alts.all fun alt => match alt.patterns with
     | .inaccessible _ :: _ => true
@@ -354,35 +341,6 @@ where
           msg := msg ++ m!"\n  {lhs} ≋ {rhs}"
         throwErrorAt alt.ref msg
 
-private abbrev isCtorIdxIneq? (e : Expr) : Option FVarId := do
-  if let some (_, lhs, _rhs) := e.ne? then
-    if
-      lhs.isApp &&
-      lhs.getAppFn.isConst &&
-      (`ctorIdx).isSuffixOf lhs.getAppFn.constName! && -- This should be an env extension maybe
-      lhs.appArg!.isFVar
-    then
-      return lhs.appArg!.fvarId!
-  none
-
-private partial def contradiction (mvarId : MVarId) : MetaM Bool := do
-  mvarId.withContext do
-    withTraceNode `Meta.Match.match (msg := (return m!"{exceptBoolEmoji ·} Match.contradiction")) do
-    trace[Meta.Match.match] m!"Match.contradiction:\n{mvarId}"
-    if (← mvarId.contradictionCore {}) then
-      trace[Meta.Match.match] "Contradiction found!"
-      return true
-    else
-      -- Try harder by splitting `ctorIdx x ≠ 23` assumptions
-      for localDecl in (← getLCtx) do
-        if let some fvarId := isCtorIdxIneq? localDecl.type then
-          trace[Meta.Match.match] "splitting ctorIdx assumption {localDecl.type}"
-          let subgoals ← mvarId.cases fvarId
-          return ← subgoals.allM (contradiction ·.mvarId)
-
-      mvarId.admit
-      return false
-
 /--
 Try to solve the problem by using the first alternative whose pending constraints can be resolved.
 -/
@@ -394,10 +352,10 @@ where
   go (alts : List Alt) : StateRefT State MetaM Unit := do
     match alts with
     | [] =>
-      let mvarId ← p.mvarId.exfalso
       /- TODO: allow users to configure which tactic is used to close leaves. -/
-      unless (← contradiction mvarId) do
-        trace[Meta.Match.match] "contradiction failed, missing alternative"
+      unless (← p.mvarId.contradictionCore {}) do
+        trace[Meta.Match.match] "missing alternative"
+        p.mvarId.admit
         modify fun s => { s with counterExamples := p.examples :: s.counterExamples }
     | alt :: _ =>
       solveCnstrs p.mvarId alt
@@ -558,29 +516,13 @@ private def throwCasesException (p : Problem) (ex : Exception) : MetaM α := do
               "- <constructor> = <constructor>, examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nil"
   | _ => throw ex
 
-private def collectCtors (p : Problem) : Array Name :=
-  p.alts.foldl (init := #[]) fun ctors alt =>
-    match alt.patterns with
-    | .ctor n _ _ _ :: _ => if ctors.contains n then ctors else ctors.push n
-    | _                  => ctors
-
 private def processConstructor (p : Problem) : MetaM (Array Problem) := do
   trace[Meta.Match.match] "constructor step"
   let x :: xs := p.vars | unreachable!
-  let interestingCtors? ←
-    -- We use a sparse case analysis only if there is at least one non-constructor pattern,
-    -- but not just because there are constructors missing (in that case we benefit from
-    -- the eager split in ruling out constructors by type or by a more explicit error message)
-    if backwards.match.sparseCases.get (← getOptions) && hasVarOrInaccessiblePattern p then
-      let ctors := collectCtors p
-      trace[Meta.Match.match] "using sparse cases: {ctors}"
-      pure (some ctors)
-    else
-      pure none
   let subgoals? ← commitWhenSome? do
      let subgoals ←
        try
-         p.mvarId.cases x.fvarId! (interestingCtors? := interestingCtors?)
+         p.mvarId.cases x.fvarId!
        catch ex =>
          if p.alts.isEmpty then
            /- If we have no alternatives and dependent pattern matching fails, then a "missing cases" error is better than a "stuck" error message. -/
@@ -603,42 +545,28 @@ private def processConstructor (p : Problem) : MetaM (Array Problem) := do
          return some subgoals
   let some subgoals := subgoals? | return #[{ p with vars := xs }]
   subgoals.mapM fun subgoal => subgoal.mvarId.withContext do
-    -- withTraceNode `Meta.Match.match (msg := (return m!"{exceptEmoji ·} case {subgoal.ctorName}")) do
-    if let some ctorName := subgoal.ctorName then
-      -- A normal constructor case
-      let subst    := subgoal.subst
-      let fields   := subgoal.fields.toList
-      let newVars  := fields ++ xs
-      let newVars  := newVars.map fun x => x.applyFVarSubst subst
-      let subex    := Example.ctor ctorName <| fields.map fun field => match field with
-        | .fvar fvarId => Example.var fvarId
-        | _            => Example.underscore -- This case can happen due to dependent elimination
-      let examples := p.examples.map <| Example.replaceFVarId x.fvarId! subex
-      let examples := examples.map <| Example.applyFVarSubst subst
-      let newAlts  := p.alts.filter fun alt => match alt.patterns with
-        | .ctor n .. :: _       => n == ctorName
-        | .var _ :: _           => true
-        | .inaccessible _ :: _  => true
-        | _                     => false
-      let newAlts  := newAlts.map fun alt => alt.applyFVarSubst subst
-      let newAlts ← newAlts.mapM fun alt => do
-        match alt.patterns with
-        | .ctor _ _ _ fields :: ps  => return { alt with patterns := fields ++ ps }
-        | .var _ :: _               => expandVarIntoCtor alt ctorName
-        | .inaccessible _ :: _      => processInaccessibleAsCtor alt ctorName
-        | _                         => unreachable!
-      return { mvarId := subgoal.mvarId, vars := newVars, alts := newAlts, examples := examples }
-    else
-      -- A catch-all case
-      let subst := subgoal.subst
-      trace[Meta.Match.match] "constructor catch-all case"
-      let examples := p.examples.map <| Example.applyFVarSubst subst
-      let newVars := p.vars.map fun x => x.applyFVarSubst subst
-      let newAlts := p.alts.filter fun alt => match alt.patterns with
-        | .ctor .. :: _ => false
-        | _             => true
-      let newAlts := newAlts.map fun alt => alt.applyFVarSubst subst
-      return { mvarId := subgoal.mvarId, alts := newAlts, vars := newVars, examples := examples }
+    let subst    := subgoal.subst
+    let fields   := subgoal.fields.toList
+    let newVars  := fields ++ xs
+    let newVars  := newVars.map fun x => x.applyFVarSubst subst
+    let subex    := Example.ctor subgoal.ctorName <| fields.map fun field => match field with
+      | .fvar fvarId => Example.var fvarId
+      | _            => Example.underscore -- This case can happen due to dependent elimination
+    let examples := p.examples.map <| Example.replaceFVarId x.fvarId! subex
+    let examples := examples.map <| Example.applyFVarSubst subst
+    let newAlts  := p.alts.filter fun alt => match alt.patterns with
+      | .ctor n .. :: _       => n == subgoal.ctorName
+      | .var _ :: _           => true
+      | .inaccessible _ :: _  => true
+      | _                     => false
+    let newAlts  := newAlts.map fun alt => alt.applyFVarSubst subst
+    let newAlts ← newAlts.mapM fun alt => do
+      match alt.patterns with
+      | .ctor _ _ _ fields :: ps  => return { alt with patterns := fields ++ ps }
+      | .var _ :: _               => expandVarIntoCtor alt subgoal.ctorName
+      | .inaccessible _ :: _      => processInaccessibleAsCtor alt subgoal.ctorName
+      | _                         => unreachable!
+    return { mvarId := subgoal.mvarId, vars := newVars, alts := newAlts, examples := examples }
 
 private def processNonVariable (p : Problem) : MetaM Problem := withGoalOf p do
   let x :: xs := p.vars | unreachable!
@@ -880,15 +808,6 @@ def processExFalso (p : Problem) : MetaM Problem := do
   let mvarId' ← p.mvarId.exfalso
   return { p with mvarId := mvarId' }
 
-private def tracedForM (xs : Array α) (process : α → StateRefT State MetaM Unit) : StateRefT State MetaM Unit :=
-  if xs.size > 1 then
-    for x in xs, i in [:xs.size] do
-      withTraceNode `Meta.Match.match (msg := (return m!"{exceptEmoji ·} subgoal {i+1}/{xs.size}")) do
-        process x
-  else
-    for x in xs do
-      process x
-
 private partial def process (p : Problem) : StateRefT State MetaM Unit := do
   traceState p
   if isDone p then
@@ -951,7 +870,7 @@ private partial def process (p : Problem) : StateRefT State MetaM Unit := do
 
   if (← isConstructorTransition p) then
     let ps ← processConstructor p
-    tracedForM ps process
+    ps.forM process
     return
 
   if isVariableTransition p then
@@ -962,12 +881,12 @@ private partial def process (p : Problem) : StateRefT State MetaM Unit := do
 
   if isValueTransition p then
     let ps ← processValue p
-    tracedForM ps process
+    ps.forM process
     return
 
   if isArrayLitTransition p then
     let ps ← processArrayLit p
-    tracedForM ps process
+    ps.forM process
     return
 
   if (← hasNatValPattern p) then

src/Lean/Meta/Tactic/Cases.lean

@@ -9,8 +9,6 @@ prelude
 public import Lean.Meta.Tactic.Induction
 public import Lean.Meta.Tactic.Acyclic
 public import Lean.Meta.Tactic.UnifyEq
-import Lean.Meta.Constructions.SparseCasesOn
-import Lean.Meta.Constructions.CtorIdx
 
 public section
 
@@ -151,8 +149,7 @@ def generalizeIndices (mvarId : MVarId) (fvarId : FVarId) : MetaM GeneralizeIndi
     generalizeIndices' mvarId fvarDecl.toExpr fvarDecl.userName
 
 structure CasesSubgoal extends InductionSubgoal where
-  /-- The constructor of this subgoal. Is `none` in the catch-all of a sparse case match -/
-  ctorName : Option Name
+  ctorName : Name
 
 namespace Cases
 
@@ -219,13 +216,11 @@ private def elimAuxIndices (s₁ : GeneralizeIndicesSubgoal) (s₂ : Array Cases
 private def toCasesSubgoals (s : Array InductionSubgoal) (ctorNames : Array Name) (majorFVarId : FVarId) (us : List Level) (params : Array Expr)
     : Array CasesSubgoal :=
   s.mapIdx fun i s =>
-    if _ : i < ctorNames.size then
-      let ctorName := ctorNames[i]
-      let ctorApp  := mkAppN (mkAppN (mkConst ctorName us) params) s.fields
-      let subst := s.subst.erase majorFVarId |>.insert majorFVarId ctorApp
-      { s with ctorName := ctorName, subst}
-    else
-      { s with ctorName := none }
+    let ctorName := ctorNames[i]!
+    let ctorApp  := mkAppN (mkAppN (mkConst ctorName us) params) s.fields
+    let s        := { s with subst := s.subst.insert majorFVarId ctorApp }
+    { ctorName           := ctorName,
+      toInductionSubgoal := s }
 
 partial def unifyEqs? (numEqs : Nat) (mvarId : MVarId) (subst : FVarSubst) (caseName? : Option Name := none): MetaM (Option (MVarId × FVarSubst)) := withIncRecDepth do
   if numEqs == 0 then
@@ -249,33 +244,17 @@ private def unifyCasesEqs (numEqs : Nat) (subgoals : Array CasesSubgoal) : MetaM
       }
 
 private def inductionCasesOn (mvarId : MVarId) (majorFVarId : FVarId) (givenNames : Array AltVarNames) (ctx : Context)
-    (useNatCasesAuxOn : Bool := false) (interestingCtors? : Option (Array Name) := none) :
-    MetaM (Array CasesSubgoal) := mvarId.withContext do
+    (useNatCasesAuxOn : Bool := false) : MetaM (Array CasesSubgoal) := mvarId.withContext do
   let majorType ← inferType (mkFVar majorFVarId)
   let (us, params) ← getInductiveUniverseAndParams majorType
-
-  if let some interestingCtors := interestingCtors? then
-    -- Avoid Init.Prelude complications
-    let hasNE := (← getEnv).contains ``Ne
-    -- We can only create a sparse casesOn if we have `ctorIdx` (in particular, if it is a type)
-    let hasCtorIdx := (← getEnv).contains (mkCtorIdxName ctx.inductiveVal.name)
-    if hasNE && hasCtorIdx && !interestingCtors.isEmpty &&
-      interestingCtors.size < ctx.inductiveVal.ctors.length then
-      let casesOn ← Lean.Meta.mkSparseCasesOn ctx.inductiveVal.name interestingCtors
-      let s ← mvarId.induction majorFVarId casesOn givenNames
-      return toCasesSubgoals s interestingCtors majorFVarId us params
-
-  let casesOn :=
-    if useNatCasesAuxOn && ctx.inductiveVal.name == ``Nat && (← getEnv).contains ``Nat.casesAuxOn then
-      ``Nat.casesAuxOn
-    else
-      mkCasesOnName ctx.inductiveVal.name
+  let mut casesOn := mkCasesOnName ctx.inductiveVal.name
+  if useNatCasesAuxOn && ctx.inductiveVal.name == ``Nat && (← getEnv).contains ``Nat.casesAuxOn then
+    casesOn := ``Nat.casesAuxOn
   let ctors   := ctx.inductiveVal.ctors.toArray
   let s ← mvarId.induction majorFVarId casesOn givenNames
   return toCasesSubgoals s ctors majorFVarId us params
 
-def cases (mvarId : MVarId) (majorFVarId : FVarId) (givenNames : Array AltVarNames := #[])
-    (useNatCasesAuxOn : Bool := false) (interestingCtors? : Option (Array Name) := none) : MetaM (Array CasesSubgoal) := do
+def cases (mvarId : MVarId) (majorFVarId : FVarId) (givenNames : Array AltVarNames := #[]) (useNatCasesAuxOn : Bool := false) : MetaM (Array CasesSubgoal) := do
   try
     mvarId.withContext do
       mvarId.checkNotAssigned `cases
@@ -289,11 +268,10 @@ def cases (mvarId : MVarId) (majorFVarId : FVarId) (givenNames : Array AltVarNam
         if (← hasIndepIndices ctx) then
           -- Simple case
           inductionCasesOn mvarId majorFVarId givenNames ctx (useNatCasesAuxOn := useNatCasesAuxOn)
-            (interestingCtors? := interestingCtors?)
         else
           let s₁ ← generalizeIndices mvarId majorFVarId
           trace[Meta.Tactic.cases] "after generalizeIndices\n{MessageData.ofGoal s₁.mvarId}"
-          let s₂ ← inductionCasesOn s₁.mvarId s₁.fvarId givenNames ctx (interestingCtors? := interestingCtors?)
+          let s₂ ← inductionCasesOn s₁.mvarId s₁.fvarId givenNames ctx
           let s₂ ← elimAuxIndices s₁ s₂
           unifyCasesEqs s₁.numEqs s₂
   catch ex =>
@@ -310,9 +288,8 @@ Apply `casesOn` using the free variable `majorFVarId` as the major premise (aka
   It enables using `Nat.casesAuxOn` instead of `Nat.casesOn`,
   which causes case splits on `n : Nat` to be represented as `0` and `n' + 1` rather than as `Nat.zero` and `Nat.succ n'`.
 -/
-def _root_.Lean.MVarId.cases (mvarId : MVarId) (majorFVarId : FVarId) (givenNames : Array AltVarNames := #[]) (useNatCasesAuxOn : Bool := false)
-  (interestingCtors? : Option (Array Name) := none) : MetaM (Array CasesSubgoal) :=
-  Cases.cases mvarId majorFVarId givenNames (useNatCasesAuxOn := useNatCasesAuxOn) (interestingCtors? := interestingCtors?)
+def _root_.Lean.MVarId.cases (mvarId : MVarId) (majorFVarId : FVarId) (givenNames : Array AltVarNames := #[]) (useNatCasesAuxOn : Bool := false) : MetaM (Array CasesSubgoal) :=
+  Cases.cases mvarId majorFVarId givenNames (useNatCasesAuxOn := useNatCasesAuxOn)
 
 /--
 Keep applying `cases` on any hypothesis that satisfies `p`.

src/Lean/Meta/Tactic/Grind/Main.lean

@@ -6,8 +6,6 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Types
-public import Lean.Meta.Tactic.Grind.Util
-public import Lean.Meta.Closure
 import Lean.PrettyPrinter
 import Lean.Meta.Tactic.ExposeNames
 import Lean.Meta.Tactic.Simp.Diagnostics
@@ -17,6 +15,7 @@ import Lean.Meta.Tactic.Grind.RevertAll
 import Lean.Meta.Tactic.Grind.PropagatorAttr
 import Lean.Meta.Tactic.Grind.Proj
 import Lean.Meta.Tactic.Grind.ForallProp
+import Lean.Meta.Tactic.Grind.Util
 import Lean.Meta.Tactic.Grind.Inv
 import Lean.Meta.Tactic.Grind.Intro
 import Lean.Meta.Tactic.Grind.EMatch
@@ -201,12 +200,8 @@ def Result.toMessageData (result : Result) : MetaM MessageData := do
   return MessageData.joinSep msgs m!"\n"
 
 private def initCore (mvarId : MVarId) (params : Params) : GrindM Goal := do
-  /-
-  **Note**: We used to use `abstractMVars` and `clearImpDetails` here.
-  These operations are now performed at `withProtectedMCtx`
-  -/
-  -- let mvarId ← mvarId.abstractMVars
-  -- let mvarId ← mvarId.clearImplDetails
+  let mvarId ← mvarId.abstractMVars
+  let mvarId ← mvarId.clearImplDetails
   let mvarId ← if params.config.clean then pure mvarId else mvarId.markAccessible
   let mvarId ← mvarId.revertAll
   let mvarId ← mvarId.unfoldReducible
@@ -238,45 +233,4 @@ def main (mvarId : MVarId) (params : Params) : MetaM Result := do profileitM Exc
     let failure? ← solve goal
     mkResult params failure?
 
-/--
-A helper combinator for executing a `grind`-based terminal tactic.
-Given an input goal `mvarId`, it first abstracts meta-variables, cleans up local hypotheses
-corresponding to internal details, creates an auxiliary meta-variable `mvarId'`, and executes `k mvarId'`.
-The execution is performed in a new meta-variable context depth to ensure that universe meta-variables
-cannot be accidentally assigned by `grind`. If `k` fails, it admits the input goal.
-
-See issue #11806 for a motivating example.
--/
-def withProtectedMCtx [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m]
-    [MonadExcept Exception m] [MonadRuntimeException m]
-    (abstractProof : Bool) (mvarId : MVarId) (k : MVarId → m α) : m α := do
-  let mvarId ← mvarId.abstractMVars
-  let mvarId ← mvarId.clearImplDetails
-  tryCatchRuntimeEx (main mvarId) fun ex => do
-    mvarId.admit
-    throw ex
-where
-  main (mvarId : MVarId) : m α := mvarId.withContext do
-    let type ← mvarId.getType
-    let (a, val) ← withNewMCtxDepth do
-      let mvar' ← mkFreshExprSyntheticOpaqueMVar type
-      let a ← k mvar'.mvarId!
-      let val ← finalize mvar'
-      return (a, val)
-    (mvarId.assign val : MetaM _)
-    return a
-
-  finalize (mvar' : Expr) : MetaM Expr := do
-    trace[grind.debug.proof] "{← instantiateMVars mvar'}"
-    let type ← inferType mvar'
-    -- `grind` proofs are often big, if `abstractProof` is true, we create an auxiliary theorem.
-    let val ← if !abstractProof then
-      instantiateMVarsProfiling mvar'
-    else if (← isProp type) then
-      mkAuxTheorem type (← instantiateMVarsProfiling mvar') (zetaDelta := true)
-    else
-      let auxName ← mkAuxDeclName `grind
-      mkAuxDefinition auxName type (← instantiateMVarsProfiling mvar') (zetaDelta := true)
-    return val
-
 end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/PropagateInj.lean

@@ -11,40 +11,36 @@ import Init.Grind.Injective
 import Lean.Meta.Tactic.Grind.PropagatorAttr
 import Lean.Meta.Tactic.Grind.Simp
 namespace Lean.Meta.Grind
-
-def getInvFor? (f : Expr) (a : Expr) : GoalM (Option (Expr × Expr)) := do
-  let some info := (← get).inj.fns.find? { expr := f } | return none
-  if let some inv := info.inv? then
-    return some inv
-  let [u, _] := info.us | unreachable!
-  let nonEmpty := mkApp2 (mkConst ``Nonempty.intro [u]) info.α a
-  let inv := mkApp5 (mkConst ``Grind.leftInv info.us) info.α info.β f info.h nonEmpty
-  let inv ← preprocessLight inv
-  let args := inv.getAppArgs
-  let heq := mkAppN (mkConst ``Grind.leftInv_eq info.us) args
-  let inv? := some (inv, heq)
-  let info := { info with inv? }
-  modify fun s => { s with inj.fns := s.inj.fns.insert { expr := f } info }
-  return inv?
-
 /--
 If `e` is an application of the form `f a` where `f` is an injective function
 in `(← get).inj.fns`, asserts `f⁻¹ (f a) = a`
 -/
 public def mkInjEq (e : Expr) : GoalM Unit := do
   let .app f a := e | return ()
-  let some (inv, heq) ← getInvFor? f a | return ()
-  let invApp := mkApp inv e
+  let some info := (← get).inj.fns.find? { expr := f } | return ()
+  let invApp := mkApp info.inv e
   internalize invApp (← getGeneration e)
   trace[grind.inj.assert] "{invApp}, {a}"
-  pushEq invApp a <| mkApp heq a
+  pushEq invApp a <| mkApp info.heq a
 
 def initInjFn (us : List Level) (α β : Expr) (f : Expr) (h : Expr) : GoalM Unit := do
-  modify fun s => { s with inj.fns := s.inj.fns.insert { expr := f } { us, α, β, h } }
   let hidx := f.toHeadIndex
+  let mut first := true
   for e in (← get).appMap.findD hidx [] do
     if e.isApp && isSameExpr e.appFn! f then
+      if first then
+        initLeftInv e.appArg!
+        first := false
       mkInjEq e
+where
+  initLeftInv (a : Expr) : GoalM Unit := do
+    let [u, _] := us | unreachable!
+    let nonEmpty := mkApp2 (mkConst ``Nonempty.intro [u]) α a
+    let inv := mkApp5 (mkConst ``Grind.leftInv us) α β f h nonEmpty
+    let inv ← preprocessLight inv
+    let args := inv.getAppArgs
+    let heq := mkAppN (mkConst ``Grind.leftInv_eq us) args
+    modify fun s => { s with inj.fns := s.inj.fns.insert { expr := f } { inv, heq } }
 
 builtin_grind_propagator propagateInj ↓Function.Injective := fun e => do
   let_expr i@Function.Injective α β f := e | return ()

src/Lean/Meta/Tactic/Grind/Types.lean

@@ -859,15 +859,8 @@ structure UnitLike.State where
   deriving Inhabited
 
 structure InjectiveInfo where
-  us   : List Level
-  α    : Expr
-  β    : Expr
-  h    : Expr
-  /--
-  Inverse function and a proof that `∀ a, inv (f a) = a`
-  **Note**: The following two fields are `none` if no `f`-application has been found yet.
-  -/
-  inv?  : Option (Expr × Expr) := none
+  inv : Expr
+  heq : Expr
   deriving Inhabited
 
 /-- State for injective theorem support. -/

src/Lean/Meta/Tactic/Induction.lean

@@ -73,8 +73,7 @@ private partial def finalize
           pure (recursor, recursorType)
         let recursor := mkApp recursor major
         let recursorType ← getTypeBody mvarId recursorType major
-        let consumedMajor := true
-        loop (pos+1+indices.size) minorIdx recursor recursorType consumedMajor subgoals
+        loop (pos+1+indices.size) minorIdx recursor recursorType true subgoals
       else
         -- consume motive
         let tag ← mvarId.getTag
@@ -82,7 +81,7 @@ private partial def finalize
         match recursorType with
         | Expr.forallE n d _ c =>
           let d := d.headBeta
-          let tag' := if numMinors == 1 then tag else tag ++ n.eraseMacroScopes
+          let tag' := if numMinors == 1 then tag else tag ++ n
           -- Remark is givenNames is not empty, then user provided explicit alternatives for each minor premise
           if c.isInstImplicit && givenNames.isEmpty then
             match (← synthInstance? d) with
@@ -106,7 +105,6 @@ private partial def finalize
             let recursor := mkApp recursor mvar
             let recursorType ← getTypeBody mvarId recursorType mvar
             -- Try to clear major premise from new goal
-            trace[Meta.Tactic.induction] "name of major premise: {major.fvarId!.name}"
             let mvarId' ← mvar.mvarId!.tryClear major.fvarId!
             let (fields, mvarId') ←  mvarId'.introN nparams minorGivenNames.varNames (useNamesForExplicitOnly := !minorGivenNames.explicit)
             let (extra,  mvarId') ← mvarId'.introNP nextra
@@ -117,12 +115,11 @@ private partial def finalize
                 let newFVarId      := extra[i - indices.size - 1]!
                 subst.insert revertedFVarId (mkFVar newFVarId)
             let fields := fields.map mkFVar
-            loop (pos+1) (minorIdx+1) recursor recursorType consumedMajor (subgoals.push { mvarId := mvarId', fields, subst})
+            loop (pos+1) (minorIdx+1) recursor recursorType consumedMajor (subgoals.push { mvarId := mvarId', fields := fields, subst := subst })
         | _ => unreachable!
     else
       unless consumedMajor do throwTacticEx `induction mvarId "ill-formed recursor"
       mvarId.assign recursor
-      trace[Meta.Tactic.induction] "finalize loop is done, {subgoals.size} subgoals"
       pure subgoals
   loop (recursorInfo.paramsPos.length + 1) 0 recursor recursorType false #[]
 
@@ -223,10 +220,9 @@ def _root_.Lean.MVarId.induction (mvarId : MVarId) (majorFVarId : FVarId) (recur
       -- Re-introduce indices and major
       let (indices', mvarId) ← mvarId.introNP indices.size
       let (majorFVarId', mvarId) ← mvarId.intro1P
-      -- Create FVarSubst with indices and major
+      -- Create FVarSubst with indices
       let baseSubst := Id.run do
         let mut subst : FVarSubst := {}
-        subst := subst.insert majorFVarId (mkFVar majorFVarId')
         let mut i := 0
         for index in indices do
           subst := subst.insert index.fvarId! (mkFVar indices'[i]!)
@@ -235,9 +231,10 @@ def _root_.Lean.MVarId.induction (mvarId : MVarId) (majorFVarId : FVarId) (recur
       trace[Meta.Tactic.induction] "after revert&intro\n{MessageData.ofGoal mvarId}"
       -- Update indices and major
       let indices := indices'.map mkFVar
-      let major := mkFVar majorFVarId'
+      let majorFVarId := majorFVarId'
+      let major := mkFVar majorFVarId
       mvarId.withContext do
-        let recursor ← mkRecursorAppPrefix mvarId `induction majorFVarId' recursorInfo indices
+        let recursor ← mkRecursorAppPrefix mvarId `induction majorFVarId recursorInfo indices
         finalize mvarId givenNames recursorInfo reverted major indices baseSubst recursor
 
 builtin_initialize registerTraceClass `Meta.Tactic.induction

src/lake/Lake/Build/Executable.lean

@@ -36,16 +36,12 @@ private def LeanExe.recBuildExe (self : LeanExe) : FetchM (Job FilePath) :=
   for mod in imports do
     for facet in mod.nativeFacets shouldExport do
       objJobs := objJobs.push <| ← facet.fetch mod
-  for link in self.moreLinkObjs do
-    objJobs := objJobs.push <| ← link.fetchIn self.pkg
   let libs := imports.foldl (·.insert ·.lib) OrdHashSet.empty |>.toArray
   for lib in libs do
     for link in lib.moreLinkObjs do
       objJobs := objJobs.push <| ← link.fetchIn lib.pkg
     for link in lib.moreLinkLibs do
       libJobs := libJobs.push <| ← link.fetchIn lib.pkg
-  for link in self.moreLinkLibs do
-    libJobs := libJobs.push <| ← link.fetchIn self.pkg
   let deps := (← (← self.pkg.transDeps.fetch).await).push self.pkg
   for dep in deps do
     for lib in dep.externLibs do

src/lake/Lake/Build/Job/Monad.lean

@@ -158,19 +158,11 @@ namespace Job
   (f : JobTask α → m (JobTask β)) (self : Job α)
 : m (Job β) := return {self with task := ← f self.task, kind := inferInstance}
 
-/-- Returns a job that has synchronously performed `act`. -/
-@[nospecialize] public protected def sync
-  [OptDataKind α] (act : JobM α) (caption := "")
-: SpawnM (Job α) := .ofFn fun fetch pkg? stack store ctx _ =>
-  .ofTask (caption := caption) <$> Task.pure <$>
-    (withLoggedIO act).toFn fetch pkg? stack store ctx {}
-
 /-- Spawn a job that asynchronously performs `act`. -/
-@[nospecialize] public protected def async
+@[inline] public protected def async
   [OptDataKind α] (act : JobM α) (prio := Task.Priority.default) (caption := "")
-: SpawnM (Job α) := .ofFn fun fetch pkg? stack store ctx _ =>
-  .ofTask (caption := caption) <$> BaseIO.asTask (prio := prio) do
-    (withLoggedIO act).toFn fetch pkg? stack store ctx {}
+: SpawnM (Job α) := .ofFn fun fetch pkg? stack store ctx _ => .ofTask (caption := caption) <$> do
+  BaseIO.asTask (prio := prio) do (withLoggedIO act).toFn fetch pkg? stack store ctx {}
 
 /-- Wait for a job to complete and return the result. -/
 @[inline] public protected def wait (self : Job α) : BaseIO (JobResult α) := do
@@ -187,13 +179,13 @@ If an error occurred, return `none` and discarded any logs produced.
 Wait for a job to complete and return the produced value.
 Logs the job's log and throws if there was an error.
 -/
-public protected def await (self : Job α) : LogIO α := do
+@[inline] public protected def await (self : Job α) : LogIO α := do
   match (← self.wait) with
   | .error n {log, ..} => log.replay; throw n
   | .ok a {log, ..} => log.replay; pure a
 
 /-- Apply `f` asynchronously to the job's output. -/
-@[nospecialize] public protected def mapM
+public protected def mapM
   [kind : OptDataKind β] (self : Job α) (f : α → JobM β)
   (prio := Task.Priority.default) (sync := false)
 : SpawnM (Job β) := .ofFn fun fetch pkg? stack store ctx trace => do
@@ -208,7 +200,7 @@ public protected def await (self : Job α) : LogIO α := do
 Apply `f` asynchronously to the job's output
 and asynchronously await the resulting job.
 -/
-@[nospecialize] public def bindM
+public def bindM
   [kind : OptDataKind β] (self : Job α) (f : α → JobM (Job β))
   (prio := Task.Priority.default) (sync := false)
 : SpawnM (Job β) := .ofFn fun fetch pkg? stack store ctx trace => do

src/lake/Lake/Build/Job/Register.lean

@@ -44,7 +44,7 @@ Registers the job for the top-level build monitor,
   return job.renew
 
 /-- Wraps stray I/O, logs, and errors in `x` into the produced job.  -/
-@[nospecialize] public def ensureJob
+public def ensureJob
   [OptDataKind α] (x : FetchM (Job α))
 : FetchM (Job α) := .ofFn fun fetch pkg? stack store ctx log => do
   let iniPos := log.endPos

src/lake/Lake/Config/LeanExe.lean

@@ -110,14 +110,6 @@ That is, the package's `weakLinkArgs` plus the executable's  `weakLinkArgs`.
 @[inline] public def weakLinkArgs (self : LeanExe) : Array String :=
   self.pkg.weakLinkArgs ++ self.config.weakLinkArgs
 
-/-- Additional objects (e.g., `.o` files, static libraries) to link to the executable. -/
-@[inline] public def moreLinkObjs (self : LeanExe) : TargetArray FilePath :=
-  self.config.moreLinkObjs
-
-/-- Additional shared libraries to link to the executable. -/
-@[inline] public def moreLinkLibs (self : LeanExe) : TargetArray Dynlib :=
-  self.config.moreLinkLibs
-
 end LeanExe
 
 /-- Locate the named, buildable, but not necessarily importable, module in the package. -/

src/lake/Lake/Util/Log.lean

@@ -437,16 +437,8 @@ from an `ELogT` (e.g., `LogIO`).
 @[inline] public def withLoggedIO
   [Monad m] [MonadLiftT BaseIO m] [MonadLog m] [MonadFinally m] (x : m α)
 : m α := do
-  let buf ← IO.mkRef { : IO.FS.Stream.Buffer }
-  let stdout ← IO.setStdout <| .ofBuffer buf
-  let stderr ← IO.setStderr <| .ofBuffer buf
-  let a ← try x finally
-    discard <| IO.setStdout stdout
-    discard <| IO.setStderr stderr
-  let buf ← liftM (m := BaseIO) buf.get
-  let out := String.fromUTF8! buf.data
-  unless out.isEmpty do
-    logInfo s!"stdout/stderr:\n{out.trim}"
+  let (out, a) ← IO.FS.withIsolatedStreams x
+  unless out.isEmpty do logInfo s!"stdout/stderr:\n{out.trim}"
   return a
 
 /-- Throw with the logged error `message`. -/

tests/bench/reduceMatch.lean

@@ -1,7 +1,5 @@
 import Lean
 
-set_option warn.sorry false
-
 /-!
   #2564. `match` reduction currently has some special cases.
   When combined with nonlinear functions like `List.insert` below,
@@ -33,7 +31,7 @@ def parts : List (List Nat) := List.insert ([1, 1, 0, 0]) <| List.insert ([0, 0,
   List.insert ([1, 0, 0, 1]) <| List.insert ([1, 1, 1, 0]) <| List.insert ([1, 0, 0, 0]) <|
   List.insert [1, 2, 3, 4] <| List.insert [5, 6, 7, 8] []
 
-run_cmd
+#eval show Lean.Elab.Command.CommandElabM _ from
   for _ in *...(10 : Nat) do
     Lean.Elab.Command.elabCommand (←
       `(example : ∀ (x) (_ : x ∈ parts) (y) (_ : y ∈ parts), x ++ y ∉ parts := by decide))

tests/lake/examples/ffi/lib/lakefile.lean

@@ -51,11 +51,3 @@ target libleanffi_shared pkg : Dynlib := do
 
 lean_lib FFI.Shared where
   moreLinkLibs := #[libleanffi_shared]
-
-/-! ## Executable-only FFI -/
-
-@[default_target]
-lean_exe standalone where
-  root := `Standalone
-  moreLinkObjs := #[libleanffi_static]
-  moreLinkLibs := #[libleanffi_shared]

tests/lake/examples/ffi/lib/lean/Standalone.lean

@@ -1,9 +0,0 @@
-@[extern "my_add"]
-opaque myAdd : UInt32 → UInt32 → UInt32
-
-@[extern "my_lean_fun"]
-opaque myLeanFun : IO String
-
-def main : IO Unit := do
-  IO.println (myAdd 1 2)
-  IO.println (← myLeanFun)

tests/lake/examples/ffi/test.sh

@@ -10,7 +10,6 @@ $LAKE -d lib build -v
 
 $LAKE exe -d app app
 $LAKE exe -d lib test
-$LAKE exe -d lib standalone
 
 # Tests that a non-precompiled build does not load anything as a dynlib/plugin
 # https://github.com/leanprover/lean4/issues/4565

tests/lake/tests/depRenaming/dep/lakefile.lean

@@ -3,5 +3,5 @@ open System Lake DSL
 
 package dep
 
-target name : String := Job.sync do
-  return  (__name__).toString
+target name : String := do
+  return .pure <| (__name__).toString

tests/lake/tests/query/lakefile.lean

@@ -13,5 +13,5 @@ lean_exe a where
 lean_exe b where
   root := `exe
 
-target foo : String := Job.sync do
-  return "foo"
+target foo : String :=
+  return .pure "foo"

tests/lean/run/double_match.lean

@@ -1,15 +1,14 @@
 /--
-trace: [Compiler.saveMono] size: 7
+trace: [Compiler.saveMono] size: 6
     def foo f x : Option Nat :=
       let _x.1 := f x;
       cases _x.1 : Option Nat
+      | Option.none =>
+        return _x.1
       | Option.some val.2 =>
         let _x.3 := Nat.add val.2 val.2;
         let _x.4 := some ◾ _x.3;
         return _x.4
-      | _ =>
-        let _x.5 := none ◾;
-        return _x.5
 -/
 #guard_msgs in
 set_option trace.Compiler.saveMono true in

tests/lean/run/grind_11086.lean

@@ -1,49 +0,0 @@
-open Sum Function
-
--- This needs to be in the library!
--- https://github.com/leanprover/lean4/pull/11085
-attribute [grind =] Prod.map_fst Prod.map_snd
-
--- Copy the definition of `Equiv` from Mathlib.
-structure Equiv (α : Sort _) (β : Sort _) where
-  protected toFun : α → β
-  protected invFun : β → α
-  protected left_inv : LeftInverse invFun toFun := by intro; first | rfl | ext <;> rfl
-  protected right_inv : RightInverse invFun toFun := by intro; first | rfl | ext <;> rfl
-
-infixl:25 " ≃ " => Equiv
-
-def sumProdDistrib (α β γ) : (α ⊕ β) × γ ≃ α × γ ⊕ β × γ :=
-  ⟨fun p => p.1.map (fun x => (x, p.2)) fun x => (x, p.2),
-    fun s => s.elim (Prod.map inl id) (Prod.map inr id), by
-      rintro ⟨_ | _, _⟩ <;> rfl, by
-      rintro (⟨_, _⟩ | ⟨_, _⟩)
-      · grind
-      · grind⟩
-
-def sumProdDistrib' (α β γ) : (α ⊕ β) × γ ≃ α × γ ⊕ β × γ :=
-  ⟨fun p => p.1.map (fun x => (x, p.2)) fun x => (x, p.2),
-    fun s => s.elim (Prod.map inl id) (Prod.map inr id), by
-      rintro ⟨_ | _, _⟩ <;> rfl, by
-      rintro (⟨_, _⟩ | ⟨_, _⟩)
-      · grind +abstractProof
-      · grind +abstractProof⟩
-
-def sumProdDistrib'' (α β γ) : (α ⊕ β) × γ ≃ α × γ ⊕ β × γ :=
-  ⟨fun p => p.1.map (fun x => (x, p.2)) fun x => (x, p.2),
-    fun s => s.elim (Prod.map inl id) (Prod.map inr id), by
-      rintro ⟨_ | _, _⟩ <;> rfl, by
-      rintro (⟨_, _⟩ | ⟨_, _⟩)
-      · grind?
-      · grind?⟩
-
-example (α β γ) (fst : α) (snd : γ) :
-    (fun p : (α ⊕ β) × γ ↦ Sum.map (fun x ↦ (x, p.snd)) (fun x ↦ (x, p.snd)) p.fst)
-      ((fun s ↦ Sum.elim (Prod.map inl id) (Prod.map inr id) s) (inl (fst, snd))) =
-    inl (fst, snd) := by
-  grind
-
-example (α β γ) :
-    RightInverse (fun s : α × γ ⊕ β × γ ↦ Sum.elim (Prod.map inl id) (Prod.map inr id) s) fun p ↦
-      Sum.map (fun x ↦ (x, p.snd)) (fun x ↦ (x, p.snd)) p.fst := by
-  rintro (⟨_, _⟩ | ⟨_, _⟩) <;> grind

tests/lean/run/grind_11088.lean

@@ -1,3 +0,0 @@
-example (f : α → β) (h : Function.Injective f)
-    : f a = f b → a = b := by
-  grind

tests/lean/run/grind_interactive.lean

@@ -494,6 +494,10 @@ h✝¹ : p ∨ ¬q
 h2 : ¬p ∨ q
 h✝ : ¬p ∨ ¬q
 ⊢ False
+---
+error: unsolved goals
+r p q : Prop
+⊢ p ∨ r → p ∨ q → p ∨ ¬q → ¬p ∨ q → ¬p ∨ ¬q → False
 -/
 #guard_msgs in
 example (r p q : Prop) : p ∨ r → p ∨ q → p ∨ ¬q → ¬p ∨ q → ¬p ∨ ¬q → False := by

tests/lean/run/grind_suggestions.lean

@@ -36,54 +36,9 @@ example : P 7 := by
 
 set_library_suggestions (fun _ _ => pure #[{ name := `p, score := 1.0 }])
 
-/--
-info: Library suggestions:
-  p
--/
-#guard_msgs in
 example : P 7 := by
-  suggestions
   grind +suggestions
 
-set_library_suggestions (fun _ _ => pure #[{ name := `p, score := 0.5 }])
-
-/--
-info: Library suggestions:
-  p (score: 0.500000)
--/
-#guard_msgs in
-example : P 7 := by
-  suggestions
-  grind +suggestions
-
-set_library_suggestions (fun _ _ => pure #[{ name := `p, score := 1.0, flag := some "←" }])
-
-/--
-info: Library suggestions:
-  p [←]
----
-error: unexpected modifier ←
--/
-#guard_msgs in
-example : P 7 := by
-  suggestions
-  grind +suggestions
-
-set_library_suggestions (fun _ _ => pure #[
-  { name := `p, score := 0.9 },
-  { name := `f, score := 0.7 }
-])
-
-/--
-info: Library suggestions:
-  p (score: 0.900000)
-  f (score: 0.700000)
--/
-#guard_msgs in
-example : P 7 := by
-  suggestions
-  grind [p]
-
 set_library_suggestions (fun _ _ => pure #[{ name := `List.append_assoc, score := 1.0 }])
 
 -- Make sure there is no warning about the redundant theorem.

tests/lean/run/issue10749.lean

@@ -22,8 +22,6 @@ def test2 (a b : List Nat) : Nat :=
   | _, [] => 4
   | _ :: _, _ :: _ => 5
 
--- Should have exactly two `casesOn`
-
 /--
 info: def test2.match_1.{u_1} : (motive : List Nat → List Nat → Sort u_1) →
   (a b : List Nat) →
@@ -53,7 +51,7 @@ info: def test3.match_1.{u_1} : (motive : List Nat → Bool → Sort u_1) →
       ((x : List Nat) → motive x true) →
         ((x : Bool) → motive [] x) → ((x : List Nat) → (x_1 : Bool) → motive x x_1) → motive a b :=
 fun motive a b h_1 h_2 h_3 =>
-  test3._sparseCasesOn_1 b (h_1 a) fun h_0 => test3._sparseCasesOn_2 a (h_2 b) fun h_0 => h_3 a b
+  Bool.casesOn b (List.casesOn a (h_2 false) fun head tail => h_3 (head :: tail) false) (h_1 a)
 -/
 #guard_msgs in #print test3.match_1
 
@@ -64,10 +62,10 @@ example (P : Nat → Prop) (x : Nat) (h : x = 12345) (hP : P 12345) : P x :=
 
 def test4 : Bool → Bool → Bool → Bool → Bool → Bool
   | _, _ , _ , _ , true => true
-  | _, _ , _ , true, _ => true
-  | _, _ , true, _ , _ => true
-  | _, true, _ , _ , _ => true
-  | true, _ , _ , _ , _ => true
+  | _, _ , _ , true , _ => true
+  | _, _ , true , _ , _ => true
+  | _, true , _ , _ , _ => true
+  | true , _ , _ , _ , _ => true
   | _ , _ , _ , _ , _ => false
 
 /--
@@ -79,44 +77,18 @@ info: def test4.match_1.{u_1} : (motive : Bool → Bool → Bool → Bool → Bo
           ((x x_5 x_6 x_7 : Bool) → motive x true x_5 x_6 x_7) →
             ((x x_5 x_6 x_7 : Bool) → motive true x x_5 x_6 x_7) →
               ((x x_5 x_6 x_7 x_8 : Bool) → motive x x_5 x_6 x_7 x_8) → motive x x_1 x_2 x_3 x_4 :=
-fun motive x x_1 x_2 x_3 x_4 h_1 h_2 h_3 h_4 h_5 h_6 =>
-  test3._sparseCasesOn_1 x_4 (h_1 x x_1 x_2 x_3) fun h_0 =>
-    test3._sparseCasesOn_1 x_3 (h_2 x x_1 x_2 x_4) fun h_0 =>
-      test3._sparseCasesOn_1 x_2 (h_3 x x_1 x_3 x_4) fun h_0 =>
-        test3._sparseCasesOn_1 x_1 (h_4 x x_2 x_3 x_4) fun h_0 =>
-          test3._sparseCasesOn_1 x (h_5 x_1 x_2 x_3 x_4) fun h_0 => h_6 x x_1 x_2 x_3 x_4
--/
-#guard_msgs in
-#print test4.match_1
-
-def test4' : Bool → Bool → Bool → Bool → Bool → Bool
-  | _, _ , _ , _ , true => true
-  | _, _ , _ , true, _ => true
-  | _, _ , true, _ , _ => true
-  | _, true, _ , _ , _ => true
-  | true, _ , _ , _ , _ => true
-  | false, false, false, false, false => false
-
-/--
-info: def test4'.match_1.{u_1} : (motive : Bool → Bool → Bool → Bool → Bool → Sort u_1) →
-  (x x_1 x_2 x_3 x_4 : Bool) →
-    ((x x_5 x_6 x_7 : Bool) → motive x x_5 x_6 x_7 true) →
-      ((x x_5 x_6 x_7 : Bool) → motive x x_5 x_6 true x_7) →
-        ((x x_5 x_6 x_7 : Bool) → motive x x_5 true x_6 x_7) →
-          ((x x_5 x_6 x_7 : Bool) → motive x true x_5 x_6 x_7) →
-            ((x x_5 x_6 x_7 : Bool) → motive true x x_5 x_6 x_7) →
-              (Unit → motive false false false false false) → motive x x_1 x_2 x_3 x_4 :=
 fun motive x x_1 x_2 x_3 x_4 h_1 h_2 h_3 h_4 h_5 h_6 =>
   Bool.casesOn x_4
     (Bool.casesOn x_3
       (Bool.casesOn x_2
-        (Bool.casesOn x_1 (Bool.casesOn x (h_6 ()) (h_5 false false false false)) (h_4 x false false false))
+        (Bool.casesOn x_1 (Bool.casesOn x (h_6 false false false false false) (h_5 false false false false))
+          (h_4 x false false false))
         (h_3 x x_1 false false))
       (h_2 x x_1 x_2 false))
     (h_1 x x_1 x_2 x_3)
 -/
 #guard_msgs in
-#print test4'.match_1
+#print test4.match_1
 
 -- Just testing the backwards compatibility option
 
@@ -132,7 +104,7 @@ def testOld (a : List Nat) : Nat :=
 /--
 info: def testOld.match_1.{u_1} : (motive : List Nat → Sort u_1) →
   (a : List Nat) → ((x : List Nat) → motive x) → (Unit → motive []) → motive a :=
-fun motive a h_1 h_2 => test3._sparseCasesOn_2 a (h_1 []) fun h_0 => h_1 a
+fun motive a h_1 h_2 => List.casesOn a (h_1 []) fun head tail => h_1 (head :: tail)
 -/
 #guard_msgs in
 #print testOld.match_1

tests/lean/run/library_suggestions.lean

@@ -16,7 +16,7 @@ set_library_suggestions Nat
 
 set_library_suggestions (fun _ _ => pure #[])
 
-/-- info: Library suggestions: -/
+/-- info: Library suggestions: [] -/
 #guard_msgs in
 example : True := by
   suggestions

tests/lean/run/library_suggestions_local.lean

@@ -16,8 +16,7 @@ set_library_suggestions Lean.LibrarySuggestions.currentFile
 -- First test: should show only myLocalTheorem
 -- (not myLocalDef since it's a def, not Lean.shouldBeFiltered since it's in Lean namespace)
 /--
-info: Library suggestions:
-  myLocalTheorem
+info: Library suggestions: [myLocalTheorem]
 -/
 #guard_msgs in
 example : True := by
@@ -31,9 +30,7 @@ def myFunction (x : Nat) : Nat := x + 1
 
 -- Second test: should show only the two theorems (not myFunction)
 /--
-info: Library suggestions:
-  anotherTheorem
-  myLocalTheorem
+info: Library suggestions: [anotherTheorem, myLocalTheorem]
 -/
 #guard_msgs in
 example : False → True := by

tests/lean/run/match1.lean

@@ -134,55 +134,24 @@ partial def natToBin' : (n : Nat) → List Bool
   | Parity.even j => false :: natToBin j
   | Parity.odd  j => true  :: natToBin j
 
--- This used to be bad until we used sparse matchers,
--- which meant that the `0` pattern does not cause the remaining
--- to have `n = .succ _`, whic breaks dependent pattern matching
+/--
+error: Tactic `cases` failed with a nested error:
+Dependent elimination failed: Failed to solve equation
+  n✝¹.succ = n✝.add n✝
+at case `Parity.even` after processing
+  (Nat.succ _), _
+the dependent pattern matcher can solve the following kinds of equations
+- <var> = <term> and <term> = <var>
+- <term> = <term> where the terms are definitionally equal
+- <constructor> = <constructor>, examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nil
+-/
+#guard_msgs in
 partial def natToBinBad (n : Nat) : List Bool :=
 match n, parity n with
 | 0, _             => []
 | _, Parity.even j => false :: natToBin j
 | _, Parity.odd  j => true  :: natToBin j
 
-set_option backwards.match.sparseCases false in
-/--
-error: Tactic `cases` failed with a nested error:
-Dependent elimination failed: Failed to solve equation
-  n✝¹.succ = n✝.add n✝
-at case `Parity.even` after processing
-  (Nat.succ _), _
-the dependent pattern matcher can solve the following kinds of equations
-- <var> = <term> and <term> = <var>
-- <term> = <term> where the terms are definitionally equal
-- <constructor> = <constructor>, examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nil
--/
-#guard_msgs in
-partial def natToBinBadOld (n : Nat) : List Bool :=
-match n, parity n with
-| 0, _             => []
-| _, Parity.even j => false :: natToBin j
-| _, Parity.odd  j => true  :: natToBin j
-
--- Even with sparse matching, this can break
-
-/--
-error: Tactic `cases` failed with a nested error:
-Dependent elimination failed: Failed to solve equation
-  n✝¹.succ = n✝.add n✝
-at case `Parity.even` after processing
-  (Nat.succ _), _
-the dependent pattern matcher can solve the following kinds of equations
-- <var> = <term> and <term> = <var>
-- <term> = <term> where the terms are definitionally equal
-- <constructor> = <constructor>, examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nil
--/
-#guard_msgs in
-partial def natToBinBad2 (n : Nat) : List Bool :=
-match n, parity n with
-| 0, _             => []
-| .succ 0, _       => [true]
-| _, Parity.even j => false :: natToBin j
-| _, Parity.odd  j => true  :: natToBin j
-
 partial def natToBin2 (n : Nat) : List Bool :=
 match n, parity n with
 | _, Parity.even 0 => []

tests/lean/run/matchMissingCase.lean

@@ -1,24 +0,0 @@
-inductive Enum where | a | b | c | d
-
-/--
-error: Missing cases:
-Enum.d
-Enum.c
--/
-#guard_msgs in
-def test : Enum → Nat
-  | .a => 0
-  | .b => 0
-
--- set_option trace.Meta.Match.match true
-
-/--
-error: Missing cases:
-Enum.d, false
-Enum.c, false
--/
-#guard_msgs(pass trace, all) in
-def test2 : Enum → Bool → Nat
-  | .a, _ => 0
-  | .b, _ => 0
-  | _, true => 0

tests/lean/run/matchOverlapInaccesible.lean

@@ -0,0 +1,72 @@
+set_option warn.sorry false
+
+inductive Parity : Nat -> Type
+| even (n) : Parity (n + n)
+| odd  (n) : Parity (Nat.succ (n + n))
+
+axiom nDiv2 (n : Nat)     : n % 2 = 0 → n = n/2 + n/2
+axiom nDiv2Succ (n : Nat) : n % 2 ≠ 0 → n = Nat.succ (n/2 + n/2)
+
+def parity (n : Nat) : Parity n :=
+if h : n % 2 = 0 then
+  Eq.ndrec (Parity.even (n/2)) (nDiv2 n h).symm
+else
+  Eq.ndrec (Parity.odd (n/2)) (nDiv2Succ n h).symm
+
+/--
+error: Tactic `cases` failed with a nested error:
+Dependent elimination failed: Failed to solve equation
+  n✝¹.succ = n✝.add n✝
+at case `Parity.even` after processing
+  (Nat.succ _), _
+the dependent pattern matcher can solve the following kinds of equations
+- <var> = <term> and <term> = <var>
+- <term> = <term> where the terms are definitionally equal
+- <constructor> = <constructor>, examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nil
+-/
+#guard_msgs in
+partial def natToBinBad (n : Nat) : List Bool :=
+match n, parity n with
+| 0, _             => []
+| _, Parity.even j => false :: natToBinBad j
+| _, Parity.odd  j => true  :: natToBinBad j
+
+
+inductive MyNat : Type where
+| zero : MyNat
+| succ : MyNat -> MyNat
+
+def MyNat.add : MyNat -> MyNat -> MyNat
+  | zero, n => n
+  | succ m, n => succ (add m n)
+
+instance : Add MyNat where
+  add := MyNat.add
+
+namespace MyNat
+
+inductive Parity : MyNat -> Type
+| even (n) : Parity (n + n)
+| odd  (n) : Parity (MyNat.succ (n + n))
+
+def parity (n : MyNat) : Parity n := sorry
+
+-- set_option trace.Meta.Match.match true
+
+/--
+error: Tactic `cases` failed with a nested error:
+Dependent elimination failed: Failed to solve equation
+  a✝.succ = n✝.add n✝
+at case `Parity.even` after processing
+  (succ _), _
+the dependent pattern matcher can solve the following kinds of equations
+- <var> = <term> and <term> = <var>
+- <term> = <term> where the terms are definitionally equal
+- <constructor> = <constructor>, examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nil
+-/
+#guard_msgs(pass trace, all) in
+partial def myNatToBinBad (n : MyNat) : List Bool :=
+match n, parity n with
+| zero, _             => []
+| _, Parity.even j => false :: myNatToBinBad j
+| _, Parity.odd  j => true  :: myNatToBinBad j

tests/lean/run/matchSparse.lean

@@ -1,83 +0,0 @@
-import Lean
-open Lean Expr Level -- just for shorter outpt
-
--- set_option trace.Meta.Match.match true
--- set_option trace.Meta.Match.debug true
--- set_option trace.Meta.Tactic.induction true
-
-def simple : Lean.Expr → Bool
-  | .sort _ => true
-  | _      => false
-
-def expensive : Lean.Expr → Lean.Expr → Bool
-  | .app (.app (.sort 1) (.sort 1)) (.sort 1), .app (.app (.sort 1) (.sort 1)) (.sort 1) => false
-  | _, _ => true
-
-/-- info: false -/
-#guard_msgs in
-#eval expensive (.app (.app (.sort 1) (.sort 1)) (.sort 1)) (.app (.app (.sort 1) (.sort 1)) (.sort 1))
-
-/-- info: true -/
-#guard_msgs in
-#eval expensive (.app (.app (.sort 2) (.sort 1)) (.sort 1)) (.app (.app (.sort 1) (.sort 1)) (.sort 1))
-
-example : expensive (.app (.app (.sort 1) (.sort 1)) (.sort 1)) (.app (.app (.sort 1) (.sort 1)) (.sort 1)) = false := rfl
-example : expensive (.app (.app (.sort 2) (.sort 1)) (.sort 1)) (.app (.app (.sort 1) (.sort 1)) (.sort 1)) = true := rfl
-
-/--
-info: expensive.match_1.{u_1} (motive : Expr → Expr → Sort u_1) (x✝ x✝¹ : Expr)
-  (h_1 :
-    Unit →
-      motive (((sort zero.succ).app (sort zero.succ)).app (sort zero.succ))
-        (((sort zero.succ).app (sort zero.succ)).app (sort zero.succ)))
-  (h_2 : (x x_1 : Expr) → motive x x_1) : motive x✝ x✝¹
--/
-#guard_msgs in
-#check expensive.match_1
-/--
-info: expensive.match_1.splitter.{u_1} (motive : Expr → Expr → Sort u_1) (x✝ x✝¹ : Expr)
-  (h_1 :
-    motive (((sort zero.succ).app (sort zero.succ)).app (sort zero.succ))
-      (((sort zero.succ).app (sort zero.succ)).app (sort zero.succ)))
-  (h_2 :
-    (x x_1 : Expr) →
-      (x = ((sort zero.succ).app (sort zero.succ)).app (sort zero.succ) →
-          x_1 = ((sort zero.succ).app (sort zero.succ)).app (sort zero.succ) → False) →
-        motive x x_1) :
-  motive x✝ x✝¹
--/
-#guard_msgs in
-#check expensive.match_1.splitter
-/--
-info: expensive.match_1.eq_1.{u_1} (motive : Expr → Expr → Sort u_1)
-  (h_1 :
-    Unit →
-      motive (((sort zero.succ).app (sort zero.succ)).app (sort zero.succ))
-        (((sort zero.succ).app (sort zero.succ)).app (sort zero.succ)))
-  (h_2 : (x x_1 : Expr) → motive x x_1) :
-  (match ((sort zero.succ).app (sort zero.succ)).app (sort zero.succ),
-      ((sort zero.succ).app (sort zero.succ)).app (sort zero.succ) with
-    | ((sort zero.succ).app (sort zero.succ)).app (sort zero.succ),
-      ((sort zero.succ).app (sort zero.succ)).app (sort zero.succ) => h_1 ()
-    | x, x_1 => h_2 x x_1) =
-    h_1 ()
--/
-#guard_msgs in
-#check expensive.match_1.eq_1
-/--
-info: expensive.match_1.eq_2.{u_1} (motive : Expr → Expr → Sort u_1) (x✝ x✝¹ : Expr)
-  (h_1 :
-    Unit →
-      motive (((sort zero.succ).app (sort zero.succ)).app (sort zero.succ))
-        (((sort zero.succ).app (sort zero.succ)).app (sort zero.succ)))
-  (h_2 : (x x_1 : Expr) → motive x x_1) :
-  (x✝ = ((sort zero.succ).app (sort zero.succ)).app (sort zero.succ) →
-      x✝¹ = ((sort zero.succ).app (sort zero.succ)).app (sort zero.succ) → False) →
-    (match x✝, x✝¹ with
-      | ((sort zero.succ).app (sort zero.succ)).app (sort zero.succ),
-        ((sort zero.succ).app (sort zero.succ)).app (sort zero.succ) => h_1 ()
-      | x, x_1 => h_2 x x_1) =
-      h_2 x✝ x✝¹
--/
-#guard_msgs in
-#check expensive.match_1.eq_2

tests/lean/run/matchSparse2.lean

@@ -1,38 +0,0 @@
-set_option linter.unusedVariables false
-
-/-! A variety of matches that failed at some point during the development of the sparse match features. -/
-
-
-inductive Finn : Nat → Type where
-  | fzero : {n : Nat} → Finn n
-  | fsucc : {n : Nat} → Finn n → Finn (n+1)
-
-def Finn.min (x : Bool) {n : Nat} (m : Nat) : Finn n → (f : Finn n) → Unit
-  | fzero, _ => ()
-  | _, fzero => ()
-  | fsucc i, fsucc j => ()
-
-def boo (x : Fin 3) : Nat :=
-  match x with
-  | 0 => 1
-  | 1 => 2
-  | 2 => 4
-
--- This only works if we do not use the sparse cases on when there are no alternatives left
-def List.nth : (as : List α) → (i : Fin as.length) → α
-  | a::as, ⟨0, _⟩   => a
-  | a::as, ⟨i+1, h⟩ => nth as ⟨i, Nat.lt_of_succ_lt_succ h⟩
-
-
--- So does this, taken from the standard library
-example : (a b : Int) → (h : a * b = 0) → a = 0 ∨ b = 0
-  | .ofNat 0, _, _ => by simp
-  | _, .ofNat 0, _ => by simp
-  | .ofNat (a+1), .negSucc b, h => by cases h
-
--- When we use the sparse cases more aggressively, we had to write it like this
-example : (a b : Int) → (h : a * b = 0) → a = 0 ∨ b = 0
-  | .ofNat 0, _, _ => by simp
-  | _, .ofNat 0, _ => by simp
-  | .ofNat (a+1), .negSucc b, h => by cases h
-  | .negSucc _, .negSucc _, h => by cases h

tests/pkg/structure_docstrings/StructureDocstrings.lean

@@ -1,2 +0,0 @@
-import StructureDocstrings.A
-import StructureDocstrings.B

tests/pkg/structure_docstrings/StructureDocstrings/A.lean

@@ -1,9 +0,0 @@
-module
-
-public section
-
-class Monoid (M : Type) extends Mul M where
-
-class DivInvMonoid (G : Type) extends Mul G where
-  /-- The power operation: `a ^ n = a * ··· * a`; `a ^ (-n) = a⁻¹ * ··· a⁻¹` (`n` times) -/
-  protected zpow : Int → G → G

tests/pkg/structure_docstrings/StructureDocstrings/B.lean

@@ -1,7 +0,0 @@
-module
-
-public import StructureDocstrings.A
-
-public section
-
-class GroupWithZero (G : Type) extends Monoid G, DivInvMonoid G where

tests/pkg/structure_docstrings/StructureDocstrings/C.lean

@@ -1,15 +0,0 @@
-module
-
-import Lean.DocString
-import Lean.Meta.Basic
-public import StructureDocstrings.B
-
-public section
-
-/-- info: The power operation: `a ^ n = a * ··· * a`; `a ^ (-n) = a⁻¹ * ··· a⁻¹` (`n` times) -/
-#guard_msgs in
-open Lean in
-run_meta do
-  let env ← getEnv
-  let some r ← Lean.findDocString? env `GroupWithZero.zpow | failure
-  logInfo r

tests/pkg/structure_docstrings/lakefile.toml

@@ -1,13 +0,0 @@
-name = "structure_docstrings"
-defaultTargets = ["StructureDocstrings", "StructureDocstringsTest"]
-
-[[lean_lib]]
-name = "StructureDocstrings"
-leanOptions = { experimental.module = true }
-roots = ["StructureDocstrings.A", "StructureDocstrings.B"]
-
-[[lean_lib]]
-name = "StructureDocstringsTest"
-# Elab.inServer to allow docstring tests to access .server level data
-leanOptions = { experimental.module = true, Elab.inServer = true }
-roots = ["StructureDocstrings.C"]

tests/pkg/structure_docstrings/lean-toolchain

@@ -1 +0,0 @@
-lean4-2

tests/pkg/structure_docstrings/test.sh

@@ -1,5 +0,0 @@
-#!/usr/bin/env bash
-set -e
-
-rm -rf .lake/build
-LEAN_ABORT_ON_PANIC=1 lake build