Mem W01p of mem W1p of tsupport subset

theorem memW01p_of_memW1p_of_tsupport_subset    {Ω : Set E} (hΩ : IsOpen Ω)    {p : ℝ} (hp : 1 < p) {u : E → ℝ}    (hu : MemW1p (ENNReal.ofReal p) u Ω)    (hu_compact : HasCompactSupport u)    (hu_sub : tsupport u ⊆ Ω) :    MemW01p (ENNReal.ofReal p) u Ω := by  have hp_enn : (1 : ℝ≥0∞) ≤ ENNReal.ofReal p := by    simpa using (ENNReal.ofReal_le_ofReal (le_of_lt hp) : ENNReal.ofReal (1 : ℝ) ≤ ENNReal.ofReal p)  rcases hu with ⟨hu_memLp, hu_grad⟩  choose g hg_memLp hg_weak using hu_grad  let G : E → E := fun x => WithLp.toLp 2 fun i => g i x  let hw : MemW1pWitness (ENNReal.ofReal p) u Ω :=    { memLp := hu_memLp      weakGrad := G      weakGrad_component_memLp := hg_memLp      isWeakGrad := hg_weak }  obtain ⟨δ, hδ_pos, hδΩ⟩ := hu_compact.isCompact.exists_cthickening_subset_open hΩ hu_sub  let K : Set E := Metric.cthickening δ (tsupport u)  have hK_compact : IsCompact K := hu_compact.isCompact.cthickening (r := δ)  have hKΩ : K ⊆ Ω := hδΩ  obtain ⟨η, hη_smooth, hη_compact, hη_range, hη_one, hη_sub⟩ :=    exists_smooth_cutoff (d := d) hK_compact hΩ hKΩ  have hη_bound : ∀ x, |η x| ≤ 1 := by    intro x    rcases hη_range ⟨x, rfl⟩ with ⟨hx0, hx1⟩    rw [abs_of_nonneg hx0]    exact hx1  have hη_fderiv_compact : HasCompactSupport (fderiv ℝ η) := hη_compact.fderiv (𝕜 := ℝ)  obtain ⟨Cη, hCη⟩ := hη_fderiv_compact.isCompact.exists_bound_of_continuousOn    ((hη_smooth.continuous_fderiv (by simp)).continuousOn)  let C₁ : ℝ := max Cη 0  have hC₁_nonneg : 0 ≤ C₁ := le_max_right _ _  have hη_grad_bound : ∀ x, ‖fderiv ℝ η x‖ ≤ C₁ := by    intro x    by_cases hx : x ∈ tsupport (fderiv ℝ η)    · exact (hCη x hx).trans (le_max_left _ _)    · have hzero : fderiv ℝ η x = 0 := image_eq_zero_of_notMem_tsupport hx      simp [C₁, hzero]  let v : E → ℝ := fun x => η x * u x  let hwCut :=    MemW1pWitness.mul_smooth_bounded_p      (d := d) (p := ENNReal.ofReal p) hp_enn hΩ hw hη_smooth      zero_le_one hC₁_nonneg hη_bound hη_grad_bound  have hv_eq_u : v = u := by    funext x    by_cases hx : x ∈ tsupport u    · have hηx : η x = 1 := hη_one x (Metric.self_subset_cthickening (tsupport u) hx)      simp [v, hηx]    · have hux : u x = 0 := image_eq_zero_of_notMem_tsupport hx      simp [v, hux]  have hv_sub : tsupport v ⊆ tsupport η := tsupport_smul_subset_left η u  have hgrad_sub :      ∀ i : Fin d, tsupport (fun x => hwCut.weakGrad x i) ⊆ tsupport η := by    intro i    exact tsupport_mul_smooth_bounded_p_weakGrad_component_subset      (d := d) (p := ENNReal.ofReal p) hp_enn hΩ hw hη_smooth zero_le_one hC₁_nonneg hη_bound      hη_grad_bound i  rcases exists_smooth_W1p_approx_of_supportedWitness      (d := d) (Ω := Ω) (K := tsupport η) hΩ hp hwCut      hη_compact.isCompact hη_sub hv_sub hgrad_sub with    ⟨φ, hφ_smooth, hφ_compact, hφ_sub, hφ_fun, hφ_grad⟩  simpa [v, hv_eq_u] using    memW01p_of_global_approx_supported hwCut φ hφ_smooth hφ_compact hφ_sub hφ_fun hφ_grad