Mem W01p of cont Diff has Compact Support subset

theorem memW01p_of_contDiff_hasCompactSupport_subset    {p : ℝ≥0∞} {Ω : Set E} (hΩ : IsOpen Ω) {f : E → ℝ}    (hf : ContDiff ℝ (⊤ : ℕ∞) f) (hf_supp : HasCompactSupport f)    (hf_sub : tsupport f ⊆ Ω) :    MemW01p p f Ω := by  let _ := (inferInstance : NeZero d)  let hw : MemW1pWitness p f Ω :=    { memLp := (hf.continuous.memLp_of_hasCompactSupport hf_supp).restrict Ω      weakGrad := fun x =>        WithLp.toLp 2 fun i => (fderiv ℝ f x) (EuclideanSpace.single i 1)      weakGrad_component_memLp := by        intro i        have hderiv_smooth : ContDiff ℝ (⊤ : ℕ∞)            (fun x => (fderiv ℝ f x) (EuclideanSpace.single i 1)) :=          (hf.fderiv_right (m := (⊤ : ℕ∞)) (by norm_cast)).clm_apply contDiff_const        exact (hderiv_smooth.continuous.memLp_of_hasCompactSupport          (hf_supp.fderiv_apply (𝕜 := ℝ) _)).restrict Ω      isWeakGrad := by        intro i        simpa [PiLp.toLp_apply] using          (HasWeakPartialDeriv.of_contDiff (Ω := Ω) (i := i)            (f := f) hΩ (hf.of_le (by norm_cast))) }  refine ⟨hw.memW1p, hw, fun _ => f, ?_, ?_, ?_, ?_, ?_⟩  · intro n    exact hf  · intro n    exact hf_supp  · intro n    exact hf_sub  · simp  · intro i    simp [hw]