Lean's equivalent for Program

Stream: lean4

[Shreyas Srinivas]

Is there a lean equivalent of Coq's Program tactic? Is it worthwhile implementing one?
https://coq.inria.fr/refman/addendum/program.html

[Mario Carneiro]

From what I know of it you can get similar behavior just using if and match