Fix the build.

leanprover-community · Mar 16, 2024 · 5e724fb · 5e724fb
1 parent 7ed9c10
commit 5e724fb
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/Mathlib/Geometry/Manifold/IntegralCurve.lean b/Mathlib/Geometry/Manifold/IntegralCurve.lean
@@ -397,7 +397,7 @@ theorem isIntegralCurveAt_eventuallyEq_of_contMDiffAt (hγt₀ : I.IsInteriorPoi
   have hdrv {g} (hg : IsIntegralCurveAt g v t₀) (h' : γ t₀ = g t₀) : ∀ᶠ t in 𝓝 t₀,
       HasDerivAt ((extChartAt I (g t₀)) ∘ g) ((fun _ ↦ v') t (((extChartAt I (g t₀)) ∘ g) t)) t ∧
       ((extChartAt I (g t₀)) ∘ g) t ∈ (fun _ ↦ s) t := by
-    filter_upwards
+    apply Filter.Eventually.and
     · apply (hsrc hg |>.and hg.eventually_hasDerivAt).mono
       rintro t ⟨ht1, ht2⟩
       rw [hv', h']

diff --git a/Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean b/Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
@@ -199,7 +199,7 @@ theorem rnDeriv_restrict (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν]
   · filter_upwards with x
     simp only [Set.indicator_apply, Pi.one_apply, ne_eq]
     split_ifs <;> simp [ENNReal.zero_ne_top]
-  · filter_upwards with x using simp [Set.indicator_apply]
+  · filter_upwards with x; simp [Set.indicator_apply]
 
 lemma rnDeriv_eq_zero_of_mutuallySingular [SigmaFinite μ] {ν' : Measure α}
     [SigmaFinite ν'] (h : μ ⟂ₘ ν) (hνν' : ν ≪ ν') :