How to port to Lean 4 some Lean-3 expression

Stream: lean4

[YurySerdyuk]

Hi !
How to port to Lean 4 expression like
theorem trans {l₁ l₂ l₃ : List α} : l₁ ≃ l₂ → l₂ ≃ l₃ → l₁ ≃ l₃
| ⟨x, y⟩ ⟨z, w⟩ := ⟨Subset.trans x z, Subset.trans w y⟩

Lean 4 gives the error to := symbol ...

[Ruben Van de Velde]

Try => instead of :=

[YurySerdyuk]

I have tried this - gives the new error:
"identifier expected" for ⟨x, y⟩ ⟨z, w⟩ - expression

[Ruben Van de Velde]

Please post a #mwe

[YurySerdyuk]

This is full code --

import Mathlib.Data.Set.Lattice
open Set

example (α : Type) (p q : α → Prop) : (∃ x, p x ∨ q x) → ∃ x, q x ∨ p x := by
  intro
  | ⟨w, Or.inl h⟩ => exact ⟨w, Or.inr h⟩
  | ⟨w, Or.inr h⟩ => exact ⟨w, Or.inl h⟩

namespace List



private def equiv (l₁ l₂ : List α) := l₁ ⊆ l₂ ∧ l₂ ⊆ l₁
  infix:50 " ≃ " => List.equiv

@[refl, simp] theorem equiv.refl (l : List α) : l ≃ l :=
  ⟨by simp, by simp⟩

@[symm] theorem equiv.symm {l₁ l₂ : List α} : l₁ ≃ l₂ → l₂ ≃ l₁ :=
  And.symm

@[trans] theorem equiv.trans {l₁ l₂ l₃ : List α} : l₁ ≃ l₂ → l₂ ≃ l₃ → l₁ ≃ l₃
  | ⟨x, y⟩ ⟨z, w⟩ => ⟨Subset.trans x z, Subset.trans w y⟩

Note, that the example after open Set is working ..

[Ruben Van de Velde]

With #backticks, please

[Marcus Rossel]

Add a comma between ⟨x, y⟩ and ⟨z, w⟩.

[YurySerdyuk]

Thanks - all is working !