From 5bf4cf8ea6a2eadeb076ef898affbe3d798ff403 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Tue, 8 Sep 2026 13:50:37 +0000
Subject: [PATCH 1/5] virtual one-field structures

---
 src/Lean/Elab.lean                  |  1 +
 src/Lean/Elab/Tactic.lean           |  1 +
 src/Lean/Meta/ExprDefEq.lean        | 21 +++++++++++++++++++++
 src/Lean/Meta/Tactic/Simp/Main.lean |  3 +++
 src/Lean/Meta/WHNF.lean             | 26 ++++++++++++++++++++++++++
 5 files changed, 52 insertions(+)

diff --git a/src/Lean/Elab.lean b/src/Lean/Elab.lean
index 2f770dd2a098..30be2ba97516 100644
--- a/src/Lean/Elab.lean
+++ b/src/Lean/Elab.lean
@@ -32,6 +32,7 @@ public import Lean.Elab.Structure
 public import Lean.Elab.Print
 public import Lean.Elab.MutualDef
 public import Lean.Elab.AuxDef
+public import Lean.Elab.TypeDef
 public import Lean.Elab.PreDefinition
 public import Lean.Elab.Deriving
 public import Lean.Elab.DeclarationRange
diff --git a/src/Lean/Elab/Tactic.lean b/src/Lean/Elab/Tactic.lean
index 4c08c9fabcff..0d26bffc81aa 100644
--- a/src/Lean/Elab/Tactic.lean
+++ b/src/Lean/Elab/Tactic.lean
@@ -46,6 +46,7 @@ public import Lean.Elab.Tactic.DiscrTreeKey
 public import Lean.Elab.Tactic.BVDecide
 public import Lean.Elab.Tactic.BoolToPropSimps
 public import Lean.Elab.Tactic.Classical
+public import Lean.Elab.Tactic.TypeDef
 public import Lean.Elab.Tactic.Impossible
 public import Lean.Elab.Tactic.Grind
 public import Lean.Elab.Tactic.Monotonicity
diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index 3bc3e69ab997..3112e3cc11b8 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -204,6 +204,25 @@ where
       else
         return false
 
+/--
+Virtual analog of `isDefEqEtaStruct`, for types declared by the `type_def` command
+(`VirtualStructureInfo`). Recognizes `b := ctorName arg`, where `ctorName` is a `type_def`-generated
+constructor, and — provided `a` is not itself such a constructor application, in which case
+`isDefEqArgs` handles the comparison more directly — reduces `a =?= b` to `projName a =?= arg`.
+Combined with `reduceVirtualProj?`, this gives `type_def`-declared types the same iota/eta behavior
+as a real one-field structure, even though `N`, `N.mk` and `N.toNat` never unfold.
+-/
+private def isDefEqVirtualEtaStruct (a b : Expr) : MetaM Bool := do
+  let .const ctorName us := b.getAppFn | return false
+  let some info ← getVirtualCtorInfo? ctorName | return false
+  unless b.getAppNumArgs == 1 do return false
+  if let .const ctorName' _ := a.getAppFn then
+    if ctorName' == info.ctorName then return false
+  if (← isDefEq (← inferType a) (← inferType b)) then
+    checkpointDefEq <| isDefEq (mkApp (mkConst info.projName us) a) b.appArg!
+  else
+    return false
+
 /--
   Try to solve `a := (fun x => t) =?= b` by eta-expanding `b`,
   resulting in `t =?= b x` (with a fresh free variable `x`).
@@ -2425,6 +2444,8 @@ private def isExprDefEqExpensive (t : Expr) (s : Expr) : MetaM Bool := do
     -- which is very costly because it requires us to unify the fields.
     if (← (isDefEqEtaStruct t s <||> isDefEqEtaStruct s t)) then
       return true
+    if (← (isDefEqVirtualEtaStruct t s <||> isDefEqVirtualEtaStruct s t)) then
+      return true
     if t.isConst && s.isConst then
       if t.constName! == s.constName! then isListLevelDefEqAux t.constLevels! s.constLevels! else return false
     else if (← pure t.isApp <&&> pure s.isApp) then
diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index b648566cb9eb..83b2a56e2a72 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -226,6 +226,9 @@ private def reduceStep (e : Expr) : SimpM Expr := do
     | none =>
     match (← reduceProjFn? e) with
     | some e => return e
+    | none =>
+    match (← reduceVirtualProj? e) with
+    | some e => return e
     | none   => pure ()
   if cfg.iota then
     match (← reduceRecMatcher? e) with
diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index a395af246ba0..d6aeca4c14ff 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -7,6 +7,7 @@ module
 
 prelude
 public import Lean.Structure
+public import Lean.Meta.VirtualStructure
 public import Lean.Util.Recognizers
 public import Lean.Util.SafeExponentiation
 public import Lean.Meta.GetUnfoldableConst
@@ -553,6 +554,24 @@ def reduceProj? (e : Expr) : MetaM (Option Expr) := do
   | .proj _ i c => project? c i
   | _           => return none
 
+/--
+Reduce `projName (ctorName a)` to `a`, where `projName`/`ctorName` are the constructor/projector
+pair auto-generated by the `type_def` command for some virtual type (see `VirtualStructureInfo`).
+This mirrors `reduceProj?`, but for virtual (`def`-based) structures rather than real ones:
+`ctorName`/`projName` have no `Expr.proj`/constructor application to pattern-match on, so we
+instead consult the `type_def` registry. Like real projection-of-constructor reduction, this is
+independent of `ctorName`/`projName`'s reducibility status, even though `type_def` marks both
+`@[irreducible]` (so that they do *not* unfold on their own).
+-/
+def reduceVirtualProj? (e : Expr) : MetaM (Option Expr) := do
+  let .const projName _ := e.getAppFn | return none
+  unless e.getAppNumArgs == 1 do return none
+  let some projInfo ← getVirtualProjInfo? projName | return none
+  let arg ← whnf e.appArg!
+  let .const ctorName _ := arg.getAppFn | return none
+  unless ctorName == projInfo.ctorName && arg.getAppNumArgs == 1 do return none
+  return some arg.appArg!
+
 /--
   Auxiliary method for reducing terms of the form `?m t_1 ... t_n` where `?m` is delayed assigned.
   Recall that we can only expand a delayed assignment when all holes/metavariables in the assigned value have been "filled".
@@ -655,6 +674,13 @@ where
           go eNew
         else
           let e := if f == f' then e else e.updateFn f'
+          -- Virtual projection-of-constructor reduction is gated like real `.proj`-node
+          -- reduction (`cfg.proj`), not like matcher/recursor reduction (`cfg.iota`): a
+          -- `type_def`-generated projector never becomes a real `Expr.proj` node (it stays an
+          -- irreducible `.app`), so this is the only place its "iota" ever gets applied.
+          unless cfg.proj matches .no do
+            if let some eNew ← reduceVirtualProj? e then
+              return ← go eNew
           unless cfg.iota do return e
           match (← reduceMatcher? e) with
           | .reduced eNew => go eNew

From 0c8bed4fda0b82287d2e9e6c87a878b033e2bb58 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Tue, 8 Sep 2026 15:11:59 +0000
Subject: [PATCH 2/5] second part

---
 src/Lean/Elab/Tactic/TypeDef.lean        | 49 +++++++++++++++
 src/Lean/Elab/TypeDef.lean               | 51 ++++++++++++++++
 src/Lean/Meta/VirtualStructure.lean      | 77 ++++++++++++++++++++++++
 tests/elab/typeDefGrind.lean             | 11 ++++
 tests/elab/typeDefVirtualEta.lean        | 17 ++++++
 tests/elab/typeDefVirtualIota.lean       | 23 +++++++
 tests/elab/typeDefWithReducibleType.lean | 19 ++++++
 7 files changed, 247 insertions(+)
 create mode 100644 src/Lean/Elab/Tactic/TypeDef.lean
 create mode 100644 src/Lean/Elab/TypeDef.lean
 create mode 100644 src/Lean/Meta/VirtualStructure.lean
 create mode 100644 tests/elab/typeDefGrind.lean
 create mode 100644 tests/elab/typeDefVirtualEta.lean
 create mode 100644 tests/elab/typeDefVirtualIota.lean
 create mode 100644 tests/elab/typeDefWithReducibleType.lean

diff --git a/src/Lean/Elab/Tactic/TypeDef.lean b/src/Lean/Elab/Tactic/TypeDef.lean
new file mode 100644
index 000000000000..6f0ebe0f693c
--- /dev/null
+++ b/src/Lean/Elab/Tactic/TypeDef.lean
@@ -0,0 +1,49 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+public import Lean.Elab.Tactic.Basic
+public import Lean.Meta.VirtualStructure
+
+public section
+
+namespace Lean.Parser.Tactic
+
+/--
+`with_reducible_type N => tacs` runs `tacs` with the `type_def`-declared type `N` -- together with
+its auto-generated constructor and projector -- temporarily relaxed from `[irreducible]` to
+`[reducible]`, restoring the original status afterward even if `tacs` fails. This is the escape
+hatch for a `type_def` type: within the block, `N`, `N.mk` and its projector unfold like ordinary
+reducible definitions, enabling the `rfl`-style defeq abuse that is disallowed everywhere else.
+-/
+syntax (name := withReducibleType) "with_reducible_type " ident " => " tacticSeq : tactic
+
+end Lean.Parser.Tactic
+
+namespace Lean.Elab.Tactic
+
+/-- Combinator underlying the `with_reducible_type` tactic; see its docstring. -/
+def withReducibleType [Monad m] [MonadEnv m] [MonadFinally m] [MonadResolveName m]
+    [MonadOptions m] [MonadLog m] [AddMessageContext m] [MonadError m]
+    (typeStx : Syntax) (t : m α) : m α := do
+  let typeName ← resolveGlobalConstNoOverload typeStx
+  let some info ← getVirtualStructureInfo? typeName
+    | throwErrorAt typeStx "'{typeName}' is not a `type_def`-declared type"
+  let names := #[info.typeName, info.ctorName, info.projName]
+  let origStatuses ← names.mapM getReducibilityStatus
+  for n in names do
+    setReducibilityStatus n .reducible
+  try
+    t
+  finally
+    for (n, s) in names.zip origStatuses do
+      setReducibilityStatus n s
+
+@[builtin_tactic Lean.Parser.Tactic.withReducibleType] def evalWithReducibleType : Tactic :=
+  fun stx => withReducibleType stx[1] (evalTactic stx[3])
+
+end Lean.Elab.Tactic
diff --git a/src/Lean/Elab/TypeDef.lean b/src/Lean/Elab/TypeDef.lean
new file mode 100644
index 000000000000..668ac7986ab2
--- /dev/null
+++ b/src/Lean/Elab/TypeDef.lean
@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+public import Lean.Elab.Command
+public import Lean.Meta.VirtualStructure
+
+public section
+
+namespace Lean.Elab.Command
+
+/--
+`type_def N := ty with proj` declares a type `N` definitionally equal to `ty`, together with a
+constructor `N.mk : ty → N` and a projector `N.proj : N → ty`, and marks all three
+`@[irreducible]`:
+```
+@[irreducible] def N := ty
+@[irreducible] def N.mk (a : ty) : N := a
+@[irreducible] def N.proj (n : N) : ty := n
+```
+This is the "irreducible type alias" pattern used to avoid defeq abuse while keeping a
+zero-overhead representation identical to `ty` (e.g. to cast `List ty` to `List N`). Unlike a
+hand-written version of this pattern, `type_def` also registers `N.mk`/`N.proj` as a virtual
+constructor/projector pair, so that `N.proj (N.mk a)` reduces to `a` (see
+`Lean.Meta.reduceVirtualProj?`) even though both stay irreducible otherwise.
+-/
+syntax (name := typeDef) "type_def " ident " := " term " with " ident : command
+
+@[builtin_command_elab typeDef]
+def elabTypeDef : CommandElab
+  | `(type_def $id:ident := $ty:term with $projId:ident) => do
+    let ctorId := mkIdentFrom id (id.getId ++ `mk) (canonical := true)
+    let typeProjId := mkIdentFrom id (id.getId ++ projId.getId) (canonical := true)
+    elabCommand <| ← `(def $id := $ty)
+    elabCommand <| ← `(def $ctorId (a : $ty) : $id := a)
+    elabCommand <| ← `(def $typeProjId (n : $id) : $ty := n)
+    elabCommand <| ← `(attribute [irreducible] $id $ctorId $typeProjId)
+    let ns ← getCurrNamespace
+    let info : VirtualStructureInfo := {
+      typeName := ns ++ id.getId
+      ctorName := ns ++ ctorId.getId
+      projName := ns ++ typeProjId.getId
+    }
+    modifyEnv (registerVirtualStructure · info)
+  | _ => throwUnsupportedSyntax
+
+end Lean.Elab.Command
diff --git a/src/Lean/Meta/VirtualStructure.lean b/src/Lean/Meta/VirtualStructure.lean
new file mode 100644
index 000000000000..c2f676bbafed
--- /dev/null
+++ b/src/Lean/Meta/VirtualStructure.lean
@@ -0,0 +1,77 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+public import Lean.EnvExtension
+
+public section
+
+namespace Lean
+
+/--
+Registered by the `type_def` command for a declaration such as
+```
+type_def N := Nat with toNat
+```
+Associates the auto-generated constructor (`N.mk`) and projector (`N.toNat`) with each other and
+with the type they wrap (`N`), so that `Lean.Meta.whnf`/`isDefEq` can treat `N.toNat (N.mk a)` and
+`N.mk (N.toNat x)` like the iota/eta reduction of a real one-field structure's constructor and
+projector, even though `N`, `N.mk` and `N.toNat` are ordinary `def`s (marked `@[irreducible]`)
+rather than a genuine inductive type.
+-/
+structure VirtualStructureInfo where
+  /-- The `type_def`-declared type. -/
+  typeName : Name
+  /-- The auto-generated constructor, wrapping a value of the underlying type as `typeName`. -/
+  ctorName : Name
+  /-- The auto-generated projector, unwrapping a `typeName` value back to the underlying type. -/
+  projName : Name
+  deriving Inhabited, Repr
+
+builtin_initialize virtualStructureTypeExt : MapDeclarationExtension VirtualStructureInfo ←
+  mkMapDeclarationExtension
+builtin_initialize virtualStructureCtorExt : MapDeclarationExtension VirtualStructureInfo ←
+  mkMapDeclarationExtension
+builtin_initialize virtualStructureProjExt : MapDeclarationExtension VirtualStructureInfo ←
+  mkMapDeclarationExtension
+
+/-- Registers `info` under its type, constructor and projector names, so all three can be looked
+up from any of them. -/
+def registerVirtualStructure (env : Environment) (info : VirtualStructureInfo) : Environment :=
+  let env := virtualStructureTypeExt.insert env info.typeName info
+  let env := virtualStructureCtorExt.insert env info.ctorName info
+  virtualStructureProjExt.insert env info.projName info
+
+namespace Environment
+
+/-- If `typeName` was declared via `type_def`, return its virtual structure info. -/
+def getVirtualStructureInfo? (env : Environment) (typeName : Name) : Option VirtualStructureInfo :=
+  virtualStructureTypeExt.find? env typeName
+
+/-- If `ctorName` is the constructor auto-generated by `type_def`, return its virtual structure
+info. -/
+def getVirtualCtorInfo? (env : Environment) (ctorName : Name) : Option VirtualStructureInfo :=
+  virtualStructureCtorExt.find? env ctorName
+
+/-- If `projName` is the projector auto-generated by `type_def`, return its virtual structure
+info. -/
+def getVirtualProjInfo? (env : Environment) (projName : Name) : Option VirtualStructureInfo :=
+  virtualStructureProjExt.find? env projName
+
+end Environment
+
+def getVirtualStructureInfo? [Monad m] [MonadEnv m] (typeName : Name) :
+    m (Option VirtualStructureInfo) :=
+  return (← getEnv).getVirtualStructureInfo? typeName
+
+def getVirtualCtorInfo? [Monad m] [MonadEnv m] (ctorName : Name) : m (Option VirtualStructureInfo) :=
+  return (← getEnv).getVirtualCtorInfo? ctorName
+
+def getVirtualProjInfo? [Monad m] [MonadEnv m] (projName : Name) : m (Option VirtualStructureInfo) :=
+  return (← getEnv).getVirtualProjInfo? projName
+
+end Lean
diff --git a/tests/elab/typeDefGrind.lean b/tests/elab/typeDefGrind.lean
new file mode 100644
index 000000000000..f582327666c8
--- /dev/null
+++ b/tests/elab/typeDefGrind.lean
@@ -0,0 +1,11 @@
+import Lean
+
+/-!
+Confirms `grind` needs no `type_def`-specific special-casing of its own: its simp-based
+normalization (`Lean.Meta.Grind.simpCore`/`dsimpCore`) reuses `Simp.mainCore`/`Simp.reduceStep`,
+which already knows how to reduce virtual projections (see `typeDefVirtualIota.lean`).
+-/
+
+type_def N := Nat with toNat
+
+example (n : Nat) : N.toNat (N.mk n) = n := by grind
diff --git a/tests/elab/typeDefVirtualEta.lean b/tests/elab/typeDefVirtualEta.lean
new file mode 100644
index 000000000000..e5edf283edfd
--- /dev/null
+++ b/tests/elab/typeDefVirtualEta.lean
@@ -0,0 +1,17 @@
+import Lean
+
+/-!
+Tests virtual structure eta for `type_def`-declared types (`Lean.Meta.isDefEqVirtualEtaStruct`):
+`N.mk (N.toNat x) = x` holds by `rfl`, just like eta for a real one-field structure, even though
+`N`/`N.mk`/`N.toNat` are irreducible. Also tests that `simp only` reduces the virtual projection
+`N.toNat (N.mk n)` the same way it does for a real structure's projection-of-constructor
+(`Lean.Meta.reduceVirtualProj?`, wired into `Simp.reduceStep`).
+-/
+
+type_def N := Nat with toNat
+
+-- Virtual eta.
+example (x : N) : N.mk (N.toNat x) = x := rfl
+
+-- `simp only` reduces the virtual projection (iota), without any lemmas.
+example (n : Nat) : N.toNat (N.mk n) = n := by simp only
diff --git a/tests/elab/typeDefVirtualIota.lean b/tests/elab/typeDefVirtualIota.lean
new file mode 100644
index 000000000000..859d5710a482
--- /dev/null
+++ b/tests/elab/typeDefVirtualIota.lean
@@ -0,0 +1,23 @@
+import Lean
+
+/-!
+Tests the `type_def` command. It generates an irreducible type alias together with a
+constructor/projector pair (`N`, `N.mk`, `N.toNat`), and registers the pair as a "virtual
+structure" so that `whnf`/`isDefEq` reduce `N.toNat (N.mk n)` to `n` (virtual iota), even though
+`N`, `N.mk` and `N.toNat` are otherwise irreducible (so `N` does not unify with `Nat` in general).
+-/
+
+type_def N := Nat with toNat
+
+-- Virtual iota: projector-of-constructor reduces by `rfl`, without unfolding `N`/`N.mk`/`N.toNat`.
+example (n : Nat) : N.toNat (N.mk n) = n := rfl
+
+-- `N` stays irreducible outside of the virtual iota pattern: it does not unify with `Nat`.
+/-- error: Type mismatch
+  n
+has type
+  Nat
+but is expected to have type
+  N -/
+#guard_msgs in
+example (n : Nat) : N := n
diff --git a/tests/elab/typeDefWithReducibleType.lean b/tests/elab/typeDefWithReducibleType.lean
new file mode 100644
index 000000000000..988d3c70a490
--- /dev/null
+++ b/tests/elab/typeDefWithReducibleType.lean
@@ -0,0 +1,19 @@
+import Lean
+
+/-!
+Tests the `with_reducible_type` tactic combinator: it is the escape hatch for a `type_def`-declared
+type, temporarily relaxing `N`/`N.mk`/`N.toNat` from `[irreducible]` to `[reducible]` for the
+duration of the tactic block (e.g. to prove `N = Nat`, which requires unfolding `N`'s definition),
+and restores the original `[irreducible]` status afterward.
+-/
+
+type_def N := Nat with toNat
+
+-- Inside the block, `N` unfolds to `Nat`.
+example : N = Nat := by with_reducible_type N => rfl
+
+-- Outside the block, `N` is irreducible again: this still fails.
+/-- but is expected to have type
+  N = Nat -/
+#guard_msgs (substring := true) in
+example : N = Nat := rfl

From 4eb73253ed0e1f8b223d3b4ede0f6753fb29e2b0 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Tue, 8 Sep 2026 16:22:34 +0000
Subject: [PATCH 3/5] newtype

---
 src/Lean/Elab.lean                                   |  2 +-
 src/Lean/Elab/{TypeDef.lean => NewType.lean}         | 12 ++++++------
 src/Lean/Elab/Tactic.lean                            |  2 +-
 src/Lean/Elab/Tactic/{TypeDef.lean => NewType.lean}  |  6 +++---
 src/Lean/Meta/ExprDefEq.lean                         |  6 +++---
 src/Lean/Meta/VirtualStructure.lean                  | 12 ++++++------
 src/Lean/Meta/WHNF.lean                              |  8 ++++----
 tests/elab/newtypeGrind.lean                         | 11 +++++++++++
 ...typeDefVirtualEta.lean => newtypeVirtualEta.lean} |  4 ++--
 ...peDefVirtualIota.lean => newtypeVirtualIota.lean} |  4 ++--
 ...ucibleType.lean => newtypeWithReducibleType.lean} |  4 ++--
 tests/elab/typeDefGrind.lean                         | 11 -----------
 12 files changed, 41 insertions(+), 41 deletions(-)
 rename src/Lean/Elab/{TypeDef.lean => NewType.lean} (79%)
 rename src/Lean/Elab/Tactic/{TypeDef.lean => NewType.lean} (85%)
 create mode 100644 tests/elab/newtypeGrind.lean
 rename tests/elab/{typeDefVirtualEta.lean => newtypeVirtualEta.lean} (81%)
 rename tests/elab/{typeDefVirtualIota.lean => newtypeVirtualIota.lean} (85%)
 rename tests/elab/{typeDefWithReducibleType.lean => newtypeWithReducibleType.lean} (90%)
 delete mode 100644 tests/elab/typeDefGrind.lean

diff --git a/src/Lean/Elab.lean b/src/Lean/Elab.lean
index 30be2ba97516..70c0f0b9096e 100644
--- a/src/Lean/Elab.lean
+++ b/src/Lean/Elab.lean
@@ -32,7 +32,7 @@ public import Lean.Elab.Structure
 public import Lean.Elab.Print
 public import Lean.Elab.MutualDef
 public import Lean.Elab.AuxDef
-public import Lean.Elab.TypeDef
+public import Lean.Elab.NewType
 public import Lean.Elab.PreDefinition
 public import Lean.Elab.Deriving
 public import Lean.Elab.DeclarationRange
diff --git a/src/Lean/Elab/TypeDef.lean b/src/Lean/Elab/NewType.lean
similarity index 79%
rename from src/Lean/Elab/TypeDef.lean
rename to src/Lean/Elab/NewType.lean
index 668ac7986ab2..61640eb25551 100644
--- a/src/Lean/Elab/TypeDef.lean
+++ b/src/Lean/Elab/NewType.lean
@@ -14,7 +14,7 @@ public section
 namespace Lean.Elab.Command
 
 /--
-`type_def N := ty with proj` declares a type `N` definitionally equal to `ty`, together with a
+`newtype N := ty with proj` declares a type `N` definitionally equal to `ty`, together with a
 constructor `N.mk : ty → N` and a projector `N.proj : N → ty`, and marks all three
 `@[irreducible]`:
 ```
@@ -24,15 +24,15 @@ constructor `N.mk : ty → N` and a projector `N.proj : N → ty`, and marks all
 ```
 This is the "irreducible type alias" pattern used to avoid defeq abuse while keeping a
 zero-overhead representation identical to `ty` (e.g. to cast `List ty` to `List N`). Unlike a
-hand-written version of this pattern, `type_def` also registers `N.mk`/`N.proj` as a virtual
+hand-written version of this pattern, `newtype` also registers `N.mk`/`N.proj` as a virtual
 constructor/projector pair, so that `N.proj (N.mk a)` reduces to `a` (see
 `Lean.Meta.reduceVirtualProj?`) even though both stay irreducible otherwise.
 -/
-syntax (name := typeDef) "type_def " ident " := " term " with " ident : command
+syntax (name := newtypeCmd) "newtype " ident " := " term " with " ident : command
 
-@[builtin_command_elab typeDef]
-def elabTypeDef : CommandElab
-  | `(type_def $id:ident := $ty:term with $projId:ident) => do
+@[builtin_command_elab newtypeCmd]
+def elabNewtype : CommandElab
+  | `(newtype $id:ident := $ty:term with $projId:ident) => do
     let ctorId := mkIdentFrom id (id.getId ++ `mk) (canonical := true)
     let typeProjId := mkIdentFrom id (id.getId ++ projId.getId) (canonical := true)
     elabCommand <| ← `(def $id := $ty)
diff --git a/src/Lean/Elab/Tactic.lean b/src/Lean/Elab/Tactic.lean
index 0d26bffc81aa..79f5ddbdda64 100644
--- a/src/Lean/Elab/Tactic.lean
+++ b/src/Lean/Elab/Tactic.lean
@@ -46,7 +46,7 @@ public import Lean.Elab.Tactic.DiscrTreeKey
 public import Lean.Elab.Tactic.BVDecide
 public import Lean.Elab.Tactic.BoolToPropSimps
 public import Lean.Elab.Tactic.Classical
-public import Lean.Elab.Tactic.TypeDef
+public import Lean.Elab.Tactic.NewType
 public import Lean.Elab.Tactic.Impossible
 public import Lean.Elab.Tactic.Grind
 public import Lean.Elab.Tactic.Monotonicity
diff --git a/src/Lean/Elab/Tactic/TypeDef.lean b/src/Lean/Elab/Tactic/NewType.lean
similarity index 85%
rename from src/Lean/Elab/Tactic/TypeDef.lean
rename to src/Lean/Elab/Tactic/NewType.lean
index 6f0ebe0f693c..c9c403432e5a 100644
--- a/src/Lean/Elab/Tactic/TypeDef.lean
+++ b/src/Lean/Elab/Tactic/NewType.lean
@@ -14,10 +14,10 @@ public section
 namespace Lean.Parser.Tactic
 
 /--
-`with_reducible_type N => tacs` runs `tacs` with the `type_def`-declared type `N` -- together with
+`with_reducible_type N => tacs` runs `tacs` with the `newtype`-declared type `N` -- together with
 its auto-generated constructor and projector -- temporarily relaxed from `[irreducible]` to
 `[reducible]`, restoring the original status afterward even if `tacs` fails. This is the escape
-hatch for a `type_def` type: within the block, `N`, `N.mk` and its projector unfold like ordinary
+hatch for a `newtype`: within the block, `N`, `N.mk` and its projector unfold like ordinary
 reducible definitions, enabling the `rfl`-style defeq abuse that is disallowed everywhere else.
 -/
 syntax (name := withReducibleType) "with_reducible_type " ident " => " tacticSeq : tactic
@@ -32,7 +32,7 @@ def withReducibleType [Monad m] [MonadEnv m] [MonadFinally m] [MonadResolveName
     (typeStx : Syntax) (t : m α) : m α := do
   let typeName ← resolveGlobalConstNoOverload typeStx
   let some info ← getVirtualStructureInfo? typeName
-    | throwErrorAt typeStx "'{typeName}' is not a `type_def`-declared type"
+    | throwErrorAt typeStx "'{typeName}' is not a `newtype`-declared type"
   let names := #[info.typeName, info.ctorName, info.projName]
   let origStatuses ← names.mapM getReducibilityStatus
   for n in names do
diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index 3112e3cc11b8..990d9a97f1c5 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -205,11 +205,11 @@ where
         return false
 
 /--
-Virtual analog of `isDefEqEtaStruct`, for types declared by the `type_def` command
-(`VirtualStructureInfo`). Recognizes `b := ctorName arg`, where `ctorName` is a `type_def`-generated
+Virtual analog of `isDefEqEtaStruct`, for types declared by the `newtype` command
+(`VirtualStructureInfo`). Recognizes `b := ctorName arg`, where `ctorName` is a `newtype`-generated
 constructor, and — provided `a` is not itself such a constructor application, in which case
 `isDefEqArgs` handles the comparison more directly — reduces `a =?= b` to `projName a =?= arg`.
-Combined with `reduceVirtualProj?`, this gives `type_def`-declared types the same iota/eta behavior
+Combined with `reduceVirtualProj?`, this gives `newtype`-declared types the same iota/eta behavior
 as a real one-field structure, even though `N`, `N.mk` and `N.toNat` never unfold.
 -/
 private def isDefEqVirtualEtaStruct (a b : Expr) : MetaM Bool := do
diff --git a/src/Lean/Meta/VirtualStructure.lean b/src/Lean/Meta/VirtualStructure.lean
index c2f676bbafed..36524a0b4f3e 100644
--- a/src/Lean/Meta/VirtualStructure.lean
+++ b/src/Lean/Meta/VirtualStructure.lean
@@ -13,9 +13,9 @@ public section
 namespace Lean
 
 /--
-Registered by the `type_def` command for a declaration such as
+Registered by the `newtype` command for a declaration such as
 ```
-type_def N := Nat with toNat
+newtype N := Nat with toNat
 ```
 Associates the auto-generated constructor (`N.mk`) and projector (`N.toNat`) with each other and
 with the type they wrap (`N`), so that `Lean.Meta.whnf`/`isDefEq` can treat `N.toNat (N.mk a)` and
@@ -24,7 +24,7 @@ projector, even though `N`, `N.mk` and `N.toNat` are ordinary `def`s (marked `@[
 rather than a genuine inductive type.
 -/
 structure VirtualStructureInfo where
-  /-- The `type_def`-declared type. -/
+  /-- The `newtype`-declared type. -/
   typeName : Name
   /-- The auto-generated constructor, wrapping a value of the underlying type as `typeName`. -/
   ctorName : Name
@@ -48,16 +48,16 @@ def registerVirtualStructure (env : Environment) (info : VirtualStructureInfo) :
 
 namespace Environment
 
-/-- If `typeName` was declared via `type_def`, return its virtual structure info. -/
+/-- If `typeName` was declared via `newtype`, return its virtual structure info. -/
 def getVirtualStructureInfo? (env : Environment) (typeName : Name) : Option VirtualStructureInfo :=
   virtualStructureTypeExt.find? env typeName
 
-/-- If `ctorName` is the constructor auto-generated by `type_def`, return its virtual structure
+/-- If `ctorName` is the constructor auto-generated by `newtype`, return its virtual structure
 info. -/
 def getVirtualCtorInfo? (env : Environment) (ctorName : Name) : Option VirtualStructureInfo :=
   virtualStructureCtorExt.find? env ctorName
 
-/-- If `projName` is the projector auto-generated by `type_def`, return its virtual structure
+/-- If `projName` is the projector auto-generated by `newtype`, return its virtual structure
 info. -/
 def getVirtualProjInfo? (env : Environment) (projName : Name) : Option VirtualStructureInfo :=
   virtualStructureProjExt.find? env projName
diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index d6aeca4c14ff..df6aeacc6321 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -556,11 +556,11 @@ def reduceProj? (e : Expr) : MetaM (Option Expr) := do
 
 /--
 Reduce `projName (ctorName a)` to `a`, where `projName`/`ctorName` are the constructor/projector
-pair auto-generated by the `type_def` command for some virtual type (see `VirtualStructureInfo`).
+pair auto-generated by the `newtype` command for some virtual type (see `VirtualStructureInfo`).
 This mirrors `reduceProj?`, but for virtual (`def`-based) structures rather than real ones:
 `ctorName`/`projName` have no `Expr.proj`/constructor application to pattern-match on, so we
-instead consult the `type_def` registry. Like real projection-of-constructor reduction, this is
-independent of `ctorName`/`projName`'s reducibility status, even though `type_def` marks both
+instead consult the `newtype` registry. Like real projection-of-constructor reduction, this is
+independent of `ctorName`/`projName`'s reducibility status, even though `newtype` marks both
 `@[irreducible]` (so that they do *not* unfold on their own).
 -/
 def reduceVirtualProj? (e : Expr) : MetaM (Option Expr) := do
@@ -676,7 +676,7 @@ where
           let e := if f == f' then e else e.updateFn f'
           -- Virtual projection-of-constructor reduction is gated like real `.proj`-node
           -- reduction (`cfg.proj`), not like matcher/recursor reduction (`cfg.iota`): a
-          -- `type_def`-generated projector never becomes a real `Expr.proj` node (it stays an
+          -- `newtype`-generated projector never becomes a real `Expr.proj` node (it stays an
           -- irreducible `.app`), so this is the only place its "iota" ever gets applied.
           unless cfg.proj matches .no do
             if let some eNew ← reduceVirtualProj? e then
diff --git a/tests/elab/newtypeGrind.lean b/tests/elab/newtypeGrind.lean
new file mode 100644
index 000000000000..1bc7852bb4ff
--- /dev/null
+++ b/tests/elab/newtypeGrind.lean
@@ -0,0 +1,11 @@
+import Lean
+
+/-!
+Confirms `grind` needs no `newtype`-specific special-casing of its own: its simp-based
+normalization (`Lean.Meta.Grind.simpCore`/`dsimpCore`) reuses `Simp.mainCore`/`Simp.reduceStep`,
+which already knows how to reduce virtual projections (see `newtypeVirtualIota.lean`).
+-/
+
+newtype N := Nat with toNat
+
+example (n : Nat) : N.toNat (N.mk n) = n := by grind
diff --git a/tests/elab/typeDefVirtualEta.lean b/tests/elab/newtypeVirtualEta.lean
similarity index 81%
rename from tests/elab/typeDefVirtualEta.lean
rename to tests/elab/newtypeVirtualEta.lean
index e5edf283edfd..9b49f453c9ff 100644
--- a/tests/elab/typeDefVirtualEta.lean
+++ b/tests/elab/newtypeVirtualEta.lean
@@ -1,14 +1,14 @@
 import Lean
 
 /-!
-Tests virtual structure eta for `type_def`-declared types (`Lean.Meta.isDefEqVirtualEtaStruct`):
+Tests virtual structure eta for `newtype`-declared types (`Lean.Meta.isDefEqVirtualEtaStruct`):
 `N.mk (N.toNat x) = x` holds by `rfl`, just like eta for a real one-field structure, even though
 `N`/`N.mk`/`N.toNat` are irreducible. Also tests that `simp only` reduces the virtual projection
 `N.toNat (N.mk n)` the same way it does for a real structure's projection-of-constructor
 (`Lean.Meta.reduceVirtualProj?`, wired into `Simp.reduceStep`).
 -/
 
-type_def N := Nat with toNat
+newtype N := Nat with toNat
 
 -- Virtual eta.
 example (x : N) : N.mk (N.toNat x) = x := rfl
diff --git a/tests/elab/typeDefVirtualIota.lean b/tests/elab/newtypeVirtualIota.lean
similarity index 85%
rename from tests/elab/typeDefVirtualIota.lean
rename to tests/elab/newtypeVirtualIota.lean
index 859d5710a482..de6b6c577e9a 100644
--- a/tests/elab/typeDefVirtualIota.lean
+++ b/tests/elab/newtypeVirtualIota.lean
@@ -1,13 +1,13 @@
 import Lean
 
 /-!
-Tests the `type_def` command. It generates an irreducible type alias together with a
+Tests the `newtype` command. It generates an irreducible type alias together with a
 constructor/projector pair (`N`, `N.mk`, `N.toNat`), and registers the pair as a "virtual
 structure" so that `whnf`/`isDefEq` reduce `N.toNat (N.mk n)` to `n` (virtual iota), even though
 `N`, `N.mk` and `N.toNat` are otherwise irreducible (so `N` does not unify with `Nat` in general).
 -/
 
-type_def N := Nat with toNat
+newtype N := Nat with toNat
 
 -- Virtual iota: projector-of-constructor reduces by `rfl`, without unfolding `N`/`N.mk`/`N.toNat`.
 example (n : Nat) : N.toNat (N.mk n) = n := rfl
diff --git a/tests/elab/typeDefWithReducibleType.lean b/tests/elab/newtypeWithReducibleType.lean
similarity index 90%
rename from tests/elab/typeDefWithReducibleType.lean
rename to tests/elab/newtypeWithReducibleType.lean
index 988d3c70a490..c31571070365 100644
--- a/tests/elab/typeDefWithReducibleType.lean
+++ b/tests/elab/newtypeWithReducibleType.lean
@@ -1,13 +1,13 @@
 import Lean
 
 /-!
-Tests the `with_reducible_type` tactic combinator: it is the escape hatch for a `type_def`-declared
+Tests the `with_reducible_type` tactic combinator: it is the escape hatch for a `newtype`-declared
 type, temporarily relaxing `N`/`N.mk`/`N.toNat` from `[irreducible]` to `[reducible]` for the
 duration of the tactic block (e.g. to prove `N = Nat`, which requires unfolding `N`'s definition),
 and restores the original `[irreducible]` status afterward.
 -/
 
-type_def N := Nat with toNat
+newtype N := Nat with toNat
 
 -- Inside the block, `N` unfolds to `Nat`.
 example : N = Nat := by with_reducible_type N => rfl
diff --git a/tests/elab/typeDefGrind.lean b/tests/elab/typeDefGrind.lean
deleted file mode 100644
index f582327666c8..000000000000
--- a/tests/elab/typeDefGrind.lean
+++ /dev/null
@@ -1,11 +0,0 @@
-import Lean
-
-/-!
-Confirms `grind` needs no `type_def`-specific special-casing of its own: its simp-based
-normalization (`Lean.Meta.Grind.simpCore`/`dsimpCore`) reuses `Simp.mainCore`/`Simp.reduceStep`,
-which already knows how to reduce virtual projections (see `typeDefVirtualIota.lean`).
--/
-
-type_def N := Nat with toNat
-
-example (n : Nat) : N.toNat (N.mk n) = n := by grind

From 1f6b78f2a3aa6c3b8dbf0d13dbefd972101811be Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Wed, 9 Sep 2026 04:46:19 +0000
Subject: [PATCH 4/5] fixes

---
 src/Lean/Elab/NewType.lean               | 92 ++++++++++++++++++------
 src/Lean/Elab/Tactic/NewType.lean        | 45 ++++++------
 src/Lean/Meta/ExprDefEq.lean             | 23 +++++-
 src/Lean/Meta/VirtualStructure.lean      |  3 +
 src/Lean/Meta/WHNF.lean                  | 19 +++--
 src/Lean/ReducibilityAttrs.lean          |  9 +++
 tests/elab/newtypeModule.lean            | 24 +++++++
 tests/elab/newtypeParams.lean            | 57 +++++++++++++++
 tests/elab/newtypeProjMVar.lean          | 24 +++++++
 tests/elab/newtypeUnsealing.lean         | 48 +++++++++++++
 tests/elab/newtypeVirtualIota.lean       | 11 +++
 tests/elab/newtypeWithReducibleType.lean | 19 -----
 12 files changed, 304 insertions(+), 70 deletions(-)
 create mode 100644 tests/elab/newtypeModule.lean
 create mode 100644 tests/elab/newtypeParams.lean
 create mode 100644 tests/elab/newtypeProjMVar.lean
 create mode 100644 tests/elab/newtypeUnsealing.lean
 delete mode 100644 tests/elab/newtypeWithReducibleType.lean

diff --git a/src/Lean/Elab/NewType.lean b/src/Lean/Elab/NewType.lean
index 61640eb25551..42d9c83c9821 100644
--- a/src/Lean/Elab/NewType.lean
+++ b/src/Lean/Elab/NewType.lean
@@ -7,45 +7,91 @@ module
 
 prelude
 public import Lean.Elab.Command
+public import Lean.Elab.DeclModifiers
+public import Lean.Elab.DeclarationRange
 public import Lean.Meta.VirtualStructure
 
 public section
 
 namespace Lean.Elab.Command
+open Meta
 
 /--
-`newtype N := ty with proj` declares a type `N` definitionally equal to `ty`, together with a
-constructor `N.mk : ty → N` and a projector `N.proj : N → ty`, and marks all three
-`@[irreducible]`:
+`newtype N params := ty with proj` declares a type `N` definitionally equal to `ty`, together with a
+constructor `N.mk` and a projector `N.proj`, and marks all three `@[irreducible]`. For example,
 ```
-@[irreducible] def N := ty
-@[irreducible] def N.mk (a : ty) : N := a
-@[irreducible] def N.proj (n : N) : ty := n
+newtype OrderDual (α : Type u) := α with ofDual
 ```
+produces
+```
+@[irreducible] def OrderDual (α : Type u) := α
+@[irreducible] def OrderDual.mk {α : Type u} (ofDual : α) : OrderDual α := ofDual
+@[irreducible] def OrderDual.ofDual {α : Type u} (self : OrderDual α) : α := self
+```
+Modifiers, parameters, universe parameters, section variables and auto-bound implicits are handled
+exactly as for `def`; as for `structure`, explicit parameters become implicit in the constructor
+and projector.
+
 This is the "irreducible type alias" pattern used to avoid defeq abuse while keeping a
 zero-overhead representation identical to `ty` (e.g. to cast `List ty` to `List N`). Unlike a
 hand-written version of this pattern, `newtype` also registers `N.mk`/`N.proj` as a virtual
-constructor/projector pair, so that `N.proj (N.mk a)` reduces to `a` (see
-`Lean.Meta.reduceVirtualProj?`) even though both stay irreducible otherwise.
+constructor/projector pair, so that `N.proj (N.mk a)` reduces to `a` and `N.mk (N.proj x)` is
+definitionally `x` (see `Lean.Meta.reduceVirtualProj?`), even though `N`, `N.mk` and `N.proj` stay
+irreducible otherwise. Use `unsealing_newtype N => ...` to locally lift the irreducibility.
+-/
+syntax (name := newtypeCmd)
+  declModifiers "newtype " declId bracketedBinder* " := " term " with " ident : command
+
+/--
+Adds the constructor `ctorName` and projector `projName` of the already elaborated `newtype`
+`declName`, whose underlying type is the body of its definition. Reading the parameters off the
+elaborated `declName` (instead of re-elaborating its binders) is what makes section variables,
+auto-bound implicits and universe parameters behave exactly as for `def`.
 -/
-syntax (name := newtypeCmd) "newtype " ident " := " term " with " ident : command
+private def addNewtypeCtorProj (declName ctorName projName fieldName : Name) : TermElabM Nat := do
+  let info ← getConstInfoDefn declName
+  let us := info.levelParams.map mkLevelParam
+  forallTelescope info.type fun params resultType => do
+    unless (← whnf resultType).isSort do
+      throwError "invalid `newtype`, the right-hand side must be a type, but has type{indentExpr resultType}"
+    let underlying := info.value.beta params
+    let self := mkAppN (mkConst declName us) params
+    let implicitParams ← params.filterMapM fun p => do
+      return if (← p.fvarId!.getDecl).binderInfo.isExplicit then some (p.fvarId!, .implicit) else none
+    -- Importers can only reduce `projName (ctorName a)` in the kernel if both bodies are exposed,
+    -- so mirror whatever the `def` elaborator decided for `declName`.
+    let exposed := (← getEnv).hasExposedBody declName
+    withNewBinderInfos implicitParams do
+      let addIdentity (name argName : Name) (argType resultType : Expr) : TermElabM Unit :=
+        withLocalDeclD argName argType fun a => do
+          let type ← mkForallFVars (params.push a) resultType
+          let value ← mkLambdaFVars (params.push a) a
+          let hints := .regular (getMaxHeight (← getEnv) value + 1)
+          let decl := .defnDecl (← mkDefinitionValInferringUnsafe name info.levelParams type value hints)
+          addDecl decl (forceExpose := exposed)
+          compileDecl decl
+      addIdentity ctorName fieldName underlying self
+      addIdentity projName `self self underlying
+    return params.size
 
 @[builtin_command_elab newtypeCmd]
 def elabNewtype : CommandElab
-  | `(newtype $id:ident := $ty:term with $projId:ident) => do
-    let ctorId := mkIdentFrom id (id.getId ++ `mk) (canonical := true)
-    let typeProjId := mkIdentFrom id (id.getId ++ projId.getId) (canonical := true)
-    elabCommand <| ← `(def $id := $ty)
-    elabCommand <| ← `(def $ctorId (a : $ty) : $id := a)
-    elabCommand <| ← `(def $typeProjId (n : $id) : $ty := n)
-    elabCommand <| ← `(attribute [irreducible] $id $ctorId $typeProjId)
-    let ns ← getCurrNamespace
-    let info : VirtualStructureInfo := {
-      typeName := ns ++ id.getId
-      ctorName := ns ++ ctorId.getId
-      projName := ns ++ typeProjId.getId
-    }
-    modifyEnv (registerVirtualStructure · info)
+  | `($mods:declModifiers newtype $declId $params* := $ty with $projId:ident) => do
+    let modifiers ← elabModifiers mods
+    let { declName, .. } ← liftTermElabM <|
+      Term.expandDeclId (← getCurrNamespace) (← getLevelNames) declId modifiers
+    let ctorName := declName ++ `mk
+    let projName := declName ++ projId.getId
+    elabCommand <| ← `($mods:declModifiers def $declId $params* := $ty)
+    let numParams ← liftTermElabM <| addNewtypeCtorProj declName ctorName projName projId.getId
+    addDeclarationRangesFromSyntax ctorName declId
+    addDeclarationRangesFromSyntax projName projId
+    addConstInfo projId projName
+    for n in [declName, ctorName, projName] do
+      setIrreducibleAttribute n
+    modifyEnv (registerVirtualStructure · { typeName := declName, ctorName, projName, numParams })
+    for n in [ctorName, projName] do
+      liftCoreM <| enableRealizationsForConst n
   | _ => throwUnsupportedSyntax
 
 end Lean.Elab.Command
diff --git a/src/Lean/Elab/Tactic/NewType.lean b/src/Lean/Elab/Tactic/NewType.lean
index c9c403432e5a..103831df8c86 100644
--- a/src/Lean/Elab/Tactic/NewType.lean
+++ b/src/Lean/Elab/Tactic/NewType.lean
@@ -14,36 +14,39 @@ public section
 namespace Lean.Parser.Tactic
 
 /--
-`with_reducible_type N => tacs` runs `tacs` with the `newtype`-declared type `N` -- together with
-its auto-generated constructor and projector -- temporarily relaxed from `[irreducible]` to
-`[reducible]`, restoring the original status afterward even if `tacs` fails. This is the escape
-hatch for a `newtype`: within the block, `N`, `N.mk` and its projector unfold like ordinary
-reducible definitions, enabling the `rfl`-style defeq abuse that is disallowed everywhere else.
+`unsealing_newtype N => tacs` runs `tacs` with the `newtype`-declared type `N` -- together with
+its auto-generated constructor and projector -- treated as `[semireducible]` instead of
+`[irreducible]`. This is the escape hatch for a `newtype`: within the block, `N`, `N.mk` and its
+projector unfold like ordinary definitions, e.g. `N = Nat` can be proved by `rfl`.
 -/
-syntax (name := withReducibleType) "with_reducible_type " ident " => " tacticSeq : tactic
+syntax (name := unsealingNewtype) "unsealing_newtype " ident " => " tacticSeq : tactic
 
 end Lean.Parser.Tactic
 
 namespace Lean.Elab.Tactic
+open Meta
 
-/-- Combinator underlying the `with_reducible_type` tactic; see its docstring. -/
-def withReducibleType [Monad m] [MonadEnv m] [MonadFinally m] [MonadResolveName m]
-    [MonadOptions m] [MonadLog m] [AddMessageContext m] [MonadError m]
-    (typeStx : Syntax) (t : m α) : m α := do
-  let typeName ← resolveGlobalConstNoOverload typeStx
-  let some info ← getVirtualStructureInfo? typeName
-    | throwErrorAt typeStx "'{typeName}' is not a `newtype`-declared type"
-  let names := #[info.typeName, info.ctorName, info.projName]
-  let origStatuses ← names.mapM getReducibilityStatus
+/--
+Runs `t` with the declarations `names` treated as `[semireducible]`. The combinator underlying
+the `unsealing_newtype` tactic; see its docstring.
+-/
+def unsealingNewtype [Monad m] [MonadEnv m] [MonadFinally m] (names : Array Name) (t : m α) :
+    m α := do
+  modifyEnv reducibilityExtraExt.pushScope
   for n in names do
-    setReducibilityStatus n .reducible
+    setLocalReducibilityStatus n .semireducible
   try
     t
   finally
-    for (n, s) in names.zip origStatuses do
-      setReducibilityStatus n s
-
-@[builtin_tactic Lean.Parser.Tactic.withReducibleType] def evalWithReducibleType : Tactic :=
-  fun stx => withReducibleType stx[1] (evalTactic stx[3])
+    modifyEnv reducibilityExtraExt.popScope
+
+@[builtin_tactic Lean.Parser.Tactic.unsealingNewtype] def evalUnsealingNewtype : Tactic :=
+  fun stx => do
+    let typeStx := stx[1]
+    let typeName ← resolveGlobalConstNoOverload typeStx
+    let some info ← getVirtualStructureInfo? typeName
+      | throwErrorAt typeStx "'{typeName}' is not a `newtype`-declared type"
+    addConstInfo typeStx typeName
+    unsealingNewtype #[info.typeName, info.ctorName, info.projName] (evalTactic stx[3])
 
 end Lean.Elab.Tactic
diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index 990d9a97f1c5..143d1e674141 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -215,11 +215,12 @@ as a real one-field structure, even though `N`, `N.mk` and `N.toNat` never unfol
 private def isDefEqVirtualEtaStruct (a b : Expr) : MetaM Bool := do
   let .const ctorName us := b.getAppFn | return false
   let some info ← getVirtualCtorInfo? ctorName | return false
-  unless b.getAppNumArgs == 1 do return false
+  unless b.getAppNumArgs == info.numParams + 1 do return false
   if let .const ctorName' _ := a.getAppFn then
     if ctorName' == info.ctorName then return false
   if (← isDefEq (← inferType a) (← inferType b)) then
-    checkpointDefEq <| isDefEq (mkApp (mkConst info.projName us) a) b.appArg!
+    let params := b.getAppArgs.extract 0 info.numParams
+    checkpointDefEq <| isDefEq (mkApp (mkAppN (mkConst info.projName us) params) a) b.appArg!
   else
     return false
 
@@ -2426,10 +2427,28 @@ private def isDefEqAppFallback (t : Expr) (s : Expr) : MetaM Bool := do
       Meta.throwIsDefEqStuck
     return false
 
+/--
+Virtual analog of `isDefEqProj.isDefEqSingleton` for `newtype`-generated projectors: solves
+`projName params (?m ...) =?= v` as `?m ... =?= ctorName params v`.
+-/
+private def isDefEqVirtualProj (t v : Expr) : MetaM Bool := do
+  let .const projName us := t.getAppFn | return false
+  let some info ← getVirtualProjInfo? projName | return false
+  unless t.getAppNumArgs == info.numParams + 1 do return false
+  let s ← whnf (t.getArg! info.numParams)
+  let sFn := s.getAppFn
+  unless sFn.isMVar do return false
+  if (← isAssignable sFn) then
+    let params := t.getAppArgs.extract 0 info.numParams
+    processAssignment' s (mkApp (mkAppN (mkConst info.ctorName us) params) v)
+  else
+    return false
+
 private def isExprDefEqExpensive (t : Expr) (s : Expr) : MetaM Bool := do
   whenUndefDo (isDefEqEta t s) do
   whenUndefDo (isDefEqEta s t) do
   if (← isDefEqProj t s) then return true
+  if (← (isDefEqVirtualProj t s <||> isDefEqVirtualProj s t)) then return true
   let t' ← whnfCore t
   let s' ← whnfCore s
   if t != t' || s != s' then
diff --git a/src/Lean/Meta/VirtualStructure.lean b/src/Lean/Meta/VirtualStructure.lean
index 36524a0b4f3e..f4f90fe036af 100644
--- a/src/Lean/Meta/VirtualStructure.lean
+++ b/src/Lean/Meta/VirtualStructure.lean
@@ -30,6 +30,9 @@ structure VirtualStructureInfo where
   ctorName : Name
   /-- The auto-generated projector, unwrapping a `typeName` value back to the underlying type. -/
   projName : Name
+  /-- The number of parameters of `typeName`. The constructor and projector take them as their
+  leading arguments, followed by the wrapped value resp. the `typeName` value. -/
+  numParams : Nat
   deriving Inhabited, Repr
 
 builtin_initialize virtualStructureTypeExt : MapDeclarationExtension VirtualStructureInfo ←
diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index df6aeacc6321..eea37961275a 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -371,6 +371,12 @@ mutual
               if let some mvarId ← getStuckMVar? (← whnf major) then
                 return mvarId
             return none
+          -- `newtype` projectors behave like `.proj` nodes, which are stuck iff their major is.
+          else if let some projInfo ← getVirtualProjInfo? fName then
+            if let some major := args[projInfo.numParams]? then
+              getStuckMVar? (← whnf major)
+            else
+              return none
           else
             return none
       | .proj _ _ e => getStuckMVar? (← whnf e)
@@ -565,12 +571,15 @@ independent of `ctorName`/`projName`'s reducibility status, even though `newtype
 -/
 def reduceVirtualProj? (e : Expr) : MetaM (Option Expr) := do
   let .const projName _ := e.getAppFn | return none
-  unless e.getAppNumArgs == 1 do return none
   let some projInfo ← getVirtualProjInfo? projName | return none
-  let arg ← whnf e.appArg!
-  let .const ctorName _ := arg.getAppFn | return none
-  unless ctorName == projInfo.ctorName && arg.getAppNumArgs == 1 do return none
-  return some arg.appArg!
+  let args := e.getAppArgs
+  let some majorArg := args[projInfo.numParams]? | return none
+  let major ← whnf majorArg
+  let .const ctorName _ := major.getAppFn | return none
+  unless ctorName == projInfo.ctorName && major.getAppNumArgs == projInfo.numParams + 1 do
+    return none
+  -- The projector may be over-applied if the wrapped value is a function.
+  return some (mkAppN major.appArg! (args.extract (projInfo.numParams + 1)))
 
 /--
   Auxiliary method for reducing terms of the form `?m t_1 ... t_n` where `?m` is delayed assigned.
diff --git a/src/Lean/ReducibilityAttrs.lean b/src/Lean/ReducibilityAttrs.lean
index fe45e3a29c12..f121ed16bf61 100644
--- a/src/Lean/ReducibilityAttrs.lean
+++ b/src/Lean/ReducibilityAttrs.lean
@@ -260,6 +260,15 @@ def getReducibilityStatus [Monad m] [MonadEnv m] (declName : Name) : m Reducibil
 def setReducibilityStatus [MonadEnv m] (declName : Name) (s : ReducibilityStatus) : m Unit :=
   modifyEnv fun env => setReducibilityStatusCore env declName s .global .anonymous
 
+/--
+Sets the reducibility attribute for the given declaration until the end of the current scope
+(as in `attribute [local ...]`). Unlike `setReducibilityStatus`, this may be used from within the
+asynchronous elaboration of a declaration since the change is not propagated to other
+environment branches.
+-/
+def setLocalReducibilityStatus [MonadEnv m] (declName : Name) (s : ReducibilityStatus) : m Unit :=
+  modifyEnv fun env => setReducibilityStatusCore env declName s .local .anonymous
+
 /-- Set the given declaration as `[reducible]` -/
 def setReducibleAttribute [MonadEnv m] (declName : Name) : m Unit :=
   setReducibilityStatus declName ReducibilityStatus.reducible
diff --git a/tests/elab/newtypeModule.lean b/tests/elab/newtypeModule.lean
new file mode 100644
index 000000000000..0b46fd0a20dc
--- /dev/null
+++ b/tests/elab/newtypeModule.lean
@@ -0,0 +1,24 @@
+module
+
+public meta import Lean
+
+/-!
+Tests `newtype` under the module system: whether the bodies of the generated constructor and
+projector are exposed to importing modules follows whatever the `def` elaborator decided for the
+type itself, since importers can only reduce `N.proj (N.mk a)` in the kernel if all three bodies are
+visible.
+-/
+
+@[expose] public newtype Exposed := Nat with toNat
+newtype Priv := Nat with toNat
+
+open Lean in
+run_meta do
+  let env ← getEnv
+  for n in [``Exposed, ``Exposed.mk, ``Exposed.toNat] do
+    unless env.hasExposedBody n do throwError "expected {n} to be exposed"
+  for n in [``Priv, ``Priv.mk, ``Priv.toNat] do
+    if env.hasExposedBody n then throwError "expected {n} not to be exposed"
+
+example (n : Nat) : Exposed.toNat (Exposed.mk n) = n := rfl
+example (x : Priv) : Priv.mk (Priv.toNat x) = x := rfl
diff --git a/tests/elab/newtypeParams.lean b/tests/elab/newtypeParams.lean
new file mode 100644
index 000000000000..22062c4a36b8
--- /dev/null
+++ b/tests/elab/newtypeParams.lean
@@ -0,0 +1,57 @@
+import Lean
+
+/-!
+Tests that `newtype` handles parameters exactly like `def`: explicit binders, universe parameters,
+section variables and auto-bound implicits. As for `structure`, explicit parameters become implicit
+in the generated constructor and projector, and virtual iota/eta as well as `unsealing_newtype`
+work in the presence of parameters.
+-/
+
+universe u
+
+newtype OrderDual (α : Type u) := α with ofDual
+
+/-- info: OrderDual.{u} (α : Type u) : Type u -/
+#guard_msgs in #check OrderDual
+/-- info: OrderDual.mk.{u} {α : Type u} (ofDual : α) : OrderDual α -/
+#guard_msgs in #check OrderDual.mk
+/-- info: OrderDual.ofDual.{u} {α : Type u} (self : OrderDual α) : α -/
+#guard_msgs in #check OrderDual.ofDual
+
+example (a : α) : OrderDual.ofDual (OrderDual.mk a) = a := rfl
+example (x : OrderDual α) : OrderDual.mk (OrderDual.ofDual x) = x := rfl
+example (a : α) : (OrderDual.mk a).ofDual = a := by simp only
+example : OrderDual α = α := by unsealing_newtype OrderDual => rfl
+
+section
+variable (β : Type) [Inhabited β]
+
+newtype Wrap := List β with toList
+
+/-- info: Wrap (β : Type) : Type -/
+#guard_msgs in #check Wrap
+/-- info: Wrap.mk {β : Type} (toList : List β) : Wrap β -/
+#guard_msgs in #check Wrap.mk
+
+-- The unused instance variable is not included, as for `def`.
+example (l : List β) : (Wrap.mk l).toList = l := rfl
+end
+
+-- Auto-bound universe levels in the binders, as for `def`.
+newtype Wrap' (γ : Type _) := Option γ with get
+
+/-- info: Wrap'.{u_1} (γ : Type u_1) : Type u_1 -/
+#guard_msgs in #check Wrap'
+/-- info: Wrap'.mk.{u_1} {γ : Type u_1} (get : Option γ) : Wrap' γ -/
+#guard_msgs in #check Wrap'.mk
+
+example (o : Option γ) : (Wrap'.mk o).get = o := rfl
+
+/-- doc -/
+private newtype Priv (n : Nat) := Fin n with val
+
+example (i : Fin 3) : (Priv.mk i).val = i := rfl
+
+/-- error: invalid `newtype`, the right-hand side must be a type, but has type
+  Nat -/
+#guard_msgs in newtype Bad := 5 with val
diff --git a/tests/elab/newtypeProjMVar.lean b/tests/elab/newtypeProjMVar.lean
new file mode 100644
index 000000000000..616eccba289c
--- /dev/null
+++ b/tests/elab/newtypeProjMVar.lean
@@ -0,0 +1,24 @@
+import Lean
+
+/-!
+Tests that a metavariable of a `newtype`-declared type can be assigned from a constraint on its
+projection, as for real single-field structures (`isDefEqProj.isDefEqSingleton`): `N.val ?m =?= v`
+is solved by `?m := N.mk v`.
+-/
+
+newtype N (α : Type) := α with val
+
+example (x : α) : ∃ y : N α, y.val = x := ⟨_, rfl⟩
+
+namespace N
+instance [OfNat α 1] : OfNat (N α) 1 := ⟨mk 1⟩
+theorem val_inj {a b : N α} : a.val = b.val ↔ a = b :=
+  ⟨fun h => congrArg mk h, fun h => congrArg val h⟩
+example [OfNat α 1] {a : N α} : a.val = 1 ↔ a = 1 := val_inj (b := 1)
+end N
+
+-- Without parameters.
+newtype M := Nat with toNat
+
+example : ∃ y : M, y.toNat = 5 := ⟨_, rfl⟩
+example : ∃ y : M, 5 = y.toNat := ⟨_, rfl⟩
diff --git a/tests/elab/newtypeUnsealing.lean b/tests/elab/newtypeUnsealing.lean
new file mode 100644
index 000000000000..b88401c0e97c
--- /dev/null
+++ b/tests/elab/newtypeUnsealing.lean
@@ -0,0 +1,48 @@
+import Lean
+
+/-!
+Tests the `unsealing_newtype` tactic combinator: it is the escape hatch for a `newtype`-declared
+type, temporarily relaxing `N`/`N.mk`/`N.toNat` from `[irreducible]` to `[semireducible]` for the
+duration of the tactic block (e.g. to prove `N = Nat`, which requires unfolding `N`'s definition),
+and restores the original `[irreducible]` status afterward.
+-/
+
+newtype N := Nat with toNat
+
+-- Inside the block, `N` unfolds to `Nat`.
+example : N = Nat := by unsealing_newtype N => rfl
+
+-- Also inside a named theorem, whose proof is elaborated asynchronously in a separate environment
+-- branch (which must not modify the global reducibility status).
+theorem foo : N = Nat := by unsealing_newtype N => rfl
+
+-- `N` is only `[semireducible]`, so it does not unfold at reducible transparency.
+theorem foo' : N = Nat := by
+  unsealing_newtype N =>
+    fail_if_success with_reducible rfl
+    rfl
+
+-- `simp`/`unfold` may unfold the definitions inside the block.
+example (n : Nat) : N.toNat (N.mk n) = n := by
+  unsealing_newtype N => simp only [N.toNat, N.mk]
+example (x : N) : N.mk x.toNat = x := by
+  unsealing_newtype N =>
+    unfold N.toNat N.mk
+    rfl
+
+-- After the block, the status is restored even within the same proof.
+example : N = Nat ∧ N = Nat := by
+  constructor
+  · unsealing_newtype N => rfl
+  · fail_if_success rfl
+    unsealing_newtype N => rfl
+
+/-- error: 'Nat' is not a `newtype`-declared type -/
+#guard_msgs in
+example : Nat = Nat := by unsealing_newtype Nat => rfl
+
+-- Outside the block, `N` is irreducible again: this still fails.
+/-- but is expected to have type
+  N = Nat -/
+#guard_msgs (substring := true) in
+example : N = Nat := rfl
diff --git a/tests/elab/newtypeVirtualIota.lean b/tests/elab/newtypeVirtualIota.lean
index de6b6c577e9a..09da6c60d2da 100644
--- a/tests/elab/newtypeVirtualIota.lean
+++ b/tests/elab/newtypeVirtualIota.lean
@@ -12,6 +12,17 @@ newtype N := Nat with toNat
 -- Virtual iota: projector-of-constructor reduces by `rfl`, without unfolding `N`/`N.mk`/`N.toNat`.
 example (n : Nat) : N.toNat (N.mk n) = n := rfl
 
+-- Over-applied projector, when the wrapped value is a function.
+newtype F := Nat → Nat with get
+newtype G (α : Type) := α → α → α with get
+
+example (f : Nat → Nat) (x : Nat) : (F.mk f).get x = f x := rfl
+example (f : Nat → Nat) (x : Nat) : (F.mk f).get x = f x := by simp only
+example (f : Nat → Nat) (x : Nat) : (F.mk f).get x = f x := by dsimp only
+example (f : α → α → α) (x y : α) : (G.mk f).get x y = f x y := rfl
+example (f : α → α → α) (x y : α) : (G.mk f).get x y = f x y := by simp only
+example (f : Nat → Nat) : (F.mk f).get = f := rfl
+
 -- `N` stays irreducible outside of the virtual iota pattern: it does not unify with `Nat`.
 /-- error: Type mismatch
   n
diff --git a/tests/elab/newtypeWithReducibleType.lean b/tests/elab/newtypeWithReducibleType.lean
deleted file mode 100644
index c31571070365..000000000000
--- a/tests/elab/newtypeWithReducibleType.lean
+++ /dev/null
@@ -1,19 +0,0 @@
-import Lean
-
-/-!
-Tests the `with_reducible_type` tactic combinator: it is the escape hatch for a `newtype`-declared
-type, temporarily relaxing `N`/`N.mk`/`N.toNat` from `[irreducible]` to `[reducible]` for the
-duration of the tactic block (e.g. to prove `N = Nat`, which requires unfolding `N`'s definition),
-and restores the original `[irreducible]` status afterward.
--/
-
-newtype N := Nat with toNat
-
--- Inside the block, `N` unfolds to `Nat`.
-example : N = Nat := by with_reducible_type N => rfl
-
--- Outside the block, `N` is irreducible again: this still fails.
-/-- but is expected to have type
-  N = Nat -/
-#guard_msgs (substring := true) in
-example : N = Nat := rfl

From c1d7ba081f44b39994e451e293cbc7df5f0bb5ad Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Wed, 9 Sep 2026 07:36:13 +0000
Subject: [PATCH 5/5] fixes, (reducibility := _)

---
 src/Init/NotationExtra.lean        | 26 ++++++++++++++++++++
 src/Init/Tactics.lean              | 33 ++++++++++++++++++++++++++
 src/Lean/Elab/NewType.lean         | 28 +---------------------
 src/Lean/Elab/Tactic/NewType.lean  | 38 +++++++++++++++---------------
 tests/elab/newtypeUnsealing.lean   | 18 ++++++++++++--
 tests/elab/newtypeVirtualIota.lean |  2 --
 6 files changed, 95 insertions(+), 50 deletions(-)

diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean
index 403cc1578424..3c42230a0edf 100644
--- a/src/Init/NotationExtra.lean
+++ b/src/Init/NotationExtra.lean
@@ -316,6 +316,32 @@ macro_rules
     `($mods:declModifiers class $id $params* $[: $ty:term]? extends $[$parents:term],*
       attribute [instance] $ctor)
 
+/--
+`newtype N params := ty with proj` declares a type `N` definitionally equal to `ty`, together with a
+constructor `N.mk` and a projector `N.proj`, and marks all three `@[irreducible]`. For example,
+```
+newtype OrderDual (α : Type u) := α with ofDual
+```
+produces
+```
+@[irreducible] def OrderDual (α : Type u) := α
+@[irreducible] def OrderDual.mk {α : Type u} (ofDual : α) : OrderDual α := ofDual
+@[irreducible] def OrderDual.ofDual {α : Type u} (self : OrderDual α) : α := self
+```
+Modifiers, parameters, universe parameters, section variables and auto-bound implicits are handled
+exactly as for `def`; as for `structure`, explicit parameters become implicit in the constructor
+and projector.
+
+This is the "irreducible type alias" pattern used to avoid defeq abuse while keeping a
+zero-overhead representation identical to `ty` (e.g. to cast `List ty` to `List N`). Unlike a
+hand-written version of this pattern, `newtype` also registers `N.mk`/`N.proj` as a virtual
+constructor/projector pair, so that `N.proj (N.mk a)` reduces to `a` and `N.mk (N.proj x)` is
+definitionally `x` (see `Lean.Meta.reduceVirtualProj?`), even though `N`, `N.mk` and `N.proj` stay
+irreducible otherwise. Use `unsealing_newtype N => ...` to locally lift the irreducibility.
+-/
+syntax (name := Lean.Parser.Command.newtypeCmd)
+  declModifiers "newtype " declId bracketedBinder* " := " term " with " ident : command
+
 namespace Lean
 syntax cdotTk := unicode("· ", ". ")
 /-- `· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. -/
diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index 4cd586b2368c..1235c9f61f55 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -1810,6 +1810,39 @@ a lemma from the list until it gets stuck.
 syntax (name := applyRules) "apply_rules" optConfig (&" only")? (args)? (using_)? : tactic
 end SolveByElim
 
+/--
+The reducibility status that `unsealing_newtype` temporarily assigns to a `newtype`-declared
+type, its constructor and its projector. Mirrors `Lean.ReducibilityStatus` without `irreducible`.
+-/
+inductive UnsealingNewtypeReducibility where
+  /-- Unfolded at reducible transparency and above. -/
+  | reducible
+  /-- Unfolded at instances transparency and above. -/
+  | instanceReducible
+  /-- Unfolded at implicit transparency and above. -/
+  | implicitReducible
+  /-- Unfolded at default transparency and above, like an ordinary definition. -/
+  | semireducible
+
+/--
+Configuration for the `unsealing_newtype` tactic.
+-/
+structure UnsealingNewtypeConfig where
+  /-- The reducibility status to use within the tactic block (default: `.semireducible`). -/
+  reducibility : UnsealingNewtypeReducibility := .semireducible
+
+/--
+`unsealing_newtype N => tacs` runs `tacs` with the `newtype`-declared type `N` -- together with
+its auto-generated constructor and projector -- treated as `[semireducible]` instead of
+`[irreducible]`. This is the escape hatch for a `newtype`: within the block, `N`, `N.mk` and its
+projector unfold like ordinary definitions, e.g. `N = Nat` can be proved by `rfl`.
+
+`unsealing_newtype (reducibility := .instanceReducible) N => tacs` uses the given reducibility
+status instead; see `UnsealingNewtypeReducibility`.
+-/
+syntax (name := unsealingNewtype)
+  "unsealing_newtype " optConfig ident " => " tacticSeq : tactic
+
 /--
 Configuration for the `exact?` and `apply?` tactics.
 -/
diff --git a/src/Lean/Elab/NewType.lean b/src/Lean/Elab/NewType.lean
index 42d9c83c9821..cac865ea2404 100644
--- a/src/Lean/Elab/NewType.lean
+++ b/src/Lean/Elab/NewType.lean
@@ -16,32 +16,6 @@ public section
 namespace Lean.Elab.Command
 open Meta
 
-/--
-`newtype N params := ty with proj` declares a type `N` definitionally equal to `ty`, together with a
-constructor `N.mk` and a projector `N.proj`, and marks all three `@[irreducible]`. For example,
-```
-newtype OrderDual (α : Type u) := α with ofDual
-```
-produces
-```
-@[irreducible] def OrderDual (α : Type u) := α
-@[irreducible] def OrderDual.mk {α : Type u} (ofDual : α) : OrderDual α := ofDual
-@[irreducible] def OrderDual.ofDual {α : Type u} (self : OrderDual α) : α := self
-```
-Modifiers, parameters, universe parameters, section variables and auto-bound implicits are handled
-exactly as for `def`; as for `structure`, explicit parameters become implicit in the constructor
-and projector.
-
-This is the "irreducible type alias" pattern used to avoid defeq abuse while keeping a
-zero-overhead representation identical to `ty` (e.g. to cast `List ty` to `List N`). Unlike a
-hand-written version of this pattern, `newtype` also registers `N.mk`/`N.proj` as a virtual
-constructor/projector pair, so that `N.proj (N.mk a)` reduces to `a` and `N.mk (N.proj x)` is
-definitionally `x` (see `Lean.Meta.reduceVirtualProj?`), even though `N`, `N.mk` and `N.proj` stay
-irreducible otherwise. Use `unsealing_newtype N => ...` to locally lift the irreducibility.
--/
-syntax (name := newtypeCmd)
-  declModifiers "newtype " declId bracketedBinder* " := " term " with " ident : command
-
 /--
 Adds the constructor `ctorName` and projector `projName` of the already elaborated `newtype`
 `declName`, whose underlying type is the body of its definition. Reading the parameters off the
@@ -74,7 +48,7 @@ private def addNewtypeCtorProj (declName ctorName projName fieldName : Name) : T
       addIdentity projName `self self underlying
     return params.size
 
-@[builtin_command_elab newtypeCmd]
+@[builtin_command_elab Lean.Parser.Command.newtypeCmd]
 def elabNewtype : CommandElab
   | `($mods:declModifiers newtype $declId $params* := $ty with $projId:ident) => do
     let modifiers ← elabModifiers mods
diff --git a/src/Lean/Elab/Tactic/NewType.lean b/src/Lean/Elab/Tactic/NewType.lean
index 103831df8c86..8f4e4e9606ab 100644
--- a/src/Lean/Elab/Tactic/NewType.lean
+++ b/src/Lean/Elab/Tactic/NewType.lean
@@ -8,45 +8,45 @@ module
 prelude
 public import Lean.Elab.Tactic.Basic
 public import Lean.Meta.VirtualStructure
+import Lean.Elab.Tactic.Config
 
 public section
 
-namespace Lean.Parser.Tactic
-
-/--
-`unsealing_newtype N => tacs` runs `tacs` with the `newtype`-declared type `N` -- together with
-its auto-generated constructor and projector -- treated as `[semireducible]` instead of
-`[irreducible]`. This is the escape hatch for a `newtype`: within the block, `N`, `N.mk` and its
-projector unfold like ordinary definitions, e.g. `N = Nat` can be proved by `rfl`.
--/
-syntax (name := unsealingNewtype) "unsealing_newtype " ident " => " tacticSeq : tactic
-
-end Lean.Parser.Tactic
-
 namespace Lean.Elab.Tactic
 open Meta
 
 /--
-Runs `t` with the declarations `names` treated as `[semireducible]`. The combinator underlying
-the `unsealing_newtype` tactic; see its docstring.
+Runs `t` with the declarations `names` treated as having reducibility status `status`. The
+combinator underlying the `unsealing_newtype` tactic; see its docstring.
 -/
-def unsealingNewtype [Monad m] [MonadEnv m] [MonadFinally m] (names : Array Name) (t : m α) :
-    m α := do
+def unsealingNewtype [Monad m] [MonadEnv m] [MonadFinally m] (names : Array Name)
+    (status : ReducibilityStatus := .semireducible) (t : m α) : m α := do
   modifyEnv reducibilityExtraExt.pushScope
   for n in names do
-    setLocalReducibilityStatus n .semireducible
+    setLocalReducibilityStatus n status
   try
     t
   finally
     modifyEnv reducibilityExtraExt.popScope
 
+declare_config_elab elabUnsealingNewtypeConfig Parser.Tactic.UnsealingNewtypeConfig
+
+def _root_.Lean.Parser.Tactic.UnsealingNewtypeReducibility.toReducibilityStatus :
+    Parser.Tactic.UnsealingNewtypeReducibility → ReducibilityStatus
+  | .reducible => .reducible
+  | .instanceReducible => .instanceReducible
+  | .implicitReducible => .implicitReducible
+  | .semireducible => .semireducible
+
 @[builtin_tactic Lean.Parser.Tactic.unsealingNewtype] def evalUnsealingNewtype : Tactic :=
   fun stx => do
-    let typeStx := stx[1]
+    let cfg ← elabUnsealingNewtypeConfig stx[1]
+    let typeStx := stx[2]
     let typeName ← resolveGlobalConstNoOverload typeStx
     let some info ← getVirtualStructureInfo? typeName
       | throwErrorAt typeStx "'{typeName}' is not a `newtype`-declared type"
     addConstInfo typeStx typeName
-    unsealingNewtype #[info.typeName, info.ctorName, info.projName] (evalTactic stx[3])
+    unsealingNewtype #[info.typeName, info.ctorName, info.projName]
+      cfg.reducibility.toReducibilityStatus (evalTactic stx[4])
 
 end Lean.Elab.Tactic
diff --git a/tests/elab/newtypeUnsealing.lean b/tests/elab/newtypeUnsealing.lean
index b88401c0e97c..e96668735d90 100644
--- a/tests/elab/newtypeUnsealing.lean
+++ b/tests/elab/newtypeUnsealing.lean
@@ -1,5 +1,3 @@
-import Lean
-
 /-!
 Tests the `unsealing_newtype` tactic combinator: it is the escape hatch for a `newtype`-declared
 type, temporarily relaxing `N`/`N.mk`/`N.toNat` from `[irreducible]` to `[semireducible]` for the
@@ -22,6 +20,22 @@ theorem foo' : N = Nat := by
     fail_if_success with_reducible rfl
     rfl
 
+-- The reducibility status can be chosen via the `reducibility` option.
+example : N = Nat := by
+  unsealing_newtype (reducibility := .reducible) N => with_reducible rfl
+example : N = Nat := by
+  unsealing_newtype (reducibility := .instanceReducible) N =>
+    fail_if_success with_reducible rfl
+    with_reducible_and_instances rfl
+example : N = Nat := by
+  unsealing_newtype (reducibility := .implicitReducible) N =>
+    fail_if_success with_reducible_and_instances rfl
+    with_implicit rfl
+example : N = Nat := by
+  unsealing_newtype (reducibility := .semireducible) N =>
+    fail_if_success with_reducible rfl
+    rfl
+
 -- `simp`/`unfold` may unfold the definitions inside the block.
 example (n : Nat) : N.toNat (N.mk n) = n := by
   unsealing_newtype N => simp only [N.toNat, N.mk]
diff --git a/tests/elab/newtypeVirtualIota.lean b/tests/elab/newtypeVirtualIota.lean
index 09da6c60d2da..2749de0ad0a5 100644
--- a/tests/elab/newtypeVirtualIota.lean
+++ b/tests/elab/newtypeVirtualIota.lean
@@ -1,5 +1,3 @@
-import Lean
-
 /-!
 Tests the `newtype` command. It generates an irreducible type alias together with a
 constructor/projector pair (`N`, `N.mk`, `N.toNat`), and registers the pair as a "virtual