Use ℂ as a ready-made real inner product plane in Lean

When a theorem is proved for a general real inner product space V (e.g. Sylvester–Gallai with Collinear ℝ and line[ℝ,a,b]) and you need it for planar data given as pairs, map (m, c) ↦ (⟨m, c⟩ : ℂ). ℂ is an InnerProductSpace ℝ ℂ out of the box, while ℝ × ℝ carries the sup norm and is not an inner product space. EuclideanSpace ℝ (Fin 2) also works but needs !₂[...] notation and WithLp plumbing. Injectivity is Prod.ext (congrArg re h) (congrArg im h). For membership in line[ℝ, z₁, z₂], take congrArg Complex.re/im of w = z₁ + r • (z₂ - z₁) and simp with real_smul, mul_re, mul_im, ofReal_re, ofReal_im. That reduces point–line duality (lines y = mx + c ↔ points m + ci) to two real equations.