solve two goals with [tac1,tac2]

Stream: mathlib4

[Kevin Buzzard]

Occasionally I see ported files which use lean 3's [tac1,tac2] trick to solve two goals with two tactics in tactic mode. Does this exist in Lean 4? Currently I'm just working around it in the obvious way.

[Mario Carneiro]

import Tactic.SeqFocus