fix

leanprover-community · Feb 11, 2025 · ca24083 · ca24083
1 parent 2a2caee
commit ca24083
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/NumberTheory/Mertens.lean b/Mathlib/NumberTheory/Mertens.lean
@@ -611,7 +611,7 @@ theorem integrableOn_Ici_fun_mul_E₁ (t : ℝ) (ht : 1 < t) :
     measurableSet_Ici
   have := isBigO.integrableAtFilter («μ» := volume) (mul_E₁_measurable.stronglyMeasurable.stronglyMeasurableAtFilter)
     (integrable_inv_mul_log_inv_sq t ht).integrableAtFilter
-  rw [integrableAtFilter_principal_iff] at this
+  rw [_root_.integrableAtFilter_principal_iff] at this
   exact this
 
 theorem integral_mul_E₁_eq_const_sub_integral (x a : ℝ) (ha : 1 < a) (hx : a ≤ x) :