De Giorgi Cutoff Test mem W01p of pos Part

theorem deGiorgiCutoffTest_memW01p_of_posPart    {Ω : Set E} [IsFiniteMeasure (volume.restrict Ω)]    (hΩ : IsOpen Ω)    {u η : E → ℝ}    (hw : MemW1pWitness 2 u Ω)    (hη : ContDiff ℝ (⊤ : ℕ∞) η)    {C₀ C₁ : ℝ}    (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁)    (hη_bound : ∀ x, |η x| ≤ C₀)    (hη_grad_bound : ∀ x, ‖fderiv ℝ η x‖ ≤ C₁)    (hη_comp : HasCompactSupport η)    (hη_sub : tsupport η ⊆ Ω)    (k : ℝ)    (hpos :      ∀ {v : E → ℝ},        MemW1pWitness 2 v Ω →          MemW1pWitness 2 (fun x => max (v x) 0) Ω) :    MemW01p 2 (deGiorgiCutoffTestGeneral η u k) Ω := by  let hwShift : MemW1pWitness 2 (fun x => u x - k) Ω := hw.sub_const hΩ k  have hw_trunc : MemW1pWitness 2 (positivePartSub u k) Ω := by    simpa [positivePartSub] using (hpos hwShift)  exact    deGiorgiCutoffTest_memW01p_of_truncWitness      hΩ hw_trunc hη hC₀ hC₁ hη_bound hη_grad_bound hη_comp hη_sub