diff --git a/Mathlib/Algebra/Category/AlgCat/FilteredColimits.lean b/Mathlib/Algebra/Category/AlgCat/FilteredColimits.lean
index b4d8bd65a4c4e1..3d2e7462804536 100644
--- a/Mathlib/Algebra/Category/AlgCat/FilteredColimits.lean
+++ b/Mathlib/Algebra/Category/AlgCat/FilteredColimits.lean
@@ -31,6 +31,7 @@ section
 
 variable {c : Cocone (F ⋙ forget₂ _ RingCat)} [IsFilteredOrEmpty J]
 
+set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency 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
@@ -41,6 +42,7 @@ private abbrev AlgCat.algebraOfIsFiltered (hc : IsColimit c) (j : J) : Algebra R
     obtain ⟨k, hjk, y, rfl⟩ := Concrete.exists_hom_ι_eq_of_isColimit _ hc x j
     simp [← dsimp% c.w hjk, ← dsimp% (c.ι.app k).hom.map_mul, Algebra.commutes']
 
+set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 /-- The cocone of the underlying diagram of rings lifted to `AlgCat R`. The algebra instance
 on the cocone point is induced from the `j`-th inclusion map. -/
@@ -57,6 +59,7 @@ private def AlgCat.coconeOfIsFiltered (hc : IsColimit c) (j : J) : Cocone F wher
     ext
     exact c.ι.naturality_apply _ _
 
+set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 /-- The lifted cocone is colimiting. -/
 private def AlgCat.isColimitCoconeOfIsFiltered (hc : IsColimit c) (j : J) :
diff --git a/Mathlib/Algebra/Exact/Sequence.lean b/Mathlib/Algebra/Exact/Sequence.lean
index b753805f0eda90..5cc990339f1579 100644
--- a/Mathlib/Algebra/Exact/Sequence.lean
+++ b/Mathlib/Algebra/Exact/Sequence.lean
@@ -48,8 +48,23 @@ public lemma sum_neg_one_pow_finrank_eq_zero_of_exact {n : ℕ} (V : Fin (n + 2)
   simp_rw [← smul_eq_mul]
   refine Fin.sum_neg_one_pow_eq_zero _ (fun i ↦ finrank k (f i).range) ?_ (fun i ↦ ?_) ?_
   · aesop
-  · grind [(h_exact i).linearMap_ker_eq, (f i.succ).finrank_range_add_finrank_ker]
-  · grind [finrank_top]
+  · #adaptation_note /-- Prior to v4.31.0-rc1, this proof was
+      ```
+      grind [(h_exact i).linearMap_ker_eq, (f i.succ).finrank_range_add_finrank_ker]
+      ```
+      -/
+    have hrn := (f i.succ).finrank_range_add_finrank_ker
+    have hker : finrank k ↥(LinearMap.ker (f i.succ)) =
+        finrank k ↥(LinearMap.range (f i.castSucc)) :=
+      congrArg (fun S : Submodule k (V i.succ.castSucc) => finrank k ↥S)
+        (h_exact i).linearMap_ker_eq
+    omega
+  · #adaptation_note /-- Prior to v4.31.0-rc1, this proof was
+      ```
+      grind [finrank_top]
+      ```
+      -/
+    rw [surj, finrank_top, Fin.succ_last]
 
 /- An unrolled version of `Module.sum_neg_one_pow_finrank_eq_zero_of_exact`. This is an auxiliary
 lemma en route to `Module.sum_neg_one_pow_finrank_eq_zero_of_exact_six`. -/
@@ -78,7 +93,7 @@ private lemma sum_neg_one_pow_finrank_eq_zero_of_exact_six_aux {V₀ V₁ V₂ V
   | 0 => ‹_› | 1 => ‹_› | 2 => ‹_› | 3 => ‹_› | 4 => ‹_› | 5 => ‹_›
   letI fs (i : Fin 5) : Vs i.castSucc →ₗ[k] Vs i.succ := match i with
   | 0 => f₀ | 1 => f₁ | 2 => f₂ | 3 => f₃ | 4 => f₄
-  simpa [Fin.sum_univ_six] using Module.sum_neg_one_pow_finrank_eq_zero_of_exact Vs fs inj
+  simpa [Fin.sum_univ_six] using! Module.sum_neg_one_pow_finrank_eq_zero_of_exact Vs fs inj
     (fun i ↦ by fin_cases i; exacts [exact₁, exact₂, exact₃, exact₄]) surj
 
 /-- This is an unrolled, universe-polymorphic version of
diff --git a/Mathlib/AlgebraicGeometry/Birational/Dominant.lean b/Mathlib/AlgebraicGeometry/Birational/Dominant.lean
index 51b3684889c0f1..f41ec7096c0df6 100644
--- a/Mathlib/AlgebraicGeometry/Birational/Dominant.lean
+++ b/Mathlib/AlgebraicGeometry/Birational/Dominant.lean
@@ -34,6 +34,7 @@ namespace Scheme
 
 namespace PartialMap
 
+set_option backward.defeqAttrib.useBackward true in
 /-- Restricting a dominant partial map to a dense open yields a dominant partial map. -/
 lemma isDominant_restrict_hom (f : X.PartialMap Y) [IsDominant f.hom] (U : X.Opens)
     (hU : Dense (U : Set X)) (hU' : U ≤ f.domain) : IsDominant (f.restrict U hU hU').hom := by
@@ -54,6 +55,7 @@ lemma isDominant_hom_iff_isDominant_restrict_hom (f : X.PartialMap Y) (U : X.Ope
   ⟨fun _ ↦ f.isDominant_restrict_hom U hU hU',
     fun _ ↦ f.isDominant_hom_of_isDominant_restrict_hom U hU hU'⟩
 
+set_option backward.defeqAttrib.useBackward true in
 /-- Dominance of the underlying morphism is invariant under equivalence of partial maps. -/
 lemma isDominant_hom_iff_of_equiv (f g : X.PartialMap Y) (h : f.equiv g) :
     IsDominant f.hom ↔ IsDominant g.hom := by
diff --git a/Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean b/Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean
index 273a47b7a997c2..7e6761fa8ed7d9 100644
--- a/Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean
+++ b/Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean
@@ -101,7 +101,7 @@ theorem d_squared (n : ℕ) : objD X (n + 1) ≫ objD X n = 0 := by
     simp_rw [S, Finset.compl_filter, Finset.mem_filter_univ, not_le] at hij'
     refine ⟨(j'.pred <| ?_, Fin.castSucc i'), ?_, ?_⟩
     · rintro rfl
-      simp only [Fin.val_zero, not_lt_zero'] at hij'
+      simp only [Fin.val_zero, not_lt_zero] at hij'
     · simpa [S] using! Nat.le_sub_one_of_lt hij'
     · simp only [φ, Fin.castLT_castSucc, Fin.succ_pred]
   · -- identification of corresponding terms in both sums
diff --git a/Mathlib/Analysis/Calculus/IteratedDeriv/Analytic.lean b/Mathlib/Analysis/Calculus/IteratedDeriv/Analytic.lean
index 1719a7631e352d..826f26c64e6cf7 100644
--- a/Mathlib/Analysis/Calculus/IteratedDeriv/Analytic.lean
+++ b/Mathlib/Analysis/Calculus/IteratedDeriv/Analytic.lean
@@ -45,7 +45,7 @@ lemma iteratedDeriv_mul_pow_sub_of_analytic {k t : ℕ} {z₀ : 𝕜} {R R₁ :
         (z - z₀) ^ (t + 1) * ((k + (t + 1))! / (t + 1)! * deriv R₁ z +
           (R₂ z + (z - z₀) * deriv R₂ z)) := by
         have hsub : HasDerivAt (· - z₀) 1 z := (hasDerivAt_id z).sub_const z₀
-        simpa using ((hsub.fun_pow (t + 1)).mul
+        simpa using! ((hsub.fun_pow (t + 1)).mul
           (((hf1 z).differentiableAt.hasDerivAt.const_mul ((k + (t + 1))! / (t + 1)! : 𝕜)).add
             (hsub.mul (hR₂ z).differentiableAt.hasDerivAt))).deriv
       _ = (z - z₀) ^ t * ((k + 1 + t)! / t ! * R₁ z + (z - z₀) * R₂' z) := by
diff --git a/Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean b/Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean
index e8ff0c1be75736..553ce537e599d6 100644
--- a/Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean
+++ b/Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean
@@ -160,6 +160,7 @@ lemma hasPointwiseRightKanExtensionAt_iff_of_equivalence
         isoWhiskerLeft L E.unitIso.symm ≪≫ L.rightUnitor) Y' Y
       (E.inverse.mapIso e.symm ≪≫ E.unitIso.symm.app Y)
 
+set_option backward.defeqAttrib.useBackward true in
 lemma HasPointwiseLeftKanExtensionAt.of_natIso {L L' : C ⥤ D} {F F' : C ⥤ H} (Y : D)
     [L.HasPointwiseLeftKanExtensionAt F Y] (e₁ : L ≅ L') (e₂ : F ≅ F') :
     L'.HasPointwiseLeftKanExtensionAt F' Y := by
@@ -176,6 +177,7 @@ lemma hasPointwiseLeftKanExtensionAt_iff_of_natIso {L L' : C ⥤ D} {F F' : C 
     L.HasPointwiseLeftKanExtensionAt F Y ↔ L'.HasPointwiseLeftKanExtensionAt F' Y :=
   ⟨fun _ ↦ .of_natIso Y e₁ e₂, fun _ ↦ .of_natIso Y e₁.symm e₂.symm⟩
 
+set_option backward.defeqAttrib.useBackward true in
 lemma HasPointwiseRightKanExtensionAt.of_natIso {L L' : C ⥤ D} {F F' : C ⥤ H} (Y : D)
     [L.HasPointwiseRightKanExtensionAt F Y] (e₁ : L ≅ L') (e₂ : F ≅ F') :
     L'.HasPointwiseRightKanExtensionAt F' Y := by
diff --git a/Mathlib/CategoryTheory/Limits/ConcreteCategory/Basic.lean b/Mathlib/CategoryTheory/Limits/ConcreteCategory/Basic.lean
index dcb5f4112bdc03..f8ee87a55d2238 100644
--- a/Mathlib/CategoryTheory/Limits/ConcreteCategory/Basic.lean
+++ b/Mathlib/CategoryTheory/Limits/ConcreteCategory/Basic.lean
@@ -188,6 +188,7 @@ theorem colimit_rep_eq_iff_exists [HasColimit F] {i j : J} (x : ToType (F.obj i)
     colimit.ι F i x = colimit.ι F j y ↔ ∃ (k : _) (f : i ⟶ k) (g : j ⟶ k), F.map f x = F.map g y :=
   ⟨Concrete.colimit_exists_of_rep_eq.{s} _ _ _, Concrete.colimit_rep_eq_of_exists _ _ _⟩
 
+set_option backward.defeqAttrib.useBackward true in
 omit [IsFiltered J] in
 theorem exists_hom_ι_eq_of_isColimit [IsFilteredOrEmpty J] {D : Cocone F} (hD : IsColimit D)
     (x : ToType D.pt) (k : J) :
diff --git a/Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean b/Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean
index 60e3c49438d50c..3d2e6fc3eec498 100644
--- a/Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean
@@ -204,6 +204,7 @@ def normalizeIsoApp' :
 @[simp] theorem normalizeIsoApp'_unit (n : NormalMonoidalObject C) :
     normalizeIsoApp' C (𝟙_ (F C)) n = ρ_ _ := rfl
 
+set_option backward.defeqAttrib.useBackward true in
 theorem normalizeIsoApp_eq :
     ∀ (X : F C) (n : N C), normalizeIsoApp C X n = normalizeIsoApp' C X n.as
   | of _, _ => rfl
@@ -279,6 +280,7 @@ theorem normalize_naturality (n : NormalMonoidalObject C) {X Y : F C} (f : X ⟶
 
 end
 
+set_option backward.defeqAttrib.useBackward true in
 /-- The isomorphism between `n ⊗ X` and `normalize X n` is natural (in both `X` and `n`, but
 naturality in `n` is trivial and was "proved" in `normalizeIsoAux`). This is the real heart
 of our proof of the coherence theorem. -/
diff --git a/Mathlib/CategoryTheory/MorphismProperty/LocalEpi.lean b/Mathlib/CategoryTheory/MorphismProperty/LocalEpi.lean
index 935459598ce7d3..3a791ea96f8fc9 100644
--- a/Mathlib/CategoryTheory/MorphismProperty/LocalEpi.lean
+++ b/Mathlib/CategoryTheory/MorphismProperty/LocalEpi.lean
@@ -47,7 +47,7 @@ def localEpi (P : ObjectProperty C) : MorphismProperty C := fun _ _ f ↦
   ∀ ⦃Z⦄, P Z → Function.Injective fun (g : _ ⟶ Z) ↦ f ≫ g
 
 instance : P.localEpi.IsMultiplicative where
-  id_mem X Z _ := by simpa using Function.injective_id
+  id_mem X Z _ := by simpa using! Function.injective_id
   comp_mem f g hf hg T hT _ _ huv := hg hT (hf hT <| by simpa using huv)
 
 lemma localEpi.of_epi {X Y : C} (f : X ⟶ Y) [Epi f] : P.localEpi f := by
@@ -101,6 +101,7 @@ variable {D : Type*} [Category* D] {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G)
   [G.Faithful] [G.Full]
 include adj
 
+set_option backward.isDefEq.respectTransparency false in
 lemma localEpi_mem_range_iff_epi {X Y : C} (f : X ⟶ Y) :
     localEpi (· ∈ Set.range G.obj) f ↔ Epi (F.map f) := by
   rw [← dsimp% (localEpi (· ∈ Set.range G.obj)).postcomp_iff _ _ (isLocal_adj_unit_app adj Y),
diff --git a/Mathlib/CategoryTheory/MorphismProperty/OverAdjunction.lean b/Mathlib/CategoryTheory/MorphismProperty/OverAdjunction.lean
index 9560db0ac8f925..536698b9fb6302 100644
--- a/Mathlib/CategoryTheory/MorphismProperty/OverAdjunction.lean
+++ b/Mathlib/CategoryTheory/MorphismProperty/OverAdjunction.lean
@@ -58,6 +58,7 @@ def Over.mapCongr [Q.RespectsIso] {X Y : T} {f g : X ⟶ Y} (hfg : f = g) (hf :
   NatIso.ofComponents (fun Y ↦ Over.isoMk (Iso.refl _))
 
 set_option backward.defeqAttrib.useBackward true in
+set_option linter.overlappingInstances false in
 /-- `Over.map` preserves identities. -/
 @[simps!]
 def Over.mapId [P.IsMultiplicative] [Q.RespectsIso] (X : T) (f : X ⟶ X := 𝟙 X)
@@ -237,6 +238,7 @@ def Under.mapCongr [Q.RespectsIso] {X Y : T} {f g : X ⟶ Y} (hfg : f = g) (hf :
   NatIso.ofComponents (fun Y ↦ Under.isoMk (Iso.refl _))
 
 set_option backward.defeqAttrib.useBackward true in
+set_option linter.overlappingInstances false in
 /-- `Under.map` preserves identities. -/
 @[simps!]
 def Under.mapId [P.IsMultiplicative] [Q.RespectsIso] (X : T) (f : X ⟶ X := 𝟙 X)
diff --git a/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean
index 19cefefefa89f7..287c35be55071b 100644
--- a/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean
+++ b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean
@@ -76,7 +76,7 @@ instance (J : Type u) [SmallCategory J] [IsCardinalFiltered J κ] :
     simp only [(isCardinalFiltered κ).prop_iff_of_iso
       (p.isColimit.coconePointUniqueUpToIso
         (Limits.isColimitCocone (colimit.isColimit (p.diag ⋙ forget PartOrdEmb)))),
-      isCardinalFiltered_iff, Limits.cocone_pt_coe]
+      isCardinalFiltered_iff]
     exact Limits.CoconePt.isCardinalFiltered_pt _ p.prop_diag_obj
 
 end PartOrdEmb
@@ -138,6 +138,7 @@ variable {J : CardinalFilteredPoset κ} (P : Set J.obj → Prop)
   [IsDirectedOrder (Subtype P)] [Nonempty (Subtype P)]
   [∀ (S : Subtype P), IsCardinalFiltered S.val κ]
 
+set_option backward.defeqAttrib.useBackward true in
 /-- Given a predicate `P : Set J.obj → Prop` on the underlying type
 of `J : CardinalFilteredPoset κ` such that all the subsets satisfying `P`
 are `κ`-filtered, this is the functor `Subtype P ⥤ CardinalFilteredPoset κ`
diff --git a/Mathlib/Data/Finsupp/Single.lean b/Mathlib/Data/Finsupp/Single.lean
index 946b894e1c2573..21adbb24170720 100644
--- a/Mathlib/Data/Finsupp/Single.lean
+++ b/Mathlib/Data/Finsupp/Single.lean
@@ -162,7 +162,7 @@ lemma apply_surjective (a : α) : Surjective fun f : α →₀ M ↦ f a :=
   RightInverse.surjective fun _ ↦ single_eq_same
 
 theorem support_single_ne_bot (i : α) (h : b ≠ 0) : (single i b).support ≠ ⊥ := by
-  simpa only [support_single_ne_zero _ h] using! singleton_ne_empty _
+  simpa only [support_single _ h] using! singleton_ne_empty _
 
 theorem support_single_disjoint {b' : M} (hb : b ≠ 0) (hb' : b' ≠ 0) {i j : α} :
     Disjoint (single i b).support (single j b').support ↔ i ≠ j := by
diff --git a/Mathlib/FieldTheory/Galois/IsGaloisGroup.lean b/Mathlib/FieldTheory/Galois/IsGaloisGroup.lean
index d0865291abcb27..948287d95fcc92 100644
--- a/Mathlib/FieldTheory/Galois/IsGaloisGroup.lean
+++ b/Mathlib/FieldTheory/Galois/IsGaloisGroup.lean
@@ -658,7 +658,7 @@ theorem map_quotientMk' [Finite G] [IsGaloisGroup G K L] (h : E ≤ F) :
     isInvariant := ⟨fun x h ↦ by
       obtain ⟨a, ha⟩ := hE.isInvariant.isInvariant (algebraMap F L x) (by
         rintro ⟨g, hg⟩
-        simpa only [← algebraMap.smul'] using congr_arg (algebraMap F L) <| h ⟨g, ⟨g, hg, rfl⟩⟩)
+        simpa only [← algebraMap.smul'] using! congr_arg (algebraMap F L) <| h ⟨g, ⟨g, hg, rfl⟩⟩)
       exact ⟨a, FaithfulSMul.algebraMap_injective F L
         (by rw [← IsScalarTower.algebraMap_apply, ha])⟩⟩ }
 
diff --git a/Mathlib/GroupTheory/FreeGroup/Basic.lean b/Mathlib/GroupTheory/FreeGroup/Basic.lean
index 95fd9a588f7de9..851a53634f6356 100644
--- a/Mathlib/GroupTheory/FreeGroup/Basic.lean
+++ b/Mathlib/GroupTheory/FreeGroup/Basic.lean
@@ -331,6 +331,7 @@ protected theorem sublist : Red L₁ L₂ → L₂ <+ L₁ :=
 theorem length_le (h : Red L₁ L₂) : L₂.length ≤ L₁.length :=
   h.sublist.length_le
 
+set_option linter.auxLemma false in
 @[to_additive (attr := deprecated "Should not be needed." (since := "2026-04-10"))]
 theorem sizeof_of_step : ∀ {L₁ L₂ : List (α × Bool)},
     Step L₁ L₂ → sizeOf L₂ < sizeOf L₁
diff --git a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
index a01264c58a03f6..311f9c917ef96f 100644
--- a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
+++ b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
@@ -853,6 +853,7 @@ lemma apply_eq_zero_of_isEmpty [IsEmpty α] {_ : MeasurableSpace α} (μ : Measu
 instance instSubsingleton [IsEmpty α] {m : MeasurableSpace α} : Subsingleton (Measure α) :=
   ⟨fun μ ν => by ext1 s _; rw [apply_eq_zero_of_isEmpty, apply_eq_zero_of_isEmpty]⟩
 
+set_option warning.simp.varHead false in
 @[nontriviality]
 theorem eq_zero_of_isEmpty [IsEmpty α] {_m : MeasurableSpace α} (μ : Measure α) : μ = 0 :=
   Subsingleton.elim μ 0
diff --git a/Mathlib/MeasureTheory/VectorMeasure/Basic.lean b/Mathlib/MeasureTheory/VectorMeasure/Basic.lean
index fe5b8cacde321f..9e55f34abbfee5 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Basic.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Basic.lean
@@ -290,6 +290,7 @@ lemma apply_eq_zero_of_isEmpty [IsEmpty α] (μ : VectorMeasure α M) (s : Set 
 instance [IsEmpty α] : Subsingleton (VectorMeasure α M) :=
   ⟨fun μ ν => by ext; rw [apply_eq_zero_of_isEmpty, apply_eq_zero_of_isEmpty]⟩
 
+set_option warning.simp.varHead false in
 @[nontriviality]
 theorem eq_zero_of_isEmpty [IsEmpty α] (μ : VectorMeasure α M) : μ = 0 :=
   Subsingleton.elim μ 0
diff --git a/Mathlib/NumberTheory/ModularForms/DimensionFormulas/LevelOne.lean b/Mathlib/NumberTheory/ModularForms/DimensionFormulas/LevelOne.lean
index 70640ff9099a42..4beb412013a4e2 100644
--- 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/Probability/Independence/Basic.lean b/Mathlib/Probability/Independence/Basic.lean
index 5d738a7df45802..680f9930fa7ed5 100644
--- a/Mathlib/Probability/Independence/Basic.lean
+++ b/Mathlib/Probability/Independence/Basic.lean
@@ -877,7 +877,7 @@ theorem iIndepFun_iff_map_fun_eq_pi_map [Fintype ι] {β : ι → Type*}
       simp
   intro h S s hs
   specialize h₀ (s := fun i ↦ if i ∈ S then s i else univ)
-    fun i ↦ by beta_reduce; split_ifs with hiS <;> simp [hiS, hs]
+    fun i ↦ by split_ifs with hiS <;> simp [hiS, hs]
   simp only [apply_ite, preimage_univ, measure_univ, Finset.prod_ite_mem, Finset.univ_inter,
     Finset.prod_ite, Finset.filter_univ_mem, iInter_ite, iInter_univ, inter_univ, h,
     Measure.pi_pi] at h₀
diff --git a/Mathlib/RingTheory/AdjoinRoot.lean b/Mathlib/RingTheory/AdjoinRoot.lean
index 24fa9f8a3e5b96..829bc3c3d9bc5b 100644
--- a/Mathlib/RingTheory/AdjoinRoot.lean
+++ b/Mathlib/RingTheory/AdjoinRoot.lean
@@ -431,7 +431,7 @@ def mapAlgEquiv (f : S ≃ₐ[R] T) (p : S[X]) (q : T[X]) (h : Associated (p.map
       -- FIXME: Coercion hell. See https://github.com/leanprover-community/mathlib4/issues/31365.
       have : (RingHomClass.toRingHom f.toRingEquiv.symm).comp (RingHomClass.toRingHom f) =
         .id S := by ext; exact f.symm_apply_apply _
-      simpa [Polynomial.map_map, this] using! map_dvd f.symm.toRingHom h.dvd)
+      simpa [Polynomial.map_map, -RingEquiv.symm_mk, this] using! map_dvd f.symm.toRingHom h.dvd)
     (by ext <;> simp) (by ext <;> simp)
 
 @[simp] lemma coe_mapAlgEquiv (f : S ≃ₐ[R] T) (p : S[X]) (q : T[X]) (h) :
@@ -442,7 +442,8 @@ def mapAlgEquiv (f : S ≃ₐ[R] T) (p : S[X]) (q : T[X]) (h : Associated (p.map
       -- FIXME: Coercion hell. See https://github.com/leanprover-community/mathlib4/issues/31365.
       have : (RingHomClass.toRingHom f.toRingEquiv.symm).comp (RingHomClass.toRingHom f) =
         .id S := by ext; exact f.symm_apply_apply _
-      simpa [Polynomial.map_map, this] using! associated_map_map f.symm.toRingHom h.symm) := rfl
+      simpa [Polynomial.map_map, -RingEquiv.symm_mk, this]
+        using! associated_map_map f.symm.toRingHom h.symm) := rfl
 
 variable (R) in
 /-- The canonical algebraic homomorphism from `AdjoinRoot f` to `AdjoinRoot g`, where
diff --git a/MathlibTest/DeprecatedModuleTest.lean b/MathlibTest/DeprecatedModuleTest.lean
deleted file mode 100644
index ee8174ed820bcd..00000000000000
--- a/MathlibTest/DeprecatedModuleTest.lean
+++ /dev/null
@@ -1,15 +0,0 @@
-import MathlibTest.DeprecatedModule --deprecated_module: ignore
-
-/-!
-This file imports a deprecated module.
--/
-
-/--
-info: Deprecated modules
-
-'MathlibTest.DeprecatedModule' deprecates to
-#[Mathlib.Tactic.Linter.DocPrime, Mathlib.Tactic.Linter.DocString]
-with message 'We can also give more details about the deprecation'
--/
-#guard_msgs in
-#show_deprecated_modules
diff --git a/MathlibTest/Linter/DeprecatedModule/Basic.lean b/MathlibTest/Linter/DeprecatedModule/Basic.lean
index ff67e02327f593..a476d729aa19ea 100644
--- a/MathlibTest/Linter/DeprecatedModule/Basic.lean
+++ b/MathlibTest/Linter/DeprecatedModule/Basic.lean
@@ -23,7 +23,7 @@ deprecated_module "We can also give more details about the deprecation" (since :
 /--
 info: Deprecated modules
 
-'MathlibTest.DeprecatedModule' deprecates to
+'MathlibTest.Linter.DeprecatedModule.Basic' deprecates to
 #[Mathlib.Tactic.Linter.DocPrime, Mathlib.Tactic.Linter.DocString]
 with message 'We can also give more details about the deprecation'
 -/
diff --git a/MathlibTest/Linter/DeprecatedModule/ImportAsAll.lean b/MathlibTest/Linter/DeprecatedModule/ImportAsAll.lean
index 0e72304a3e6819..c907b2a98d84eb 100644
--- a/MathlibTest/Linter/DeprecatedModule/ImportAsAll.lean
+++ b/MathlibTest/Linter/DeprecatedModule/ImportAsAll.lean
@@ -2,7 +2,7 @@
 -- Core Lean 4 generates deprecation warnings at import time.
 module
 
-import all MathlibTest.DeprecatedModuleNew -- deprecated_module: ignore
+import all MathlibTest.Linter.DeprecatedModule.ImportBase -- deprecated_module: ignore
 
 /-!
 This file imports a deprecated module with `import all`.
@@ -12,7 +12,7 @@ This file imports a deprecated module with `import all`.
 /--
 info: Deprecated modules
 
-'MathlibTest.DeprecatedModuleNew' deprecates to
+'MathlibTest.Linter.DeprecatedModule.ImportBase' deprecates to
 #[Mathlib.Tactic.Linter.DocPrime, Mathlib.Tactic.Linter.DocString]
 with message 'Testing public import deprecation'
 -/
diff --git a/MathlibTest/Linter/DeprecatedModule/ImportAsMeta.lean b/MathlibTest/Linter/DeprecatedModule/ImportAsMeta.lean
index 2efa6ca38cb261..f07458478418d8 100644
--- a/MathlibTest/Linter/DeprecatedModule/ImportAsMeta.lean
+++ b/MathlibTest/Linter/DeprecatedModule/ImportAsMeta.lean
@@ -11,7 +11,7 @@ This file imports a deprecated module with `meta import`.
 /--
 info: Deprecated modules
 
-'MathlibTest.DeprecatedModuleNew' deprecates to
+'MathlibTest.Linter.DeprecatedModule.ImportBase' deprecates to
 #[Mathlib.Tactic.Linter.DocPrime, Mathlib.Tactic.Linter.DocString]
 with message 'Testing public import deprecation'
 -/
diff --git a/MathlibTest/Linter/DeprecatedModule/ImportAsPlain.lean b/MathlibTest/Linter/DeprecatedModule/ImportAsPlain.lean
index 04624921b56905..488930f8a45591 100644
--- a/MathlibTest/Linter/DeprecatedModule/ImportAsPlain.lean
+++ b/MathlibTest/Linter/DeprecatedModule/ImportAsPlain.lean
@@ -1,16 +1,19 @@
-import MathlibTest.Linter.DeprecatedModule.ImportBase
+-- This file tests that a plain `import` of a deprecated module produces warnings.
+-- Core Lean 4 generates deprecation warnings at import time.
+module --deprecated_module: ignore
 
-/--
-warning: Testing public import deprecation
-'MathlibTest.Linter.DeprecatedModule.ImportBase' has been deprecated: please replace this import by
+import MathlibTest.Linter.DeprecatedModule.ImportBase
 
-import Mathlib.Tactic.Linter.DocPrime
-import Mathlib.Tactic.Linter.DocString
+/-!
+This file imports a deprecated module with a plain `import`.
+-/
 
+/--
+info: Deprecated modules
 
-Note: This linter can be disabled with `set_option linter.deprecated.module false`
+'MathlibTest.Linter.DeprecatedModule.ImportBase' deprecates to
+#[Mathlib.Tactic.Linter.DocPrime, Mathlib.Tactic.Linter.DocString]
+with message 'Testing public import deprecation'
 -/
 #guard_msgs in
-/-!
-This file imports a deprecated module.
--/
+#show_deprecated_modules
diff --git a/MathlibTest/Linter/DeprecatedModule/ImportAsPublic.lean b/MathlibTest/Linter/DeprecatedModule/ImportAsPublic.lean
index aa0cea9b3cdb24..02b241512b58e4 100644
--- a/MathlibTest/Linter/DeprecatedModule/ImportAsPublic.lean
+++ b/MathlibTest/Linter/DeprecatedModule/ImportAsPublic.lean
@@ -12,7 +12,7 @@ This file imports a deprecated module with `public import`.
 /--
 info: Deprecated modules
 
-'MathlibTest.DeprecatedModuleNew' deprecates to
+'MathlibTest.Linter.DeprecatedModule.ImportBase' deprecates to
 #[Mathlib.Tactic.Linter.DocPrime, Mathlib.Tactic.Linter.DocString]
 with message 'Testing public import deprecation'
 -/
diff --git a/MathlibTest/Linter/DeprecatedModule/ImportsAsPublicMeta.lean b/MathlibTest/Linter/DeprecatedModule/ImportsAsPublicMeta.lean
index f011d03dccfd8a..b40913f6d1c4e7 100644
--- a/MathlibTest/Linter/DeprecatedModule/ImportsAsPublicMeta.lean
+++ b/MathlibTest/Linter/DeprecatedModule/ImportsAsPublicMeta.lean
@@ -11,7 +11,7 @@ This file imports a deprecated module with `public meta import`.
 /--
 info: Deprecated modules
 
-'MathlibTest.DeprecatedModuleNew' deprecates to
+'MathlibTest.Linter.DeprecatedModule.ImportBase' deprecates to
 #[Mathlib.Tactic.Linter.DocPrime, Mathlib.Tactic.Linter.DocString]
 with message 'Testing public import deprecation'
 -/