Mem W01p smul

theorem MemW01p.smul    {Ω : Set E} {u : E → ℝ} (c : ℝ)    (hu : MemW01p 2 u Ω) :    MemW01p 2 (fun x => c * u x) Ω := by  let _ := (inferInstance : NeZero d)  rcases hu with ⟨_, hwu, φ, hφ_smooth, hφ_compact, hφ_sub, hφ_fun, hφ_grad⟩  refine ⟨(hwu.smul c).memW1p, hwu.smul c, fun n x => c * φ n x, ?_, ?_, ?_, ?_, ?_⟩  · intro n    simpa [smul_eq_mul] using (contDiff_const.mul (hφ_smooth n))  · intro n    simpa [Pi.smul_apply, smul_eq_mul] using (hφ_compact n).smul_left (f := fun _ : E => c)  · intro n    simpa [Pi.smul_apply, smul_eq_mul] using      (tsupport_smul_subset_right (fun _ : E => c) (φ n)).trans (hφ_sub n)  ·    have hscaled :        Tendsto          (fun n =>            ‖c‖ₑ * eLpNorm (fun x => φ n x - u x) 2 (volume.restrict Ω))          atTop (nhds (‖c‖ₑ * 0)) :=      ENNReal.Tendsto.const_mul hφ_fun (Or.inr ENNReal.coe_ne_top)    have hEq :        (fun n => eLpNorm (fun x => c * φ n x - c * u x) 2 (volume.restrict Ω)) =          (fun n => ‖c‖ₑ * eLpNorm (fun x => φ n x - u x) 2 (volume.restrict Ω)) := by      funext n      have hfun :          (fun x => c * φ n x - c * u x) = c • (fun x => φ n x - u x) := by        ext x        simp [Pi.smul_apply, smul_eq_mul]        ring      rw [hfun, eLpNorm_const_smul]    rw [hEq]    simpa using hscaled  · intro i    have hscaled :        Tendsto          (fun n =>            ‖c‖ₑ *              eLpNorm                (fun x => (fderiv ℝ (φ n) x) (EuclideanSpace.single i 1) - hwu.weakGrad x i)                2 (volume.restrict Ω))          atTop (nhds (‖c‖ₑ * 0)) :=      ENNReal.Tendsto.const_mul (hφ_grad i) (Or.inr ENNReal.coe_ne_top)    have hEq :        (fun n =>          eLpNorm            (fun x =>              (fderiv ℝ (fun y => c * φ n y) x) (EuclideanSpace.single i 1) -                (hwu.smul c).weakGrad x i)            2 (volume.restrict Ω)) =          (fun n =>            ‖c‖ₑ *              eLpNorm                (fun x => (fderiv ℝ (φ n) x) (EuclideanSpace.single i 1) - hwu.weakGrad x i)                2 (volume.restrict Ω)) := by      funext n      have hfun :          (fun x =>            (fderiv ℝ (fun y => c * φ n y) x) (EuclideanSpace.single i 1) -              (hwu.smul c).weakGrad x i) =            c • (fun x =>              (fderiv ℝ (φ n) x) (EuclideanSpace.single i 1) - hwu.weakGrad x i) := by        ext x        have hfd : fderiv ℝ (fun y => c * φ n y) x = c • fderiv ℝ (φ n) x := by          simpa [smul_eq_mul] using congrFun (fderiv_const_smul_field (𝕜 := ℝ) (f := φ n) c) x        simp [MemW1pWitness.smul, Pi.smul_apply, smul_eq_mul, hfd]        ring      rw [hfun, eLpNorm_const_smul]    rw [hEq]    simpa using hscaled