Mem W1p Witness weak Grad ae eq zero on zero Set

theorem MemW1pWitness.weakGrad_ae_eq_zero_on_zeroSet    {Ω : Set E} (hΩ : IsOpen Ω) {u : E → ℝ}    (hw : MemW1pWitness 2 u Ω) :    ∀ i : Fin d, ∀ᵐ x ∂(volume.restrict Ω), u x = 0 → hw.weakGrad x i = 0 := by  intro i  let uMk : E → ℝ := AEMeasurable.mk u hw.memLp.aemeasurable  have hu_meas : Measurable uMk := hw.memLp.aemeasurable.measurable_mk  have hu_ae : u =ᵐ[volume.restrict Ω] uMk := hw.memLp.aemeasurable.ae_eq_mk  have hGMk :      ∀ j : Fin d, HasWeakPartialDeriv' (d := d) j (fun x => hw.weakGrad x j) uMk Ω := by    intro j    exact stampacchia_congr_ae      (HasWeakPartialDeriv.toStampacchia (hw.isWeakGrad j)) hu_ae  have huMk_memW1p : MemW1p 2 uMk Ω := by    refine ⟨hw.memLp.ae_eq hu_ae, ?_⟩    intro j    exact ⟨fun x => hw.weakGrad x j, hw.weakGrad_component_memLp j, by      simpa [HasWeakPartialDeriv'] using hGMk j⟩  have hzero_mk :      ∀ᵐ x ∂(volume.restrict Ω), uMk x = 0 → hw.weakGrad x i = 0 :=    DeGiorgi.weakGrad_ae_eq_zero_on_zeroSet hΩ huMk_memW1p hGMk i      (hw.weakGrad_component_memLp i) hu_meas  filter_upwards [hu_ae, hzero_mk] with x hx hzero hx_zero  exact hzero (by simpa [hx] using hx_zero)