chore: adaptations for nightly-2026-05-03 (#215)

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

Author: kim-em

Archive/Imo/Imo1988Q6.lean

@@ -171,7 +171,7 @@ theorem constant_descent_vieta_jumping (x y : ℕ) {claim : Prop} {H : ℕ → 
   rw [exceptional_empty, Set.diff_empty]
   -- Now we are ready to prove that p' = (c, m_x) lies on the upper branch.
   -- We need to check two conditions: H(c, m_x) and c < m_x.
-  constructor <;> dsimp only
+  constructor
   · -- The first condition is not so hard. After all, c is the other root of the quadratic equation.
     rw [H_symm, H_quad]
     simpa using h_root

Counterexamples/Phillips.lean

@@ -284,8 +284,7 @@ theorem exists_discrete_support_nonpos (f : BoundedAdditiveMeasure α) :
     intro n
     rw [div_le_iff₀' (show (0 : ℝ) < 2 by simp), hε]
     convert hF (s n) u using 2
-    · dsimp
-      ext x
+    · ext x
       simp only [u, not_exists, mem_iUnion, mem_diff]
       tauto
     · congr 1

Mathlib/Algebra/Algebra/NonUnitalHom.lean

@@ -348,7 +348,7 @@ variable (R A B)
 variable [DistribMulAction R B]
 
 /-- The first projection of a product is a non-unital algebra homomorphism. -/
-@[simps]
+@[simps toFun]
 def fst : A × B →ₙₐ[R] A where
   toFun := Prod.fst
   map_zero' := rfl
@@ -357,7 +357,7 @@ def fst : A × B →ₙₐ[R] A where
   map_mul' _ _ := rfl
 
 /-- The second projection of a product is a non-unital algebra homomorphism. -/
-@[simps]
+@[simps toFun]
 def snd : A × B →ₙₐ[R] B where
   toFun := Prod.snd
   map_zero' := rfl
@@ -369,7 +369,7 @@ variable {R A B}
 variable [DistribMulAction R C]
 
 /-- The prod of two morphisms is a morphism. -/
-@[simps]
+@[simps toFun]
 def prod (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) : A →ₙₐ[R] B × C where
   toFun := Pi.prod f g
   map_zero' := by simp only [Pi.prod, Prod.mk_zero_zero, map_zero]

Mathlib/Algebra/Algebra/Unitization.lean

@@ -672,7 +672,7 @@ section coe
 
 /-- The coercion from a non-unital `R`-algebra `A` to its unitization `Unitization R A`
 realized as a non-unital algebra homomorphism. -/
-@[simps]
+@[simps toFun]
 def inrNonUnitalAlgHom (R A : Type*) [CommSemiring R] [NonUnitalSemiring A] [Module R A] :
     A →ₙₐ[R] Unitization R A where
   toFun := (↑)
@@ -763,7 +763,7 @@ def _root_.NonUnitalAlgHom.toAlgHom (φ : A →ₙₐ[R] C) : Unitization R A 
 set_option backward.isDefEq.respectTransparency false in
 /-- Non-unital algebra homomorphisms from `A` into a unital `R`-algebra `C` lift uniquely to
 `Unitization R A →ₐ[R] C`. This is the universal property of the unitization. -/
-@[simps! apply symm_apply apply_apply]
+@[simps! apply symm_apply]
 def lift : (A →ₙₐ[R] C) ≃ (Unitization R A →ₐ[R] C) where
   toFun := NonUnitalAlgHom.toAlgHom
   invFun φ := φ.toNonUnitalAlgHom.comp (inrNonUnitalAlgHom R A)
@@ -800,7 +800,7 @@ variable [StarModule R C]
 
 /-- Non-unital star algebra homomorphisms from `A` into a unital star `R`-algebra `C` lift uniquely
 to `Unitization R A →⋆ₐ[R] C`. This is the universal property of the unitization. -/
-@[simps! apply symm_apply apply_apply]
+@[simps! apply symm_apply]
 def starLift : (A →⋆ₙₐ[R] C) ≃ (Unitization R A →⋆ₐ[R] C) :=
 { toFun := fun φ ↦
   { toAlgHom := Unitization.lift φ.toNonUnitalAlgHom

Mathlib/Algebra/Category/AlgCat/Basic.lean

@@ -187,6 +187,7 @@ def free : Type u ⥤ AlgCat.{u} R where
   obj S := of R (FreeAlgebra R S)
   map f := ofHom <| FreeAlgebra.lift _ <| FreeAlgebra.ι _ ∘ f
 
+set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 /-- The free/forget adjunction for `R`-algebras. -/
 def adj : free.{u} R ⊣ forget (AlgCat.{u} R) :=

Mathlib/Algebra/Category/AlgCat/Limits.lean

@@ -19,6 +19,8 @@ Further, these limits are preserved by the forgetful functor --- that is,
 the underlying types are just the limits in the category of types.
 -/
 
+set_option backward.defeqAttrib.useBackward true
+
 @[expose] public section
 
 

Mathlib/Algebra/Category/CoalgCat/ComonEquivalence.lean

@@ -132,11 +132,10 @@ theorem tensorObj_comul (K L : CoalgCat R) :
       = (TensorProduct.tensorTensorTensorComm R K K L L).toLinearMap
       ∘ₗ TensorProduct.map Coalgebra.comul Coalgebra.comul := by
   rw [ofComonObjCoalgebraStruct_comul]
-  simp only [Comon.monoidal_tensorObj_comon_comul, Equivalence.symm_inverse,
-    comonEquivalence_functor, toComon_obj, toComonObj_X, ModuleCat.of_coe,
+  simp only [Comon.monoidal_tensorObj_comon_comul,
     MonObj.tensorObj.mul_def, unop_comp, unop_tensorObj, unop_tensorHom,
     BraidedCategory.unop_tensorμ, tensorμ_eq_tensorTensorTensorComm, ModuleCat.hom_comp,
-    ModuleCat.hom_ofHom, LinearEquiv.comp_toLinearMap_eq_iff]
+    ModuleCat.hom_ofHom]
   rfl
 
 theorem tensorHom_toLinearMap (f : M →ₗc[R] N) (g : P →ₗc[R] Q) :
@@ -180,6 +179,7 @@ theorem comul_tensorObj_tensorObj_right :
     AlgebraTensorModule.tensorTensorTensorComm_eq]
   rfl
 
+set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 attribute [local simp] MonObj.tensorObj.one_def MonObj.tensorObj.mul_def in
 theorem comul_tensorObj_tensorObj_left :

Mathlib/Algebra/Category/ContinuousCohomology/Basic.lean

@@ -43,6 +43,8 @@ See `ContinuousCohomology.MultiInd.d`.
 - Show that short exact sequences induce long exact sequences in certain scenarios.
 -/
 
+set_option backward.defeqAttrib.useBackward true
+
 @[expose] public section
 
 open CategoryTheory Functor ContinuousMap

Mathlib/Algebra/Category/Grp/AB.lean

@@ -24,12 +24,14 @@ universe u
 
 open CategoryTheory Limits
 
+set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 instance {J C : Type*} [Category* J] [Category* C] [HasColimitsOfShape J C] [Preadditive C] :
     (colim (J := J) (C := C)).Additive where
 
 variable {J : Type u} [SmallCategory J] [IsFiltered J]
 
+set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 noncomputable instance :
     (colim (J := J) (C := AddCommGrpCat.{u})).PreservesHomology :=
@@ -77,12 +79,11 @@ instance : HasExactLimitsOfShape (Discrete J) (AddCommGrpCat.{u}) := by
           IsLimit.conePointUniqueUpToIso, limit.cone, AddCommGrpCat.HasLimit.productLimitCone,
           Iso.trans_inv, Functor.mapIso_inv, IsLimit.uniqueUpToIso_inv, Cone.forget_map,
           IsLimit.liftConeMorphism_hom, limit.isLimit_lift, Iso.symm_inv, Functor.mapIso_hom,
-          IsLimit.uniqueUpToIso_hom, lim_obj, lim_map, Iso.trans_hom, Iso.symm_hom,
-          AddCommGrpCat.HasLimit.lift, Functor.const_obj_obj, Category.assoc, limit.lift_map_assoc,
-          Pi.cone_pt, iX, iY]
+          IsLimit.uniqueUpToIso_hom, lim_map, Iso.trans_hom, Iso.symm_hom,
+          AddCommGrpCat.HasLimit.lift, Category.assoc, limit.lift_map_assoc, iX, iY]
         ext g j
         change _ = (_ ≫ limit.π (Discrete.functor fun j ↦ Y.obj { as := j }) ⟨j⟩) _
-        simp only [Discrete.functor_obj_eq_as, productIsProduct', limit.lift_π, Fan.mk_pt,
+        simp only [Discrete.functor_obj_eq_as, productIsProduct', limit.lift_π,
           Fan.mk_π_app, Pi.map_apply]
         change _ = (_ ≫ _ ≫ limit.π Y ⟨j⟩) _
         simp

Mathlib/Algebra/Category/Grp/Adjunctions.lean

@@ -65,6 +65,7 @@ theorem free_map_coe {α β : Type u} {f : α ⟶ β} (x : FreeAbelianGroup α)
     (free.map f) x = f <$> x :=
   rfl
 
+set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 /-- The free-forgetful adjunction for abelian groups.
 -/