mathlib

71d01152 - chore(measure_theory/tactic): remove the measurability attribute from two lemmas (#15295)

chore(measure_theory/tactic): remove the measurability attribute from two lemmas (#15295) The measurability tactic applied `set.finite.measurable_set` to every set (when the space had measurable singletons) and got stuck.