Tactic chapter/FAQ: add creation of a fresh unique name

[bodoai]

Proposal:

Add the following q&a to the FAQ:

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