mathlib3

aa6dc575 - chore(measure_theory/function/l1_space): drop `integrable.sub'` (#14309)

chore(measure_theory/function/l1_space): drop `integrable.sub'` (#14309) It used to have weaker TC assumptions than `integrable.sub` but now it's just a weaker version of it.