∀ {p : ENNReal} {𝕜 : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring 𝕜] [inst_1 : AddCommGroup α]
  [inst_2 : AddCommGroup β] (x : WithLp p (α × β)) (c : 𝕜) [inst_3 : Module 𝕜 α] [inst_4 : Module 𝕜 β],
  (c • x).fst = c • x.fst