diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index e88606a4acb4..865fb8f96bd0 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -8,6 +8,14 @@ import Init.Notation
 set_option linter.missingDocs true -- keep it documented
 
 namespace Lean.Parser.Tactic
+
+/--
+`as_aux_lemma => tac` does the same as `tac`, except that it wraps the resulting expression
+into an auxiliary lemma. In some cases, this significantly reduces the size of expressions
+because the proof term is not duplicated.
+-/
+syntax (name := as_aux_lemma) "as_aux_lemma" " => " tacticSeq : tactic
+
 /--
 `with_annotate_state stx t` annotates the lexical range of `stx : Syntax` with
 the initial and final state of running tactic `t`.
diff --git a/src/Lean/Elab/Tactic.lean b/src/Lean/Elab/Tactic.lean
index 31e99106a5c9..80bb56a321c0 100644
--- a/src/Lean/Elab/Tactic.lean
+++ b/src/Lean/Elab/Tactic.lean
@@ -47,3 +47,5 @@ import Lean.Elab.Tactic.Classical
 import Lean.Elab.Tactic.Grind
 import Lean.Elab.Tactic.Monotonicity
 import Lean.Elab.Tactic.Try
+import Lean.Elab.Tactic.AsAuxLemma
+import Lean.Elab.Tactic.TreeTacAttr
diff --git a/src/Lean/Elab/Tactic/AsAuxLemma.lean b/src/Lean/Elab/Tactic/AsAuxLemma.lean
new file mode 100644
index 000000000000..6d6c81d5bbc1
--- /dev/null
+++ b/src/Lean/Elab/Tactic/AsAuxLemma.lean
@@ -0,0 +1,26 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joachim Breitner
+-/
+prelude
+import Init.Tactics
+import Lean.Elab.Tactic.Basic
+import Lean.Elab.Tactic.Meta
+import Lean.MetavarContext
+import Lean.Meta.Closure
+
+open Lean Meta Elab Tactic Parser.Tactic
+
+@[builtin_tactic as_aux_lemma]
+def elabAsAuxLemma : Lean.Elab.Tactic.Tactic
+| `(tactic| as_aux_lemma => $s) =>
+  liftMetaTactic fun mvarId => do
+    let (mvars, _) ← runTactic mvarId s
+    unless mvars.isEmpty do
+      throwError "Cannot abstract term into auxiliary lemma because there are open goals."
+    let e ← instantiateMVars (mkMVar mvarId)
+    let e ← mkAuxTheorem (`Lean.Elab.Tactic.AsAuxLemma ++ (← mkFreshUserName `auxLemma)) (← mvarId.getType) e
+    mvarId.assign e
+    return []
+| _ => throwError "Invalid as_aux_lemma syntax"
diff --git a/src/Lean/Elab/Tactic/TreeTacAttr.lean b/src/Lean/Elab/Tactic/TreeTacAttr.lean
new file mode 100644
index 000000000000..2a31c9d3d206
--- /dev/null
+++ b/src/Lean/Elab/Tactic/TreeTacAttr.lean
@@ -0,0 +1,12 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+prelude
+import Lean.Meta.Tactic.Simp
+
+open Lean.Meta
+
+builtin_initialize treeTacExt : SimpExtension
+  ← registerSimpAttr `Std.Internal.tree_tac "simp theorems used by internal DTreeMap lemmas"
diff --git a/tests/lean/run/as_aux_lemma.lean b/tests/lean/run/as_aux_lemma.lean
new file mode 100644
index 000000000000..0dd9dc05b68e
--- /dev/null
+++ b/tests/lean/run/as_aux_lemma.lean
@@ -0,0 +1,47 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+import Lean.Environment
+import Lean.Meta.Basic
+import Lean.Util.NumObjs
+
+open Lean Meta
+
+abbrev testProp := ∀ n : Nat, n = 0 + n
+
+def thmUsingTactic : testProp := by as_aux_lemma =>
+  intro n
+  induction n
+  · rfl
+  · next ih =>
+    rw [← Nat.succ_eq_add_one, Nat.add_succ, ← ih]
+
+def thmWithoutTactic : testProp := by
+  intro n
+  induction n
+  · rfl
+  · next ih =>
+    rw [← Nat.succ_eq_add_one, Nat.add_succ, ← ih]
+
+open Lean
+
+def size (name : Name) : MetaM Nat := do
+  let env ← getEnv
+  let mut totalSize : Nat := 0
+  for (constantName, info) in env.constants do
+    if name = constantName then
+      if let some e := info.value? then
+        let numObjs ← e.numObjs
+        totalSize := totalSize + numObjs
+  return totalSize
+
+/--
+info: as_aux_lemma makes proof term smaller : true
+-/
+#guard_msgs in
+run_meta do
+  let sizeUsingTactic ← size `thmUsingTactic
+  let sizeWithoutTactic ← size `thmWithoutTactic
+  logInfo m!"as_aux_lemma makes proof term smaller : {decide <| sizeUsingTactic < sizeWithoutTactic}"