mathlib

25dded2d - chore(measure_theory/bochner_integration): make proofs shorter (#1871)

chore(measure_theory/bochner_integration): make proofs shorter (#1871) * More consistent use of the dot notation * Revert "More consistent use of the dot notation" This reverts commit 854a499a9be105b42ca486eb25593a2379b07404. * Revert "Revert "More consistent use of the dot notation"" This reverts commit 57aaf22695c031fc8dcc581110cc9d1ac397f695. * fix things Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>