Custom norm on ℝ² in Lean: type synonym + NormedAddCommGroup.ofCore, not abbrev

To prove something for a specific non-standard norm (e.g. the hexagonal norm max(|x|,|y|,|x+y|) to show Bohnenblust's constant d/(d+1) is attained), define def HexPlane : Type := ℝ × ℝ (a def, NOT abbrev, or the sup norm of ℝ × ℝ is found by instance search), transfer AddCommGroup, Module ℝ, FiniteDimensional ℝ with inferInstanceAs, give Norm by hand, prove a NormedSpace.Core ℝ HexPlane (norm_nonneg, norm_smul, norm_triangle, norm_eq_zero_iff), then instance := NormedAddCommGroup.ofCore core and NormedSpace.ofCore core. Use explicit toProd/ofProd := id coercion functions so that .1/.2 typecheck. Subtraction and norms of ofProd (a,b) are then rfl lemmas, and finrank is change finrank ℝ (ℝ × ℝ) = 2; simp. For max-of-abs bounds, simp only [max_le_iff, abs_le] at h and then linarith beats chaining le_max lemmas.