chore: adaptations for nightly-2026-05-11 (#220)

kim-em · mathlib-nightly-testing[bot] · kim-em · commit e120c768fce4 · 2026-05-13T13:04:40.000Z
Co-authored-by: mathlib-nightly-testing[bot] &lt;mathlib-nightly-testing[bot]@users.noreply.github.com&gt;
diff --git a/Mathlib/Algebra/Homology/HomotopyCategory/Plus.lean b/Mathlib/Algebra/Homology/HomotopyCategory/Plus.lean
@@ -32,6 +32,7 @@ open HomologicalComplex
 
 variable {C} [HasBinaryBiproducts C]
 
+set_option backward.defeqAttrib.useBackward true in
 lemma plus_cylinder (K : CochainComplex C ℤ) (hK : CochainComplex.plus C K) :
     CochainComplex.plus C (cylinder K) := by
   obtain ⟨n, hn⟩ := hK
@@ -110,6 +111,7 @@ instance : (plus C).IsStableUnderShift ℤ where
           plus_quotient_obj_iff]
         exact ⟨q - n, K.isStrictlyGE_shift q n (q - n) (by lia)⟩ }
 
+set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 instance [HasZeroObject C] [HasBinaryBiproducts C] :
     (plus C).IsTriangulatedClosed₃ where
@@ -202,6 +204,7 @@ section
 variable [HasZeroObject C] [HasBinaryBiproducts C]
 
 open HomologicalComplex in
+set_option backward.defeqAttrib.useBackward true in
 instance :
     (quotient C).IsLocalization
       ((homotopyEquivalences C (.up ℤ)).inverseImage (CochainComplex.Plus.ι C)) :=
diff --git a/Mathlib/Algebra/Homology/HomotopyFiber.lean b/Mathlib/Algebra/Homology/HomotopyFiber.lean
@@ -44,6 +44,7 @@ instance [HasBinaryBiproducts C] : HasHomotopyFiber φ where
 
 variable [HasHomotopyFiber φ] [DecidableRel c.Rel]
 
+set_option backward.defeqAttrib.useBackward true in
 instance : HasHomotopyCofiber ((opFunctor C c).map φ.op) where
   hasBinaryBiproduct i j hij := by
     have := HasHomotopyFiber.hasBinaryBiproduct φ j i hij
@@ -58,6 +59,7 @@ end
 
 variable (K) [∀ i, HasBinaryBiproduct (K.X i) (K.X i)]
 
+set_option backward.defeqAttrib.useBackward true in
 instance (i : α) : HasBinaryBiproduct (K.op.X i) (K.op.X i) := by
   dsimp; infer_instance
 
@@ -84,6 +86,7 @@ noncomputable def pathObject := (unopFunctor C c.symm).obj (op K.op.cylinder)
 
 namespace pathObject
 
+set_option backward.defeqAttrib.useBackward true in
 lemma isZero_X (i : α) (h₁ : IsZero (K.X i)) (h₂ : ∀ (j : α), c.Rel j i → IsZero (K.X j)) :
     IsZero (K.pathObject.X i) := by
   apply IsZero.unop
diff --git a/Mathlib/Algebra/Homology/Opposite.lean b/Mathlib/Algebra/Homology/Opposite.lean
@@ -454,6 +454,7 @@ open HomologicalComplex
 
 variable {V : Type*} [Category* V] {ι : Type*} {c : ComplexShape ι} [Preadditive V]
 
+set_option backward.defeqAttrib.useBackward true in
 /-- The opposite of a homotopy between morphisms of homological complexes. -/
 @[simps]
 def op {F G : HomologicalComplex V c} {φ₁ φ₂ : F ⟶ G} (h : Homotopy φ₁ φ₂) :
@@ -466,6 +467,7 @@ def op {F G : HomologicalComplex V c} {φ₁ φ₂ : F ⟶ G} (h : Homotopy φ
     nth_rw 2 [add_comm]
     rfl)
 
+set_option backward.defeqAttrib.useBackward true in
 /-- The homotopy between morphisms of homological complexes that is deduced
 from a homotopy in the opposite category. -/
 @[simps]
diff --git a/Mathlib/AlgebraicGeometry/Morphisms/FlatRank.lean b/Mathlib/AlgebraicGeometry/Morphisms/FlatRank.lean
@@ -265,6 +265,7 @@ lemma Scheme.Hom.finrank_eq_one_of_isIso (f : X ⟶ Y) [IsIso f] : finrank f = 1
   · exact RingHom.Finite.id R
   · exact RingHom.Flat.id ↑R
 
+set_option backward.defeqAttrib.useBackward true in
 /-- A finite flat locally finitely presented morphism is an isomorphism if and only if
 its rank is constant equal to `1`. -/
 nonrec lemma Scheme.Hom.isIso_iff_finrank_eq : IsIso f ↔ finrank f = 1 := by
diff --git a/Mathlib/AlgebraicTopology/DoldKan/SplitSimplicialObject.lean b/Mathlib/AlgebraicTopology/DoldKan/SplitSimplicialObject.lean
@@ -226,19 +226,22 @@ noncomputable def toKaroubiNondegComplexIsoN₁ :
     simp only [πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty, Karoubi.comp_f,
       HomologicalComplex.comp_f, N₁_obj_p, Karoubi.id_f]
 
+set_option backward.defeqAttrib.useBackward true in
 @[reassoc (attr := simp)]
 lemma toKaroubiNondegComplexIsoN₁_hom_f_PInfty :
     dsimp% s.toKaroubiNondegComplexIsoN₁.hom.f ≫ PInfty =
       s.toKaroubiNondegComplexIsoN₁.hom.f := by
   simpa using s.toKaroubiNondegComplexIsoN₁.hom.comm
 
+set_option backward.defeqAttrib.useBackward true in
 @[reassoc (attr := simp)]
 lemma toKaroubiNondegComplexIsoN₁_hom_inv_id_f :
     dsimp% s.toKaroubiNondegComplexIsoN₁.hom.f ≫ s.toKaroubiNondegComplexIsoN₁.inv.f = 𝟙 _ := by
   rw [← dsimp% [-Karoubi.comp_f] Karoubi.comp_f s.toKaroubiNondegComplexIsoN₁.hom
     s.toKaroubiNondegComplexIsoN₁.inv, Iso.hom_inv_id]
   simp
 
+set_option backward.defeqAttrib.useBackward true in
 /-- Given a splitting `s` of a simplicial object `X` in a preadditive category,
 this is the split epimorphism from the alternating face map complex of `X` to the chain
 complex `s.nondegComplex`. -/
@@ -247,6 +250,7 @@ noncomputable def toNondegComplex : K[X] ⟶ s.nondegComplex :=
   (fullyFaithfulToKaroubi _).preimage
     ({ f := by exact PInfty } ≫ s.toKaroubiNondegComplexIsoN₁.inv)
 
+set_option backward.defeqAttrib.useBackward true in
 /-- Given a splitting `s` of a simplicial object `X` in a preadditive category,
 this is the split monomormphism from the chain complex `s.nondegComplex` to
 the alternating face map complex fo `X`. -/
@@ -255,20 +259,24 @@ noncomputable def fromNondegComplex : s.nondegComplex ⟶ K[X] :=
   (fullyFaithfulToKaroubi _).preimage
     (s.toKaroubiNondegComplexIsoN₁.hom ≫ { f := PInfty })
 
+set_option backward.defeqAttrib.useBackward true in
 @[reassoc (attr := simp)]
 lemma PInfty_toNondegComplex : PInfty ≫ s.toNondegComplex = s.toNondegComplex :=
   (toKaroubi _).map_injective (by simp [toNondegComplex])
 
+set_option backward.defeqAttrib.useBackward true in
 @[reassoc (attr := simp)]
 lemma fromNondegComplex_toNondegComplex :
     s.fromNondegComplex ≫ s.toNondegComplex = 𝟙 _ :=
   (toKaroubi _).map_injective (by simp [toNondegComplex, fromNondegComplex])
 
+set_option backward.defeqAttrib.useBackward true in
 @[reassoc]
 lemma toNondegComplex_f (n : ℕ) :
     s.toNondegComplex.f n = PInfty.f n ≫ s.toKaroubiNondegComplexIsoN₁.inv.f.f n := by
   simp [toNondegComplex, fullyFaithfulToKaroubi]
 
+set_option backward.defeqAttrib.useBackward true in
 @[reassoc]
 lemma fromNondegComplex_f (n : ℕ) :
     s.fromNondegComplex.f n = s.ι n ≫ PInfty.f n := by
@@ -281,6 +289,7 @@ instance isSplitEpi_toNondegComplex : IsSplitEpi s.toNondegComplex where
 instance isSplitMono_fromNondegComplex : IsSplitMono s.fromNondegComplex where
   exists_splitMono := ⟨⟨s.toNondegComplex, by simp⟩⟩
 
+set_option backward.defeqAttrib.useBackward true in
 @[reassoc (attr := simp)]
 lemma toNondegComplex_fromNondegComplex :
     s.toNondegComplex ≫ s.fromNondegComplex = PInfty :=
diff --git a/Mathlib/AlgebraicTopology/ModelCategory/LeftHomotopy.lean b/Mathlib/AlgebraicTopology/ModelCategory/LeftHomotopy.lean
@@ -83,6 +83,7 @@ def postcomp {f g : X ⟶ Y} (h : P.LeftHomotopy f g) {Z : C} (p : Y ⟶ Z) :
     P.LeftHomotopy (f ≫ p) (g ≫ p) where
   h := h.h ≫ p
 
+set_option backward.defeqAttrib.useBackward true in
 /-- Left homotopies in a full subcategory identify to left homotopies in the
 ambient category. -/
 noncomputable def fullSubcategoryEquiv {P : ObjectProperty C} {X Y : P.FullSubcategory}
diff --git a/Mathlib/AlgebraicTopology/ModelCategory/RightHomotopy.lean b/Mathlib/AlgebraicTopology/ModelCategory/RightHomotopy.lean
@@ -86,6 +86,7 @@ def precomp {f g : X ⟶ Y} (h : P.RightHomotopy f g) {Z : C} (i : Z ⟶ X) :
     P.RightHomotopy (i ≫ f) (i ≫ g) where
   h := i ≫ h.h
 
+set_option backward.defeqAttrib.useBackward true in
 /-- Right homotopies in a full subcategory identify to right homotopies in the
 ambient category. -/
 noncomputable def fullSubcategoryEquiv {P : ObjectProperty C} {X Y : P.FullSubcategory}
diff --git a/Mathlib/AlgebraicTopology/SimplicialObject/DeltaZeroIter.lean b/Mathlib/AlgebraicTopology/SimplicialObject/DeltaZeroIter.lean
@@ -149,11 +149,13 @@ namespace Augmented
 
 variable (Y : Augmented C)
 
+set_option backward.defeqAttrib.useBackward true in
 @[reassoc (attr := simp)]
 lemma δ₀Iter_hom_app {n m : ℕ} (i : ℕ) (hi : n + i = m := by lia) :
     dsimp% Y.left.δ₀Iter i hi ≫ Y.hom.app (op ⦋n⦌) = Y.hom.app (op ⦋m⦌) := by
   simpa using Y.hom.naturality (SimplexCategory.δ₀Iter i hi).op
 
+set_option backward.defeqAttrib.useBackward true in
 @[reassoc (attr := simp)]
 lemma σ₀Iter_hom_app {n m : ℕ} (i : ℕ) (hi : n + i = m := by lia) :
     dsimp% Y.left.σ₀Iter i hi ≫ Y.hom.app (op ⦋m⦌) = Y.hom.app (op ⦋n⦌) := by
diff --git a/Mathlib/AlgebraicTopology/SimplicialObject/Split.lean b/Mathlib/AlgebraicTopology/SimplicialObject/Split.lean
@@ -289,6 +289,7 @@ theorem cofan_inj_epi_naturality {Δ₁ Δ₂ : SimplexCategoryᵒᵖ} (A : Inde
   rw [assoc, ← X.map_comp]
   rfl
 
+set_option backward.defeqAttrib.useBackward true in
 /-- The image of a splitting of simplicial object by a functor which preserves
 finite coproducts -/
 @[simps]
diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/Homology/Nondegenerate.lean b/Mathlib/AlgebraicTopology/SimplicialSet/Homology/Nondegenerate.lean
@@ -223,6 +223,7 @@ noncomputable def normalizedChainComplexFunctorObj : SSet.{w} ⥤ ChainComplex C
   obj X := X.normalizedChainComplex R
   map f := normalizedChainComplexMap f R
 
+set_option backward.defeqAttrib.useBackward true in
 /-- The morphism `X.toNormalizedChainComplex R` for any simplicial set `X`,
 as a natural transformation. -/
 @[simps]
diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/KanComplex.lean b/Mathlib/AlgebraicTopology/SimplicialSet/KanComplex.lean
@@ -62,7 +62,6 @@ lemma exists_lift_of_kanComplex [KanComplex X]
 /-- If `X` is a Kan complex and `f : ∀ (j : Fin (n + 2)) (_ : j ≠ i), Δ[n] ⟶ X`
 is a compatible family of morphisms (which defines a morphism `Λ[n + 1, i] ⟶ X`),
 then this is a lifting `Δ[n + 1] ⟶ X`. -/
-@[no_expose]
 noncomputable def liftOfKanComplex [KanComplex X] (hf : horn.IsCompatible f) :
     Δ[n + 1] ⟶ X :=
   hf.exists_lift_of_kanComplex.choose
diff --git a/Mathlib/CategoryTheory/GuitartExact/HorizontalComposition.lean b/Mathlib/CategoryTheory/GuitartExact/HorizontalComposition.lean
@@ -40,6 +40,7 @@ def whiskerHorizontal (α : T' ⟶ T) (β : B ⟶ B') :
 
 namespace GuitartExact
 
+set_option backward.defeqAttrib.useBackward true in
 /-- A 2-square stays Guitart exact if we replace the top and bottom functors
 by isomorphic functors. See also `whiskerHorizontal_iff`. -/
 lemma whiskerHorizontal [w.GuitartExact] (α : T ≅ T') (β : B ≅ B') :
@@ -85,6 +86,7 @@ def hComp' {T₁₂ : C₁ ⥤ C₃} {B₁₂ : D₁ ⥤ D₃} (eT : T₁ ⋙ T
 
 namespace GuitartExact
 
+set_option backward.defeqAttrib.useBackward true in
 instance hComp [w.GuitartExact] [w'.GuitartExact] :
     (w ≫ₕ w').GuitartExact := by
   rw [← guitartExact_op_iff]
@@ -98,6 +100,7 @@ instance hComp' {T₁₂ : C₁ ⥤ C₃} {B₁₂ : D₁ ⥤ D₃} (eT : T₁ 
   dsimp only [TwoSquare.hComp']
   infer_instance
 
+set_option backward.defeqAttrib.useBackward true in
 /-- The canonical isomorphism between
 `w.costructuredArrowRightwards Y₁ ⋙ w'.costructuredArrowRightwards (B₁.obj Y₁)` and
 `(w ≫ₕ w').costructuredArrowRightwards Y₁`. -/
@@ -133,6 +136,7 @@ lemma hComp'_iff_of_essSurj
     (w.hComp' w' eT eB).GuitartExact ↔ w'.GuitartExact :=
   ⟨fun _ ↦ of_hComp' w w' eT eB, fun _ ↦ inferInstance⟩
 
+set_option backward.defeqAttrib.useBackward true in
 lemma hComp_iff_of_equivalences (eT : C₂ ≌ C₃) (eB : D₂ ≌ D₃)
     (w' : eT.functor ⋙ V₃ ≅ V₂ ⋙ eB.functor) :
     (w ≫ₕ w'.hom).GuitartExact ↔ w.GuitartExact := by
diff --git a/Mathlib/CategoryTheory/GuitartExact/Quotient.lean b/Mathlib/CategoryTheory/GuitartExact/Quotient.lean
@@ -46,6 +46,7 @@ variable {C₀ C H₀ H : Type*} [Category* C₀] [Category* C] [Category* H₀]
   {T : C₀ ⥤ H₀} {L : C₀ ⥤ C} {R : H₀ ⥤ H} {B : C ⥤ H}
   [T.EssSurj] [T.Full] [B.Full]
 
+set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 lemma quotient_of_nonempty_leftHomotopy (e : T ⋙ R ≅ L ⋙ B)
     (he : ∀ ⦃X₀ : C₀⦄ ⦃Y : C⦄ (f₀ f₁ : L.obj X₀ ⟶ Y) (_ : B.map f₀ = B.map f₁),
diff --git a/Mathlib/CategoryTheory/Limits/Chosen/End.lean b/Mathlib/CategoryTheory/Limits/Chosen/End.lean
@@ -51,6 +51,7 @@ lemma chosenCoend.condition {i j : J} (f : i ⟶ j) :
 
 variable {F}
 
+set_option backward.defeqAttrib.useBackward true in
 /-- Morphisms out of the chosen coend are determined by their composites with `chosenCoend.ι`. -/
 @[ext]
 lemma chosenCoend.hom_ext {X : C} {f g : chosenCoend F ⟶ X}
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean
@@ -923,19 +923,22 @@ variable {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [HasPullbacksAlong g]
 
 namespace IsPullback
 
+set_option backward.defeqAttrib.useBackward true in
 /-- An `IsPullback` square yields an isomorphism `Over.mk fst ≅ Over.mk (pullback.fst f g)`
 in `Over X`. -/
 noncomputable def isoOverPullback {P : C} {fst : P ⟶ X} {snd : P ⟶ Y}
     (h : IsPullback fst snd f g) :
     Over.mk fst ≅ Over.mk (pullback.fst f g) :=
   Over.isoMk (h.isoIsPullback _ _ (IsPullback.of_hasPullback f g)) (by simp)
 
+set_option backward.defeqAttrib.useBackward true in
 @[reassoc (attr := simp)]
 lemma isoOverPullback_hom_left_comp_snd {P : C} {fst : P ⟶ X} {snd : P ⟶ Y}
     (h : IsPullback fst snd f g) :
     dsimp% h.isoOverPullback.hom.left ≫ pullback.snd f g = snd :=
   h.isoIsPullback_hom_snd _ _ (IsPullback.of_hasPullback f g)
 
+set_option backward.defeqAttrib.useBackward true in
 /-- An isomorphism `Over.mk p ≅ Over.mk (pullback.fst f g)` in `Over X` yields
 an `IsPullback` square. -/
 lemma of_over_iso {P : C} {p : P ⟶ X}
@@ -945,6 +948,7 @@ lemma of_over_iso {P : C} {p : P ⟶ X}
     ((Over.forget X).mapIso e) (Iso.refl _) (Iso.refl _) (Iso.refl _)
     (by simpa using Over.w e.hom) (by simp) (by simp) (by simp)
 
+set_option backward.defeqAttrib.useBackward true in
 /-- An `IsPullback` square over a cospan `(f, g)` is equivalent to an isomorphism
 `Over.mk fst ≅ Over.mk (pullback.fst f g)` in `Over X`, together with the
 second projection being determined by the isomorphism. -/
diff --git a/Mathlib/CategoryTheory/Localization/DerivabilityStructure/OfLocalizedEquivalences.lean b/Mathlib/CategoryTheory/Localization/DerivabilityStructure/OfLocalizedEquivalences.lean
@@ -82,6 +82,7 @@ lemma isLeftDerivabilityStructure_of_isLocalizedEquivalence
   rw [B.isLeftDerivabilityStructure_iff W₁'.Q W₂'.Q F e']
   apply TwoSquare.GuitartExact.of_hComp iso.inv
 
+set_option backward.defeqAttrib.useBackward true in
 lemma isLeftDerivabilityStructure_iff_of_isLocalizedEquivalence
     [L.functor.EssSurj] [R.functor.Full] [R.IsInduced]
     (iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor)
diff --git a/Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean b/Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean
@@ -377,6 +377,7 @@ section
 
 variable [Φ.functor.IsEquivalence] [Φ.IsInduced] [W₂.RespectsIso]
 
+set_option backward.defeqAttrib.useBackward true in
 attribute [local simp] Functor.asEquivalence_counitIso_hom_app
   Functor.asEquivalence_counitIso_inv_app in
 /-- The inverse of a localizer morphism `Φ : LocalizerMorphism W₁ W₂`,
@@ -392,10 +393,12 @@ noncomputable def inv : LocalizerMorphism W₂ W₁ where
       (Arrow.isoMk (Φ.functor.asEquivalence.counitIso.app _)
         (Φ.functor.asEquivalence.counitIso.app _))).2 hf
 
+set_option backward.defeqAttrib.useBackward true in
 instance : Φ.inv.functor.IsEquivalence := by
   dsimp
   infer_instance
 
+set_option backward.defeqAttrib.useBackward true in
 attribute [local simp] Functor.asEquivalence_inverse
   Functor.asEquivalence_counitIso_hom_app Functor.asEquivalence_counitIso_inv_app in
 instance : Φ.inv.IsInduced where
@@ -406,6 +409,7 @@ instance : Φ.inv.IsInduced where
       (Arrow.isoMk (Φ.functor.asEquivalence.counitIso.app _)
         (Φ.functor.asEquivalence.counitIso.app _))
 
+set_option backward.defeqAttrib.useBackward true in
 lemma isLocalizedEquivalence_of_isInduced :
     Φ.IsLocalizedEquivalence := by
   refine IsLocalizedEquivalence.of_equivalence _ (fun X Y f hf ↦ ?_)
diff --git a/Mathlib/CategoryTheory/Monoidal/Cartesian/Ring.lean b/Mathlib/CategoryTheory/Monoidal/Cartesian/Ring.lean
@@ -36,10 +36,12 @@ def yonedaRingObj (R : C) [RingObj R] : Cᵒᵖ ⥤ RingCat.{v} where
       map_mul' _ _ := MonObj.comp_mul _ _ _
       map_add' _ _ := AddMonObj.comp_add _ _ _ }
 
+set_option backward.defeqAttrib.useBackward true in
 @[simp]
 lemma yonedaRingObj_map_apply {R : C} [RingObj R] {X Y : Cᵒᵖ} (f : X ⟶ Y) (x : X.unop ⟶ R) :
     dsimp% (yonedaRingObj R).map f x = f.unop ≫ x := rfl
 
+set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 /-- The yoneda embedding of `RingObjCat C` into presheaves of rings. -/
 def yonedaRing : RingObjCat C ⥤ Cᵒᵖ ⥤ RingCat.{v} where
@@ -58,10 +60,12 @@ def yonedaCommRingObj (R : C) [CommRingObj R] : Cᵒᵖ ⥤ CommRingCat.{v} wher
   obj X := .of (X.unop ⟶ R)
   map f := CommRingCat.ofHom ((yonedaRingObj R).map f).hom
 
+set_option backward.defeqAttrib.useBackward true in
 @[simp]
 lemma yonedaCommRingObj_map_apply {R : C} [CommRingObj R] {X Y : Cᵒᵖ} (f : X ⟶ Y) (x : X.unop ⟶ R) :
     dsimp% (yonedaCommRingObj R).map f x = f.unop ≫ x := rfl
 
+set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 /-- The yoneda embedding of `CommRingObjCat C` into presheaves of commutative rings. -/
 @[simps obj]
diff --git a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean
@@ -175,6 +175,7 @@ instance [A.IsTriangulated] :
     (triangulatedLocalizerMorphism A B).functor.IsTriangulated :=
   inferInstanceAs A.ι.IsTriangulated
 
+set_option backward.defeqAttrib.useBackward true in
 lemma trW_inverseImage_ι_iff [A.IsTriangulated] {X Y : A.FullSubcategory} (f : X ⟶ Y) :
     (B.inverseImage A.ι).trW f ↔ (A ⊓ B).trW f.hom := by
   simp only [trW_iff]
@@ -190,6 +191,7 @@ lemma trW_inverseImage_ι_iff [A.IsTriangulated] {X Y : A.FullSubcategory} (f :
     · cat_disch
     · simp [dsimp% (A.ι.commShiftIso (1 : ℤ)).inv_hom_id_app X]
 
+set_option backward.defeqAttrib.useBackward true in
 lemma inverseImage_opEquivalence_inverse_trW_inverseImage_ι_op [A.IsTriangulated]
     [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] :
     (B.op.inverseImage A.op.ι).trW.inverseImage A.opEquivalence.inverse =
@@ -205,6 +207,7 @@ variable [A.IsVerdierRightLocalizing B]
   (L₁ : A.FullSubcategory ⥤ D₁) (L₂ : C ⥤ D₂)
   [L₁.IsLocalization (B.inverseImage A.ι).trW] [L₂.IsLocalization B.trW]
 
+set_option backward.defeqAttrib.useBackward true in
 instance : ((A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂).Full := by
   let F := (A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂
   have : L₁.EssSurj := Localization.essSurj L₁ (B.inverseImage A.ι).trW
@@ -237,6 +240,7 @@ instance [Preadditive D₁] [Preadditive D₂] [L₁.Additive] [L₂.Additive] :
     (A.triangulatedLocalizerMorphism B).functor L₁ L₂ F
   exact Functor.additive_of_iso e
 
+set_option backward.defeqAttrib.useBackward true in
 instance : ((A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂).Faithful := by
   letI := Localization.preadditive L₁ (B.inverseImage A.ι).trW
   letI := Localization.preadditive L₂ B.trW
diff --git a/Mathlib/Condensed/Light/Epi.lean b/Mathlib/Condensed/Light/Epi.lean
@@ -135,6 +135,7 @@ instance : Epi (Limits.Pi.map f) :=
       Functor.ofOpSequence_map_homOfLE_succ]
     infer_instance)
 
+set_option backward.defeqAttrib.useBackward true in
 instance : (lim (J := Discrete ℕ) (C := LightCondMod R)).PreservesEpimorphisms where
   preserves f _ := by
     have : lim.map f = (Pi.isoLimit _).inv ≫ Limits.Pi.map (f.app ⟨·⟩) ≫ (Pi.isoLimit _).hom := by
diff --git a/Mathlib/NumberTheory/ModularForms/DimensionFormulas/LevelOne.lean b/Mathlib/NumberTheory/ModularForms/DimensionFormulas/LevelOne.lean
@@ -6,7 +6,6 @@ Authors: Chris Birkbeck
 module -- shake: keep-all
 
 public import Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
-public import Mathlib.Tactic.Linter.DeprecatedModule
 
 deprecated_module "Use `Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula` instead."
   (since := "2026-05-06")
diff --git a/Mathlib/NumberTheory/ModularForms/LevelOne.lean b/Mathlib/NumberTheory/ModularForms/LevelOne.lean
@@ -6,7 +6,6 @@ Authors: Chris Birkbeck
 module -- shake: keep-all
 
 public import Mathlib.NumberTheory.ModularForms.LevelOne.Basic
-public import Mathlib.Tactic.Linter.DeprecatedModule
 
 deprecated_module "Use `Mathlib.NumberTheory.ModularForms.LevelOne.Basic` instead."
   (since := "2026-05-06")
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8e1db9dde3100736e39943b355d076c6f3b38fff",
+   "rev": "c566127911e3b1176bd9a67136897c9c9f96a67c",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2026-05-10
+leanprover/lean4:nightly-2026-05-11
