Moser Reg Power Cutoff Witness grad

lemma moserRegPowerCutoffWitness_grad    {u η : E → ℝ} {s ε N p Cη : ℝ}    (hs : 0 < s) (hs1 : s ≤ 1) (hε : 0 < ε) (hN : 0 ≤ N)    (hu1 : MemW1pWitness 2 u (Metric.ball (0 : E) 1))    (hη : ContDiff ℝ (⊤ : ℕ∞) η)    (hη_bound : ∀ x, |η x| ≤ 1)    (hη_grad_bound : ∀ x, ‖fderiv ℝ η x‖ ≤ Cη)    (x : E) (i : Fin d) :    (moserRegPowerCutoffWitness (d := d) (p := p)      hs hs1 hε hN hu1 hη hη_bound hη_grad_bound).weakGrad x i =      η x * (moserRegClippedPosPartWitness (d := d) (u := u) (p := p)        hs hs1 hε hN hu1).weakGrad x i +      (fderiv ℝ η x) (EuclideanSpace.single i 1) *        moserRegPow ε N p (min (max (u x) 0) N) := by  -- moserRegPowerCutoffWitness = hwComp.mul_smooth_bounded η  -- mul_smooth_bounded.weakGrad x i = η x * hw.weakGrad x i + ∂ᵢη(x) * u(x)  -- This is definitionally true by the construction.  set_option maxHeartbeats 400000 in  simp only [moserRegPowerCutoffWitness, MemW1pWitness.mul_smooth_bounded,    moserRegClippedPosPartWitness, WithLp.ofLp_add, WithLp.ofLp_smul,    smul_eq_mul, Pi.add_apply, Pi.smul_apply]