∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : NormedAddCommGroup α]
  [inst_1 : NormedAddCommGroup β], WithLp.instProdNormedAddCommGroup p α β = WithLp.instProdNormedAddCommGroup p α β