chore: adaptations for nightly-2026-05-07

Cache/Requests.lean

@@ -94,7 +94,7 @@ def findMathlibRemote (mathlibDepPath : FilePath) : IO String := do
       let remoteUrl := parts[1]!.takeWhile (· != ' ') |>.copy -- Remove (fetch) or (push) suffix
 
       -- Check if this remote points to leanprover-community/mathlib4
-      let isMathlibRepo := remoteUrl.containsSubstr "leanprover-community/mathlib4"
+      let isMathlibRepo := remoteUrl.contains "leanprover-community/mathlib4"
 
       if isMathlibRepo then
         if remoteName == "origin" then

Mathlib/Algebra/Colimit/DirectLimit.lean

@@ -613,10 +613,10 @@ lemma map₀_algebraMap (i : ι) (r : R) :
 instance : Algebra R (DirectLimit G f) where
   algebraMap := map₀RingHom (f := f).comp (algebraMap R (∀ i, G i))
   commutes' r := DirectLimit.induction f fun i _ ↦ by
-    dsimp [Pi.algebraMap_def]
+    dsimp [Pi.algebraMap_def, map₀RingHom]
     rw [map₀_algebraMap i, mul_def, mul_def, Algebra.commutes]
   smul_def' r := DirectLimit.induction _ fun i _ => by
-    dsimp [Pi.algebraMap_def]
+    dsimp [Pi.algebraMap_def, map₀RingHom]
     rw [smul_def, map₀_algebraMap i, mul_def, Algebra.smul_def']
 
 lemma algebraMap_def (i : ι) (r : R) :
@@ -871,7 +871,6 @@ variable [Nonempty ι]
 
 variable (G f) in
 /-- The canonical map from a component to the direct limit. -/
-@[simps]
 def of (i) : G i →ₙₐ[R] DirectLimit G f where
   toFun x := ⟦⟨i, x⟩⟧
   __ := (DirectLimit.NonUnitalRing.of G f i)
@@ -886,7 +885,7 @@ variable (G f) in
 that respect the directed system structure (i.e. make some diagram commute) give rise
 to a unique map out of the direct limit.
 -/
-@[simps]
+@[simps toFun]
 def lift (g : ∀ i, G i →ₙₐ[R] P) (Hg : ∀ i j hij x, g j (f i j hij x) = g i x) :
     DirectLimit G f →ₙₐ[R] P where
   toFun := _root_.DirectLimit.lift _ (g · ·) fun i j h x ↦ (Hg i j h x).symm

Mathlib/Algebra/Group/Defs.lean

@@ -15,6 +15,7 @@ public import Mathlib.Tactic.MkIffOfInductiveProp
 public import Mathlib.Tactic.OfNat
 public import Mathlib.Data.Nat.Notation
 public import Mathlib.Tactic.Simps.Basic
+public import Mathlib.Tactic.AdaptationNote
 
 /-!
 # Typeclasses for (semi)groups and monoids

Mathlib/Algebra/Group/Nat/Even.lean

@@ -8,6 +8,7 @@ module
 public import Mathlib.Algebra.Group.Even
 public import Mathlib.Algebra.Group.Nat.Defs
 public import Mathlib.Data.Nat.Sqrt
+public import Mathlib.Tactic.Attr.Register
 
 /-!
 # `IsSquare` and `Even` for natural numbers

Mathlib/Algebra/Homology/DerivedCategory/Basic.lean

@@ -114,15 +114,17 @@ variable (C) in
 def quotientCompQhIso : HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh ≅ Q :=
   HomologicalComplexUpToQuasiIso.quotientCompQhIso C (ComplexShape.up ℤ)
 
+#adaptation_note /-- Prior to nightly-2026-05-07, the LHS of these statements was guarded with
+`dsimp%`; it now reports `made no progress`, so we write the (already-reduced) form directly. -/
 @[reassoc (attr := simp)]
 lemma quotientCompQhIso_hom_naturality {K L : CochainComplex C ℤ} (f : K ⟶ L) :
-    dsimp% Qh.map ((HomotopyCategory.quotient _ _).map f) ≫ (quotientCompQhIso C).hom.app L =
+    Qh.map ((HomotopyCategory.quotient _ _).map f) ≫ (quotientCompQhIso C).hom.app L =
       (quotientCompQhIso C).hom.app K ≫ Q.map f :=
   (quotientCompQhIso C).hom.naturality f
 
 @[reassoc]
 lemma quotientCompQhIso_inv_naturality {K L : CochainComplex C ℤ} (f : K ⟶ L) :
-    dsimp% Q.map f ≫ (quotientCompQhIso C).inv.app L =
+    Q.map f ≫ (quotientCompQhIso C).inv.app L =
       (quotientCompQhIso C).inv.app K ≫ Qh.map ((HomotopyCategory.quotient _ _).map f) :=
   (quotientCompQhIso C).inv.naturality f
 

Mathlib/Algebra/Homology/DerivedCategory/KInjective.lean

@@ -56,8 +56,8 @@ lemma quasiIso_iff {K L : CochainComplex C ℤ} [K.IsKInjective] [L.IsKInjective
   obtain ⟨g, hg⟩ := (Qh_map_bijective _ _).surjective
     ((quotientCompQhIso C).hom.app L ≫ inv (Q.map f) ≫ (quotientCompQhIso C).inv.app K)
   refine ⟨g, (Qh_map_bijective _ _).injective ?_, (Qh_map_bijective _ _).injective ?_⟩
-  · simp [hg]
-  · simp [hg, ← quotientCompQhIso_inv_naturality, -NatTrans.naturality]
+  · simp [hg]; rfl
+  · simp [hg, ← quotientCompQhIso_inv_naturality, -NatTrans.naturality]; rfl
 
 end IsKInjective
 

Mathlib/Algebra/Homology/DerivedCategory/KProjective.lean

@@ -57,8 +57,8 @@ lemma quasiIso_iff {K L : CochainComplex C ℤ} [K.IsKProjective] [L.IsKProjecti
   obtain ⟨g, hg⟩ := (Qh_map_bijective _ _).surjective
     ((quotientCompQhIso C).hom.app L ≫ inv (Q.map f) ≫ (quotientCompQhIso C).inv.app K)
   refine ⟨g, (Qh_map_bijective _ _).injective ?_, (Qh_map_bijective _ _).injective ?_⟩
-  · simp [hg]
-  · simp [hg, ← quotientCompQhIso_inv_naturality f, -NatTrans.naturality]
+  · simp [hg]; rfl
+  · simp [hg, ← quotientCompQhIso_inv_naturality f, -NatTrans.naturality]; rfl
 
 end IsKProjective
 

Mathlib/Algebra/Homology/Embedding/ExtendHomotopy.lean

@@ -222,7 +222,12 @@ lemma HomologicalComplex.homotopyEquivalences_extendMap_iff
     (e : ComplexShape.Embedding c c') [e.IsRelIff] :
     homotopyEquivalences C c' (extendMap f e) ↔
       homotopyEquivalences C c f := by
-  simp [← HomotopyCategory.inverseImage_quotient_isomorphisms,
+  #adaptation_note /-- Prior to nightly-2026-05-07, `dsimp%` was used directly inline as the last
+  argument to the original `simp`; it now reports `made no progress` so we apply
+  `NatIso.isIso_map_iff` via a `change` + `rw` after the rest of the simp set has done its work. -/
+  simp only [← HomotopyCategory.inverseImage_quotient_isomorphisms,
     MorphismProperty.inverseImage_iff, MorphismProperty.isomorphisms.iff,
-    ← isIso_iff_of_reflects_iso _ (e.extendHomotopyFunctor C),
-    dsimp% NatIso.isIso_map_iff (e.extendHomotopyFunctorFactors C) f]
+    ← isIso_iff_of_reflects_iso _ (e.extendHomotopyFunctor C)]
+  change _ ↔ IsIso ((HomotopyCategory.quotient C c ⋙ e.extendHomotopyFunctor C).map f)
+  rw [NatIso.isIso_map_iff (e.extendHomotopyFunctorFactors C) f]
+  rfl

Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

@@ -548,8 +548,8 @@ lemma isStableUnderBaseChange (hP : RingHom.IsStableUnderBaseChange Q) :
   · rw [IsZariskiLocalAtSource.iff_of_openCover (P := P)
       (Scheme.Pullback.openCoverOfRight Y.affineCover f g)]
     intro i
-    simp only [Scheme.Pullback.openCoverOfRight_f,
-      limit.lift_π, PullbackCone.mk_π_app, Category.comp_id]
+    simp only [Scheme.Pullback.openCoverOfRight_f, limit.lift_π, PullbackCone.mk_π_app,
+      Category.comp_id]
     apply this _ (comp_of_isOpenImmersion _ _ _ H) inferInstance
   rw [iff_of_isAffine (P := P)] at H ⊢
   exact hP.pullback_fst_appTop _ (isLocal_ringHomProperty P).respectsIso _ _ H

Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Functor.lean

@@ -203,8 +203,8 @@ an affine open cover of `Proj ℬ` consisting of `D(f(s))` for `s ∈ A` positiv
 set_option backward.isDefEq.respectTransparency false in
 theorem map_comp : map (g.comp f) (irrelevant_le_map_comp hf hg) = map g hg ≫ map f hf := by
   refine (mapAffineOpenCover _ <| irrelevant_le_map_comp hf hg).openCover.hom_ext _ _ fun s ↦ ?_
-  simp only [Scheme.AffineOpenCover.openCover_f,
-    mapAffineOpenCover_f, awayι_comp_map (g.comp f) _ s.1.2 _ s.2.2]
+  simp only [Scheme.AffineOpenCover.openCover_f, mapAffineOpenCover_f,
+    awayι_comp_map (g.comp f) _ s.1.2 _ s.2.2]
   simp [awayι_comp_map_assoc _ _ _ _ (map_mem f s.2.2), awayι_comp_map _ _ _ _ s.2.2]
 
 set_option backward.isDefEq.respectTransparency false in

Mathlib/AlgebraicGeometry/Restrict.lean

@@ -767,8 +767,7 @@ set_option backward.isDefEq.respectTransparency false in
 noncomputable def arrowResLEAppIso (f : X ⟶ Y) (U : Y.Opens) (V : X.Opens) (e : V ≤ f ⁻¹ᵁ U) :
     Arrow.mk ((f.resLE U V e).appTop) ≅ Arrow.mk (f.appLE U V e) :=
   Arrow.isoMk U.topIso V.topIso <| by
-  simp only [Scheme.Opens.topIso_hom,
-    eqToHom_op, Arrow.mk_hom, Scheme.Hom.map_appLE]
+  simp only [Scheme.Opens.topIso_hom, eqToHom_op, Arrow.mk_hom, Scheme.Hom.map_appLE]
   rw [Scheme.Hom.appTop, ← Scheme.Hom.appLE_eq_app, Scheme.Hom.resLE_appLE, Scheme.Hom.appLE_map]
 
 lemma Scheme.Hom.isPullback_resLE

Mathlib/CategoryTheory/Discrete/Basic.lean

@@ -323,6 +323,7 @@ def piEquivalenceFunctorDiscrete (J : Type u₂) (C : Type u₁) [Category.{v₁
       obtain rfl : f = 𝟙 _ := rfl
       simp))) (by cat_disch)
 
+set_option backward.defeqAttrib.useBackward true in
 /-- `piEquivalenceFunctorDiscrete` is compatible with `evaluation`. -/
 @[simps!]
 def piEquivalenceFunctorDiscreteCompEvaluationIso (C : Type*) [Category* C] {J : Type*} (j : J) :

Mathlib/CategoryTheory/Limits/FilteredColimitCommutesProduct.lean

@@ -61,6 +61,8 @@ maps `k : ∀ i, I i` to `∏ᶜ fun (s : α) => (F s).obj (k s)`. -/
 noncomputable abbrev pointwiseProduct : (∀ i, I i) ⥤ C :=
   Functor.pi F ⋙ Pi.functor α
 
+set_option backward.defeqAttrib.useBackward true in
+set_option backward.isDefEq.respectTransparency false in
 attribute [local simp] Functor.pi in
 /-- `pointwiseProduct` is invariant under re-indexing. -/
 @[simps!]
@@ -81,6 +83,8 @@ noncomputable def coconePointwiseProduct (c : ∀ i, Cocone (F i)) :
   pt := ∏ᶜ fun i ↦ (c i).pt
   ι := Functor.whiskerRight (NatTrans.pi fun i ↦ (c i).ι) _ ≫ (Pi.constCompPiIsoConst _).hom
 
+set_option backward.defeqAttrib.useBackward true in
+set_option backward.isDefEq.respectTransparency false in
 /-- `coconePointwiseProduct` is invariant under isomorphisms of cocones. -/
 noncomputable def coconePointwiseProductIso {c c' : ∀ i, Cocone (F i)} (e : ∀ i, c i ≅ c' i) :
     coconePointwiseProduct c ≅ coconePointwiseProduct c' :=
@@ -99,6 +103,7 @@ noncomputable def colimitPointwiseProductToProductColimit [∀ i, HasColimit (F
 
 variable [∀ i, HasColimit (F i)] [HasColimit (pointwiseProduct F)]
 
+set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 @[reassoc (attr := simp)]
 theorem ι_colimitPointwiseProductToProductColimit_π (k : ∀ i, I i) (s : α) :
@@ -126,6 +131,8 @@ noncomputable def pointwiseProductCompEvaluation (d : D) :
   NatIso.ofComponents (fun k => piObjIso _ _)
     (fun f => Pi.hom_ext _ _ (by simp [Functor.pi, ← NatTrans.comp_app]))
 
+set_option backward.defeqAttrib.useBackward true in
+set_option backward.isDefEq.respectTransparency false in
 /-- In a functor category, `coconePointwiseProduct` commutes with evaluation. -/
 noncomputable def evaluationCoconePointwiseProductIso (X : D) (c : ∀ i, Cocone (F i)) :
     ((evaluation D C).obj X).mapCocone (coconePointwiseProduct c) ≅
@@ -199,6 +206,8 @@ lemma IsIPCOfShape.of_isIso
   obtain ⟨_, h⟩ := H J F
   rwa [IsColimit.nonempty_isColimit_iff_isIso_desc (colimit.isColimit _)]
 
+set_option backward.defeqAttrib.useBackward true in
+set_option backward.isDefEq.respectTransparency false in
 attribute [local simp] Functor.pi in
 lemma IsIPCOfShape.of_equiv {ι' : Type*} [HasProductsOfShape ι' C] [IsIPCOfShape.{w} ι C]
     (e : ι ≃ ι') :

Mathlib/CategoryTheory/Limits/HasLimits.lean

@@ -489,6 +489,7 @@ def lim : (J ⥤ C) ⥤ C where
     apply Limits.limit.hom_ext; intro j
     simp [assoc]
 
+set_option backward.isDefEq.respectTransparency false in
 /-- The natural transformation induced by `limit.π`. -/
 @[simps]
 def lim.π (j : J) : lim ⟶ (evaluation J C).obj j where
@@ -1074,6 +1075,7 @@ def colim : (J ⥤ C) ⥤ C where
   obj F := colimit F
   map α := colimMap α
 
+set_option backward.isDefEq.respectTransparency false in
 /-- The natural transformation induced by `colimit.ι`. -/
 @[simps]
 def colim.ι (j : J) : (evaluation J C).obj j ⟶ colim where

Mathlib/CategoryTheory/Limits/Shapes/BinaryBiproducts.lean

@@ -322,6 +322,8 @@ structure BinaryBicone.IsBilimit {P Q : C} (b : BinaryBicone P Q) where
 attribute [inherit_doc BinaryBicone.IsBilimit] BinaryBicone.IsBilimit.isLimit
   BinaryBicone.IsBilimit.isColimit
 
+set_option backward.defeqAttrib.useBackward true in
+set_option backward.isDefEq.respectTransparency false in
 /-- If a binary bicone for `P` and `Q` is bilimit, then the binary bicone for `P'` and `Q'`
 obtained using isomorphisms `P ≅ P'` and `Q ≅ Q'` is also bilimit. -/
 def BinaryBicone.IsBilimit.ofIso {P Q P' Q' : C} {b : BinaryBicone P Q} (hb : b.IsBilimit)

Mathlib/CategoryTheory/Limits/Shapes/Products.lean

@@ -997,26 +997,30 @@ noncomputable def Pi.functor [HasProductsOfShape α C] : (α → C) ⥤ C where
   obj f := ∏ᶜ f
   map {f g} t := Pi.map t
 
+set_option backward.defeqAttrib.useBackward true in
 /-- The natural transformation induced by `Pi.π`. -/
 @[simps]
 def Pi.functorπ [HasProductsOfShape α C] (a : α) :
     Pi.functor α ⟶ Pi.eval (fun _ ↦ C) a where
   app f := Pi.π f a
 
+set_option backward.defeqAttrib.useBackward true in
 variable (α) in
 /-- Up to pre-composing with an equivalence of categories, `Pi.functor` is isomorphic to `lim`. -/
 @[simps!]
 def piEquivalenceFunctorDiscreteCompLim [HasProductsOfShape α C] :
     (piEquivalenceFunctorDiscrete α C).functor ⋙ lim ≅ Pi.functor _ :=
   NatIso.ofComponents fun _ ↦ Iso.refl _
 
+set_option backward.defeqAttrib.useBackward true in
 @[reassoc]
 lemma piEquivalenceFunctorDiscreteCompLim_comp_functorπ [HasProductsOfShape α C] (a : α) :
     (piEquivalenceFunctorDiscreteCompLim (C := C) α).hom ≫ Pi.functorπ a =
       Functor.whiskerLeft _ (lim.π <| Discrete.mk a) ≫
         (piEquivalenceFunctorDiscreteCompEvaluationIso _ _).hom := by
   cat_disch
 
+set_option backward.defeqAttrib.useBackward true in
 attribute [local simp] Functor.pi in
 /-- The `∏ᶜ` functor composed with the pointwise constant functor `Π i, I i ⥤ (α → C)` is isomorphic
 to the constant functor with value `∏ᶜ X`. -/
@@ -1034,12 +1038,14 @@ noncomputable def Sigma.functor [HasCoproductsOfShape α C] : (α → C) ⥤ C w
   obj f := ∐ f
   map {f g} t := Sigma.map t
 
+set_option backward.defeqAttrib.useBackward true in
 /-- The natural transformation induced by `Sigma.ι`. -/
 @[simps]
 def Sigma.functorι [HasCoproductsOfShape α C] (a : α) :
     Pi.eval (fun _ ↦ C) a ⟶ Sigma.functor α where
   app f := Sigma.ι f a
 
+set_option backward.defeqAttrib.useBackward true in
 variable (α) in
 /-- Up to pre-composing with an equivalence of categories, `Sigma.functor` is isomorphic
 to `colim`. -/
@@ -1048,6 +1054,7 @@ def piEquivalenceFunctorDiscreteCompColim [HasCoproductsOfShape α C] :
     (piEquivalenceFunctorDiscrete α C).functor ⋙ colim ≅ Sigma.functor _ :=
   NatIso.ofComponents fun _ ↦ Iso.refl _
 
+set_option backward.defeqAttrib.useBackward true in
 @[reassoc]
 lemma piEquivalenceFunctorDiscreteCompColim_comp_functorι [HasCoproductsOfShape α C] (a : α) :
     Functor.whiskerLeft _ (colim.ι <| .mk a) ≫ (piEquivalenceFunctorDiscreteCompColim α).hom =
@@ -1058,6 +1065,7 @@ lemma piEquivalenceFunctorDiscrete_functor_comp_colim [HasCoproductsOfShape α C
     (piEquivalenceFunctorDiscrete α C).functor ⋙ colim = Sigma.functor _ :=
   rfl
 
+set_option backward.defeqAttrib.useBackward true in
 attribute [local simp] Functor.pi in
 /-- The `∐` functor composed with the pointwise constant functor `Π i, I i ⥤ (α → C)` is isomorphic
 to the constant functor with value `∐ X`. -/

Mathlib/CategoryTheory/MorphismProperty/Factorization.lean

@@ -247,6 +247,8 @@ instance [HasFunctorialFactorization W₁ W₂] (J : Type*) [Category* J] :
     HasFunctorialFactorization (W₁.functorCategory J) (W₂.functorCategory J) :=
   ⟨⟨(functorialFactorizationData W₁ W₂).functorCategory J⟩⟩
 
+set_option backward.defeqAttrib.useBackward true in
+set_option backward.isDefEq.respectTransparency false in
 variable {W₁ W₂} in
 /-- The term in `MapFactorizationData (W₁.inverseImage F) (W₂.inverseImage F) f`
 deduced from `h : MapFactorizationData W₁ W₂ (F.map f)` when `F` is an equivalence
@@ -260,10 +262,12 @@ noncomputable def MapFactorizationData.ofIsEquivalence {F : D ⥤ C}
   p := F.preimage ((F.objObjPreimageIso h.Z).hom ≫ h.p)
   hi := by
     refine (W₁.arrow_mk_iso_iff ?_).1 h.hi
-    exact Arrow.isoMk (Iso.refl _) (F.objObjPreimageIso h.Z).symm
+    refine Arrow.isoMk (Iso.refl _) (F.objObjPreimageIso h.Z).symm ?_
+    simp [F.map_preimage]
   hp := by
     refine (W₂.arrow_mk_iso_iff ?_).1 h.hp
-    exact Arrow.isoMk (F.objObjPreimageIso h.Z).symm (Iso.refl _)
+    refine Arrow.isoMk (F.objObjPreimageIso h.Z).symm (Iso.refl _) ?_
+    simp [F.map_preimage]
   fac := F.map_injective (by simp)
 
 instance (F : D ⥤ C) [F.IsEquivalence]

Mathlib/CategoryTheory/MorphismProperty/LiftingProperty.lean

@@ -185,8 +185,17 @@ lemma Functor.hasLiftingProperty_iff_of_isEquivalence
     {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) :
     HasLiftingProperty (G.map i) (G.map p) ↔
       HasLiftingProperty i p := by
+  #adaptation_note /-- Prior to nightly-2026-05-07, the next three lines were just
+  ```
   simp only [dsimp% G.asEquivalence.toAdjunction.hasLiftingProperty_iff,
     ← MorphismProperty.rlp_ofHoms_iff_hasLiftingProperty Unit]
+  ```
+  This is a temporary repair, and authors/maintainers are encouraged to either find a better repair,
+  or identify a minimal example of an underlying problem in Lean.
+  -/
+  change HasLiftingProperty (G.asEquivalence.functor.map i) (G.asEquivalence.functor.map p) ↔ _
+  rw [G.asEquivalence.toAdjunction.hasLiftingProperty_iff]
+  simp only [← MorphismProperty.rlp_ofHoms_iff_hasLiftingProperty Unit]
   exact MorphismProperty.arrow_mk_iso_iff _
     (Arrow.isoMk (G.asEquivalence.unitIso.symm.app _)
       (G.asEquivalence.unitIso.symm.app _)

Mathlib/CategoryTheory/ObjectProperty/Opposite.lean

@@ -137,6 +137,7 @@ lemma unop_isoClosure (P : ObjectProperty Cᵒᵖ) :
     P.isoClosure.unop = P.unop.isoClosure := by
   rw [← op_injective_iff, P.unop.op_isoClosure, op_unop, op_unop]
 
+set_option backward.defeqAttrib.useBackward true in
 /-- Given `P : ObjectProperty C`, this is the equivalence between `P.op.FullSubcategory`
 and `P.FullSubcategoryᵒᵖ`. -/
 @[simps]

Mathlib/CategoryTheory/Opposites.lean

@@ -310,6 +310,7 @@ set_option backward.defeqAttrib.useBackward true in
 protected def FullyFaithful.op {F : C ⥤ D} (hF : F.FullyFaithful) : F.op.FullyFaithful where
   preimage {X Y} f := .op <| hF.preimage f.unop
 
+set_option backward.defeqAttrib.useBackward true in
 /-- A functor is fully faithful when its opposite is fully faithful. -/
 protected def FullyFaithful.unop {F : Cᵒᵖ ⥤ Dᵒᵖ} (hF : F.FullyFaithful) :
     F.unop.FullyFaithful where

Mathlib/CategoryTheory/Shift/SingleFunctorsLift.lean

@@ -46,6 +46,7 @@ noncomputable def shiftIso (n a a' : A) (h : n + a = a') :
       isoWhiskerLeft _ (G.commShiftIso n) ≪≫ (Functor.associator _ _ _).symm ≪≫
       isoWhiskerRight (hΦ a') _ ≪≫ F.shiftIso n a a' h ≪≫ (hΦ a).symm)
 
+set_option backward.defeqAttrib.useBackward true in
 private lemma map_shiftIso_hom_app (n a a' : A) (h : n + a = a') (X : C) :
     dsimp% G.map ((lift.shiftIso hΦ n a a' h).hom.app X) =
       (G.commShiftIso n).hom.app _ ≫ (shiftFunctor E n).map ((hΦ a').hom.app X) ≫
@@ -54,6 +55,7 @@ private lemma map_shiftIso_hom_app (n a a' : A) (h : n + a = a') (X : C) :
 
 end lift
 
+set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 /-- Let `C`, `D` and `E` be categories. Let `A` be an additive monoid.
 Assume that `D` and `E` have shifts by `A` and that we have
@@ -78,13 +80,15 @@ noncomputable def lift : SingleFunctors C D A where
     rw [F.shiftIso_add n m a a' a'' ha' ha'']
     simp [commShiftIso_add, ← Functor.map_comp_assoc, -Functor.map_comp]
 
+set_option backward.defeqAttrib.useBackward true in
 @[reassoc]
 lemma map_lift_shiftIso_hom_app (n a a' : A) (h : n + a = a') (X : C) :
     dsimp% G.map (((lift F G Φ hΦ).shiftIso n a a' h).hom.app X) =
       (G.commShiftIso n).hom.app _ ≫ (shiftFunctor E n).map ((hΦ a').hom.app X) ≫
         (F.shiftIso n a a' h).hom.app X ≫ (hΦ a).inv.app X :=
   lift.map_shiftIso_hom_app ..
 
+set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 /-- After postcomposition with the fully faithful functor `G`,
 `lift F G Φ hΦ` becomes isomorphic to `F`. -/
@@ -96,6 +100,7 @@ noncomputable def liftPostcompIso : (lift F G Φ hΦ).postcomp G ≅ F :=
     dsimp at this
     simp [map_lift_shiftIso_hom_app, this])
 
+set_option backward.defeqAttrib.useBackward true in
 instance [Preadditive C] [Preadditive D] [Preadditive E] [G.Additive] (a : A)
     [(F.functor a).Additive] : ((lift F G Φ hΦ).functor a).Additive := by
   have : ((lift F G Φ hΦ).functor a ⋙ G).Additive := by

Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean

@@ -122,7 +122,7 @@ theorem equiv_symm_eq_apply {X : C} {P : Cᵒᵖ ⥤ D} {S : J.Cover X} [HasMult
     -- We can hint `ConcreteCategory.hom (Y := P.obj (op I.Y))` below to put it into `simp`-normal
     -- form, but that doesn't seem to fix the `erw`s below...
     (Multiequalizer.ι (S.index P) I) ((Meq.equiv P S).symm x) = x I := by
-  simp [← equiv_apply]
+  simp [- GrothendieckTopology.Cover.index_left, ← equiv_apply]
 
 end Meq