feat: abstract tactic

Mathlib.lean

@@ -5117,6 +5117,7 @@ import Mathlib.SetTheory.ZFC.Rank
 import Mathlib.Std.Data.HashMap
 import Mathlib.Tactic
 import Mathlib.Tactic.Abel
+import Mathlib.Tactic.Abstract
 import Mathlib.Tactic.AdaptationNote
 import Mathlib.Tactic.Algebraize
 import Mathlib.Tactic.ApplyAt

Mathlib/Tactic.lean

@@ -1,4 +1,5 @@
 import Mathlib.Tactic.Abel
+import Mathlib.Tactic.Abstract
 import Mathlib.Tactic.AdaptationNote
 import Mathlib.Tactic.Algebraize
 import Mathlib.Tactic.ApplyAt

Mathlib/Tactic/Abstract.lean

@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2025 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn, Sven Manthe
+-/
+import Mathlib.Init
+import Lean.Elab.Tactic.Simp
+
+/-! # The `abstract` tactic -/
+
+open Lean Meta Elab Tactic Term
+
+/--
+Usage: `abstract <tacticSeq>`.
+
+The abstract tactic executes the provided tactic sequence, and "hides" its proof behind a new
+auxiliary lemma. This is mostly useful to hide long proofs in the statement of a theorem, since
+certain tactics can be slow if the goal contains a large proof as subterm.
+-/
+elab "abstract" tacs:ppDedent(tacticSeq) : tactic => do
+  if (← getGoals).length ≠ 1 then
+    throwError "Abstract failed. There are {(← getGoals).length} goals. Expected exactly 1 goal."
+  let target ← getMainTarget
+  if !(← isProp target) then
+    throwError "Abstract failed. The current goal is not propositional."
+  let goal ← getMainGoal
+  let newGoal ← mkFreshExprMVar target
+  setGoals [newGoal.mvarId!]
+  evalTactic tacs
+  setGoals [goal]
+  let auxName := (← getDeclName?).get! ++ `abstract ++ (← mkFreshId)
+  goal.assign <| ← mkAuxTheorem auxName target newGoal

MathlibTest/Abstract.lean

@@ -0,0 +1,23 @@
+import Mathlib.Tactic.Abstract
+import Mathlib.Tactic.Core
+import Mathlib.Lean.Name
+
+open Lean
+
+theorem foo (x : Fin 1) : x = ⟨0, by abstract omega⟩ := Subsingleton.elim ..
+
+-- We don't test the precise type of `foo`, since I don't know how robust
+-- the generated unique number is (currently 87)
+run_cmd do
+  let some t := (← getEnv).find? `foo | unreachable!
+  if !t.type.foldConsts false (fun n b ↦ b || n matches .num _ _) then
+    throwError "no aux-lemma in the type of foo"
+
+/-- error: Abstract failed. The current goal is not propositional. -/
+#guard_msgs in
+example (n : Nat) : n = by abstract exact 0 := sorry
+
+/-- error: Abstract failed. There are 2 goals. Expected exactly 1 goal. -/
+#guard_msgs in
+example (f : True ∧ True → Nat) (n : Nat) :
+  n = f (by constructor; abstract trivial; trivial) := sorry