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

Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com>

Author: kim-em

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

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]

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

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 :=

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}

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}

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

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

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 ↦ ?_)

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]