zetaDelta

Mathlib/CategoryTheory/Abelian/NonPreadditive.lean

@@ -117,7 +117,7 @@ instance : Epi (Abelian.factorThruImage f) :=
     calc
       f ≫ h = (p ≫ i) ≫ h := (Abelian.image.fac f).symm ▸ rfl
       _ = ((t ≫ kernel.ι g) ≫ i) ≫ h := ht ▸ rfl
-      _ = t ≫ u ≫ h := by simp only [u, Category.assoc]
+      _ = t ≫ u ≫ h := by simp +zetaDelta only [u, Category.assoc]
       _ = t ≫ 0 := hu.w ▸ rfl
       _ = 0 := HasZeroMorphisms.comp_zero _ _
   -- h factors through the cokernel of f via some l.
@@ -153,7 +153,7 @@ instance : Mono (Abelian.factorThruCoimage f) :=
       calc
         h ≫ f = h ≫ p ≫ i := (Abelian.coimage.fac f).symm ▸ rfl
         _ = h ≫ p ≫ cokernel.π g ≫ t := ht ▸ rfl
-        _ = h ≫ u ≫ t := by simp only [u, Category.assoc]
+        _ = h ≫ u ≫ t := by simp +zetaDelta only [u, Category.assoc]
         _ = 0 ≫ t := by rw [← Category.assoc, hu.w]
         _ = 0 := zero_comp
     -- h factors through the kernel of f via some l.

Mathlib/CategoryTheory/GradedObject/Trifunctor.lean

@@ -345,7 +345,7 @@ noncomputable def isColimitCofan₃MapBifunctor₁₂BifunctorMapObj (j : J) :
   refine IsColimit.ofIsoColimit (isColimitCofanMapObjComp Z p' ρ₁₂.q r ρ₁₂.hpq j
     (fun ⟨i₁₂, i₃⟩ h => c₁₂'' ⟨⟨i₁₂, i₃⟩, h⟩) (fun ⟨i₁₂, i₃⟩ h => h₁₂'' ⟨⟨i₁₂, i₃⟩, h⟩) c hc)
     (Cocones.ext (Iso.refl _) (fun ⟨⟨i₁, i₂, i₃⟩, h⟩ => ?_))
-  dsimp [Cofan.inj, c₁₂'', Z]
+  dsimp +zetaDelta [Cofan.inj, c₁₂'', Z]
   rw [comp_id, Functor.map_id, id_comp]
   rfl
 
@@ -523,7 +523,7 @@ noncomputable def isColimitCofan₃MapBifunctorBifunctor₂₃MapObj (j : J) :
   refine IsColimit.ofIsoColimit (isColimitCofanMapObjComp Z p' ρ₂₃.q r ρ₂₃.hpq j
     (fun ⟨i₁, i₂₃⟩ h => c₂₃'' ⟨⟨i₁, i₂₃⟩, h⟩) (fun ⟨i₁, i₂₃⟩ h => h₂₃'' ⟨⟨i₁, i₂₃⟩, h⟩) c hc)
     (Cocones.ext (Iso.refl _) (fun ⟨⟨i₁, i₂, i₃⟩, h⟩ => ?_))
-  dsimp [Cofan.inj, c₂₃'']
+  dsimp +zetaDelta [Cofan.inj, c₂₃'']
   rw [comp_id, id_comp]
   rfl
 

Mathlib/CategoryTheory/Limits/Constructions/LimitsOfProductsAndEqualizers.lean

@@ -166,19 +166,19 @@ lemma preservesLimit_of_preservesEqualizers_and_product :
     let I := equalizer s t
     let i : I ⟶ P := equalizer.ι s t
     apply preservesLimit_of_preserves_limit_cone
-        (buildIsLimit s t (by simp [s]) (by simp [t]) (limit.isLimit _) (limit.isLimit _)
-          (limit.isLimit _))
+        (buildIsLimit s t (by simp +zetaDelta [s]) (by simp +zetaDelta [t]) (limit.isLimit _)
+          (limit.isLimit _) (limit.isLimit _))
     apply IsLimit.ofIsoLimit (buildIsLimit _ _ _ _ _ _ _) _
     · exact Fan.mk _ fun j => G.map (Pi.π _ j)
     · exact Fan.mk (G.obj Q) fun f => G.map (Pi.π _ f)
     · apply G.map s
     · apply G.map t
     · intro f
-      dsimp [s, Fan.mk]
+      dsimp +zetaDelta [s, Fan.mk]
       simp only [← G.map_comp, limit.lift_π]
       congr
     · intro f
-      dsimp [t, Fan.mk]
+      dsimp +zetaDelta [t, Fan.mk]
       simp only [← G.map_comp, limit.lift_π]
       apply congrArg G.map
       dsimp
@@ -191,7 +191,7 @@ lemma preservesLimit_of_preservesEqualizers_and_product :
     · apply isLimitForkMapOfIsLimit
       apply equalizerIsEqualizer
     · refine Cones.ext (Iso.refl _) ?_
-      intro j; dsimp; simp
+      intro j; dsimp +zetaDelta ; simp
 -- See note [dsimp, simp].
 
 end
@@ -382,8 +382,8 @@ lemma preservesColimit_of_preservesCoequalizers_and_coproduct :
     let I := coequalizer s t
     let i : P ⟶ I := coequalizer.π s t
     apply preservesColimit_of_preserves_colimit_cocone
-        (buildIsColimit s t (by simp [s]) (by simp [t]) (colimit.isColimit _) (colimit.isColimit _)
-          (colimit.isColimit _))
+        (buildIsColimit s t (by simp +zetaDelta [s]) (by simp +zetaDelta [t]) (colimit.isColimit _)
+          (colimit.isColimit _) (colimit.isColimit _))
     apply IsColimit.ofIsoColimit (buildIsColimit _ _ _ _ _ _ _) _
     · refine Cofan.mk (G.obj Q) fun j => G.map ?_
       apply Sigma.ι _ j
@@ -392,11 +392,11 @@ lemma preservesColimit_of_preservesCoequalizers_and_coproduct :
     · apply G.map s
     · apply G.map t
     · intro f
-      dsimp [s, Cofan.mk]
+      dsimp +zetaDelta [s, Cofan.mk]
       simp only [← G.map_comp, colimit.ι_desc]
       congr
     · intro f
-      dsimp [t, Cofan.mk]
+      dsimp +zetaDelta [t, Cofan.mk]
       simp only [← G.map_comp, colimit.ι_desc]
       dsimp
     · refine Cofork.ofπ (G.map i) ?_
@@ -409,7 +409,7 @@ lemma preservesColimit_of_preservesCoequalizers_and_coproduct :
       apply coequalizerIsCoequalizer
     refine Cocones.ext (Iso.refl _) ?_
     intro j
-    dsimp
+    dsimp +zetaDelta
     simp
 -- See note [dsimp, simp].
 

Mathlib/CategoryTheory/Limits/VanKampen.lean

@@ -352,7 +352,7 @@ theorem IsUniversalColimit.map_reflective
     · intro j
       rw [← Category.assoc, Iso.comp_inv_eq]
       ext
-      all_goals simp only [PreservesPullback.iso_hom_fst, PreservesPullback.iso_hom_snd,
+      all_goals simp +zetaDelta only [PreservesPullback.iso_hom_fst, PreservesPullback.iso_hom_snd,
           pullback.lift_fst, pullback.lift_snd, Category.assoc,
           Functor.mapCocone_ι_app, ← Gl.map_comp]
       · rw [IsIso.comp_inv_eq, adj.counit_naturality]
@@ -363,7 +363,8 @@ theorem IsUniversalColimit.map_reflective
         rw [Category.comp_id, Category.assoc]
   have :
       cf.hom ≫ (PreservesPullback.iso _ _ _).hom ≫ pullback.fst _ _ ≫ adj.counit.app _ = 𝟙 _ := by
-    simp only [IsIso.inv_hom_id, Iso.inv_hom_id_assoc, Category.assoc, pullback.lift_fst_assoc]
+    simp +zetaDelta only [IsIso.inv_hom_id, Iso.inv_hom_id_assoc, Category.assoc,
+      pullback.lift_fst_assoc]
   have : IsIso cf := by
     apply @Cocones.cocone_iso_of_hom_iso (i := ?_)
     rw [← IsIso.eq_comp_inv] at this
@@ -373,12 +374,12 @@ theorem IsUniversalColimit.map_reflective
   · exact ⟨IsColimit.precomposeHomEquiv β c' <|
       (isColimitOfPreserves Gl Hc'').ofIsoColimit (asIso cf).symm⟩
   · ext j
-    dsimp
+    dsimp +zetaDelta
     simp only [Category.comp_id, Category.id_comp, Category.assoc,
       Functor.map_comp, pullback.lift_snd]
   · intro j
     apply IsPullback.of_right _ _ (IsPullback.of_hasPullback _ _)
-    · dsimp [α']
+    · dsimp +zetaDelta [α']
       simp only [Category.comp_id, Category.id_comp, Category.assoc, Functor.map_comp,
         pullback.lift_fst]
       rw [← Category.comp_id (Gr.map f)]
@@ -390,7 +391,7 @@ theorem IsUniversalColimit.map_reflective
       dsimp
       simp only [Category.comp_id, Adjunction.right_triangle_components, Category.id_comp,
         Category.assoc]
-    · dsimp
+    · dsimp +zetaDelta
       simp only [Category.comp_id, Category.id_comp, Category.assoc, Functor.map_comp,
         pullback.lift_snd]
 
@@ -506,7 +507,7 @@ theorem BinaryCofan.isVanKampen_iff (c : BinaryCofan X Y) :
     have : F' = pair X' Y' := by
       apply Functor.hext
       · rintro ⟨⟨⟩⟩ <;> rfl
-      · rintro ⟨⟨⟩⟩ ⟨j⟩ ⟨⟨rfl : _ = j⟩⟩ <;> simp
+      · rintro ⟨⟨⟩⟩ ⟨j⟩ ⟨⟨rfl : _ = j⟩⟩ <;> simp +zetaDelta
     clear_value X' Y'
     subst this
     change BinaryCofan X' Y' at c'

Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean

@@ -385,9 +385,9 @@ noncomputable def Hom.comp {X Y Z : C} (z₁ : Hom W X Y) (z₂ : Hom W Y Z) : H
       obtain ⟨Z, u, hu, fac₃⟩ := HasLeftCalculusOfFractions.ext _ _ _ a₁.hs eq
       simp only [assoc] at fac₃
       refine ⟨Z, w₁.s ≫ u, u, ?_, ?_, ?_⟩
-      · dsimp
+      · dsimp +zetaDelta
         simp only [assoc]
-      · dsimp
+      · dsimp +zetaDelta
         simp only [assoc, fac₃]
       · dsimp
         simp only [assoc]
@@ -401,21 +401,21 @@ noncomputable def Hom.comp {X Y Z : C} (z₁ : Hom W X Y) (z₂ : Hom W Y Z) : H
       obtain ⟨Z, u, hu, fac₄⟩ := HasLeftCalculusOfFractions.ext _ _ _ a₁.hs eq
       simp only [assoc] at fac₄
       refine ⟨Z, q.f ≫ u, q.s ≫ u, ?_, ?_, ?_⟩
-      · simp only [assoc, reassoc_of% fac₃]
+      · simp +zetaDelta only [assoc, reassoc_of% fac₃]
       · rw [assoc, assoc, assoc, assoc, fac₄, reassoc_of% hft]
-      · simp only [assoc, ← reassoc_of% fac₃]
+      · simp +zetaDelta only [assoc, ← reassoc_of% fac₃]
         exact W.comp_mem _ _ b.hs (W.comp_mem _ _ z₂.hs
           (W.comp_mem _ _ w₂.hs (W.comp_mem _ _ q.hs hu)))
     · have eq : a₂.s ≫ z₂.f ≫ w₂.s = a₂.s ≫ t₂ ≫ w₂.f := by
         rw [← fac₂', reassoc_of% fac₂]
       obtain ⟨Z, u, hu, fac₄⟩ := HasLeftCalculusOfFractions.ext _ _ _ a₂.hs eq
       simp only [assoc] at fac₄
       refine ⟨Z, u, w₂.s ≫ u, ?_, ?_, ?_⟩
-      · dsimp
+      · dsimp +zetaDelta
         simp only [assoc]
-      · dsimp
+      · dsimp +zetaDelta
         simp only [assoc, fac₄]
-      · dsimp
+      · dsimp +zetaDelta
         simp only [assoc]
         exact W.comp_mem _ _ b.hs (W.comp_mem _ _ z₂.hs (W.comp_mem _ _ w₂.hs hu))
 

Mathlib/CategoryTheory/Localization/DerivabilityStructure/Constructor.lean

@@ -92,9 +92,9 @@ lemma isConnected :
   refine Zigzag.trans ?_ (Zigzag.trans this ?_)
   · exact Zigzag.of_hom (eqToHom (by aesop))
   · apply Zigzag.of_inv
-    refine CostructuredArrow.homMk (StructuredArrow.homMk ρ.X₁.hom (by simp)) ?_
+    refine CostructuredArrow.homMk (StructuredArrow.homMk ρ.X₁.hom (by simp +zetaDelta)) ?_
     ext
-    dsimp
+    dsimp +zetaDelta
     rw [← cancel_epi (isoOfHom L W₂ ρ.w.left ρ.hw.1).hom, isoOfHom_hom,
       isoOfHom_hom_inv_id_assoc, ← L.map_comp_assoc, Arrow.w_mk_right, Arrow.mk_hom,
       L.map_comp, assoc, isoOfHom_hom_inv_id_assoc, fac]

Mathlib/CategoryTheory/Monoidal/Mon_.lean

@@ -519,10 +519,10 @@ instance monMonoidalStruct : MonoidalCategoryStruct (Mon_ C) :=
       tensorObj _ _ ⟶ tensorObj _ _ :=
     { hom := f.hom ⊗ g.hom
       one_hom := by
-        dsimp
+        dsimp +zetaDelta
         slice_lhs 2 3 => rw [← tensor_comp, Hom.one_hom f, Hom.one_hom g]
       mul_hom := by
-        dsimp
+        dsimp +zetaDelta
         slice_rhs 1 2 => rw [tensorμ_natural]
         slice_lhs 2 3 => rw [← tensor_comp, Hom.mul_hom f, Hom.mul_hom g, tensor_comp]
         simp only [Category.assoc] }

Mathlib/CategoryTheory/MorphismProperty/Limits.lean

@@ -252,7 +252,7 @@ lemma IsStableUnderProductsOfShape.mk (J : Type*)
     (IsLimit.conePointUniqueUpToIso hc₂ (limit.isLimit X₂) ≪≫ (Pi.isoLimit _).symm) ?_
   apply limit.hom_ext
   rintro ⟨j⟩
-  simp
+  simp +zetaDelta
 
 /-- The condition that a property of morphisms is stable by finite products. -/
 class IsStableUnderFiniteProducts : Prop where

Mathlib/CategoryTheory/Sites/CoverLifting.lean

@@ -145,7 +145,7 @@ lemma liftAux_map {Y : C} (f : G.obj Y ⟶ X) {W : C} (g : W ⟶ Y) (i : S.Arrow
             { g₁ := 𝟙 _
               g₂ := h
               w := by simpa using w.symm }
-        simpa using s.condition r )
+        simpa +zetaDelta using s.condition r )
 
 lemma liftAux_map' {Y Y' : C} (f : G.obj Y ⟶ X) (f' : G.obj Y' ⟶ X) {W : C}
     (a : W ⟶ Y) (b : W ⟶ Y') (w : G.map a ≫ f = G.map b ≫ f') :

Mathlib/Combinatorics/Hall/Finite.lean

@@ -109,7 +109,8 @@ theorem hall_hard_inductive_step_A {n : ℕ} (hn : Fintype.card ι = n + 1)
     have key : ∀ {x}, y ≠ f' x := by
       intro x h
       simpa [t', ← h] using hfr x
-    by_cases h₁ : z₁ = x <;> by_cases h₂ : z₂ = x <;> simp [h₁, h₂, hfinj.eq_iff, key, key.symm]
+    by_cases h₁ : z₁ = x <;> by_cases h₂ : z₂ = x <;>
+      simp +zetaDelta [h₁, h₂, hfinj.eq_iff, key, key.symm]
   · intro z
     simp only [ne_eq, Set.mem_setOf_eq]
     split_ifs with hz

Mathlib/Data/Fintype/Card.lean

@@ -1100,7 +1100,7 @@ theorem List.exists_pw_disjoint_with_card {α : Type*} [Fintype α]
     intro a ha
     conv_rhs => rw [← List.map_id a]
     rw [List.map_pmap]
-    simp only [Fin.valEmbedding_apply, Fin.val_mk, List.pmap_eq_map, List.map_id', List.map_id]
+    simp +zetaDelta [Fin.valEmbedding_apply, Fin.val_mk, List.pmap_eq_map, List.map_id']
   use l.map (List.map (Fintype.equivFin α).symm)
   constructor
   · -- length

Mathlib/Logic/Denumerable.lean

@@ -242,7 +242,7 @@ theorem ofNat_surjective_aux : ∀ {x : ℕ} (hx : x ∈ s), ∃ n, ofNat s n =
         (fun (y : ℕ) (hy : y ∈ s) => ⟨y, hy⟩)
         (by intros a ha; simpa using (List.mem_filter.mp ha).2) with ht
     have hmt : ∀ {y : s}, y ∈ t ↔ y < ⟨x, hx⟩ := by
-      simp [List.mem_filter, Subtype.ext_iff_val, ht]
+      simp +zetaDelta [List.mem_filter, Subtype.ext_iff_val, ht]
     have wf : ∀ m : s, List.maximum t = m → ↑m < x := fun m hmax => by
       simpa using hmt.mp (List.maximum_mem hmax)
     cases' hmax : List.maximum t with m

Mathlib/Order/Filter/Basic.lean

@@ -533,7 +533,7 @@ theorem iInf_sets_eq {f : ι → Filter α} (h : Directed (· ≥ ·) f) [ne : N
         exact ⟨c, inter_mem (ha hx) (hb hy)⟩ }
   have : u = iInf f := eq_iInf_of_mem_iff_exists_mem mem_iUnion
   -- Porting note: it was just `congr_arg filter.sets this.symm`
-  (congr_arg Filter.sets this.symm).trans <| by simp only
+  (congr_arg Filter.sets this.symm).trans <| by simp +zetaDelta only
 
 theorem mem_iInf_of_directed {f : ι → Filter α} (h : Directed (· ≥ ·) f) [Nonempty ι] (s) :
     s ∈ iInf f ↔ ∃ i, s ∈ f i := by

Mathlib/RingTheory/Nilpotent/Defs.lean

@@ -132,7 +132,7 @@ lemma nilpotencyClass_eq_succ_iff {k : ℕ} :
     nilpotencyClass x = k + 1 ↔ x ^ (k + 1) = 0 ∧ x ^ k ≠ 0 := by
   let s : Set ℕ := {k | x ^ k = 0}
   have : ∀ k₁ k₂ : ℕ, k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s := fun k₁ k₂ h_le hk₁ ↦ pow_eq_zero_of_le h_le hk₁
-  simp [s, nilpotencyClass, Nat.sInf_upward_closed_eq_succ_iff this]
+  simp +zetaDelta [s, nilpotencyClass, Nat.sInf_upward_closed_eq_succ_iff this]
 
 @[simp] lemma nilpotencyClass_zero [Nontrivial R] :
     nilpotencyClass (0 : R) = 1 :=