Running tactics at the meta level

Stream: lean4

[Anand Rao]

I would like to run Lean tactics such as intro or apply through meta-level code. For instance, I want to modify something such as

syntax (name := mytac) "mytac" : tactic

@[tactic mytac] def mytacT : Tactic := fun stx => do
  let goals ← getGoals
  logInfo m!"The goals are {goals}"
  return ()

example : Unit → Unit := by
  mytac
  intro
  exact ()

to automatically introduce the hypotheses (via the intro tactic). It appears that the liftMetaTactic does something of this sort, but I have not been able to find a concrete example demonstrating how to integrate pre-existing tactics in the Lean4 source code. I would be grateful if someone could help me understand how to modify the above code to run such tactics at the meta-level.

[Siddhartha Gadgil]

Most of these tactics are lifts of stuff at the meta level, for example apply is a lift of Lean.Meta.apply. It is likely that for your usage you can use the meta level stuff directly (I do this a lot).

[Siddhartha Gadgil]

What do you want to introduce in the example?