[#15109] test toolchain: stricter check for dsimp lemmas

batteries/Batteries/Data/Fin/Coding.lean

@@ -106,13 +106,15 @@ def encodeChar (c : Char) : Fin Char.count :=
   else
     Char.ofNatAux (i.val + (Char.maxSurrogate + 1 - Char.minSurrogate)) (by grind)
 
+set_option dsimp.resynthInstances false in
 @[simp] theorem encodeChar_decodeChar (x) : encodeChar (decodeChar x) = x := by
   simp only [decodeChar, encodeChar]
   split
   · simp [*]
   · have : ¬ x.val + (Char.maxSurrogate + 1 - Char.minSurrogate) < Char.minSurrogate := by grind
     simp [*]
 
+set_option dsimp.resynthInstances false in
 @[simp] theorem decodeChar_encodeChar (x) : decodeChar (encodeChar x) = x := by
   ext; simp only [decodeChar, encodeChar]
   split

batteries/Batteries/Data/Int.lean

@@ -42,6 +42,7 @@ def ofBits (f : Fin n → Bool) :=
   · have hlt := Nat.ofBits_lt_two_pow f
     simp [subNatNat_of_lt hlt, testBit, Nat.sub_sub, Nat.testBit_two_pow_sub_succ hlt, h]
 
+set_option dsimp.resynthInstances false in
 @[simp] theorem testBit_ofBits_ge {f : Fin n → Bool} (h : i ≥ n) :
     (ofBits f).testBit i = decide (ofBits f < 0) := by
   simp only [ofBits]

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2026-09-09
+leanprover/lean4-pr-releases:pr-release-15109-ae44bc8

mathlib4/Mathlib/Algebra/Category/AlgCat/FilteredColimits.lean

@@ -34,6 +34,7 @@ variable {c : Cocone (F ⋙ forget₂ _ RingCat)} [IsFilteredOrEmpty J]
 
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
+set_option dsimp.resynthInstances false in
 /-- (Implementation): The algebra instance on the cocone point of the underlying diagram of rings
 is induced from the `j`-th inclusion map. Any choice of `j` gives a propositionally equal algebra
 instance. -/

mathlib4/Mathlib/Algebra/Category/AlgCat/Limits.lean

@@ -70,6 +70,7 @@ instance limitAlgebra :
   inferInstanceAs <| Algebra R (Shrink (sectionsSubalgebra F))
 
 set_option backward.isDefEq.respectTransparency false in
+set_option dsimp.resynthInstances false in
 /-- `limit.π (F ⋙ forget (AlgCat R)) j` as an `AlgHom`. -/
 def limitπAlgHom (j) :
     (Types.Small.limitCone (F ⋙ forget (AlgCat R))).pt →ₐ[R]

mathlib4/Mathlib/Algebra/Category/AlgCat/TensorAlgebra.lean

@@ -37,6 +37,7 @@ variable (R : Type u) [CommRing R]
 
 set_option backward.isDefEq.respectTransparency false in
 set_option backward.defeqAttrib.useBackward true in
+set_option dsimp.resynthInstances false in
 /-- Taking the tensor algebra forms a left adjoint of the forgetful functor from `AlgCat R` to
 `ModuleCat R`. -/
 @[simps]

mathlib4/Mathlib/Algebra/Category/Grp/Colimits.lean

@@ -129,6 +129,7 @@ lemma quotToQuotUlift_ι [DecidableEq J] (j : J) (x : F.obj j) :
 
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
+set_option dsimp.resynthInstances false in
 /--
 The obvious additive map from `Quot (F ⋙ uliftFunctor.{u'})` to `Quot F`.
 -/

mathlib4/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean

@@ -75,6 +75,7 @@ open scoped MonObj
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 attribute [-instance] Functor.LaxMonoidal.comp Functor.Monoidal.instComp in
+set_option dsimp.resynthInstances false in
 /-- Implementation, see `leftExactFunctorForgetEquivalence`.
 This is the complicated bit, where we show that forgetting the group structure in the image of
 `F` and then reconstructing it recovers the group structure we started with. -/

mathlib4/Mathlib/Algebra/Category/ModuleCat/Differentials/Basic.lean

@@ -115,6 +115,7 @@ differential map `B → KaehlerDifferential f`. -/
 noncomputable abbrev d (b : B) : KaehlerDifferential f := (D f).d b
 
 set_option backward.isDefEq.respectTransparency false in
+set_option dsimp.resynthInstances false in
 @[ext]
 lemma ext {M : ModuleCat B} {α β : KaehlerDifferential f ⟶ M}
     (h : ∀ (b : B), α (d b) = β (d b)) : α = β := by

mathlib4/Mathlib/Algebra/Category/ModuleCat/Kernels.lean

@@ -44,6 +44,7 @@ def kernelIsLimit : IsLimit (kernelCone f) :=
 
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
+set_option dsimp.resynthInstances false in
 /-- Construct an `IsLimit` structure of kernels given `Function.Exact`. -/
 noncomputable
 def isLimitKernelFork (f : M ⟶ N) (g : N ⟶ P) (H : Function.Exact f.hom g.hom)

mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf.lean

@@ -213,6 +213,7 @@ lemma ofPresheaf_presheaf : (ofPresheaf M map_smul).presheaf = M := rfl
 end
 
 set_option backward.isDefEq.respectTransparency.types false in
+set_option dsimp.resynthInstances false in
 /-- The morphism of presheaves of modules `M₁ ⟶ M₂` given by a morphism
 of abelian presheaves `M₁.presheaf ⟶ M₂.presheaf`
 which satisfy a suitable linearity condition. -/

mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Free.lean

@@ -74,6 +74,7 @@ noncomputable def freeObjDesc (φ : F ⟶ G.presheaf ⋙ forget _) : freeObj F 
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 variable (F R) in
+set_option dsimp.resynthInstances false in
 /-- The unit of `PresheafOfModules.freeAdjunction`. -/
 @[simps]
 noncomputable def freeAdjunctionUnit : F ⟶ (freeObj (R := R) F).presheaf ⋙ forget _ where
@@ -82,6 +83,7 @@ noncomputable def freeAdjunctionUnit : F ⟶ (freeObj (R := R) F).presheaf ⋙ f
 
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
+set_option dsimp.resynthInstances false in
 /-- The bijection `(freeObj F ⟶ G) ≃ (F ⟶ G.presheaf ⋙ forget _)` when
 `F` is a presheaf of types and `G` a presheaf of modules. -/
 noncomputable def freeHomEquiv : (freeObj F ⟶ G) ≃ (F ⟶ G.presheaf ⋙ forget _) where
@@ -98,6 +100,7 @@ lemma free_hom_ext {ψ ψ' : freeObj F ⟶ G}
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 variable (R) in
+set_option dsimp.resynthInstances false in
 /-- The free presheaf of modules functor is left adjoint to the forget functor
 `PresheafOfModules.{u} R ⥤ Cᵒᵖ ⥤ Type u`. -/
 noncomputable def freeAdjunction :

mathlib4/Mathlib/Algebra/Category/ModuleCat/Topology/Basic.lean

@@ -412,6 +412,7 @@ def freeObj (X : TopCat.{v}) : TopModuleCat.{max v u} R :=
 lemma coe_freeObj (X : TopCat.{v}) : freeObj R X = (X →₀ R) := rfl
 
 set_option backward.isDefEq.respectTransparency false in
+set_option dsimp.resynthInstances false in
 /-- The free topological module over a topological space is functorial. -/
 noncomputable
 def freeMap {X Y : TopCat.{v}} (f : X ⟶ Y) : freeObj R X ⟶ freeObj R Y :=
@@ -442,6 +443,7 @@ def free : TopCat.{v} ⥤ TopModuleCat.{max v u} R :=
 
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
+set_option dsimp.resynthInstances false in
 /-- The free-forgetful adjoint for `TopModuleCat R`. -/
 noncomputable
 def freeAdj : free.{max v u} R ⊣ forget₂ (TopModuleCat.{max v u} R) TopCat.{max v u} where

mathlib4/Mathlib/Algebra/Category/ModuleCat/Ulift.lean

@@ -75,6 +75,7 @@ instance : Limits.PreservesFiniteLimits (uliftFunctor.{v', v} R) :=
 
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
+set_option dsimp.resynthInstances false in
 lemma uliftFunctor_map_exact (S : ShortComplex (ModuleCat.{v} R)) (h : S.Exact) :
     (S.map (uliftFunctor R)).Exact := by
   rw [CategoryTheory.ShortComplex.ShortExact.moduleCat_exact_iff_function_exact]

mathlib4/Mathlib/Algebra/Category/MonCat/Adjunctions.lean

@@ -96,6 +96,7 @@ def free : Type u ⥤ AddCommMonCat.{u} where
 
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
+set_option dsimp.resynthInstances false in
 /-- The free-forgetful adjunction for commutative monoids. -/
 noncomputable
 def adj : free ⊣ forget AddCommMonCat.{u} where

mathlib4/Mathlib/Algebra/Category/Ring/Under/Property.lean

@@ -141,6 +141,7 @@ open RingHom
 
 variable {P}
 
+set_option dsimp.resynthInstances false in
 set_option backward.isDefEq.respectTransparency.types false in
 set_option backward.defeqAttrib.useBackward true in
 lemma CommRingCat.preservesLimit_parallelPair_tensorProd_iff_tensorEqualizer_bijective

mathlib4/Mathlib/Algebra/GroupWithZero/Indicator.lean

@@ -68,6 +68,7 @@ variable [MulZeroOneClass M₀] {s t : Set ι} {i : ι}
 lemma inter_indicator_one : (s ∩ t).indicator (1 : ι → M₀) = s.indicator 1 * t.indicator 1 :=
   funext fun _ ↦ by simp only [← inter_indicator_mul, Pi.mul_apply, Pi.one_apply, one_mul]; congr
 
+set_option dsimp.resynthInstances false in
 set_option backward.isDefEq.respectTransparency false in
 lemma indicator_prod_one {t : Set κ} {j : κ} :
     (s ×ˢ t).indicator (1 : ι × κ → M₀) (i, j) = s.indicator 1 i * t.indicator 1 j := by

mathlib4/Mathlib/Algebra/Homology/DerivedCategory/Basic.lean

@@ -95,6 +95,7 @@ variable {C}
 def Q : CochainComplex C ℤ ⥤ DerivedCategory C := HomologicalComplexUpToQuasiIso.Q
 
 set_option backward.isDefEq.respectTransparency false in
+set_option dsimp.resynthInstances false in
 instance : (Q (C := C)).IsLocalization
     (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) := by
   dsimp only [Q, DerivedCategory]
@@ -129,6 +130,7 @@ lemma quotientCompQhIso_inv_naturality {K L : CochainComplex C ℤ} (f : K ⟶ L
   (quotientCompQhIso C).inv.naturality f
 
 set_option backward.isDefEq.respectTransparency false in
+set_option dsimp.resynthInstances false in
 instance : Qh.IsLocalization (HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) := by
   dsimp [Qh, DerivedCategory]
   infer_instance

mathlib4/Mathlib/Algebra/Homology/HomotopyCategory/Plus.lean

@@ -297,6 +297,7 @@ noncomputable instance :
     F.mapHomotopyCategory (.up ℤ)) _).CommShift ℤ)
 
 set_option backward.isDefEq.respectTransparency false in
+set_option dsimp.resynthInstances false in
 instance [HasZeroObject C] [HasBinaryBiproducts C] [HasZeroObject D] [HasBinaryBiproducts D] :
     (F.mapHomotopyCategoryPlus).IsTriangulated := by
   dsimp only [mapHomotopyCategoryPlus]

mathlib4/Mathlib/Algebra/Lie/UniversalEnveloping.lean

@@ -87,6 +87,7 @@ def ι : L →ₗ⁅R⁆ UniversalEnvelopingAlgebra R L :=
 variable {A : Type u₃} [Ring A] [Algebra R A] (f : L →ₗ⁅R⁆ A)
 
 set_option backward.isDefEq.respectTransparency false in
+set_option dsimp.resynthInstances false in
 /-- The universal property of the universal enveloping algebra: Lie algebra morphisms into
 associative algebras lift to associative algebra morphisms from the universal enveloping algebra. -/
 def lift : (L →ₗ⁅R⁆ A) ≃ (UniversalEnvelopingAlgebra R L →ₐ[R] A) where

mathlib4/Mathlib/Algebra/Module/Presentation/Differentials.lean

@@ -72,12 +72,14 @@ lemma comm₂₃' : pres.toExtension.toKaehler.comp pres.cotangentSpaceBasis.rep
   ext
   simp
 
+set_option dsimp.resynthInstances false in
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 /-- The canonical map `(σ →₀ S) →ₗ[S] pres.toExtension.Cotangent`. -/
 noncomputable def hom₁ : (σ →₀ S) →ₗ[S] pres.toExtension.Cotangent :=
   Finsupp.linearCombination S (fun r ↦ Extension.Cotangent.mk ⟨pres.relation r, by simp⟩)
 
+set_option dsimp.resynthInstances false in
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 lemma hom₁_single (r : σ) :
@@ -109,6 +111,7 @@ the transparency bump that instance-implicit arguments would otherwise receive.
 Potential fix: Mark `Generators.toExtension` implicit-reducible; then `respectTransparency false`
 and `instanceSearchTypes false` can both go.
 -/
+set_option dsimp.resynthInstances false in
 set_option backward.isDefEq.respectTransparency.instanceSearchTypes false in
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
@@ -138,6 +141,7 @@ lemma surjective_hom₁ : Function.Surjective (hom₁ pres) := by
   simp only [LinearMap.coe_mk, AddHom.coe_mk, hom₁_single, φ]
   rfl
 
+set_option dsimp.resynthInstances false in
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 lemma comm₁₂_single (r : σ) :

mathlib4/Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean

@@ -465,6 +465,7 @@ theorem mul_sum {S : Type*} [NonUnitalNonAssocSemiring S] (b : S) (s : SkewMonoi
   simp only [sum, Finsupp.sum, Finset.mul_sum]
 
 set_option backward.isDefEq.respectTransparency false in
+set_option dsimp.resynthInstances false in
 /-- Analogue of `Finsupp.sum_ite_eq'` for `SkewMonoidAlgebra`. -/
 @[deprecated Finsupp.sum_ite_eq' +typeChanged (since := "2026-07-04")]
 theorem sum_ite_eq' {N : Type*} [AddCommMonoid N] [DecidableEq G] (f : SkewMonoidAlgebra k G)

mathlib4/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/UnionProd.lean

@@ -100,13 +100,15 @@ lemma isIndex_succ (l : Fin d) :
       (x.cast hd).simplex.1 l.succ = k.succ ∧
       (x.cast hd).simplex.2 l.succ = (x.cast hd).simplex.2 l.castSucc := Iff.rfl
 
+set_option dsimp.resynthInstances false in
 lemma mem_range_left (i : Fin (m + 2)) (hi : i ≠ k.castSucc) :
     i ∈ Set.range (x.cast hd).simplex.1 := by
   subst hd
   have := x.notMem
   simp [Subcomplex.mem_unionProd_iff, mem_horn_iff_notMem_range] at this
   tauto
 
+set_option dsimp.resynthInstances false in
 lemma mem_range_right (i : Fin (n + 1)) :
     i ∈ Set.range (x.cast hd).simplex.2 := by
   subst hd
@@ -206,6 +208,7 @@ variable {x} {hd : x.dim = d + 1} {l : Fin (d + 1)} (hl : IsIndex x hd l.succ)
 
 include hl
 
+set_option dsimp.resynthInstances false in
 set_option backward.isDefEq.respectTransparency.types false in
 /-- The type (II) simplex obtained as a face of a type (I) simplex. -/
 @[simps -isSimp]

mathlib4/Mathlib/AlgebraicTopology/SimplicialSet/Homotopy.lean

@@ -63,6 +63,7 @@ lemma h₁ (H : Homotopy f g) : ι₁ ≫ H.h = g :=
   RelativeMorphism.Homotopy.h₁ H
 
 set_option backward.isDefEq.respectTransparency false in
+set_option dsimp.resynthInstances false in
 /-- If `H : Homotopy f g` is a homotopy between morphisms of simplicial sets
 `f : X ⟶ Y` and `g : X ⟶ Y` (i.e. `H.h` is a morphism `X ⊗ Δ[1] ⟶ Y` inducing
 `f` and `g`), then this is the corresponding (combinatorial) homotopy of

mathlib4/Mathlib/AlgebraicTopology/SimplicialSet/Monoidal.lean

@@ -248,6 +248,7 @@ variable {X Y : SSet.{u}} (S : X.Subcomplex) (T : Y.Subcomplex)
 /-- Given `S ≤ X` and `T ≤ Y`, this is the subcomplex of `X ⊗ Y` given by `(X ⊗ T) ⊔ (S ⊗ Y)`. -/
 def unionProd : (X ⊗ Y).Subcomplex := ((⊤ : X.Subcomplex).prod T) ⊔ (S.prod ⊤)
 
+set_option dsimp.resynthInstances false in
 set_option backward.defeqAttrib.useBackward true in
 lemma mem_unionProd_iff {n : SimplexCategoryᵒᵖ} (x : (X ⊗ Y).obj n) :
     dsimp% x ∈ (unionProd S T).obj _ ↔ x.2 ∈ T.obj _ ∨ x.1 ∈ S.obj _ := by
@@ -304,6 +305,7 @@ lemma isPushout : IsPushout (S.ι ▷ (T : SSet)) ((S : SSet) ◁ T.ι)
     (prodIso _ _ ≪≫ whiskerLeftIso _ (topIso Y))
     (Iso.refl _) rfl rfl rfl rfl
 
+set_option dsimp.resynthInstances false in
 set_option backward.isDefEq.respectTransparency.types false in
 @[simp]
 lemma preimage_β_hom : (unionProd S T).preimage (β_ _ _).hom = unionProd T S := by

mathlib4/Mathlib/AlgebraicTopology/SimplicialSet/ProdStdSimplexOne.lean

@@ -99,6 +99,7 @@ lemma ofSimplex_le_filtration {i j : Fin (p + 1)} (hij : i ≤ j) :
     Subcomplex.ofSimplex (nonDegenerateEquiv i.val).val) ⟨i, hij⟩
 
 variable (p) in
+set_option dsimp.resynthInstances false in
 lemma filtration_zero :
     filtration.{u} (0 : Fin (p + 1)) = .ofSimplex (nonDegenerateEquiv 0).val :=
   le_antisymm (by simp [filtration]) (ofSimplex_le_filtration.{u} (by rfl))

mathlib4/Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean

@@ -1047,6 +1047,7 @@ private lemma faaDiBruno_aux2 {m : ℕ} (q : FormalMultilinearSeries 𝕜 F G)
 
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
+set_option dsimp.resynthInstances false in
 /-- *Faa di Bruno* formula: If two functions `g` and `f` have Taylor series up to `n` given by
 `q` and `p`, then `g ∘ f` also has a Taylor series, given by `q.taylorComp p`. -/
 theorem HasFTaylorSeriesUpToOn.comp {n : WithTop ℕ∞} {g : F → G} {f : E → F}

mathlib4/Mathlib/Analysis/Calculus/IteratedDeriv/FaaDiBruno.lean

@@ -63,6 +63,7 @@ theorem iteratedDeriv_vcomp_eq_sum_orderedFinpartition
     uniqueDiffOn_univ (mem_univ x) (mapsTo_univ f _) hi
 
 set_option backward.isDefEq.respectTransparency false in
+set_option dsimp.resynthInstances false in
 theorem iteratedDerivWithin_vcomp_two
     (hg : ContDiffWithinAt 𝕜 2 g t (f x)) (hf : ContDiffWithinAt 𝕜 2 f s x)
     (ht : UniqueDiffOn 𝕜 t) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) (hst : MapsTo f s t) :
@@ -86,6 +87,7 @@ theorem iteratedDeriv_vcomp_two (hg : ContDiffAt 𝕜 2 g (f x)) (hf : ContDiffA
   exact iteratedDerivWithin_vcomp_two hg hf uniqueDiffOn_univ
     uniqueDiffOn_univ (mem_univ x) (mapsTo_univ f _)
 
+set_option dsimp.resynthInstances false in
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 theorem iteratedDerivWithin_vcomp_three

mathlib4/Mathlib/Analysis/Convex/Visible.lean

@@ -188,6 +188,7 @@ lemma IsClosed.convexHull_subset_affineSpan_isVisible (hs : IsClosed (convexHull
       hxz.mem_convexHull_isVisible hx hz) (ne_of_mem_of_not_mem hz hx).symm
 
 open Submodule in
+set_option dsimp.resynthInstances false in
 /-- If `s` is a closed set of dimension `d` and `x` is a point outside of its convex hull,
 then `x` sees at least `d` points of the convex hull of `s` that actually lie in `s`. -/
 lemma rank_le_card_isVisible (hs : IsClosed (convexHull ℝ s)) (hx : x ∉ convexHull ℝ s) :

mathlib4/Mathlib/Analysis/InnerProductSpace/PiL2.lean

@@ -259,6 +259,7 @@ def DirectSum.IsInternal.isometryL2OfOrthogonalFamily [DecidableEq ι] {V : ι 
   · congr <;> simp
 
 set_option backward.isDefEq.respectTransparency false in
+set_option dsimp.resynthInstances false in
 @[simp]
 theorem DirectSum.IsInternal.isometryL2OfOrthogonalFamily_symm_apply [DecidableEq ι]
     {V : ι → Submodule 𝕜 E} (hV : DirectSum.IsInternal V)

mathlib4/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ModuleEmbedding/GabrielPopescu.lean

@@ -123,6 +123,7 @@ theorem GabrielPopescu.full (G : C) (hG : IsSeparator G) : (preadditiveCoyonedaO
     ext q
     simpa [-comp_epiDesc] using! Sigma.ι _ q ≫= comp_epiDesc _ _ h
 
+set_option dsimp.resynthInstances false in
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 theorem GabrielPopescu.preservesInjectiveObjects (G : C) (hG : IsSeparator G) :

mathlib4/Mathlib/CategoryTheory/Bicategory/Functor/Oplax.lean

@@ -172,6 +172,7 @@ lemma mapComp'_eq_mapComp {b₀ b₁ b₂ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶
 
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
+set_option dsimp.resynthInstances false in
 /-- Composition of oplax functors. -/
 --@[simps]
 def comp (F : B ⥤ᵒᵖᴸ C) (G : C ⥤ᵒᵖᴸ D) : B ⥤ᵒᵖᴸ D where

mathlib4/Mathlib/CategoryTheory/Bicategory/Yoneda.lean

@@ -93,6 +93,7 @@ def yoneda₀ (x : B) : Pseudofunctor Bᵒᵖ Cat.{w, v} where
 
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
+set_option dsimp.resynthInstances false in
 /-- Postcomposing of a 1-morphism seen as a strong transformation between pseudofunctors. -/
 @[simps!]
 def postcomp₂ {a b : B} (f : a ⟶ b) : yoneda₀ a ⟶ yoneda₀ b where
@@ -112,6 +113,7 @@ def postcomposing₂ (a b : B) : (a ⟶ b) ⥤ (yoneda₀ a ⟶ yoneda₀ b) whe
 
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
+set_option dsimp.resynthInstances false in
 /-- The Yoneda pseudofunctor from `B` to `Bᵒᵖ ⥤ᵖ Cat`.
 
 It consists of the following:

mathlib4/Mathlib/CategoryTheory/Category/Cat/Limit.lean

@@ -137,6 +137,7 @@ theorem limit_π_homDiagram_eqToHom {F : J ⥤ Cat.{v, v}} (X Y : limit (F ⋙ C
 
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
+set_option dsimp.resynthInstances false in
 /-- Auxiliary definition: the proposed cone is a limit cone. -/
 def limitConeIsLimit (F : J ⥤ Cat.{v, v}) : IsLimit (limitCone F) where
   lift := limitConeLift F

mathlib4/Mathlib/CategoryTheory/Comma/StructuredArrow/Functor.lean

@@ -60,6 +60,7 @@ def functor (T : C ⥤ D) : D ⥤ Cat where
 variable {E : Type u₃} [Category.{v₃} E]
 variable (L : C ⥤ D) (R : E ⥤ D)
 
+set_option dsimp.resynthInstances false in
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 /-- The functor used to establish the equivalence `grothendieckPrecompFunctorEquivalence` between
@@ -71,6 +72,7 @@ def grothendieckPrecompFunctorToComma : Grothendieck (R ⋙ functor L) ⥤ Comma
 
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
+set_option dsimp.resynthInstances false in
 /-- Fibers of `grothendieckPrecompFunctorToComma L R`, composed with `Comma.fst L R`, are isomorphic
 to the projection `proj L (R.obj X)`. -/
 @[simps!]
@@ -79,6 +81,7 @@ def ιCompGrothendieckPrecompFunctorToCommaCompFst (X : E) :
     proj L (R.obj X) :=
   NatIso.ofComponents (fun X => Iso.refl _) (fun _ => by simp)
 
+set_option dsimp.resynthInstances false in
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 /-- The inverse functor used to establish the equivalence `grothendieckPrecompFunctorEquivalence`