Mem W1p Witness ae eq p

theorem MemW1pWitness.ae_eq_p    {Ω : Set E} (hΩ : IsOpen Ω) {p : ℝ} (hp : 1 ≤ p) {f : E → ℝ}    (hw₁ hw₂ : MemW1pWitness (ENNReal.ofReal p) f Ω) :    hw₁.weakGrad =ᵐ[volume.restrict Ω] hw₂.weakGrad := by  let _ := (inferInstance : NeZero d)  have hp_enn : (1 : ℝ≥0∞) ≤ ENNReal.ofReal p := by    simpa using (ENNReal.ofReal_le_ofReal hp : ENNReal.ofReal (1 : ℝ) ≤ ENNReal.ofReal p)  have hcomp :      ∀ i : Fin d,        (fun x => hw₁.weakGrad x i) =ᵐ[volume.restrict Ω] (fun x => hw₂.weakGrad x i) := by    intro i    exact HasWeakPartialDeriv.ae_eq hΩ (hw₁.isWeakGrad i) (hw₂.isWeakGrad i)      ((hw₁.weakGrad_component_memLp i).locallyIntegrable hp_enn)      ((hw₂.weakGrad_component_memLp i).locallyIntegrable hp_enn)  filter_upwards [ae_all_iff.2 hcomp] with x hx  ext i  exact hx i