diff --git a/src/measure_theory/tactic.lean b/src/measure_theory/tactic.lean
index c737dcc5ae7a7..195407aa7b0ee 100644
--- 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
index 9b874480962ca..c7b66ea22e345 100644
--- 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 : β) :