Revert "wip tinkering"

This reverts commit 113d0cf.

Mathlib/Geometry/Manifold/Bordisms.lean

@@ -216,15 +216,6 @@ def trivial (hequiv : H ≃ₜ EuclideanSpace ℝ (Fin n)) [h: Fact (finrank ℝ
   f := fun _ ↦ PUnit.unit
   hf := continuous_const
 
-variable (α : Type*)
-#synth TopologicalSpace (WithLp 2   α)
-
-def WithLp.prodEquivSum (α β 𝕜 : Type*) [NontriviallyNormedField 𝕜] :
-    (WithLp 2 (PiLp 2 (fun _ : α ↦ 𝕜))) × (EuclideanSpace 𝕜 β) ≃ₜ EuclideanSpace 𝕜 (α ⊕ β) where
-  toEquiv := (Equiv.sumArrowEquivProdArrow α β 𝕜).symm
-  continuous_toFun := sorry
-  continuous_invFun := sorry
-
 def EuclideanSpace.prodEquivSum (α β 𝕜 : Type*) [NontriviallyNormedField 𝕜] :
     (EuclideanSpace 𝕜 α) × (EuclideanSpace 𝕜 β) ≃ₜ EuclideanSpace 𝕜 (α ⊕ β) where
   toEquiv := (Equiv.sumArrowEquivProdArrow α β 𝕜).symm
@@ -271,7 +262,6 @@ instance {n : ℕ} (s t : SingularNManifold X n k) :
   haveI := ChartedSpace.comp (EuclideanSpace ℝ (Fin n)) t.H t.M
   infer_instance
 
--- missing: if M is a manifold w.r.t. I over (E, H), this transfer across a homeo
 instance {n : ℕ} (s t : SingularNManifold X n k) : IsManifold (𝓡 n) k (s.M ⊕ t.M) := sorry
 
 /-- The disjoint union of two singular `n`-manifolds on `X` is a singular `n`-manifold on `X`. -/