Fundamental theorem of variational calculus

lemma fundamental_theorem_of_variational_calculus {f : X → V}    (μ : Measure X) [IsFiniteMeasureOnCompacts μ] [μ.IsOpenPosMeasure]    [OpensMeasurableSpace X]    (hf : IsTestFunction f) (hg : ∀ g, IsTestFunction g → ∫ x, ⟪f x, g x⟫_ℝ ∂μ = 0) :    f = 0 := by  have hf' := hg f hf  rw [MeasureTheory.integral_eq_zero_iff_of_nonneg] at hf'  · rw [Continuous.ae_eq_iff_eq] at hf'    · funext x      have hf'' := congrFun hf' x      simpa using hf''    · have hf : Continuous f := hf.smooth.continuous      fun_prop    · fun_prop  · intro x    simp only [Pi.zero_apply]    apply real_inner_self_nonneg'  · apply IsTestFunction.integrable    exact IsTestFunction.inner hf hf