From 193761250a9869327056b499a7f49d676ed5e3a9 Mon Sep 17 00:00:00 2001 From: Patrick Massot Date: Sun, 17 Sep 2023 06:02:31 +0000 Subject: [PATCH] fix: don't zeta-expand in filter_upwards (#7213) --- Mathlib/MeasureTheory/Integral/FundThmCalculus.lean | 1 + Mathlib/Order/Filter/Basic.lean | 2 +- Mathlib/Probability/Independence/Kernel.lean | 1 - Mathlib/Probability/Martingale/Centering.lean | 1 + Mathlib/Topology/DenseEmbedding.lean | 1 + 5 files changed, 4 insertions(+), 2 deletions(-) diff --git a/Mathlib/MeasureTheory/Integral/FundThmCalculus.lean b/Mathlib/MeasureTheory/Integral/FundThmCalculus.lean index 0cc238a6d448e..0d752c284a518 100644 --- a/Mathlib/MeasureTheory/Integral/FundThmCalculus.lean +++ b/Mathlib/MeasureTheory/Integral/FundThmCalculus.lean @@ -1217,6 +1217,7 @@ theorem integral_eq_sub_of_hasDerivAt_of_tendsto (hab : a < b) {fa fb} have Fderiv : ∀ x ∈ Ioo a b, HasDerivAt F (f' x) x := by refine' fun x hx => (hderiv x hx).congr_of_eventuallyEq _ filter_upwards [Ioo_mem_nhds hx.1 hx.2] with _ hy + unfold_let F rw [update_noteq hy.2.ne, update_noteq hy.1.ne'] have hcont : ContinuousOn F (Icc a b) := by rw [continuousOn_update_iff, continuousOn_update_iff, Icc_diff_right, Ico_diff_left] diff --git a/Mathlib/Order/Filter/Basic.lean b/Mathlib/Order/Filter/Basic.lean index 58eb3fe079586..7c921125a2e84 100644 --- a/Mathlib/Order/Filter/Basic.lean +++ b/Mathlib/Order/Filter/Basic.lean @@ -266,7 +266,7 @@ elab_rules : tactic return [m.mvarId!] liftMetaTactic fun goal => do goal.apply (← mkConstWithFreshMVarLevels ``Filter.univ_mem') config - evalTactic <|← `(tactic| dsimp only [Set.mem_setOf_eq]) + evalTactic <|← `(tactic| dsimp (config := {zeta := false}) only [Set.mem_setOf_eq]) if let some l := wth then evalTactic <|← `(tactic| intro $[$l]*) if let some e := usingArg then diff --git a/Mathlib/Probability/Independence/Kernel.lean b/Mathlib/Probability/Independence/Kernel.lean index aa735dde46dc1..4437d42287b00 100644 --- a/Mathlib/Probability/Independence/Kernel.lean +++ b/Mathlib/Probability/Independence/Kernel.lean @@ -553,7 +553,6 @@ theorem iIndepSets.piiUnionInter_of_not_mem {π : ι → Set (Set Ω)} {a : ι} have has : a ∉ s := fun has_mem => haS (hs_mem has_mem) filter_upwards [h_μ_t1, h_μ_inter] with a' ha1 ha2 rw [ha2, Finset.prod_insert has, h_t2, mul_comm, ha1] - simp only [ite_true] /-- The measurable space structures generated by independent pi-systems are independent. -/ theorem iIndepSets.iIndep [IsMarkovKernel κ] (m : ι → MeasurableSpace Ω) diff --git a/Mathlib/Probability/Martingale/Centering.lean b/Mathlib/Probability/Martingale/Centering.lean index e7274e7cc878a..62f8a15682030 100644 --- a/Mathlib/Probability/Martingale/Centering.lean +++ b/Mathlib/Probability/Martingale/Centering.lean @@ -147,6 +147,7 @@ theorem martingalePart_add_ae_eq [SigmaFiniteFiltration μ ℱ] {f g : ℕ → (hf.integrable n).add <| hgint n) refine' (eventuallyEq_iff_sub.2 _).symm filter_upwards [hhmgle.eq_zero_of_predictable hhpred n] with ω hω + unfold_let h at hω rw [Pi.sub_apply] at hω rw [hω, Pi.sub_apply, martingalePart] simp [hg0] diff --git a/Mathlib/Topology/DenseEmbedding.lean b/Mathlib/Topology/DenseEmbedding.lean index 0c15cbf4162c6..4f0f5265292fd 100644 --- a/Mathlib/Topology/DenseEmbedding.lean +++ b/Mathlib/Topology/DenseEmbedding.lean @@ -201,6 +201,7 @@ theorem continuousAt_extend [T3Space γ] {b : β} {f : α → γ} (di : DenseInd have V₁_in : V₁ ∈ 𝓝 b := by filter_upwards [hf] rintro x ⟨c, hc⟩ + unfold_let φ rwa [di.extend_eq_of_tendsto hc] obtain ⟨V₂, V₂_in, V₂_op, hV₂⟩ : ∃ V₂ ∈ 𝓝 b, IsOpen V₂ ∧ ∀ x ∈ i ⁻¹' V₂, f x ∈ V' := by simpa [and_assoc] using