Structure extensionality

Stream: lean4

[Jesse Vogel]

Does there exist a tactic which, given as goal the equality of two instances of a structure, splits it up into one goal for each field of the structure? In Lean3, I could label my structure with @[ext] and then use the ext tactic, but this does work anymore in Lean4. As an example, consider:

structure Struct (α β : Type) where
  fst : α
  snd : β

example (x₁ y₁ : α) (x₂ y₂ : β) (h₁ : x₁ = y₁) (h₂ : x₂ = y₂) : Struct.mk x₁ x₂ = Struct.mk y₁ y₂ := by {
  ext; -- does not exist ..
}

I want to split the goal into x₁ = y₁ and x₂ = y₂. How do I do this?