application to a point in the product not written as a pair

Stream: general

[A.]

In @Igor Khavkine's PR #26300 a reviewer wrote with regard to a particular statement

Instead of using two points x₁ and x₂, could you use a single point x in E₁ × E₂, with x.1 and x.2? This is strictly more general, as otherwise your statement wouldn't apply directly to a point which is not written as a pair (x₁, x₂).

I wondered what this meant as, in a simple invocation like the one below, such a statement does indeed apply directly to a point x in E₁ × E₂. Is some other context in which it wouldn't?

import Mathlib.Analysis.Normed.Group.Constructions

variable {E₁ E₂ : Type*} [NormedAddCommGroup E₁] [NormedAddCommGroup E₂]
theorem obvs {x₁ : E₁} {x₂ : E₂} (h : ‖(x₁, x₂)‖ ≤ 3) : ‖(x₁, x₂)‖ ≤ 5 := by linarith

variable (x : E₁ × E₂) (h : ‖x‖ ≤ 3)
#check obvs h

[Ruben Van de Velde]

Huh, really?

[Yury G. Kudryashov]

While it isn't more general (x = (x.1, x.2) is defeq in Lean 4), sometimes having both versions helps Lean unify the theorem with the goal/hypotheses.

[A.]

Thanks! I guess that comes under the heading "other contexts". (But I don't think the review suggestion was to provide both versions?)

[Kevin Buzzard]

I kind of feel like the x.1, x.2 version is more idiomatic? But this might be because I'm old enough to remember Lean 3, where x = (x.1, x.2) was not rfl but (a,b).1=a was, and so the suggested version really was more general.