mathlib

2123bc38 - feat(measure_theory/measurable_space_def): add `generate_from_induction` (#15342)

feat(measure_theory/measurable_space_def): add `generate_from_induction` (#15342) This lemma does (almost?) the same thing as `induction (ht : measurable_set[generate_from C] t)`, but the hypotheses in the generated subgoals are much easier to read.