Has Weak Partial Deriv ae eq

theorem HasWeakPartialDeriv.ae_eq {Ω : Set E} (hΩ : IsOpen Ω)    {i : Fin d} {g₁ g₂ f : E → ℝ}    (h1 : HasWeakPartialDeriv i g₁ f Ω) (h2 : HasWeakPartialDeriv i g₂ f Ω)    (hg₁ : LocallyIntegrable g₁ (volume.restrict Ω))    (hg₂ : LocallyIntegrable g₂ (volume.restrict Ω)) :    g₁ =ᵐ[volume.restrict Ω] g₂ := by  suffices h : ∀ᵐ x ∂(volume.restrict Ω), (g₁ - g₂) x = 0 by    filter_upwards [h] with x hx    simp [sub_eq_zero] at hx    exact hx  rw [ae_restrict_iff' hΩ.measurableSet]  apply IsOpen.ae_eq_zero_of_integral_contDiff_smul_eq_zero hΩ  · exact locallyIntegrableOn_of_locallyIntegrable_restrict (hg₁.sub hg₂)  · intro φ hφ hφ_supp hφ_tsupport    have eq1 := h1 φ hφ hφ_supp hφ_tsupport    have eq2 := h2 φ hφ hφ_supp hφ_tsupport    have h_eq : ∫ x in Ω, g₁ x * φ x = ∫ x in Ω, g₂ x * φ x := by      linarith    have h_zero : ∀ x, x ∉ Ω → φ x • (g₁ - g₂) x = 0 := by      intro x hx      have hφx : φ x = 0 := by        by_contra h        exact hx (hφ_tsupport (subset_tsupport _ h))      simp [hφx]    rw [← setIntegral_eq_integral_of_forall_compl_eq_zero h_zero]    simp_rw [Pi.sub_apply, smul_eq_mul, mul_sub]    rw [integral_sub]    · simp_rw [mul_comm (φ _)]      linarith    ·      have : Integrable (fun x => φ x • g₁ x) (volume.restrict Ω) :=        hg₁.integrable_smul_left_of_hasCompactSupport hφ.continuous hφ_supp      simpa [smul_eq_mul] using this    ·      have : Integrable (fun x => φ x • g₂ x) (volume.restrict Ω) :=        hg₂.integrable_smul_left_of_hasCompactSupport hφ.continuous hφ_supp      simpa [smul_eq_mul] using this