From c1f091842f81be83a37a10dad192dc9650f66ee5 Mon Sep 17 00:00:00 2001
From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com>
Date: Sat, 18 Feb 2023 19:32:38 +0900
Subject: [PATCH] minor generalizations (#848)

- fixes #846
- fixes #845
---
 CHANGELOG_UNRELEASED.md      |  5 +++++
 theories/lebesgue_integral.v | 14 +++++---------
 theories/measure.v           |  2 +-
 3 files changed, 11 insertions(+), 10 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 23444475d..a738ad0ab 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -154,6 +154,11 @@
   + `xsection_preimage_snd`, `ysection_preimage_fst`
 - in `constructive_ereal.v`:
   + `oppeD`, `oppeB`
+- in `measure.v`:
+  + lemma `eq_measure`
+- in `lebesgue_integral.v`:
+  + lemma `integrable_abse`
+
 
 ### Deprecated
 
diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
index d96545c23..3c0ea3e2c 100644
--- a/theories/lebesgue_integral.v
+++ b/theories/lebesgue_integral.v
@@ -3781,14 +3781,11 @@ Local Open Scope ereal_scope.
 Context d (T : measurableType d) (R : realType).
 Variable (mu : {measure set T -> \bar R}).
 
-Lemma integrable_abse (D : set T) : measurable D ->
-  forall f : T -> \bar R, mu.-integrable D f -> mu.-integrable D (abse \o f).
+Lemma integrable_abse (D : set T) (f : T -> \bar R) :
+  mu.-integrable D f -> mu.-integrable D (abse \o f).
 Proof.
-move=> mD f [mf fi]; split; first exact: measurable_funT_comp.
-apply: le_lt_trans fi; apply: ge0_le_integral => //.
-- by apply: measurable_funT_comp => //; exact: measurable_funT_comp.
-- exact: measurable_funT_comp.
-- by move=> t Dt //=; rewrite abse_id.
+move=> [mf foo]; split; first exact: measurable_funT_comp.
+by under eq_integral do rewrite abse_id.
 Qed.
 
 Lemma integrable_summable (F : (set T)^nat) (g : T -> \bar R):
@@ -3799,8 +3796,7 @@ Proof.
 move=> tF mF fi.
 rewrite /summable -(_ : [set _ | true] = setT); last exact/seteqP.
 rewrite -nneseries_esum//.
-case: (fi) => _; rewrite ge0_integral_bigcup//; last first.
-  by apply: integrable_abse => //; exact: bigcup_measurable.
+case: (fi) => _; rewrite ge0_integral_bigcup//; last exact: integrable_abse.
 apply: le_lt_trans; apply: lee_lim.
 - exact: is_cvg_ereal_nneg_natsum_cond.
 - by apply: is_cvg_ereal_nneg_natsum_cond => n _ _; exact: integral_ge0.
diff --git a/theories/measure.v b/theories/measure.v
index 4ea753533..69e2a26f4 100644
--- a/theories/measure.v
+++ b/theories/measure.v
@@ -1518,7 +1518,7 @@ HB.instance Definition _ := isContent.Build d R T mu
 HB.instance Definition _ := isMeasure0.Build d R T mu measure_semi_sigma_additive.
 HB.end.
 
-Lemma eq_measure d (T : measurableType d) (R : realType)
+Lemma eq_measure d (T : measurableType d) (R : realFieldType)
   (m1 m2 : {measure set T -> \bar R}) :
   (m1 = m2 :> (set T -> \bar R)) -> m1 = m2.
 Proof.