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.lean b/src/Lean/Elab.lean
index 2f770dd2a098..70c0f0b9096e 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.NewType
 public import Lean.Elab.PreDefinition
 public import Lean.Elab.Deriving
 public import Lean.Elab.DeclarationRange
diff --git a/src/Lean/Elab/NewType.lean b/src/Lean/Elab/NewType.lean
new file mode 100644
index 000000000000..cac865ea2404
--- /dev/null
+++ b/src/Lean/Elab/NewType.lean
@@ -0,0 +1,71 @@
+/-
+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.Elab.DeclModifiers
+public import Lean.Elab.DeclarationRange
+public import Lean.Meta.VirtualStructure
+
+public section
+
+namespace Lean.Elab.Command
+open Meta
+
+/--
+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`.
+-/
+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 Lean.Parser.Command.newtypeCmd]
+def elabNewtype : CommandElab
+  | `($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.lean b/src/Lean/Elab/Tactic.lean
index 4c08c9fabcff..79f5ddbdda64 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.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/NewType.lean b/src/Lean/Elab/Tactic/NewType.lean
new file mode 100644
index 000000000000..8f4e4e9606ab
--- /dev/null
+++ b/src/Lean/Elab/Tactic/NewType.lean
@@ -0,0 +1,52 @@
+/-
+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
+import Lean.Elab.Tactic.Config
+
+public section
+
+namespace Lean.Elab.Tactic
+open Meta
+
+/--
+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)
+    (status : ReducibilityStatus := .semireducible) (t : m α) : m α := do
+  modifyEnv reducibilityExtraExt.pushScope
+  for n in names do
+    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 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]
+      cfg.reducibility.toReducibilityStatus (evalTactic stx[4])
+
+end Lean.Elab.Tactic
diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index 3bc3e69ab997..143d1e674141 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -204,6 +204,26 @@ where
       else
         return false
 
+/--
+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 `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
+  let .const ctorName us := b.getAppFn | return false
+  let some info ← getVirtualCtorInfo? ctorName | 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
+    let params := b.getAppArgs.extract 0 info.numParams
+    checkpointDefEq <| isDefEq (mkApp (mkAppN (mkConst info.projName us) params) 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`).
@@ -2407,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
@@ -2425,6 +2463,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/VirtualStructure.lean b/src/Lean/Meta/VirtualStructure.lean
new file mode 100644
index 000000000000..f4f90fe036af
--- /dev/null
+++ b/src/Lean/Meta/VirtualStructure.lean
@@ -0,0 +1,80 @@
+/-
+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 `newtype` command for a declaration such as
+```
+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
+`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 `newtype`-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
+  /-- 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 ←
+  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 `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 `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 `newtype`, 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/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index a395af246ba0..eea37961275a 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
@@ -370,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)
@@ -553,6 +560,27 @@ 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 `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 `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
+  let .const projName _ := e.getAppFn | return none
+  let some projInfo ← getVirtualProjInfo? projName | return none
+  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.
   Recall that we can only expand a delayed assignment when all holes/metavariables in the assigned value have been "filled".
@@ -655,6 +683,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
+          -- `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
+              return ← go eNew
           unless cfg.iota do return e
           match (← reduceMatcher? e) with
           | .reduced eNew => go eNew
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/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/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..e96668735d90
--- /dev/null
+++ b/tests/elab/newtypeUnsealing.lean
@@ -0,0 +1,62 @@
+/-!
+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
+
+-- 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]
+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/newtypeVirtualEta.lean b/tests/elab/newtypeVirtualEta.lean
new file mode 100644
index 000000000000..9b49f453c9ff
--- /dev/null
+++ b/tests/elab/newtypeVirtualEta.lean
@@ -0,0 +1,17 @@
+import Lean
+
+/-!
+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`).
+-/
+
+newtype 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/newtypeVirtualIota.lean b/tests/elab/newtypeVirtualIota.lean
new file mode 100644
index 000000000000..2749de0ad0a5
--- /dev/null
+++ b/tests/elab/newtypeVirtualIota.lean
@@ -0,0 +1,32 @@
+/-!
+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).
+-/
+
+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
+has type
+  Nat
+but is expected to have type
+  N -/
+#guard_msgs in
+example (n : Nat) : N := n