Zero Weakmulti Deriv U

lemma zeroWeakmultiDerivU {d : ℕ+} {n : ℕ} (U : Set (Fin d → ℝ)) (hU : IsOpen U)    (s : Fin n → Fin d) :    ∃ h : HasWeakMultiDerivU U (0 : Lp_locU d 1 U) s,      WeakmultiderivU U (0 : Lp_locU d 1 U) s h      =ᵐ[μU d U] (0 : (Fin d → ℝ) →ₘ[μU d U] ℝ) := by    classical    have hzero : IsWeakMultiDerivU U s (0 : Lp_locU d 1 U) 0 := by        rw [isWeakMultiDerivU_iff]        intro ψ hψ        have h0_ae : ∀ᵐ x ∂μU d U, ((0 : Lp_locU d 1 U) : (Fin d → ℝ) → ℝ) x = 0 := by          rw [show ((0 : Lp_locU d 1 U) : (Fin d → ℝ) →ₘ[μU d U] ℝ) = 0 from rfl,              show (0 : (Fin d → ℝ) →ₘ[μU d U] ℝ) =                  AEEqFun.mk 0 aestronglyMeasurable_zero from rfl]          exact AEEqFun.coeFn_mk 0 aestronglyMeasurable_zero        rw [integral_eq_zero_of_ae (h0_ae.mono fun x hx => by rw [hx, zero_smul, Pi.zero_apply]),            integral_eq_zero_of_ae (h0_ae.mono fun x hx => by rw [hx, smul_zero, Pi.zero_apply]),          smul_zero]    let h0 : HasWeakMultiDerivU U (0 : Lp_locU d 1 U) s := ⟨0, hzero⟩    exact ⟨h0, WeakmultiderivU_unique hU s 0 h0 0 hzero⟩