mathlib3

206a5f77 - feat(measure_theory/integral/bochner): Add a rewrite lemma saying the ennreal coercion of an integral of a nonnegative function equals the lintegral of the ennreal coercion of the function. (#13701)

feat(measure_theory/integral/bochner): Add a rewrite lemma saying the ennreal coercion of an integral of a nonnegative function equals the lintegral of the ennreal coercion of the function. (#13701) This PR adds a rewrite lemma `of_real_integral_eq_lintegral_of_real` that is very similar to `lintegral_coe_eq_integral`, but for nonnegative real-valued functions instead of nnreal-valued functions. Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>