From b1016a12d4e5ea7ac2f6bfd996d695b591ad081c Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 22 Nov 2024 10:29:36 +1100 Subject: [PATCH] zetaDelta --- Mathlib/Algebra/Homology/ShortComplex/Abelian.lean | 5 +++-- Mathlib/CategoryTheory/Idempotents/FunctorCategories.lean | 4 ++-- Mathlib/CategoryTheory/Sites/CoverPreserving.lean | 2 +- Mathlib/Order/LiminfLimsup.lean | 6 +++--- 4 files changed, 9 insertions(+), 8 deletions(-) diff --git a/Mathlib/Algebra/Homology/ShortComplex/Abelian.lean b/Mathlib/Algebra/Homology/ShortComplex/Abelian.lean index 7bc3d040b42d2..93693ef267ac6 100644 --- a/Mathlib/Algebra/Homology/ShortComplex/Abelian.lean +++ b/Mathlib/Algebra/Homology/ShortComplex/Abelian.lean @@ -84,7 +84,8 @@ noncomputable def ofAbelian : S.LeftHomologyData := by IsLimit.conePointUniqueUpToIso_hom_comp _ _ WalkingParallelPair.zero have fac : f' = Abelian.factorThruImage S.f ≫ e.hom ≫ kernel.ι γ := by rw [hf', he] - simp only [f', kernel.lift_ι, abelianImageToKernel, ← cancel_mono (kernel.ι S.g), assoc] + simp +zetaDelta only [f', kernel.lift_ι, abelianImageToKernel, ← cancel_mono (kernel.ι S.g), + assoc] have hπ : IsColimit (CokernelCofork.ofπ _ wπ) := CokernelCofork.IsColimit.ofπ _ _ (fun x hx => cokernel.desc _ x (by @@ -150,7 +151,7 @@ noncomputable def ofAbelian : S.RightHomologyData := by IsColimit.comp_coconePointUniqueUpToIso_hom _ _ WalkingParallelPair.one have fac : g' = cokernel.π γ ≫ e.hom ≫ Abelian.factorThruCoimage S.g := by rw [hg', reassoc_of% he] - simp only [g', cokernel.π_desc, ← cancel_epi (cokernel.π S.f), + simp +zetaDelta only [g', cokernel.π_desc, ← cancel_epi (cokernel.π S.f), cokernel_π_comp_cokernelToAbelianCoimage_assoc] have hι : IsLimit (KernelFork.ofι _ wι) := KernelFork.IsLimit.ofι _ _ diff --git a/Mathlib/CategoryTheory/Idempotents/FunctorCategories.lean b/Mathlib/CategoryTheory/Idempotents/FunctorCategories.lean index aa1af4a9269f3..2559910722dc8 100644 --- a/Mathlib/CategoryTheory/Idempotents/FunctorCategories.lean +++ b/Mathlib/CategoryTheory/Idempotents/FunctorCategories.lean @@ -70,14 +70,14 @@ instance functor_category_isIdempotentComplete [IsIdempotentComplete C] : let e : F ⟶ Y := { app := fun j => equalizer.lift (p.app j) (by simpa only [comp_id] using (congr_app hp j).symm) - naturality := fun j j' φ => equalizer.hom_ext (by simp) } + naturality := fun j j' φ => equalizer.hom_ext (by simp +zetaDelta ) } use Y, i, e constructor · ext j dsimp rw [assoc, equalizer.lift_ι, ← equalizer.condition, id_comp, comp_id] · ext j - simp + simp +zetaDelta namespace KaroubiFunctorCategoryEmbedding variable {J C} diff --git a/Mathlib/CategoryTheory/Sites/CoverPreserving.lean b/Mathlib/CategoryTheory/Sites/CoverPreserving.lean index 54301e987ef0b..775d146a42705 100644 --- a/Mathlib/CategoryTheory/Sites/CoverPreserving.lean +++ b/Mathlib/CategoryTheory/Sites/CoverPreserving.lean @@ -132,7 +132,7 @@ theorem compatiblePreservingOfFlat {C : Type u₁} [Category.{v₁} C] {D : Type simp conv_lhs => rw [eq₁] conv_rhs => rw [eq₂] - simp only [op_comp, Functor.map_comp, types_comp_apply, eqToHom_op, eqToHom_map] + simp +zetaDelta only [op_comp, Functor.map_comp, types_comp_apply, eqToHom_op, eqToHom_map] apply congr_arg -- Porting note: was `congr 1` which for some reason doesn't do anything here -- despite goal being of the form f a = f b, with f=`ℱ.val.map (Quiver.Hom.op c'.pt.hom)` /- diff --git a/Mathlib/Order/LiminfLimsup.lean b/Mathlib/Order/LiminfLimsup.lean index 25404163646dc..50aad0fb2d80a 100644 --- a/Mathlib/Order/LiminfLimsup.lean +++ b/Mathlib/Order/LiminfLimsup.lean @@ -1462,7 +1462,7 @@ theorem HasBasis.liminf_eq_ciSup_ciInf {v : Filter ι} apply Subset.antisymm · apply iUnion_subset (fun j ↦ ?_) by_cases hj : j ∈ m - · have : j = liminf_reparam f s p j := by simp only [liminf_reparam, hj, ite_true] + · have : j = liminf_reparam f s p j := by simp +zetaDelta only [liminf_reparam, hj, ite_true] conv_lhs => rw [this] apply subset_iUnion _ j · simp only [m, mem_setOf_eq, ← nonempty_iInter_Iic_iff, not_nonempty_iff_eq_empty] at hj @@ -1475,8 +1475,8 @@ theorem HasBasis.liminf_eq_ciSup_ciInf {v : Filter ι} apply (Iic_ciInf _).symm change liminf_reparam f s p j ∈ m by_cases Hj : j ∈ m - · simpa only [liminf_reparam, if_pos Hj] using Hj - · simp only [liminf_reparam, if_neg Hj] + · simpa +zetaDelta only [liminf_reparam, if_pos Hj] using Hj + · simp +zetaDelta only [liminf_reparam, if_neg Hj] have Z : ∃ n, (exists_surjective_nat (Subtype p)).choose n ∈ m ∨ ∀ j, j ∉ m := by rcases (exists_surjective_nat (Subtype p)).choose_spec j0 with ⟨n, rfl⟩ exact ⟨n, Or.inl hj0⟩