leanprover-community · kim-em · Mar 24, 2026 · Mar 24, 2026 · Mar 26, 2026 · Mar 26, 2026
diff --git a/.github/workflows/build_template.yml b/.github/workflows/build_template.yml
@@ -222,7 +222,7 @@ jobs:
 
       - name: validate lake-manifest.json inputRevs
         # Only enforce this on the main mathlib4 repository, not on nightly-testing
-        if: github.repository == 'leanprover-community/mathlib4'
+        if: github.repository == 'leanprover-community/mathlib4' && github.ref_name != 'nightly-testing'
         shell: bash
         run: |
           cd pr-branch

diff --git a/Archive/Examples/IfNormalization/Result.lean b/Archive/Examples/IfNormalization/Result.lean
@@ -24,6 +24,7 @@ We add some local simp lemmas so we can unfold the definitions of the normalizat
 attribute [local simp] normalized hasNestedIf hasConstantIf hasRedundantIf disjoint vars
   List.disjoint
 
+set_option warning.simp.varHead false in
 attribute [local simp] apply_ite ite_eq_iff'
 
 variable {b : Bool} {f : ℕ → Bool} {i : ℕ} {t e : IfExpr}

diff --git a/Archive/Imo/Imo2024Q6.lean b/Archive/Imo/Imo2024Q6.lean
@@ -55,6 +55,7 @@ lemma Aquaesulian.injective : Function.Injective f := by
   · exact (h.eq_of_apply_eq_inl he.symm hc).symm
   · exact h.eq_of_apply_eq_inl he hc
 
+set_option warning.simp.varHead false in
 @[simp]
 lemma Aquaesulian.apply_zero : f 0 = 0 := by
   refine h.injective ?_
@@ -68,6 +69,7 @@ lemma Aquaesulian.apply_neg_apply_add (x : G) : f (-(f x)) + x = 0 := by
   · rw [add_neg_cancel, h.apply_zero] at hc
     exact hc.symm
 
+set_option warning.simp.varHead false in
 @[simp]
 lemma Aquaesulian.apply_neg_apply (x : G) : f (-(f x)) = -x := by
   rw [← add_eq_zero_iff_eq_neg]

diff --git a/Mathlib/Algebra/BigOperators/Group/List/Basic.lean b/Mathlib/Algebra/BigOperators/Group/List/Basic.lean
@@ -244,11 +244,8 @@ lemma prod_map_erase [DecidableEq α] (f : α → M) {a} :
 
 @[to_additive] lemma Perm.prod_eq (h : Perm l₁ l₂) : prod l₁ = prod l₂ := h.foldr_op_eq
 
--- In order to make `to_additive` work, this theorem is adjusted to `List.sum_reverse` from core
-@[to_additive existing, simp]
-lemma prod_reverse [One α] [Mul α] [@Std.Associative α (· * ·)] [@Std.Commutative α (· * ·)]
-    [@Std.LawfulLeftIdentity α α (· * ·) 1] (l : List α) : prod l.reverse = prod l :=
-  @List.sum_reverse α ⟨1⟩ ⟨(· * ·)⟩ _ _ _ l
+set_option linter.existingAttributeWarning false in
+attribute [to_additive existing] prod_reverse
 
 @[to_additive]
 lemma prod_mul_prod_eq_prod_zipWith_mul_prod_drop :

diff --git a/Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean b/Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean
@@ -141,7 +141,7 @@ noncomputable instance monoidalCategory :
 
 open BraidedCategory
 
-instance symmetricCategory :
+noncomputable instance symmetricCategory :
     SymmetricCategory (PresheafOfModules.{u} (R ⋙ forget₂ _ _)) where
   braiding M₁ M₂ :=
     isoMk (fun X ↦ braiding (C := ModuleCat (R.obj X)) (M₁.obj X) (M₂.obj X))

diff --git a/Mathlib/Algebra/CharP/Two.lean b/Mathlib/Algebra/CharP/Two.lean
@@ -64,6 +64,7 @@ theorem natCast_cases (n : ℕ) : (n : R) = 0 ∨ (n : R) = 1 :=
 theorem natCast_eq_mod (n : ℕ) : (n : R) = (n % 2 : ℕ) := by
   simp [natCast_eq_ite, Nat.even_iff]
 
+set_option warning.simp.varHead false in
 @[scoped simp]
 theorem ofNat_eq_mod (n : ℕ) [n.AtLeastTwo] : (ofNat(n) : R) = (ofNat(n) % 2 : ℕ) :=
   natCast_eq_mod n

diff --git a/Mathlib/Algebra/Group/Ext.lean b/Mathlib/Algebra/Group/Ext.lean
@@ -109,11 +109,7 @@ theorem CancelMonoid.toRightCancelMonoid_injective {M : Type u} :
 theorem CancelCommMonoid.toCommMonoid_injective {M : Type u} :
     Function.Injective (@CancelCommMonoid.toCommMonoid M) := by
   rintro @⟨@⟨@⟨⟩⟩⟩ @⟨@⟨@⟨⟩⟩⟩ h
-  #adaptation_note /-- Before leanprover/lean4#13166, the last line was `grind`.
-  The new type-directed canonicalizer tries to synthesize `Monoid M` / `CommMonoid M` to normalize
-  sub-expressions, but fails because after `rintro` the instances exist only as destructured fields
-  in the local context, not as registered typeclass instances. -/
-  cases h; rfl
+  grind
 
 @[to_additive (attr := ext)]
 theorem CancelCommMonoid.ext {M : Type*} ⦃m₁ m₂ : CancelCommMonoid M⦄

diff --git a/Mathlib/Algebra/Module/Submodule/LinearMap.lean b/Mathlib/Algebra/Module/Submodule/LinearMap.lean
@@ -177,7 +177,7 @@ theorem subtype_comp_codRestrict (p : Submodule R₂ M₂) (h : ∀ b, f b ∈ p
 section
 
 variable {M₂' : Type*} [AddCommMonoid M₂'] [Module R₂ M₂']
-(p : M₂' →ₗ[R₂] M₂) (hp : Injective p) (h : ∀ c, f c ∈ range p)
+  (p : M₂' →ₗ[R₂] M₂) (hp : Injective p) (h : ∀ c, f c ∈ range p)
 
 /-- A linear map `f : M → M₂` whose values lie in the image of an injective linear map
 `p : M₂' → M₂` admits a unique lift to a linear map `M → M₂'`. -/

diff --git a/Mathlib/Algebra/Order/Floor/Div.lean b/Mathlib/Algebra/Order/Floor/Div.lean
@@ -248,6 +248,7 @@ noncomputable instance instFloorDiv : FloorDiv α (ι →₀ β) where
   zero_floorDiv a := by ext; exact zero_floorDiv _
 
 lemma floorDiv_def (f : ι →₀ β) (a : α) : f ⌊/⌋ a = f.mapRange (· ⌊/⌋ a) (zero_floorDiv _) := rfl
+set_option warning.simp.otherHead false in
 @[norm_cast] lemma coe_floorDiv (f : ι →₀ β) (a : α) : f ⌊/⌋ a = fun i ↦ f i ⌊/⌋ a := rfl
 @[simp] lemma floorDiv_apply (f : ι →₀ β) (a : α) (i : ι) : (f ⌊/⌋ a) i = f i ⌊/⌋ a := rfl
 
@@ -267,6 +268,7 @@ noncomputable instance instCeilDiv : CeilDiv α (ι →₀ β) where
   zero_ceilDiv a := by ext; exact zero_ceilDiv _
 
 lemma ceilDiv_def (f : ι →₀ β) (a : α) : f ⌈/⌉ a = f.mapRange (· ⌈/⌉ a) (zero_ceilDiv _) := rfl
+set_option warning.simp.otherHead false in
 @[norm_cast] lemma coe_ceilDiv_def (f : ι →₀ β) (a : α) : f ⌈/⌉ a = fun i ↦ f i ⌈/⌉ a := rfl
 @[simp] lemma ceilDiv_apply (f : ι →₀ β) (a : α) (i : ι) : (f ⌈/⌉ a) i = f i ⌈/⌉ a := rfl
 

diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/Horn.lean b/Mathlib/AlgebraicTopology/SimplicialSet/Horn.lean
@@ -94,7 +94,7 @@ lemma horn_obj_eq_univ {n : ℕ} (i : Fin (n + 1)) (m : ℕ) (h : m + 1 < n := b
       Finset.card_singleton, add_le_add_iff_right] at this
     have : n ≤ m + 1 := by simpa using this.trans Finset.card_image_le
     lia
-  have : ∃ j, ¬j = i ∧ ∀ (i : Fin (m + 1)), ¬(stdSimplex.objEquiv.symm.{u} f) i = j :=
+  have : ∃ j, ¬j = i ∧ ∀ (i : Fin (m + 1)), ¬(stdSimplex.objEquiv.{u}.symm f) i = j :=
     ⟨j, hij, fun k hk ↦ hj ⟨k, hk⟩⟩
   simpa [horn_eq_iSup] using this
 
@@ -140,7 +140,7 @@ lemma face_le_horn_iff {n : ℕ} (S : Finset (Fin (n + 2))) (j : Fin (n + 2)) :
 
 lemma objEquiv_symm_notMem_horn_of_isIso {n : ℕ} (i : Fin (n + 1))
     {d : SimplexCategory} (f : d ⟶ ⦋n⦌) [IsIso f] :
-    stdSimplex.objEquiv.symm.{u} f ∉ Λ[n, i].obj (op d) := by
+    stdSimplex.objEquiv.{u}.symm f ∉ Λ[n, i].obj (op d) := by
   rw [mem_horn_iff, ne_eq, not_not]
   ext i
   simpa using Or.inr ⟨inv f i, by simp [stdSimplex.coe_asOrderHom_objEquiv_symm.{u}]⟩

diff --git a/Mathlib/Analysis/Analytic/ChangeOrigin.lean b/Mathlib/Analysis/Analytic/ChangeOrigin.lean
@@ -43,7 +43,7 @@ open scoped NNReal ENNReal Topology
 open Filter Set
 
 variable {𝕜 E F : Type*} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
-[NormedAddCommGroup F] [NormedSpace 𝕜 F]
+  [NormedAddCommGroup F] [NormedSpace 𝕜 F]
 
 namespace FormalMultilinearSeries
 

diff --git a/Mathlib/Analysis/Distribution/Distribution.lean b/Mathlib/Analysis/Distribution/Distribution.lean
@@ -192,7 +192,7 @@ end mapCLM
 section DiracDelta
 
 /-- The Dirac delta distribution. This is zero if `x` does not belong to `Ω`. -/
-def delta (x : E) : 𝓓'^{n}(Ω, ℝ) where
+noncomputable def delta (x : E) : 𝓓'^{n}(Ω, ℝ) where
   toFun f := f x
   map_add' _ _ := rfl
   map_smul' _ _ := rfl

diff --git a/Mathlib/Analysis/Normed/Module/Ray.lean b/Mathlib/Analysis/Normed/Module/Ray.lean
@@ -22,7 +22,7 @@ public section
 open Real
 
 variable {E : Type*} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {F : Type*}
-[NormedAddCommGroup F] [NormedSpace ℝ F]
+  [NormedAddCommGroup F] [NormedSpace ℝ F]
 
 namespace SameRay
 

diff --git a/Mathlib/Analysis/Normed/Operator/Basic.lean b/Mathlib/Analysis/Normed/Operator/Basic.lean
@@ -79,7 +79,7 @@ theorem closedBall_subset_range_iff_surjective [RingHomSurjective σ₁₂] {f :
     by simp_all⟩
 
 variable {F' 𝓕' : Type*} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [Nontrivial F']
-{τ : 𝕜 →+* ℝ} [FunLike 𝓕' E F'] [SemilinearMapClass 𝓕' τ E F']
+  {τ : 𝕜 →+* ℝ} [FunLike 𝓕' E F'] [SemilinearMapClass 𝓕' τ E F']
 
 theorem sphere_subset_range_iff_surjective [RingHomSurjective τ] {f : 𝓕'} {x : F'} {r : ℝ}
     (hr : 0 < r) : sphere x r ⊆ Set.range f ↔ (⇑f).Surjective := by

diff --git a/Mathlib/Analysis/SpecialFunctions/Integrals/Basic.lean b/Mathlib/Analysis/SpecialFunctions/Integrals/Basic.lean
@@ -331,11 +331,7 @@ theorem integral_cos_mul_complex {z : ℂ} (hz : z ≠ 0) (a b : ℝ) :
   have b : HasDerivAt (fun y => y * z : ℂ → ℂ) z ↑x := hasDerivAt_mul_const _
   have c : HasDerivAt (Complex.sin ∘ fun y : ℂ => (y * z)) _ ↑x := HasDerivAt.comp (𝕜 := ℂ) x a b
   have d := HasDerivAt.comp_ofReal (c.div_const z)
-  #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
-  (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal.
-  It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in the new
-  canonicalizer; a minimization would help. The original proof was: `grind` -/
-  simpa [hz, mul_comm] using d
+  grind
 
 theorem integral_cos_sq_sub_sin_sq :
     ∫ x in a..b, cos x ^ 2 - sin x ^ 2 = sin b * cos b - sin a * cos a := by

diff --git a/Mathlib/CategoryTheory/Sites/Precoverage.lean b/Mathlib/CategoryTheory/Sites/Precoverage.lean
@@ -126,6 +126,7 @@ alias mem_coverings_of_isIso := HasIsos.mem_coverings_of_isIso
 alias sup_mem_coverings := IsStableUnderSup.sup_mem_coverings
 alias hasPullbacks_of_mem := HasPullbacks.hasPullbacks_of_mem
 
+set_option warning.simp.varHead false in
 attribute [local simp] Presieve.ofArrows.obj_idx Presieve.ofArrows.hom_idx in
 lemma mem_coverings_of_isPullback {J : Precoverage C} [IsStableUnderBaseChange J]
     {ι : Type w} {S : C} {X : ι → C}
@@ -146,6 +147,7 @@ lemma mem_coverings_of_isPullback {J : Precoverage C} [IsStableUnderBaseChange J
     refine le_antisymm (fun Z g ⟨i⟩ ↦ .mk _) fun Z g hg ↦ ?_
     exact .mk' (Sum.inl ⟨⟨_, _⟩, hg⟩) (by cat_disch) (by cat_disch)
 
+set_option warning.simp.varHead false in
 attribute [local simp] Presieve.ofArrows.obj_idx Presieve.ofArrows.hom_idx in
 lemma comp_mem_coverings {J : Precoverage C} [IsStableUnderComposition J] {ι : Type w}
     {S : C} {X : ι → C} (f : ∀ i, X i ⟶ S) (hf : Presieve.ofArrows X f ∈ J S)

diff --git a/Mathlib/CategoryTheory/Sites/Sheaf.lean b/Mathlib/CategoryTheory/Sites/Sheaf.lean
@@ -353,7 +353,7 @@ abbrev Sheaf.homEquiv {X Y : Sheaf J A} : (X ⟶ Y) ≃ (X.obj ⟶ Y.obj) :=
 def sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf :
     sheafToPresheaf J A ⋙ yoneda ⋙ (Functor.whiskeringLeft _ _ _).obj (sheafToPresheaf J A).op ≅
       yoneda :=
-  Functor.isoWhiskerLeft _ (Functor.isoWhiskerRight uliftYonedaIsoYoneda.symm.{max u₁ v₂} _) ≪≫
+  Functor.isoWhiskerLeft _ (Functor.isoWhiskerRight uliftYonedaIsoYoneda.{max u₁ v₂}.symm _) ≪≫
     (fullyFaithfulSheafToPresheaf J A).compUliftYonedaCompWhiskeringLeft ≪≫
     uliftYonedaIsoYoneda
 
@@ -368,7 +368,7 @@ def sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf :
     (sheafToPresheaf J A).op ⋙ coyoneda ⋙
       (Functor.whiskeringLeft _ _ _).obj (sheafToPresheaf J A) ≅
       coyoneda :=
-  Functor.isoWhiskerLeft _ (Functor.isoWhiskerRight uliftCoyonedaIsoCoyoneda.symm.{max u₁ v₂} _) ≪≫
+  Functor.isoWhiskerLeft _ (Functor.isoWhiskerRight uliftCoyonedaIsoCoyoneda.{max u₁ v₂}.symm _) ≪≫
     (fullyFaithfulSheafToPresheaf J A).compUliftCoyonedaCompWhiskeringLeft ≪≫
     uliftCoyonedaIsoCoyoneda
 

diff --git a/Mathlib/CategoryTheory/Sites/Sieves.lean b/Mathlib/CategoryTheory/Sites/Sieves.lean
@@ -1256,13 +1256,13 @@ def uliftNatTransOfLe {S T : Sieve X} (h : S ≤ T) :
 /-- A variant of `Sieve.functorInclusion` with universe lifting. -/
 @[simps! app]
 def uliftFunctorInclusion (S : Sieve X) :
-    S.uliftFunctor ⟶ uliftYoneda.obj.{w} X :=
+    S.uliftFunctor ⟶ uliftYoneda.{w}.obj X :=
   Functor.whiskerRight S.functorInclusion CategoryTheory.uliftFunctor
 
 /-- A variant of `Sieve.toFunctor` with universe lifting. -/
 @[simps]
 def toUliftFunctor (S : Sieve X) {Y : C} (f : Y ⟶ X) (hf : S f) :
-    uliftYoneda.obj.{w} Y ⟶ Sieve.uliftFunctor.{w} S where
+    uliftYoneda.{w}.obj Y ⟶ Sieve.uliftFunctor.{w} S where
   app Z := TypeCat.ofHom fun g ↦ ⟨g.down ≫ f, S.downward_closed hf g.down⟩
 
 theorem uliftNatTransOfLe_comm {S T : Sieve X} (h : S ≤ T) :
@@ -1279,7 +1279,7 @@ instance uliftFunctorInclusion_is_mono (S : Sieve X) :
 
 /-- A variant of `Sieve.sieveOfSubfunctor` with universe lifting. -/
 @[simps]
-def sieveOfUliftSubfunctor {R : Cᵒᵖ ⥤ Type (max w v₁)} (f : R ⟶ uliftYoneda.obj.{w} X) :
+def sieveOfUliftSubfunctor {R : Cᵒᵖ ⥤ Type max w v₁} (f : R ⟶ uliftYoneda.{w}.obj X) :
     Sieve X where
   arrows Y g := ∃ t, f.app (Opposite.op Y) t = { down := g }
   downward_closed := by

diff --git a/Mathlib/CategoryTheory/Yoneda.lean b/Mathlib/CategoryTheory/Yoneda.lean
@@ -1290,15 +1290,15 @@ variable {C : Type u₁} [Category.{v₁} C]
 /-- `FullyFaithful.homEquiv` as a natural isomorphism. -/
 @[simps! hom_app inv_app]
 def homNatIso {D : Type u₂} [Category.{v₂} D] {F : C ⥤ D} (hF : F.FullyFaithful) (X : C) :
-    F.op ⋙ uliftYoneda.obj.{v₁} (F.obj X) ≅ uliftYoneda.obj.{v₂} X :=
+    F.op ⋙ uliftYoneda.{v₁}.obj (F.obj X) ≅ uliftYoneda.{v₂}.obj X :=
   NatIso.ofComponents
     (fun Y => Equiv.toIso (Equiv.ulift.trans <| hF.homEquiv.symm.trans Equiv.ulift.symm))
     (fun f => by ext; exact Equiv.ulift.injective (hF.map_injective (by simp)))
 
 /-- `FullyFaithful.homEquiv` as a natural isomorphism. -/
 @[deprecated homNatIso (since := "2025-10-28")]
 def homNatIsoMaxRight {D : Type u₂} [Category.{max v₁ v₂} D] {F : C ⥤ D} (hF : F.FullyFaithful)
-    (X : C) : F.op ⋙ yoneda.obj (F.obj X) ≅ uliftYoneda.obj.{v₂} X :=
+    (X : C) : F.op ⋙ yoneda.obj (F.obj X) ≅ uliftYoneda.{v₂}.obj X :=
   isoWhiskerLeft F.op (uliftYonedaIsoYoneda.symm.app _) ≪≫ hF.homNatIso _ ≪≫
     NatIso.ofComponents (fun _ => Equiv.toIso (Equiv.ulift.trans Equiv.ulift.symm))
 
@@ -1318,15 +1318,15 @@ def compUliftYonedaCompWhiskeringLeft {D : Type u₂} [Category.{v₂} D] {F : C
 @[deprecated compUliftYonedaCompWhiskeringLeft (since := "2025-10-28")]
 def compYonedaCompWhiskeringLeftMaxRight {D : Type u₂} [Category.{max v₁ v₂} D] {F : C ⥤ D}
     (hF : F.FullyFaithful) : F ⋙ yoneda ⋙ (whiskeringLeft _ _ _).obj F.op ≅ uliftYoneda.{v₂} := by
-  refine isoWhiskerLeft F (isoWhiskerRight uliftYonedaIsoYoneda.symm.{v₁} _) ≪≫
+  refine isoWhiskerLeft F (isoWhiskerRight uliftYonedaIsoYoneda.{v₁}.symm _) ≪≫
     hF.compUliftYonedaCompWhiskeringLeft ≪≫
     NatIso.ofComponents (fun _ => NatIso.ofComponents
       (fun _ => Equiv.toIso (Equiv.ulift.trans Equiv.ulift.symm)))
 
 /-- `FullyFaithful.homEquiv` as a natural isomorphism, using coyoneda. -/
 @[simps! hom_app inv_app]
 def homNatIso' {D : Type u₂} [Category.{v₂} D] {F : C ⥤ D} (hF : F.FullyFaithful) (X : C) :
-    F ⋙ uliftCoyoneda.obj.{v₁} (op (F.obj X)) ≅ uliftCoyoneda.obj.{v₂} (op X) :=
+    F ⋙ uliftCoyoneda.{v₁}.obj (op (F.obj X)) ≅ uliftCoyoneda.{v₂}.obj (op X) :=
   NatIso.ofComponents
     (fun Y => Equiv.toIso (Equiv.ulift.trans <| hF.homEquiv.symm.trans Equiv.ulift.symm))
     (fun f => by ext; exact Equiv.ulift.injective (hF.map_injective (by simp)))

diff --git a/Mathlib/Combinatorics/Matroid/Init.lean b/Mathlib/Combinatorics/Matroid/Init.lean
@@ -16,6 +16,4 @@ This module defines the `Matroid` Aesop rule set which is used by the
 they're declared is imported, so we must put this declaration into its own file.
 -/
 
-public section
-
 declare_aesop_rule_sets [Matroid]
diff --git a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
@@ -651,11 +651,7 @@ lemma exists_isCycle_of_two_le_isEdgeReachable {u v : V} (huv : u ≠ v) {n :
     (h : G.IsEdgeReachable n u v) : ∃ w : G.Walk u u, w.IsCycle := by
   classical
   obtain ⟨w, hw, h⟩ := exists_adj_isEdgeReachable_two huv (h.anti hn)
-  #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
-  (replacing grind's canonicalizer with a type-directed normalizer), this was just
-  `have := @h {s(u, w)} (by simp)`. It is not yet clear whether this is due to defeq abuse in
-  Mathlib or a problem in the new canonicalizer; a minimization would help. -/
-  have := @h {s(u, w)} (by simp only [Set.encard_singleton, Nat.cast_ofNat]; decide)
+  have := @h {s(u, w)} (by simp)
   obtain ⟨w, p, hp₁, hp₂⟩ := adj_and_reachable_delete_edges_iff_exists_cycle.mp ⟨hw, this⟩
   exact ⟨p.rotate _ (p.fst_mem_support_of_mem_edges hp₂), hp₁.rotate _⟩
 

diff --git a/Mathlib/Combinatorics/SimpleGraph/Init.lean b/Mathlib/Combinatorics/SimpleGraph/Init.lean
@@ -16,6 +16,4 @@ This module defines the `SimpleGraph` Aesop rule set which is used by the
 they're declared is imported, so we must put this declaration into its own file.
 -/
 
-public section
-
 declare_aesop_rule_sets [SimpleGraph]
diff --git a/Mathlib/Data/Fin/VecNotation.lean b/Mathlib/Data/Fin/VecNotation.lean
@@ -413,8 +413,7 @@ theorem vecAlt1_vecAppend (v : Fin (n + 1) → α) :
       simp only [Nat.mod_add_mod,
         Nat.mod_eq_sub_mod h, show 1 % (n + 2) = 1 from Nat.mod_eq_of_lt (by lia)]
       refine (Nat.mod_eq_of_lt ?_).symm
-      #adaptation_note /-- After leanprover/lean4#13166, the `lia` tactic was timing out here. -/
-      omega
+      lia
 
 @[simp]
 theorem vecHead_vecAlt0 (hm : m + 2 = n + 1 + (n + 1)) (v : Fin (m + 2) → α) :

diff --git a/Mathlib/Data/Finset/Attr.lean b/Mathlib/Data/Finset/Attr.lean
@@ -14,8 +14,6 @@ public import Aesop.Frontend
 This file defines `finsetNonempty`, an aesop rule set to prove that a given finset is nonempty.
 -/
 
-public section
-
 -- `finsetNonempty` rules try to prove that a given finset is nonempty,
 -- for use in positivity extensions.
 declare_aesop_rule_sets [finsetNonempty] (default := true)
diff --git a/Mathlib/Data/Matrix/Reflection.lean b/Mathlib/Data/Matrix/Reflection.lean
@@ -207,10 +207,6 @@ example [NonUnitalNonAssocSemiring α] (a₁₁ a₁₂ a₂₁ a₂₂ b₁ b
 def etaExpand {m n} (A : Matrix (Fin m) (Fin n) α) : Matrix (Fin m) (Fin n) α :=
   Matrix.of (FinVec.etaExpand fun i => FinVec.etaExpand fun j => A i j)
 
-#adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
-(replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal.
-It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in the new
-canonicalizer; a minimization would help. The original proof was: `grind` -/
 /-- This can be used to prove
 ```lean
 example (A : Matrix (Fin 2) (Fin 2) α) :

diff --git a/Mathlib/Data/Sym/Sym2/Init.lean b/Mathlib/Data/Sym/Sym2/Init.lean
@@ -16,6 +16,4 @@ visible once the file in which they're declared is imported, so we must put this
 declaration into its own file.
 -/
 
-public section
-
 declare_aesop_rule_sets [Sym2]
diff --git a/Mathlib/FieldTheory/Finite/Basic.lean b/Mathlib/FieldTheory/Finite/Basic.lean
@@ -239,6 +239,16 @@ theorem pow_card_pow (n : ℕ) (a : K) : a ^ q ^ n = a := by
 
 end
 
+section
+
+variable [Field K] [Fintype K]
+
+open Lean in
+instance instGrindPowIdentity : Grind.PowIdentity K (Fintype.card K) where
+  pow_eq := pow_card
+
+end
+
 variable (K) [Field K] [Fintype K]
 
 /-- The cardinality `q` is a power of the characteristic of `K`. -/

diff --git a/Mathlib/Geometry/Manifold/Algebra/LieGroup.lean b/Mathlib/Geometry/Manifold/Algebra/LieGroup.lean
@@ -296,7 +296,7 @@ functions `f : M → N` is `C^n` whenever the denominator is non-zero.
 section Div
 
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞}
-{H : Type*} [TopologicalSpace H] {E : Type*}
+  {H : Type*} [TopologicalSpace H] {E : Type*}
   [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type*}
   [TopologicalSpace G] [ChartedSpace H G] [GroupWithZero G] [ContMDiffInv₀ I n G]
   [ContMDiffMul I n G]

diff --git a/Mathlib/GroupTheory/FreeGroup/Basic.lean b/Mathlib/GroupTheory/FreeGroup/Basic.lean
@@ -331,14 +331,14 @@ protected theorem sublist : Red L₁ L₂ → L₂ <+ L₁ :=
 theorem length_le (h : Red L₁ L₂) : L₂.length ≤ L₁.length :=
   h.sublist.length_le
 
-
-@[to_additive]
+@[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₁
   | _, _, @Step.not _ L1 L2 x b => by
     induction L1 with
     | nil =>
-      dsimp
+      -- This was just `dsimp` prior to https://github.com/leanprover/lean4/pull/13320
+      dsimp [sizeOf, _sizeOf_1]
       lia
     | cons hd tl ih =>
       dsimp

diff --git a/Mathlib/Logic/Embedding/Set.lean b/Mathlib/Logic/Embedding/Set.lean
@@ -162,6 +162,7 @@ the natural injection from the sigma-type `(i : ι) × ↑(s i)` to `α`. -/
     obtain rfl : i = j := h.eq (not_disjoint_iff.2 ⟨_, hx, hx'⟩)
     rfl
 
+set_option warning.simp.otherHead false in
 @[norm_cast] lemma Function.Embedding.coe_sigmaSet {s : ι → Set α} (h) :
     (Function.Embedding.sigmaSet h : ((i : ι) × s i) → α) = fun x ↦ x.2.1 := rfl
 

diff --git a/Mathlib/MeasureTheory/Measure/AddContent.lean b/Mathlib/MeasureTheory/Measure/AddContent.lean
@@ -68,7 +68,7 @@ open scoped ENNReal Topology Function
 namespace MeasureTheory
 
 variable {α : Type*} {C : Set (Set α)} {s t : Set α} {I : Finset (Set α)}
-{G : Type*} [AddCommMonoid G]
+  {G : Type*} [AddCommMonoid G]
 
 variable (G) in
 /-- An additive content is a set function with value 0 at the empty set which is finitely additive

diff --git a/Mathlib/MeasureTheory/VectorMeasure/AddContent.lean b/Mathlib/MeasureTheory/VectorMeasure/AddContent.lean
@@ -27,7 +27,7 @@ open scoped symmDiff
 namespace MeasureTheory.VectorMeasure
 
 variable {α : Type*} {hα : MeasurableSpace α} {E : Type*} [NormedAddCommGroup E]
-[CompleteSpace E] {μ : Measure α}
+  [CompleteSpace E] {μ : Measure α}
 
 /-- A finitely additive vector measure which is dominated by a finite positive measure is in
 fact countably additive. -/