∀ (p p_1 : ENNReal) (e_p : p = p_1) {ι : Type u_2} (α : ι → Type u_3) [inst : Fact (1 ≤ p)] [inst_1 : Fintype ι]
  [inst_2 : (i : ι) → SeminormedAddCommGroup (α i)],
  PiLp.seminormedAddCommGroupToPi p α = PiLp.seminormedAddCommGroupToPi p_1 α