From 3234792696da100b254a447a819335dbdd1a934e Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Tue, 28 Jan 2025 17:50:39 +0100
Subject: [PATCH 1/9] code to bootstrap

---
 src/Init/Tactics.lean                 |  8 ++++++++
 src/Lean/Elab/Tactic.lean             |  2 ++
 src/Lean/Elab/Tactic/AsAuxLemma.lean  | 26 ++++++++++++++++++++++++++
 src/Lean/Elab/Tactic/TreeTacAttr.lean |  7 +++++++
 4 files changed, 43 insertions(+)
 create mode 100644 src/Lean/Elab/Tactic/AsAuxLemma.lean
 create mode 100644 src/Lean/Elab/Tactic/TreeTacAttr.lean

diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index e88606a4acb4..acc8781d2c2c 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.
+-/
+scoped 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 add9aea409c2..eb516c428617 100644
--- a/src/Lean/Elab/Tactic.lean
+++ b/src/Lean/Elab/Tactic.lean
@@ -46,3 +46,5 @@ import Lean.Elab.Tactic.BoolToPropSimps
 import Lean.Elab.Tactic.Classical
 import Lean.Elab.Tactic.Grind
 import Lean.Elab.Tactic.Monotonicity
+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..7a4f6e0ee063
--- /dev/null
+++ b/src/Lean/Elab/Tactic/AsAuxLemma.lean
@@ -0,0 +1,26 @@
+/-
+Copyright (c) 2022 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+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 "Left-over goals, cannot abstract"
+    let e ← instantiateMVars (mkMVar mvarId)
+    let e ← mkAuxTheorem (`Std.DTreeMap.Internal.Impl ++ (← mkFreshUserName `test)) (← 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..821a82878121
--- /dev/null
+++ b/src/Lean/Elab/Tactic/TreeTacAttr.lean
@@ -0,0 +1,7 @@
+prelude
+import Lean.Meta.Tactic.Simp
+
+open Lean Elab Tactic Meta
+
+builtin_initialize treeTacExt : Meta.SimpExtension
+  ← Meta.registerSimpAttr `Std.Internal.tree_tac "simp theorems used by internal DTreeMap lemmas"

From a12244e4d3501b80c657ffd6f2cffc767ed3a1bd Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Tue, 28 Jan 2025 18:24:22 +0100
Subject: [PATCH 2/9] cleanup

---
 src/Lean/Elab/Tactic/TreeTacAttr.lean | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Elab/Tactic/TreeTacAttr.lean b/src/Lean/Elab/Tactic/TreeTacAttr.lean
index 821a82878121..f3ef0d730bd1 100644
--- a/src/Lean/Elab/Tactic/TreeTacAttr.lean
+++ b/src/Lean/Elab/Tactic/TreeTacAttr.lean
@@ -1,7 +1,12 @@
+/-
+Copyright (c) 2022 Microsoft Corporation. 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 Elab Tactic Meta
+open Lean.Meta
 
-builtin_initialize treeTacExt : Meta.SimpExtension
-  ← Meta.registerSimpAttr `Std.Internal.tree_tac "simp theorems used by internal DTreeMap lemmas"
+builtin_initialize treeTacExt : SimpExtension
+  ← registerSimpAttr `Std.Internal.tree_tac "simp theorems used by internal DTreeMap lemmas"

From 68343f8ec28ea5356fdf45c92ae6e3384e915a32 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Wed, 29 Jan 2025 08:27:35 +0100
Subject: [PATCH 3/9] apply suggestions

---
 src/Lean/Elab/Tactic/AsAuxLemma.lean  | 6 +++---
 src/Lean/Elab/Tactic/TreeTacAttr.lean | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Elab/Tactic/AsAuxLemma.lean b/src/Lean/Elab/Tactic/AsAuxLemma.lean
index 7a4f6e0ee063..1ff65d87ffaf 100644
--- a/src/Lean/Elab/Tactic/AsAuxLemma.lean
+++ b/src/Lean/Elab/Tactic/AsAuxLemma.lean
@@ -1,7 +1,7 @@
 /-
-Copyright (c) 2022 Microsoft Corporation. All rights reserved.
+Copyright (c) Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Paul Reichert
+Authors: Joachim Breitner
 -/
 prelude
 import Init.Tactics
@@ -20,7 +20,7 @@ def elabAsAuxLemma : Lean.Elab.Tactic.Tactic
     unless mvars.isEmpty do
       throwError "Left-over goals, cannot abstract"
     let e ← instantiateMVars (mkMVar mvarId)
-    let e ← mkAuxTheorem (`Std.DTreeMap.Internal.Impl ++ (← mkFreshUserName `test)) (← mvarId.getType) e
+    let e ← mkAuxTheorem (`Std.Internal.AuxLemmas ++ (← mkFreshUserName `test)) (← 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
index f3ef0d730bd1..9ff9013a18f7 100644
--- a/src/Lean/Elab/Tactic/TreeTacAttr.lean
+++ b/src/Lean/Elab/Tactic/TreeTacAttr.lean
@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2022 Microsoft Corporation. All rights reserved.
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/

From 3d0e37ce1345da474a1a740caaae7a0cb763f162 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Wed, 29 Jan 2025 08:32:26 +0100
Subject: [PATCH 4/9] improve aux lemma naming

---
 src/Lean/Elab/Tactic/AsAuxLemma.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Tactic/AsAuxLemma.lean b/src/Lean/Elab/Tactic/AsAuxLemma.lean
index 1ff65d87ffaf..8cae8ec7e887 100644
--- a/src/Lean/Elab/Tactic/AsAuxLemma.lean
+++ b/src/Lean/Elab/Tactic/AsAuxLemma.lean
@@ -20,7 +20,7 @@ def elabAsAuxLemma : Lean.Elab.Tactic.Tactic
     unless mvars.isEmpty do
       throwError "Left-over goals, cannot abstract"
     let e ← instantiateMVars (mkMVar mvarId)
-    let e ← mkAuxTheorem (`Std.Internal.AuxLemmas ++ (← mkFreshUserName `test)) (← mvarId.getType) e
+    let e ← mkAuxTheorem (`Lean.Elab.Tactic.AsAuxLemma ++ (← mkFreshUserName `test)) (← mvarId.getType) e
     mvarId.assign e
     return []
 | _ => throwError "Invalid as_aux_lemma syntax"

From dbdb93d2196807df9a3eb9e11184247a0592f06f Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Thu, 30 Jan 2025 10:14:33 +0100
Subject: [PATCH 5/9] does this trigger a new CI?


From 49b2cac1cbac44610d00cd4be4e216a0cfd8f7a7 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Thu, 30 Jan 2025 22:48:05 +0100
Subject: [PATCH 6/9] remarks and tests

---
 src/Init/Tactics.lean                 |  2 +-
 src/Lean/Elab/Tactic/AsAuxLemma.lean  |  6 ++--
 src/Lean/Elab/Tactic/TreeTacAttr.lean |  2 +-
 tests/lean/run/as_aux_lemma.lean      | 49 +++++++++++++++++++++++++++
 tests/lean/run/tree_tac_attr.lean     | 10 ++++++
 5 files changed, 64 insertions(+), 5 deletions(-)
 create mode 100644 tests/lean/run/as_aux_lemma.lean
 create mode 100644 tests/lean/run/tree_tac_attr.lean

diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index acc8781d2c2c..865fb8f96bd0 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -14,7 +14,7 @@ namespace Lean.Parser.Tactic
 into an auxiliary lemma. In some cases, this significantly reduces the size of expressions
 because the proof term is not duplicated.
 -/
-scoped syntax (name := as_aux_lemma) "as_aux_lemma" " => " tacticSeq : tactic
+syntax (name := as_aux_lemma) "as_aux_lemma" " => " tacticSeq : tactic
 
 /--
 `with_annotate_state stx t` annotates the lexical range of `stx : Syntax` with
diff --git a/src/Lean/Elab/Tactic/AsAuxLemma.lean b/src/Lean/Elab/Tactic/AsAuxLemma.lean
index 8cae8ec7e887..6d6c81d5bbc1 100644
--- a/src/Lean/Elab/Tactic/AsAuxLemma.lean
+++ b/src/Lean/Elab/Tactic/AsAuxLemma.lean
@@ -1,5 +1,5 @@
 /-
-Copyright (c) Lean FRO, LLC. All rights reserved.
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joachim Breitner
 -/
@@ -18,9 +18,9 @@ def elabAsAuxLemma : Lean.Elab.Tactic.Tactic
   liftMetaTactic fun mvarId => do
     let (mvars, _) ← runTactic mvarId s
     unless mvars.isEmpty do
-      throwError "Left-over goals, cannot abstract"
+      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 `test)) (← mvarId.getType) e
+    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
index 9ff9013a18f7..2a31c9d3d206 100644
--- a/src/Lean/Elab/Tactic/TreeTacAttr.lean
+++ b/src/Lean/Elab/Tactic/TreeTacAttr.lean
@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/
diff --git a/tests/lean/run/as_aux_lemma.lean b/tests/lean/run/as_aux_lemma.lean
new file mode 100644
index 000000000000..ad9591680937
--- /dev/null
+++ b/tests/lean/run/as_aux_lemma.lean
@@ -0,0 +1,49 @@
+import Lean.Meta.Basic
+import Lean.Util.NumObjs
+import Lean.Elab.Tactic
+import Init.Tactics
+
+open Lean Meta Elab Tactic Parser.Tactic
+
+elab_rules : 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 []
+
+namespace Test
+
+def thm : ∀ n : Nat, n = 0 + n := by as_aux_lemma =>
+  intro n
+  induction n
+  · rfl
+  · next ih =>
+    rw [← Nat.succ_eq_add_one, Nat.add_succ, ← ih]
+
+end Test
+
+open Lean
+
+def size (ns : Name) : MetaM Nat := do
+  let env ← getEnv
+  let mut totalSize : Nat := 0
+  for (name, info) in env.constants do
+    if ns.isPrefixOf name then
+      if let some e := info.value? then
+        let numObjs ← e.numObjs
+        totalSize := totalSize + numObjs
+  return totalSize
+
+/--
+info: theorem smaller than auxiliary lemma: true
+-/
+#guard_msgs in
+run_meta do
+  let thmSize ← size `Test
+  let auxSize ← size `Lean.Elab.Tactic.AsAuxLemma
+  logInfo m!"theorem smaller than auxiliary lemma: {decide $ thmSize < auxSize}"
diff --git a/tests/lean/run/tree_tac_attr.lean b/tests/lean/run/tree_tac_attr.lean
new file mode 100644
index 000000000000..f1a2ecf595f7
--- /dev/null
+++ b/tests/lean/run/tree_tac_attr.lean
@@ -0,0 +1,10 @@
+prelude
+import Init.Data.List.Basic
+
+@[tree_tac]
+theorem a : [1, 2] ++ [3] = [1, 2, 3] := rfl
+
+@[tree_tac]
+theorem b : [1, 2, 3].length = 3 := sorry
+
+example : ([1, 2] ++ [3]).length = 3 := by simp only [tree_tac]

From 19679a3e6479a7836799621219a562b40ac6c75b Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Fri, 31 Jan 2025 08:56:28 +0100
Subject: [PATCH 7/9] tests

---
 tests/lean/run/as_aux_lemma.lean | 41 +++++++++++++-------------------
 1 file changed, 17 insertions(+), 24 deletions(-)

diff --git a/tests/lean/run/as_aux_lemma.lean b/tests/lean/run/as_aux_lemma.lean
index ad9591680937..b66429592cbf 100644
--- a/tests/lean/run/as_aux_lemma.lean
+++ b/tests/lean/run/as_aux_lemma.lean
@@ -1,49 +1,42 @@
+import Lean.Environment
 import Lean.Meta.Basic
 import Lean.Util.NumObjs
-import Lean.Elab.Tactic
-import Init.Tactics
 
-open Lean Meta Elab Tactic Parser.Tactic
+open Lean Meta
 
-elab_rules : 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 []
+abbrev testProp := ∀ n : Nat, n = 0 + n
 
-namespace Test
-
-def thm : ∀ n : Nat, n = 0 + n := by as_aux_lemma =>
+def thmUsingTactic : testProp := by as_aux_lemma =>
   intro n
   induction n
   · rfl
   · next ih =>
     rw [← Nat.succ_eq_add_one, Nat.add_succ, ← ih]
 
-end Test
+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 (ns : Name) : MetaM Nat := do
+def size (name : Name) : MetaM Nat := do
   let env ← getEnv
   let mut totalSize : Nat := 0
-  for (name, info) in env.constants do
-    if ns.isPrefixOf name then
+  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: theorem smaller than auxiliary lemma: true
+info: as_aux_lemma makes proof term smaller : true
 -/
 #guard_msgs in
 run_meta do
-  let thmSize ← size `Test
-  let auxSize ← size `Lean.Elab.Tactic.AsAuxLemma
-  logInfo m!"theorem smaller than auxiliary lemma: {decide $ thmSize < auxSize}"
+  let sizeUsingTactic ← size `thmUsingTactic
+  let sizeWithoutTactic ← size `thmWithoutTactic
+  logInfo m!"as_aux_lemma makes proof term smaller : {decide <| sizeUsingTactic < sizeWithoutTactic}"

From ce122f92ec0fec5bc2ecc712b062a62a37d1a2df Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Fri, 31 Jan 2025 09:28:46 +0100
Subject: [PATCH 8/9] remove slightly unnecessary test for simp attribute

---
 tests/lean/run/tree_tac_attr.lean | 10 ----------
 1 file changed, 10 deletions(-)
 delete mode 100644 tests/lean/run/tree_tac_attr.lean

diff --git a/tests/lean/run/tree_tac_attr.lean b/tests/lean/run/tree_tac_attr.lean
deleted file mode 100644
index f1a2ecf595f7..000000000000
--- a/tests/lean/run/tree_tac_attr.lean
+++ /dev/null
@@ -1,10 +0,0 @@
-prelude
-import Init.Data.List.Basic
-
-@[tree_tac]
-theorem a : [1, 2] ++ [3] = [1, 2, 3] := rfl
-
-@[tree_tac]
-theorem b : [1, 2, 3].length = 3 := sorry
-
-example : ([1, 2] ++ [3]).length = 3 := by simp only [tree_tac]

From 938e89395d8db50297308ee39374099376a72057 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Fri, 31 Jan 2025 09:31:54 +0100
Subject: [PATCH 9/9] add license header

---
 tests/lean/run/as_aux_lemma.lean | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/tests/lean/run/as_aux_lemma.lean b/tests/lean/run/as_aux_lemma.lean
index b66429592cbf..0dd9dc05b68e 100644
--- a/tests/lean/run/as_aux_lemma.lean
+++ b/tests/lean/run/as_aux_lemma.lean
@@ -1,3 +1,8 @@
+/-
+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