Is Open ae eq of integral cont Diff smul eq

lemma IsOpen.ae_eq_of_integral_contDiff_smul_eq {d : ℕ+} {U : Set (Fin d → ℝ)} {hU : IsOpen U}  {f : (Fin d → ℝ) →ₘ[μU d U] ℝ} {g : (Fin d → ℝ) →ₘ[μU d U] ℝ}  {hf : LocallyIntegrableOn f U volume}  {hg : LocallyIntegrableOn g U volume}  (h : ∀ ψ : (Fin d → ℝ) → ℝ, ψ ∈ Cc_inftyU d U →      ∫ x, ψ x • (f : (Fin d → ℝ) → ℝ) x ∂volume    = ∫ x, ψ x • (g : (Fin d → ℝ) → ℝ) x ∂volume)  : f =ᵐ[μU d U] g := by     have : ∀ᵐ (x : Fin ↑d → ℝ), x ∈ U → f x - g x = 0 := by      apply IsOpen.ae_eq_zero_of_integral_contDiff_smul_eq_zero hU (hf.sub hg)      intro ψ ψ_diff ψ_comp ψ_supp      have Cc_psi : ψ ∈ Cc_inftyU d U := by exact ⟨ψ_comp, ψ_supp, ψ_diff⟩      simp only [Pi.sub_apply, smul_sub]       rw [integral_sub, sub_eq_zero]      · exact h ψ Cc_psi      · exact IntMulLocalintComp U hf ψ_comp ψ_supp ψ_diff.continuous      · exact IntMulLocalintComp U hg ψ_comp ψ_supp ψ_diff.continuous     show f =ᵐ[volume.restrict U] g    rw [Filter.EventuallyEq, ae_restrict_iff' hU.measurableSet]    filter_upwards [this] with x hx    simpa [sub_eq_zero] using hx