Gradient identification for a smooth representative

Extracted from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46, with shared dependency placement.

theorem Algsuperdiff.ae_eq_euclideanGradient_of_ae_eq_of_contDiff {d : ℕ} {U V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (hVU : V ⊆ U) [MeasureTheory.IsFiniteMeasure (HCPolySupport.volumeMeasureOn V)] (h : HCPolySupport.H1Function U) {v : HCPolySupport.Vec d → ℝ} (hv : ContDiff ℝ 1 v) (hae : v =ᵐ[MeasureTheory.volume.restrict V] h.toFun) : HCPolySupport.euclideanGradient v =ᵐ[MeasureTheory.volume.restrict V] h.grad

A C¹ representative has the weak gradient of the a.e.-equal H¹ function on an arbitrary open subdomain.