From ea2b745e575232eb7c474801ded022a47c4eb5a4 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 5 Nov 2025 23:17:53 +0100
Subject: [PATCH] chore: new module system adjustments for the Mathlib port
 (#11093)

---
 src/Lean/Expr.lean              |  8 ++++----
 src/Lean/Meta/Tactic/Cases.lean | 18 +++++++-----------
 2 files changed, 11 insertions(+), 15 deletions(-)

diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean
index 10bfa56626..3d5195bc25 100644
--- a/src/Lean/Expr.lean
+++ b/src/Lean/Expr.lean
@@ -704,7 +704,7 @@ def mkSimpleThunk (type : Expr) : Expr :=
 /--
 `.lit l` is now the preferred form.
 -/
-def mkLit (l : Literal) : Expr :=
+@[match_pattern, expose] def mkLit (l : Literal) : Expr :=
   .lit l
 
 /--
@@ -712,7 +712,7 @@ Return the "raw" natural number `.lit (.natVal n)`.
 This is not the default representation used by the Lean frontend.
 See `mkNatLit`.
 -/
-def mkRawNatLit (n : Nat) : Expr :=
+@[match_pattern, expose] def mkRawNatLit (n : Nat) : Expr :=
   mkLit (.natVal n)
 
 /--
@@ -720,12 +720,12 @@ Return a natural number literal used in the frontend. It is a `OfNat.ofNat` appl
 Recall that all theorems and definitions containing numeric literals are encoded using
 `OfNat.ofNat` applications in the frontend.
 -/
-def mkNatLit (n : Nat) : Expr :=
+@[match_pattern, expose] def mkNatLit (n : Nat) : Expr :=
   let r := mkRawNatLit n
   mkApp3 (mkConst ``OfNat.ofNat [levelZero]) (mkConst ``Nat) r (mkApp (mkConst ``instOfNatNat) r)
 
 /-- Return the string literal `.lit (.strVal s)` -/
-def mkStrLit (s : String) : Expr :=
+@[match_pattern, expose] def mkStrLit (s : String) : Expr :=
   mkLit (.strVal s)
 
 @[export lean_expr_mk_bvar] def mkBVarEx : Nat → Expr := mkBVar
diff --git a/src/Lean/Meta/Tactic/Cases.lean b/src/Lean/Meta/Tactic/Cases.lean
index 53e1b30429..ab5dbc5923 100644
--- a/src/Lean/Meta/Tactic/Cases.lean
+++ b/src/Lean/Meta/Tactic/Cases.lean
@@ -155,7 +155,6 @@ namespace Cases
 
 structure Context where
   inductiveVal     : InductiveVal
-  casesOnVal       : DefinitionVal
   nminors          : Nat := inductiveVal.ctors.length
   majorDecl        : LocalDecl
   majorTypeFn      : Expr
@@ -171,16 +170,13 @@ private def mkCasesContext? (majorFVarId : FVarId) : MetaM (Option Context) := d
     let majorType ← whnf majorDecl.type
     majorType.withApp fun f args => matchConstInduct f (fun _ => pure none) fun ival _ =>
       if args.size != ival.numIndices + ival.numParams then pure none
-      else match env.find? (Name.mkStr ival.name "casesOn") with
-        | ConstantInfo.defnInfo cval =>
-          return some {
-            inductiveVal  := ival,
-            casesOnVal    := cval,
-            majorDecl     := majorDecl,
-            majorTypeFn   := f,
-            majorTypeArgs := args
-          }
-        | _ => pure none
+      else if !env.contains (Name.mkStr ival.name "casesOn") then pure none
+      else return some {
+        inductiveVal  := ival,
+        majorDecl     := majorDecl,
+        majorTypeFn   := f,
+        majorTypeArgs := args
+      }
 
 /--
 We say the major premise has independent indices IF