zetaDelta

leanprover-community · Nov 21, 2024 · 8964f49 · 8964f49
1 parent b1016a1
commit 8964f49
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/Mathlib/CategoryTheory/Sites/Over.lean b/Mathlib/CategoryTheory/Sites/Over.lean
@@ -77,7 +77,7 @@ lemma overEquiv_pullback {X : C} {Y₁ Y₂ : Over X} (f : Y₁ ⟶ Y₂) (S : S
     let T := Over.mk (b ≫ W.hom)
     let c : T ⟶ Y₁ := Over.homMk g (by dsimp [T]; rw [← Over.w a, ← reassoc_of% w, Over.w f])
     let d : T ⟶ W := Over.homMk b
-    refine ⟨T, c, 𝟙 Z, ?_, by simp [c]⟩
+    refine ⟨T, c, 𝟙 Z, ?_, by simp +zetaDelta [c]⟩
     rw [show c ≫ f = d ≫ a by ext; exact w]
     exact S.downward_closed h _
 

diff --git a/Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean b/Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean
@@ -722,7 +722,7 @@ noncomputable def schroederBernstein {f : α → β} {g : β → α} (hf : Measu
     have : Aᶜ = g '' Bᶜ := by
       apply compl_injective
       rw [← Afp]
-      simp
+      simp +zetaDelta
     rw [this]
     exact (hg.equivImage _).symm
   have Fmono : ∀ {A B}, A ⊆ B → F A ⊆ F B := fun h =>