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.
leanprover-community · Jul 28, 2022 · 71d0115 · 71d0115
1 parent af21308
commit 71d0115
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 2 deletions.
diff --git a/src/measure_theory/tactic.lean b/src/measure_theory/tactic.lean
@@ -59,9 +59,7 @@ attribute [measurability]
   measurable_set.const
   measurable_set.insert
   measurable_set_eq
-  set.finite.measurable_set
   finset.measurable_set
-  set.countable.measurable_set
   measurable_space.measurable_set_top
 
 namespace tactic

diff --git a/test/measurability.lean b/test/measurability.lean
@@ -44,6 +44,12 @@ example (hf : measurable f) (hs₁ : measurable_set s₁) (ht₂ : measurable_se
   measurable_set ((f ⁻¹' t₂) ∩ s₁) :=
 by measurability
 
+/-- `ℝ` is a good test case because it verifies many assumptions, hence many lemmas apply and we
+are more likely to detect a bad lemma. In a previous version of the tactic, `measurability` got
+stuck trying to apply `set.finite.measurable_set` here. -/
+example {a b : ℝ} : measurable_set (set.Icc a b) :=
+by measurability
+
 -- Tests on functions
 
 example [has_mul β] [has_measurable_mul₂ β] (hf : measurable f) (c : β) :