∀ (p : ENNReal) {𝕜 : Type u_1} {α : Type u_2} {β : Type u_3} {α' : Type u_5} {β' : Type u_6} [hp : Fact (1 ≤ p)]
  [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup α] [inst_2 : Module 𝕜 α] [inst_3 : SeminormedAddCommGroup β]
  [inst_4 : Module 𝕜 β] [inst_5 : SeminormedAddCommGroup α'] [inst_6 : Module 𝕜 α'] [inst_7 : SeminormedAddCommGroup β']
  [inst_8 : Module 𝕜 β'] (f : α ≃ₗᵢ[𝕜] α') (g : β ≃ₗᵢ[𝕜] β') (a : WithLp p (α' × β')),
  (LinearIsometryEquiv.withLpProdCongr p f g).symm a = WithLp.toLp p ((f.prodCongr g.toLinearEquiv).symm a.ofLp)