From 83668a24c77da62ea7268f9db1f1ede57a925854 Mon Sep 17 00:00:00 2001
From: Lorenzo Luccioli <lorenzoluccioli@gmail.com>
Date: Wed, 7 Aug 2024 13:39:18 +0200
Subject: [PATCH] bug fix

---
 TestingLowerBounds/CurvatureMeasure.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/TestingLowerBounds/CurvatureMeasure.lean b/TestingLowerBounds/CurvatureMeasure.lean
index 174278cc..f21db113 100644
--- a/TestingLowerBounds/CurvatureMeasure.lean
+++ b/TestingLowerBounds/CurvatureMeasure.lean
@@ -152,6 +152,7 @@ theorem convex_taylor (hf : ConvexOn ℝ univ f) (hf_cont : Continuous f) {a b :
   let g := StieltjesFunction.id + StieltjesFunction.const (-b)
   have hg : g = fun x ↦ x - b := rfl
   rw [← hg, integral_stieltjes_meas_by_parts g hf.rightDerivStieltjes]
+  swap; · rw [hg]; fun_prop
   simp only [Real.volume_eq_stieltjes_id, add_apply, id_apply, id_eq, const_apply, add_right_neg,
     zero_mul, zero_sub, measure_add, measure_const, add_zero, neg_sub, sub_neg_eq_add, g]
   rfl