ext <;> dsimp
a b : Point
⊢ (match a, b with
    | { x := x₁, y := y₁, z := z₁ }, { x := x₂, y := y₂, z := z₂ } => { x := x₁ + x₂, y := y₁ + y₂, z := z₁ + z₂ }) =
    match b, a with
    | { x := x₁, y := y₁, z := z₁ }, { x := x₂, y := y₂, z := z₂ } => { x := x₁ + x₂, y := y₁ + y₂, z := z₁ + z₂ }
case x
a b : Point
⊢ a.x + b.x = b.x + a.x

case y
a b : Point
⊢ a.y + b.y = b.y + a.y

case z
a b : Point
⊢ a.z + b.z = b.z + a.z