From fa70395ff91401a145756cf64354abbd94fd41c3 Mon Sep 17 00:00:00 2001
From: igler <bodo.igler@hs-rm.de>
Date: Tue, 4 Mar 2025 10:38:49 +0100
Subject: [PATCH] add creation of a fresh unique name

---
 lean/main/09_tactics.lean | 24 +++++++++++++++++++++++-
 1 file changed, 23 insertions(+), 1 deletion(-)

diff --git a/lean/main/09_tactics.lean b/lean/main/09_tactics.lean
index 5cd7a1a..3ef0743 100644
--- a/lean/main/09_tactics.lean
+++ b/lean/main/09_tactics.lean
@@ -582,7 +582,7 @@ elab "faq_throw_error" : tactic =>
 -- tactic 'faq_throw_error' failed, throwing an error at the current goal
 -- ⊢ ∀ (b : Bool), b = true
 
-/-!
+/-
 **Q: What is the difference between `Lean.Elab.Tactic.*` and `Lean.Meta.Tactic.*`?**
 
 A: `Lean.Meta.Tactic.*` contains low level code that uses the `Meta` monad to
@@ -590,6 +590,28 @@ implement basic features such as rewriting. `Lean.Elab.Tactic.*` contains
 high-level code that connects the low level development in `Lean.Meta` to the
 tactic infrastructure and the parsing front-end.
 
+**Q: How do I create a fresh unique name?**
+
+A: Use `Lean.Core.mkFreshUserName <name-basis>`.
+
+This creates a new (unused) inaccessible name based on name-basis. -/
+
+elab " faq_fresh_hyp_name " : tactic =>
+  Lean.Elab.Tactic.withMainContext do
+    -- create fresh name based on name `h`
+    let h := Lean.mkIdent (← Lean.Core.mkFreshUserName `h)
+    -- create new hypothesis with this fresh name
+    Lean.Elab.Tactic.evalTactic (← `(tactic| have $h : 1 + 1 = 2 := by simp))
+    -- use hypothesis
+    Lean.Elab.Tactic.evalTactic (← `(tactic| rewrite [$h:ident]))
+    -- remove hypothesis
+    Lean.Elab.Tactic.evalTactic (← `(tactic| clear $h))
+
+example : 1 + 1 = 2 := by
+  faq_fresh_hyp_name
+  rfl
+
+/-!
 ## Exercises
 
 1. Consider the theorem `p ∧ q ↔ q ∧ p`. We could either write its proof as a proof term, or construct it using the tactics.