use patch here?

[affeldt-aist]

analysis/theories/lebesgue_integral.v

Line 3420 in c518e2a

\int[mu]_(x in E `&` D) f x = \int[mu]_(x in E) (f x * (\1_D x)%:E).

i.e., f \_ D instead of f \* \1_ D ?

[affeldt-aist]

We went on to use f \_ D instead

analysis/theories/lebesgue_integral.v

Lines 3556 to 3557 in 0a9b2aa

	Lemma integralEpatch (D : set T) (mD : measurable D) (f : T -> \bar R) :
	\int[mu]_(x in D) f x = \int[mu]_(x in D) (f \_ D) x.

that felt more appropriate in practice when developing the corollary to the FTC1.