From cb18d5e6498851271a3600aae6fd61b5f811da58 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Sat, 11 Apr 2026 03:35:29 +0000
Subject: [PATCH 1/3] chore: cleanup of adaptation notes

---
 Mathlib/Algebra/Category/AlgCat/Limits.lean   |  1 -
 .../Category/ContinuousCohomology/Basic.lean  |  1 -
 Mathlib/Algebra/Category/ModuleCat/Basic.lean | 24 ++++---------------
 .../Sheaf/PushforwardContinuous.lean          |  1 -
 .../ModuleCat/Sheaf/Quasicoherent.lean        |  1 -
 Mathlib/Algebra/Category/ModuleCat/Stalk.lean |  4 +---
 Mathlib/Algebra/Category/Ring/Limits.lean     |  3 ---
 Mathlib/AlgebraicGeometry/AffineSpace.lean    |  1 -
 .../Cover/MorphismProperty.lean               |  3 +--
 .../Analysis/InnerProductSpace/Adjoint.lean   |  2 --
 Mathlib/Analysis/Real/Hyperreal.lean          |  6 ++---
 .../Limits/Shapes/IsTerminal.lean             |  4 +---
 .../CategoryTheory/Monoidal/Transport.lean    |  2 +-
 .../CategoryTheory/ObjectProperty/Shift.lean  |  3 ---
 .../CategoryTheory/Shift/Localization.lean    |  6 -----
 Mathlib/CategoryTheory/Shift/Quotient.lean    |  3 ---
 Mathlib/Data/Int/LeastGreatest.lean           | 14 ++---------
 Mathlib/Data/Multiset/Fintype.lean            |  3 ---
 Mathlib/Data/NNRat/Defs.lean                  |  3 +--
 Mathlib/Data/Rat/Floor.lean                   |  3 +--
 .../Euclidean/Angle/Oriented/Affine.lean      |  1 -
 Mathlib/GroupTheory/Coxeter/Inversion.lean    |  6 -----
 Mathlib/RingTheory/Etale/QuasiFinite.lean     |  4 ----
 Mathlib/RingTheory/Flat/Equalizer.lean        |  2 --
 Mathlib/RingTheory/Morita/Matrix.lean         |  2 --
 Mathlib/RingTheory/PicardGroup.lean           |  1 -
 .../RingTheory/RingHom/StandardSmooth.lean    |  1 -
 Mathlib/RingTheory/Smooth/Fiber.lean          |  1 -
 .../RingTheory/Valuation/Discrete/Basic.lean  | 10 --------
 Mathlib/Topology/Instances/Rat.lean           |  3 +--
 Mathlib/Topology/Sheaves/Skyscraper.lean      |  4 +---
 31 files changed, 16 insertions(+), 107 deletions(-)

diff --git a/Mathlib/Algebra/Category/AlgCat/Limits.lean b/Mathlib/Algebra/Category/AlgCat/Limits.lean
index de213535b02027..bbf62034028113 100644
--- a/Mathlib/Algebra/Category/AlgCat/Limits.lean
+++ b/Mathlib/Algebra/Category/AlgCat/Limits.lean
@@ -67,7 +67,6 @@ instance limitAlgebra :
     Algebra R (Types.Small.limitCone (F ⋙ forget (AlgCat.{w} R))).pt :=
   inferInstanceAs <| Algebra R (Shrink (sectionsSubalgebra F))
 
-#adaptation_note /-- After nightly-2026-02-23 we need this to avoid timeouts. -/
 set_option backward.isDefEq.respectTransparency false in
 /-- `limit.π (F ⋙ forget (AlgCat R)) j` as an `AlgHom`. -/
 def limitπAlgHom (j) :
diff --git a/Mathlib/Algebra/Category/ContinuousCohomology/Basic.lean b/Mathlib/Algebra/Category/ContinuousCohomology/Basic.lean
index 4ae79a0b75ea21..ca58f2c132d596 100644
--- a/Mathlib/Algebra/Category/ContinuousCohomology/Basic.lean
+++ b/Mathlib/Algebra/Category/ContinuousCohomology/Basic.lean
@@ -199,7 +199,6 @@ def kerHomogeneousCochainsZeroEquiv
   continuous_invFun := continuous_induced_rng.mpr
     (continuous_induced_rng.mpr ((ContinuousLinearMap.const R G).cont.comp continuous_subtype_val))
 
-#adaptation_note /-- After nightly-2026-02-23 we need this to avoid timeouts. -/
 set_option backward.isDefEq.respectTransparency false in
 open ShortComplex HomologyData in
 /-- `H⁰_cont(G, X) ≅ Xᴳ`. -/
diff --git a/Mathlib/Algebra/Category/ModuleCat/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Basic.lean
index bafaeb53dcfd33..f7f850e3d730a6 100644
--- a/Mathlib/Algebra/Category/ModuleCat/Basic.lean
+++ b/Mathlib/Algebra/Category/ModuleCat/Basic.lean
@@ -509,26 +509,10 @@ def smulNatTrans : R →+* End (forget₂ (ModuleCat R) AddCommGrpCat) where
   toFun r :=
     { app := fun M => M.smul r
       naturality := fun _ _ _ => smul_naturality _ r }
-  map_one' := NatTrans.ext (by
-    #adaptation_note /-- Prior to https://github.com/leanprover/lean4/pull/12244
-    this was just `cat_disch`. -/
-    simp +instances only [forget₂_obj, map_one, End.one_def]
-    cat_disch)
-  map_zero' := NatTrans.ext (by
-    #adaptation_note /-- Prior to https://github.com/leanprover/lean4/pull/12244
-    this was just `cat_disch`. -/
-    simp +instances only [forget₂_obj, map_zero]
-    cat_disch)
-  map_mul' _ _ := NatTrans.ext (by
-    #adaptation_note /-- Prior to https://github.com/leanprover/lean4/pull/12244
-    this was just `cat_disch`. -/
-    simp +instances only [forget₂_obj, map_mul, End.mul_def]
-    cat_disch)
-  map_add' _ _ := NatTrans.ext (by
-    #adaptation_note /-- Prior to https://github.com/leanprover/lean4/pull/12244
-    this was just `cat_disch`. -/
-    simp +instances only [forget₂_obj, map_add]
-    cat_disch)
+  map_one' := by cat_disch
+  map_zero' := by cat_disch
+  map_mul' _ _ := by cat_disch
+  map_add' _ _ := by cat_disch
 
 /-- Given `A : AddCommGrpCat` and a ring morphism `R →+* End A`, this is a type synonym
 for `A`, on which we shall define a structure of `R`-module. -/
diff --git a/Mathlib/Algebra/Category/ModuleCat/Sheaf/PushforwardContinuous.lean b/Mathlib/Algebra/Category/ModuleCat/Sheaf/PushforwardContinuous.lean
index 92f9cf23a5ee12..97b8c79bee3287 100644
--- a/Mathlib/Algebra/Category/ModuleCat/Sheaf/PushforwardContinuous.lean
+++ b/Mathlib/Algebra/Category/ModuleCat/Sheaf/PushforwardContinuous.lean
@@ -95,7 +95,6 @@ variable {K' : GrothendieckTopology D'} {K'' : GrothendieckTopology D''}
   [Functor.IsContinuous G K K'] [Functor.IsContinuous (F ⋙ G) J K']
   (ψ : R ⟶ (G.sheafPushforwardContinuous RingCat.{u} K K').obj R')
 
-#adaptation_note /-- After nightly-2026-02-23 we need this to avoid timeouts. -/
 /-- The composition of two pushforward functors on categories of sheaves of modules
 identify to the pushforward for the composition. -/
 noncomputable def pushforwardComp :
diff --git a/Mathlib/Algebra/Category/ModuleCat/Sheaf/Quasicoherent.lean b/Mathlib/Algebra/Category/ModuleCat/Sheaf/Quasicoherent.lean
index e9940526f9d18c..a96d057c4ff585 100644
--- a/Mathlib/Algebra/Category/ModuleCat/Sheaf/Quasicoherent.lean
+++ b/Mathlib/Algebra/Category/ModuleCat/Sheaf/Quasicoherent.lean
@@ -354,7 +354,6 @@ variable [∀ X, (J.over X).HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat
   [∀ X Y, HasSheafify ((J.over X).over Y) AddCommGrpCat.{u}]
   [∀ X Y, ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat.{u}]
 
-#adaptation_note /-- After nightly-2026-02-23 we need this to avoid timeouts. -/
 /-- Given an cover `X` and a quasicoherent data for `M` restricted onto each `Mᵢ`, we may glue them
 into a quasicoherent data of `M` itself. -/
 noncomputable def QuasicoherentData.bind {R : Sheaf J RingCat.{u}}
diff --git a/Mathlib/Algebra/Category/ModuleCat/Stalk.lean b/Mathlib/Algebra/Category/ModuleCat/Stalk.lean
index f2ed26bb2b2a16..66979c36fa0d38 100644
--- a/Mathlib/Algebra/Category/ModuleCat/Stalk.lean
+++ b/Mathlib/Algebra/Category/ModuleCat/Stalk.lean
@@ -58,9 +58,7 @@ def colimit.smul (r : (R ⋙ forget _).ColimitType) (m : (M ⋙ forget _).Colimi
     refine Functor.ιColimitType_eq_of_map_eq_map _ _ _ α β ?_
     simp [*, ← R.map_comp_apply, ← M.map_comp_apply, -Functor.map_comp]
 
-#adaptation_note /-- As of nightly-2026-02-10, we need to increase the maxHeartbeats limits here,
-and as of nightly-2026-02-23, we also need `backward.whnf.reducibleClassField`
-to avoid needing even more. -/
+#adaptation_note /-- As of nightly-2026-02-10, we need to increase the maxHeartbeats limits here. -/
 set_option backward.isDefEq.respectTransparency false in
 set_option maxHeartbeats 700000 in --
 set_option synthInstance.maxHeartbeats 40000 in
diff --git a/Mathlib/Algebra/Category/Ring/Limits.lean b/Mathlib/Algebra/Category/Ring/Limits.lean
index b227d825badd9a..87a0c69019f32c 100644
--- a/Mathlib/Algebra/Category/Ring/Limits.lean
+++ b/Mathlib/Algebra/Category/Ring/Limits.lean
@@ -422,7 +422,6 @@ instance limitCommRing :
     (RingCat.sectionsSubring.{v, u} (F ⋙ forget₂ CommRingCat RingCat.{u}))
   inferInstanceAs <| CommRing (Shrink _)
 
-#adaptation_note /-- After nightly-2026-02-23 we need this to avoid timeouts. -/
 /-- We show that the forgetful functor `CommRingCat ⥤ RingCat` creates limits.
 
 All we need to do is notice that the limit point has a `CommRing` instance available,
@@ -502,8 +501,6 @@ instance forget₂Ring_preservesLimitsOfSize [UnivLE.{v, u}] :
 instance forget₂Ring_preservesLimits : PreservesLimits (forget₂ CommRingCat RingCat.{u}) :=
   CommRingCat.forget₂Ring_preservesLimitsOfSize.{u, u}
 
-#adaptation_note /-- After nightly-2026-02-23 this requires more heartbeats. -/
-set_option maxHeartbeats 400000 in -- see note above
 /-- An auxiliary declaration to speed up typechecking.
 -/
 def forget₂CommSemiRingPreservesLimitsAux :
diff --git a/Mathlib/AlgebraicGeometry/AffineSpace.lean b/Mathlib/AlgebraicGeometry/AffineSpace.lean
index 7d723d36745e68..d5b16ad687c9f1 100644
--- a/Mathlib/AlgebraicGeometry/AffineSpace.lean
+++ b/Mathlib/AlgebraicGeometry/AffineSpace.lean
@@ -202,7 +202,6 @@ def isoOfIsAffine [IsAffine S] :
           simp only [eval₂_X]
           exact homOfVector_appTop_coord _ _ _
 
-#adaptation_note /-- After nightly-2026-02-23 we need this to avoid timeouts. -/
 @[simp]
 lemma isoOfIsAffine_hom_appTop [IsAffine S] :
     (isoOfIsAffine n S).hom.appTop =
diff --git a/Mathlib/AlgebraicGeometry/Cover/MorphismProperty.lean b/Mathlib/AlgebraicGeometry/Cover/MorphismProperty.lean
index 003dfc1d0f2271..533fbe95d15a9b 100644
--- a/Mathlib/AlgebraicGeometry/Cover/MorphismProperty.lean
+++ b/Mathlib/AlgebraicGeometry/Cover/MorphismProperty.lean
@@ -102,8 +102,7 @@ def Cover.mkOfCovers (J : Type*) (obj : J → Scheme.{u}) (map : (j : J) → obj
   f := map
   mem₀ := by
     simp_rw [presieve₀_mem_precoverage_iff, Set.mem_range]
-    #adaptation_note /-- This was `grind` before nightly-2026-02-05. -/
-    exact ⟨covers, map_prop⟩
+    grind
 
 /-- An isomorphism `X ⟶ Y` is a `P`-cover of `Y`. -/
 @[simps! I₀ X f]
diff --git a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean
index 5074f6c238d65b..4b018614b21b92 100644
--- a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean
+++ b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean
@@ -964,8 +964,6 @@ lemma coe_symm_linearIsometryEquiv_apply (e : H ≃ₗᵢ[𝕜] H) :
 theorem conjStarAlgEquiv_unitaryLinearIsometryEquiv (u : unitary (H →L[𝕜] H)) :
     (linearIsometryEquiv u).conjStarAlgEquiv = conjStarAlgAut 𝕜 _ u := rfl
 
-#adaptation_note /-- The maxHeartbeats bump is required after leanprover/lean4#12564. -/
-set_option maxHeartbeats 400000 in -- see adaptation note
 theorem conjStarAlgAut_symm_unitaryLinearIsometryEquiv (u : H ≃ₗᵢ[𝕜] H) :
     conjStarAlgAut 𝕜 (H →L[𝕜] H) (linearIsometryEquiv.symm u) = u.conjStarAlgEquiv := by
   simp [← conjStarAlgEquiv_unitaryLinearIsometryEquiv]
diff --git a/Mathlib/Analysis/Real/Hyperreal.lean b/Mathlib/Analysis/Real/Hyperreal.lean
index b983012320ecbd..9e0769a6349fc1 100644
--- a/Mathlib/Analysis/Real/Hyperreal.lean
+++ b/Mathlib/Analysis/Real/Hyperreal.lean
@@ -39,12 +39,10 @@ def Hyperreal : Type :=
 
 noncomputable section
 
-#adaptation_note
-/-- After nightly-2025-05-07 we had to remove `deriving Inhabited` on `Hyperreal` above,
-as there is a new error about this instance having to be noncomputable, and `deriving` doesn't allow
-for adding this! -/
 namespace Hyperreal
 
+deriving instance Inhabited for Hyperreal
+
 @[inherit_doc] notation "ℝ*" => Hyperreal
 
 instance : Field ℝ* :=
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean b/Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean
index 4aee9b7ad762aa..cc177de68ac636 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean
@@ -115,9 +115,7 @@ def isInitialEquivUnique (F : Discrete.{0} PEmpty.{1} ⥤ C) (X : C) :
     { desc := fun s => (u s.pt).default
       uniq := fun s _ _ => (u s.pt).2 _ }
   left_inv := by dsimp [Function.LeftInverse]; intro; simp only [eq_iff_true_of_subsingleton]
-  right_inv := by
-    #adaptation_note /-- 19-07-2025 grind stopped working -/
-    intro x; dsimp
+  right_inv := by grind
 
 /-- An object `X` is initial if for every `Y` there is a unique morphism `X ⟶ Y`
     (as an instance). -/
diff --git a/Mathlib/CategoryTheory/Monoidal/Transport.lean b/Mathlib/CategoryTheory/Monoidal/Transport.lean
index 407bffeffde5a5..69b2ec027cf40d 100644
--- a/Mathlib/CategoryTheory/Monoidal/Transport.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Transport.lean
@@ -152,7 +152,7 @@ def transportStruct (e : C ≌ D) : MonoidalCategoryStruct.{v₂} D where
       e.counitIso.app _
 
 #adaptation_note /-- Prior to https://github.com/leanprover/lean4/pull/12244
-the fields `whiskerList_eq` and following were all filled by the `cat_disch` auto_param. -/
+the fields `whiskerLeft_eq` and following were all filled by the `cat_disch` auto_param. -/
 attribute [local simp] transportStruct in
 /-- Transport a monoidal structure along an equivalence of (plain) categories.
 -/
diff --git a/Mathlib/CategoryTheory/ObjectProperty/Shift.lean b/Mathlib/CategoryTheory/ObjectProperty/Shift.lean
index 443719dfe48e84..b08036902eb037 100644
--- a/Mathlib/CategoryTheory/ObjectProperty/Shift.lean
+++ b/Mathlib/CategoryTheory/ObjectProperty/Shift.lean
@@ -200,9 +200,6 @@ instance commShiftι : P.ι.CommShift A :=
   Functor.CommShift.ofHasShiftOfFullyFaithful _ _ _
 
 -- these definitions are made irreducible to prevent any abuse of defeq
-#adaptation_note /-- After https://github.com/leanprover/lean4/pull/12247
-this requires `allowUnsafeReducibility`. -/
-set_option allowUnsafeReducibility true in
 attribute [irreducible] hasShift commShiftι
 
 section
diff --git a/Mathlib/CategoryTheory/Shift/Localization.lean b/Mathlib/CategoryTheory/Shift/Localization.lean
index c03498e720f226..7e5fb2bdf46ea0 100644
--- a/Mathlib/CategoryTheory/Shift/Localization.lean
+++ b/Mathlib/CategoryTheory/Shift/Localization.lean
@@ -105,9 +105,6 @@ noncomputable instance MorphismProperty.commShift_Q :
     W.Q.CommShift A :=
   Functor.CommShift.localized W.Q W A
 
-#adaptation_note /-- After https://github.com/leanprover/lean4/pull/12247
-this requires `allowUnsafeReducibility`. -/
-set_option allowUnsafeReducibility true in
 attribute [irreducible] HasShift.localization MorphismProperty.commShift_Q
 
 variable [W.HasLocalization]
@@ -122,9 +119,6 @@ noncomputable instance MorphismProperty.commShift_Q' :
     W.Q'.CommShift A :=
   Functor.CommShift.localized W.Q' W A
 
-#adaptation_note /-- After https://github.com/leanprover/lean4/pull/12247
-this requires `allowUnsafeReducibility`. -/
-set_option allowUnsafeReducibility true in
 attribute [irreducible] HasShift.localization' MorphismProperty.commShift_Q'
 
 end
diff --git a/Mathlib/CategoryTheory/Shift/Quotient.lean b/Mathlib/CategoryTheory/Shift/Quotient.lean
index 88904e0a96fe70..78dc5a48487829 100644
--- a/Mathlib/CategoryTheory/Shift/Quotient.lean
+++ b/Mathlib/CategoryTheory/Shift/Quotient.lean
@@ -59,9 +59,6 @@ noncomputable instance Quotient.functor_commShift [r.IsCompatibleWithShift A] :
   Functor.CommShift.ofInduced _ _ _ _
 
 -- the construction is made irreducible in order to prevent timeouts and abuse of defeq
-#adaptation_note /-- After https://github.com/leanprover/lean4/pull/12247
-doing so requires `allowUnsafeReducibility`. -/
-set_option allowUnsafeReducibility true in
 attribute [irreducible] HasShift.quotient Quotient.functor_commShift
 
 namespace Quotient
diff --git a/Mathlib/Data/Int/LeastGreatest.lean b/Mathlib/Data/Int/LeastGreatest.lean
index ce16ccb13a6770..3b26d8563d063f 100644
--- a/Mathlib/Data/Int/LeastGreatest.lean
+++ b/Mathlib/Data/Int/LeastGreatest.lean
@@ -77,12 +77,7 @@ theorem exists_least_of_bdd
 
 theorem coe_leastOfBdd_eq {P : ℤ → Prop} [DecidablePred P] {b b' : ℤ} (Hb : ∀ z : ℤ, P z → b ≤ z)
     (Hb' : ∀ z : ℤ, P z → b' ≤ z) (Hinh : ∃ z : ℤ, P z) :
-    (leastOfBdd b Hb Hinh : ℤ) = leastOfBdd b' Hb' Hinh := by
-  #adaptation_note /-- 2025-09-30 (https://github.com/leanprover/lean4/issues/10622)
-    Used to be `grind` -/
-  rcases leastOfBdd b Hb Hinh with ⟨n, hn, h2n⟩
-  rcases leastOfBdd b' Hb' Hinh with ⟨n', hn', h2n'⟩
-  exact le_antisymm (h2n _ hn') (h2n' _ hn)
+    (leastOfBdd b Hb Hinh : ℤ) = leastOfBdd b' Hb' Hinh := by grind
 
 /-- A computable version of `exists_greatest_of_bdd`: given a decidable predicate on the
 integers, with an explicit upper bound and a proof that it is somewhere true, return
@@ -118,11 +113,6 @@ theorem exists_greatest_of_bdd
 
 theorem coe_greatestOfBdd_eq {P : ℤ → Prop} [DecidablePred P] {b b' : ℤ}
     (Hb : ∀ z : ℤ, P z → z ≤ b) (Hb' : ∀ z : ℤ, P z → z ≤ b') (Hinh : ∃ z : ℤ, P z) :
-    (greatestOfBdd b Hb Hinh : ℤ) = greatestOfBdd b' Hb' Hinh := by
-  #adaptation_note /-- 2025-09-30 (https://github.com/leanprover/lean4/issues/10622)
-    Used to be `grind` -/
-  rcases greatestOfBdd b Hb Hinh with ⟨n, hn, h2n⟩
-  rcases greatestOfBdd b' Hb' Hinh with ⟨n', hn', h2n'⟩
-  exact le_antisymm (h2n' _ hn) (h2n _ hn')
+    (greatestOfBdd b Hb Hinh : ℤ) = greatestOfBdd b' Hb' Hinh := by grind
 
 end Int
diff --git a/Mathlib/Data/Multiset/Fintype.lean b/Mathlib/Data/Multiset/Fintype.lean
index edfb7d5554871f..199d56ee906797 100644
--- a/Mathlib/Data/Multiset/Fintype.lean
+++ b/Mathlib/Data/Multiset/Fintype.lean
@@ -170,9 +170,6 @@ def coeEquiv (m : Multiset α) : m ≃ m.toEnumFinset where
 theorem toEmbedding_coeEquiv_trans (m : Multiset α) :
     m.coeEquiv.toEmbedding.trans (Function.Embedding.subtype _) = m.coeEmbedding := by ext <;> rfl
 
-#adaptation_note /-- Before https://github.com/leanprover/lean4/pull/12247
-this was `@[irreducible]`, which is no longer allowed at the definition site,
-and must be applied afterwards. -/
 instance fintypeCoe : Fintype m :=
   Fintype.ofEquiv m.toEnumFinset m.coeEquiv.symm
 
diff --git a/Mathlib/Data/NNRat/Defs.lean b/Mathlib/Data/NNRat/Defs.lean
index 9b5723f21fb33f..ca8946906ac17d 100644
--- a/Mathlib/Data/NNRat/Defs.lean
+++ b/Mathlib/Data/NNRat/Defs.lean
@@ -307,11 +307,10 @@ theorem toNNRat_mul (hp : 0 ≤ p) : toNNRat (p * q) = toNNRat p * toNNRat q :=
 
 end Rat
 
-#adaptation_note /-- We can remove `_root_.` after https://github.com/leanprover/lean4/pull/12504 -/
 /-- The absolute value on `ℚ` as a map to `ℚ≥0`. -/
 @[pp_nodot]
 def Rat.nnabs (x : ℚ) : ℚ≥0 :=
-  ⟨abs x, _root_.abs_nonneg x⟩
+  ⟨abs x, abs_nonneg x⟩
 
 @[norm_cast, simp]
 theorem Rat.coe_nnabs (x : ℚ) : (Rat.nnabs x : ℚ) = abs x := rfl
diff --git a/Mathlib/Data/Rat/Floor.lean b/Mathlib/Data/Rat/Floor.lean
index f9f9cd5bfb37c8..1298ab818f4333 100644
--- a/Mathlib/Data/Rat/Floor.lean
+++ b/Mathlib/Data/Rat/Floor.lean
@@ -394,8 +394,7 @@ theorem fract_inv_num_lt_num_of_pos {q : ℚ} (q_pos : 0 < q) : (fract q⁻¹).n
       suffices ((q.den : ℤ) - q.num * ⌊q_inv⌋).natAbs.Coprime q.num.natAbs from
         mod_cast Rat.num_div_eq_of_coprime q_num_pos this
       have tmp := Nat.coprime_sub_mul_floor_rat_div_of_coprime q.reduced.symm
-      #adaptation_note /-- We can remove `_root_.` after https://github.com/leanprover/lean4/pull/12504 -/
-      simpa only [Nat.cast_natAbs, _root_.abs_of_nonneg q_num_pos.le] using tmp
+      simpa only [Nat.cast_natAbs, abs_of_nonneg q_num_pos.le] using tmp
     rwa [this]
   -- to show the claim, start with the following inequality
   have q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * q⁻¹.den < q⁻¹.den := by
diff --git a/Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean b/Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
index 38b364527eb96d..83ac8836a8ecdb 100644
--- a/Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
+++ b/Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
@@ -311,7 +311,6 @@ theorem oangle_eq_oangle_of_dist_eq {p₁ p₂ p₃ : P} (h : dist p₁ p₂ = d
   rw [oangle, oangle, ← vsub_sub_vsub_cancel_left p₃ p₂ p₁, ← vsub_sub_vsub_cancel_left p₂ p₃ p₁,
     o.oangle_sub_eq_oangle_sub_rev_of_norm_eq h]
 
-#adaptation_note /-- After nightly-2026-02-23 we need this to avoid timeouts. -/
 /-- The angle at the apex of an isosceles triangle is `π` minus twice a base angle, oriented
 angle-at-point form. -/
 theorem oangle_eq_pi_sub_two_zsmul_oangle_of_dist_eq {p₁ p₂ p₃ : P} (hn : p₂ ≠ p₃)
diff --git a/Mathlib/GroupTheory/Coxeter/Inversion.lean b/Mathlib/GroupTheory/Coxeter/Inversion.lean
index d67bc2f8373bd5..89718224b961a6 100644
--- a/Mathlib/GroupTheory/Coxeter/Inversion.lean
+++ b/Mathlib/GroupTheory/Coxeter/Inversion.lean
@@ -424,12 +424,6 @@ theorem IsReduced.nodup_rightInvSeq {ω : List B} (rω : cs.IsReduced ω) : List
   set! t := (ris ω).getD j 1 with h₁
   set! t' := (ris (ω.eraseIdx j)).getD (j' - 1) 1 with h₂
   have h₃ : t' = (ris ω).getD j' 1 := by
-    #adaptation_note
-    /--
-    This was previously `grind [cs.getD_rightInvSeq, drop_of_length_le, drop_drop]`,
-    which no longer works after changes to `grind` annotation lemmas in
-    https://github.com/leanprover/lean4/pull/12170
-    -/
     grind only [cs.getD_rightInvSeq, = eraseIdx_eq_take_drop_succ, = getElem?_eraseIdx,
       = drop_append, drop_of_length_le, drop_drop, = length_append, = length_take, = length_drop,
       = min_def]
diff --git a/Mathlib/RingTheory/Etale/QuasiFinite.lean b/Mathlib/RingTheory/Etale/QuasiFinite.lean
index 078c5230eb917b..e55f0e06ef5519 100644
--- a/Mathlib/RingTheory/Etale/QuasiFinite.lean
+++ b/Mathlib/RingTheory/Etale/QuasiFinite.lean
@@ -198,8 +198,6 @@ lemma Algebra.exists_notMem_and_isIntegral_forall_mem_of_ne_of_liesOver
     exact H (Ideal.mul_mem_left _ (s₂ ^ m) this)
   · rw [map_pow]; exact Ideal.notMem_of_isUnit _ (.pow _ (IsLocalization.Away.algebraMap_isUnit _))
 
-#adaptation_note /-- The maxHeartbeats bump is required after leanprover/lean4#12564. -/
-set_option maxHeartbeats 400000 in -- see adaptation note
 lemma Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux
     {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [Algebra.FiniteType R S]
     (p : Ideal R) [p.IsPrime] (q : Ideal S) [q.IsPrime] [q.LiesOver p] [Algebra.QuasiFiniteAt R q] :
@@ -295,9 +293,7 @@ lemma Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux
       (P''.over_def P)).comp_algebraMap, ← Polynomial.map_map, ← ha']
     simp
 
-#adaptation_note /-- The maxHeartbeats bump is required after leanprover/lean4#12564. -/
 set_option backward.isDefEq.respectTransparency false in
-set_option maxHeartbeats 400000 in -- see adaptation note
 lemma Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux₂
     {R S R' R'' : Type*} [CommRing R] [CommRing S] [Algebra R S] [Algebra.FiniteType R S]
     [CommRing R'] [Algebra R R'] [CommRing R''] [Algebra R R''] [Algebra R'' S]
diff --git a/Mathlib/RingTheory/Flat/Equalizer.lean b/Mathlib/RingTheory/Flat/Equalizer.lean
index a45c81de1c044d..b7f81329767bdc 100644
--- a/Mathlib/RingTheory/Flat/Equalizer.lean
+++ b/Mathlib/RingTheory/Flat/Equalizer.lean
@@ -308,8 +308,6 @@ lemma AlgHom.tensorEqualizerEquiv_apply [Module.Flat R T]
     AlgHom.tensorEqualizerEquiv S T f g x = AlgHom.tensorEqualizer S T f g x :=
   rfl
 
-#adaptation_note /-- After nightly-2026-02-23 this requires more heartbeats. -/
-set_option maxHeartbeats 400000 in -- see note
 variable (R A) in
 attribute [local instance] Algebra.TensorProduct.rightAlgebra in
 /--
diff --git a/Mathlib/RingTheory/Morita/Matrix.lean b/Mathlib/RingTheory/Morita/Matrix.lean
index cbcea31c61af09..9ff7019a2ca928 100644
--- a/Mathlib/RingTheory/Morita/Matrix.lean
+++ b/Mathlib/RingTheory/Morita/Matrix.lean
@@ -128,7 +128,6 @@ def fromModuleCatToModuleCatLinearEquiv (M : Type*) [AddCommGroup M] [Module R M
     simp [← hy]
   right_inv x := by simp
 
-#adaptation_note /-- After nightly-2026-02-23 we need this to avoid timeouts. -/
 set_option backward.isDefEq.respectTransparency false in
 /-- The natural isomorphism showing that `toModuleCat` is the left inverse of `toMatrixModCat`. -/
 def MatrixModCat.unitIso (i : ι) :
@@ -178,7 +177,6 @@ def MatrixModCat.counitIso (i : ι) :
     ext
     simp [toModuleCatFromModuleCatLinearEquiv]
 
-#adaptation_note /-- After nightly-2026-02-23 we need this to avoid timeouts. -/
 set_option backward.isDefEq.respectTransparency false in
 /-- `ModuleCat.toMatrixModCat R ι` and `MatrixModCat.toModuleCat R i` together form
   an equivalence of categories. -/
diff --git a/Mathlib/RingTheory/PicardGroup.lean b/Mathlib/RingTheory/PicardGroup.lean
index b0c2f3756f533a..a9d2c7f2fe7e60 100644
--- a/Mathlib/RingTheory/PicardGroup.lean
+++ b/Mathlib/RingTheory/PicardGroup.lean
@@ -848,7 +848,6 @@ the group of the invertible `R`-submodules in `A` modulo the principal submodule
   (QuotientGroup.congr _ _ (.refl _) ((Subgroup.map_id _).trans (ker_unitsToPic R A).symm)).trans <|
   (quotientKerEquivRange _).trans <| .subgroupCongr (range_unitsToPic R A)
 
-#adaptation_note /-- After nightly-2026-02-23 we need this to avoid timeouts. -/
 /-- The class group of a domain is isomorphic to the Picard group. -/
 @[simps!] noncomputable def ClassGroup.equivPic (R) [CommRing R] [IsDomain R] :
     ClassGroup R ≃* Pic R :=
diff --git a/Mathlib/RingTheory/RingHom/StandardSmooth.lean b/Mathlib/RingTheory/RingHom/StandardSmooth.lean
index 909972f2daf5b4..ec9fe9abc85930 100644
--- a/Mathlib/RingTheory/RingHom/StandardSmooth.lean
+++ b/Mathlib/RingTheory/RingHom/StandardSmooth.lean
@@ -193,7 +193,6 @@ lemma isStandardSmoothOfRelativeDimension_stableUnderCompositionWithLocalization
       IsStandardSmoothOfRelativeDimension.algebraMap_isLocalizationAway s
     zero_add n ▸ IsStandardSmoothOfRelativeDimension.comp this hf
 
-#adaptation_note /-- After nightly-2026-02-23 we need this to avoid timeouts. -/
 set_option backward.isDefEq.respectTransparency false in
 variable (R S) in
 /-- Every standard smooth homomorphism `R → S` factors into `R -> R[X₁,...,Xₙ] → S`
diff --git a/Mathlib/RingTheory/Smooth/Fiber.lean b/Mathlib/RingTheory/Smooth/Fiber.lean
index 64f6fdbf895fd5..d08b6d01b08b22 100644
--- a/Mathlib/RingTheory/Smooth/Fiber.lean
+++ b/Mathlib/RingTheory/Smooth/Fiber.lean
@@ -53,7 +53,6 @@ variable [IsLocalRing R] [IsLocalRing S] [IsLocalHom (algebraMap R S)]
   [Algebra.FormallySmooth 𝓀[R] (𝓀[R] ⊗[R] S)]
 
 set_option backward.isDefEq.respectTransparency false in
-attribute [local irreducible] KaehlerDifferential in
 attribute [local instance] TensorProduct.rightAlgebra in
 /--
 Let `(R, m, k)` be a local ring, `(S, M, K)` be a local `R`-algebra that is `R`-flat such that
diff --git a/Mathlib/RingTheory/Valuation/Discrete/Basic.lean b/Mathlib/RingTheory/Valuation/Discrete/Basic.lean
index 5e93a761a8186f..12ccca57600159 100644
--- a/Mathlib/RingTheory/Valuation/Discrete/Basic.lean
+++ b/Mathlib/RingTheory/Valuation/Discrete/Basic.lean
@@ -147,17 +147,7 @@ instance : v.IsNontrivial := by
     intro y x
     specialize h1 x
     aesop
-  #adaptation_note
-  /-- Until nightly-2026-01-07, this was:
-  ```
   aesop (add safe forward [generator_lt_one, generator_zpowers_eq_valueGroup])
-  ```
-  This proof works as of 2026-01-30, but is about 4 times slower than the proof below.
-  -/
-  simp_all only [ne_eq]
-  have : generator v < 1 := generator_lt_one v
-  have : zpowers (generator v) = valueGroup v := generator_zpowers_eq_valueGroup v
-  simp_all only [zpowers_eq_bot, lt_self_iff_false]
 
 lemma valueGroup_genLTOne_eq_generator : (valueGroup v).genLTOne = generator v :=
   ((valueGroup v).genLTOne_unique (generator_lt_one v) (generator_zpowers_eq_valueGroup v)).symm
diff --git a/Mathlib/Topology/Instances/Rat.lean b/Mathlib/Topology/Instances/Rat.lean
index 88faf904be5d49..7e397c38c87dad 100644
--- a/Mathlib/Topology/Instances/Rat.lean
+++ b/Mathlib/Topology/Instances/Rat.lean
@@ -83,8 +83,7 @@ theorem uniformContinuous_add : UniformContinuous fun p : ℚ × ℚ => p.1 + p.
 theorem uniformContinuous_neg : UniformContinuous (@Neg.neg ℚ _) :=
   Metric.uniformContinuous_iff.2 fun ε ε0 =>
     ⟨_, ε0, fun _ _ h => by
-      #adaptation_note /-- We can remove `_root_.` after https://github.com/leanprover/lean4/pull/12504 -/
-      simpa only [_root_.abs_sub_comm, dist_eq, cast_neg, neg_sub_neg] using h⟩
+      simpa only [abs_sub_comm, dist_eq, cast_neg, neg_sub_neg] using h⟩
 
 instance : IsUniformAddGroup ℚ :=
   IsUniformAddGroup.mk' Rat.uniformContinuous_add Rat.uniformContinuous_neg
diff --git a/Mathlib/Topology/Sheaves/Skyscraper.lean b/Mathlib/Topology/Sheaves/Skyscraper.lean
index 43286251ca933f..03fd76ce024b01 100644
--- a/Mathlib/Topology/Sheaves/Skyscraper.lean
+++ b/Mathlib/Topology/Sheaves/Skyscraper.lean
@@ -232,9 +232,7 @@ theorem skyscraperPresheaf_isSheaf : (skyscraperPresheaf p₀ A).IsSheaf := by
           dsimp [skyscraperPresheaf]
           rw [if_neg]
           · exact terminalIsTerminal
-          · #adaptation_note /-- 2024-03-24
-            Previously the universe annotation was not needed here. -/
-            exact Set.notMem_empty PUnit.unit.{u + 1})))
+          · exact Set.notMem_empty PUnit.unit.{u + 1})))
 
 /--
 The skyscraper presheaf supported at `p₀` with value `A` is the sheaf that assigns `A` to all opens

From cb009dbf7e66b5af6daced2f592791dc96013ec3 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Sat, 11 Apr 2026 23:44:56 +0000
Subject: [PATCH 2/3] revert one

---
 Mathlib/Topology/Sheaves/Skyscraper.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Topology/Sheaves/Skyscraper.lean b/Mathlib/Topology/Sheaves/Skyscraper.lean
index 03fd76ce024b01..43286251ca933f 100644
--- a/Mathlib/Topology/Sheaves/Skyscraper.lean
+++ b/Mathlib/Topology/Sheaves/Skyscraper.lean
@@ -232,7 +232,9 @@ theorem skyscraperPresheaf_isSheaf : (skyscraperPresheaf p₀ A).IsSheaf := by
           dsimp [skyscraperPresheaf]
           rw [if_neg]
           · exact terminalIsTerminal
-          · exact Set.notMem_empty PUnit.unit.{u + 1})))
+          · #adaptation_note /-- 2024-03-24
+            Previously the universe annotation was not needed here. -/
+            exact Set.notMem_empty PUnit.unit.{u + 1})))
 
 /--
 The skyscraper presheaf supported at `p₀` with value `A` is the sheaf that assigns `A` to all opens

From 99fb87ba04519c8a70a289bd18ece24e3e988222 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 21 Apr 2026 03:30:15 +0000
Subject: [PATCH 3/3] thought I'd fixed this, not sure where the commit went

---
 Mathlib/Analysis/Real/Hyperreal.lean | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Analysis/Real/Hyperreal.lean b/Mathlib/Analysis/Real/Hyperreal.lean
index 9e0769a6349fc1..35e64c6c0f343c 100644
--- a/Mathlib/Analysis/Real/Hyperreal.lean
+++ b/Mathlib/Analysis/Real/Hyperreal.lean
@@ -33,16 +33,15 @@ principle on `Hyperreal`.
 
 open ArchimedeanClass Filter Germ Topology
 
+noncomputable section
+
 /-- Hyperreal numbers on the ultrafilter extending the cofinite filter. -/
 def Hyperreal : Type :=
   Germ (hyperfilter ℕ : Filter ℕ) ℝ
-
-noncomputable section
+deriving Inhabited
 
 namespace Hyperreal
 
-deriving instance Inhabited for Hyperreal
-
 @[inherit_doc] notation "ℝ*" => Hyperreal
 
 instance : Field ℝ* :=