fix: don't zeta-expand in filter_upwards (#7213)

leanprover-community · Sep 17, 2023 · 1937612 · 1937612
1 parent 8b0612f
commit 1937612
Show file tree

Hide file tree

Showing 5 changed files with 4 additions and 2 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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