From 8964f4917ccd1c51c8a05671cb0eb606352bc42c Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 22 Nov 2024 10:31:26 +1100 Subject: [PATCH] zetaDelta --- Mathlib/CategoryTheory/Sites/Over.lean | 2 +- Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/CategoryTheory/Sites/Over.lean b/Mathlib/CategoryTheory/Sites/Over.lean index f012575ed625c..dbfa56a73efc0 100644 --- 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 index 0a63d44706834..121d811d99d2a 100644 --- 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 =>