zetaDelta

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

Hide file tree

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