diff --git a/.github/workflows/build_template.yml b/.github/workflows/build_template.yml
index 2e415aa594a647..0fd1d3fa405a0f 100644
--- 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
index e76444515c5b42..8af518d298d0c3 100644
--- 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
index 8e26eb7b9494f6..97d7b6d4ed16dd 100644
--- 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
index 10b0b3e4b5e08d..96546ee4f9951f 100644
--- 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
index e593c19088e76d..4778e592b7948a 100644
--- 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
index 19803221084e16..225971bc7c3983 100644
--- 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
index 4de2994db58ed2..3874fa32780c75 100644
--- 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
index 68d86fc001983e..5654a2b9333ef0 100644
--- 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
index 25998333bb4b4a..523dd9abe57ed2 100644
--- 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
index 70e0fbfb413bf6..a7c651c699abb9 100644
--- 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
index 19d6228da2c365..b95041cfe9ed39 100644
--- 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
index 931ea029f07803..c392c764bd5753 100644
--- 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
index ceb5c4bad4b473..e64bc5f6d23f02 100644
--- 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
index 49d9315288ad5e..373c330c5bef08 100644
--- 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
index 394fbeedb00916..fa5e72f7efabca 100644
--- 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
index c0a15ddcefc338..2292a10b1b816d 100644
--- 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
index 86dcd725acb774..097301a47b8a34 100644
--- 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
index 2cbb5c089d5dea..5715339400c477 100644
--- 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
index 8411abbbf0b19b..6a82173c4b022b 100644
--- a/Mathlib/CategoryTheory/Yoneda.lean
+++ b/Mathlib/CategoryTheory/Yoneda.lean
@@ -1290,7 +1290,7 @@ 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)))
@@ -1298,7 +1298,7 @@ def homNatIso {D : Type u₂} [Category.{v₂} D] {F : C ⥤ D} (hF : F.FullyFai
 /-- `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,7 +1318,7 @@ 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)))
@@ -1326,7 +1326,7 @@ def compYonedaCompWhiskeringLeftMaxRight {D : Type u₂} [Category.{max v₁ v
 /-- `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
index 6e434c01bdf627..bf806f06d08923 100644
--- 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
index dc25d0afbcfa1a..eb59c192fc81c4 100644
--- 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
index e33f62ae3c0e25..0928e07666be5f 100644
--- 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
index 9da254a61f272d..11479cbb45ed13 100644
--- 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
index 19a757ed46f9aa..a8894132142c32 100644
--- 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
index 6e45ce70128528..2c82f38918ffcc 100644
--- 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
index cda8468ef86fa9..69faa4d163130c 100644
--- 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
index 8c5a618609a8e4..5f6aed0703b1bc 100644
--- 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
index 0a996e925745b1..f3f9d6131ba33e 100644
--- 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
index 71199bb1f3d78b..95fd9a588f7de9 100644
--- 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
index 1eb4b2947b9212..4036dffb4dc419 100644
--- 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
index 7de59dcceb7473..cf63b02efd8989 100644
--- 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
index b296f2ba2d867e..1b2399ac8c7fd0 100644
--- 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. -/
diff --git a/Mathlib/Order/Bounded.lean b/Mathlib/Order/Bounded.lean
index dddc3d771498da..6ab52893a60e3b 100644
--- a/Mathlib/Order/Bounded.lean
+++ b/Mathlib/Order/Bounded.lean
@@ -5,7 +5,6 @@ Authors: Violeta Hernández Palacios
 -/
 module
 
-public import Mathlib.Tactic.Linter.DeprecatedModule
 public import Mathlib.Order.RelClasses
 public import Mathlib.Order.Interval.Set.Basic
 public import Mathlib.Order.Bounds.Defs
diff --git a/Mathlib/Probability/Kernel/Defs.lean b/Mathlib/Probability/Kernel/Defs.lean
index ca32d6bd9fcb3a..2362506ade3a96 100644
--- a/Mathlib/Probability/Kernel/Defs.lean
+++ b/Mathlib/Probability/Kernel/Defs.lean
@@ -288,11 +288,13 @@ lemma apply_congr_of_mem_measurableAtom (κ : Kernel α β) {y' y : α} (hy' : y
   ext s hs
   exact mem_of_mem_measurableAtom hy' (κ.measurable_coe hs (measurableSet_singleton (κ y s))) rfl
 
+set_option warning.simp.varHead false in
 @[nontriviality]
 lemma eq_zero_of_isEmpty_left (κ : Kernel α β) [h : IsEmpty α] : κ = 0 := by
   ext a
   exact h.elim a
 
+set_option warning.simp.varHead false in
 @[nontriviality]
 lemma eq_zero_of_isEmpty_right (κ : Kernel α β) [IsEmpty β] : κ = 0 := by
   ext a
diff --git a/Mathlib/RingTheory/Flat/Rank.lean b/Mathlib/RingTheory/Flat/Rank.lean
index a7a380d3a50fdb..7f5eae009c9a13 100644
--- a/Mathlib/RingTheory/Flat/Rank.lean
+++ b/Mathlib/RingTheory/Flat/Rank.lean
@@ -36,6 +36,7 @@ attribute [local instance] Module.free_of_flat_of_isLocalRing
 
 variable {R S : Type*} [CommRing R] [CommRing S] [Algebra R S] [Module.Flat R S] [Module.Finite R S]
 
+set_option backward.isDefEq.respectTransparency false in
 lemma PrimeSpectrum.rankAtStalk_pos_iff_mem_range_comap (p : PrimeSpectrum R) :
     0 < Module.rankAtStalk (R := R) S p ↔ p ∈ Set.range (PrimeSpectrum.comap (algebraMap R S)) := by
   rw [Module.rankAtStalk_eq, Module.finrank_pos_iff, p.nontrivial_iff_mem_rangeComap]
diff --git a/Mathlib/RingTheory/Ideal/Maps.lean b/Mathlib/RingTheory/Ideal/Maps.lean
index 6d2d703b36c2a3..a31eb62ccc79f1 100644
--- a/Mathlib/RingTheory/Ideal/Maps.lean
+++ b/Mathlib/RingTheory/Ideal/Maps.lean
@@ -421,18 +421,18 @@ If infinitely many of the `Rᵢ` are nontrivial, then there exists an ideal of `
 is not of the form `Πᵢ Iᵢ`, namely the ideal of finitely supported elements of `Πᵢ Rᵢ`
 (it is also not a principal ideal).) -/
 @[simps!] def piOrderIso [Finite ι] : Ideal (Π i, R i) ≃o Π i, Ideal (R i) := .symm
-{ toFun := pi
-  invFun I i := I.map (Pi.evalRingHom R i)
-  left_inv _ := funext map_evalRingHom_pi
-  right_inv I := by
-    ext r
-    simp_rw [mem_pi, mem_map_iff_of_surjective (Pi.evalRingHom R _) (Function.surjective_eval _)]
-    refine ⟨(fun ⟨r', hr'⟩ ↦ ?_) ∘ Classical.skolem.mp, fun hr i ↦ ⟨r, hr, rfl⟩⟩
-    have := Fintype.ofFinite ι
-    classical rw [show r = ∑ i, Pi.single i 1 * r' i from funext fun i ↦ by
-      rw [← (hr' _).2, Finset.sum_apply, Fintype.sum_eq_single i fun j ne ↦ by simp [ne]]; simp]
-    exact sum_mem fun i _ ↦ I.mul_mem_left _ (hr' i).1
-  map_rel_iff' := pi_le_pi_iff }
+  { toFun := pi
+    invFun I i := I.map (Pi.evalRingHom R i)
+    left_inv _ := funext map_evalRingHom_pi
+    right_inv I := by
+      ext r
+      simp_rw [mem_pi, mem_map_iff_of_surjective (Pi.evalRingHom R _) (Function.surjective_eval _)]
+      refine ⟨(fun ⟨r', hr'⟩ ↦ ?_) ∘ Classical.skolem.mp, fun hr i ↦ ⟨r, hr, rfl⟩⟩
+      have := Fintype.ofFinite ι
+      classical rw [show r = ∑ i, Pi.single i 1 * r' i from funext fun i ↦ by
+        rw [← (hr' _).2, Finset.sum_apply, Fintype.sum_eq_single i fun j ne ↦ by simp [ne]]; simp]
+      exact sum_mem fun i _ ↦ I.mul_mem_left _ (hr' i).1
+    map_rel_iff' := pi_le_pi_iff }
 
 instance [Finite ι] [∀ i, IsPrincipalIdealRing (R i)] : IsPrincipalIdealRing (Π i, R i) where
   principal I := by
diff --git a/Mathlib/RingTheory/MvPolynomial/Groebner.lean b/Mathlib/RingTheory/MvPolynomial/Groebner.lean
index d377151ef834f4..f7bd5500a53354 100644
--- a/Mathlib/RingTheory/MvPolynomial/Groebner.lean
+++ b/Mathlib/RingTheory/MvPolynomial/Groebner.lean
@@ -212,13 +212,13 @@ theorem div {ι : Type*} {b : ι → MvPolynomial σ R}
 termination_by WellFounded.wrap
   ((isWellFounded_iff m.syn fun x x_1 ↦ x < x_1).mp m.wf) (m.toSyn (m.degree f))
 decreasing_by
-· exact deg_reduce
-· apply degree_sub_LTerm_lt
-  intro hf0
-  apply hf'0
-  simp only [subLTerm, sub_eq_zero]
-  nth_rewrite 1 [eq_C_of_degree_eq_zero hf0, hf0]
-  simp
+  · exact deg_reduce
+  · apply degree_sub_LTerm_lt
+    intro hf0
+    apply hf'0
+    simp only [subLTerm, sub_eq_zero]
+    nth_rewrite 1 [eq_C_of_degree_eq_zero hf0, hf0]
+    simp
 
 /-!
 Module doc as workaround for a parser error that prevents using `set_option`
diff --git a/Mathlib/RingTheory/Perfection.lean b/Mathlib/RingTheory/Perfection.lean
index 4a4117cdd01125..b705efb5863b4c 100644
--- a/Mathlib/RingTheory/Perfection.lean
+++ b/Mathlib/RingTheory/Perfection.lean
@@ -838,6 +838,8 @@ namespace Tilt
 noncomputable instance [Fact p.Prime] [hvp : Fact (v p ≠ 1)] : Field (Tilt K v O hv p) :=
   haveI := Fact.mk <| mt hv.one_of_isUnit <| (map_natCast (algebraMap O K) p).symm ▸ hvp.1
   haveI := PreTilt.isDomain K v O hv p
+  #adaptation_note /-- This `letI` was not needed prior to nightly-2026-04-15. -/
+  letI : CommRing (PreTilt O p) := inferInstance
   inferInstanceAs <| Field (FractionRing _)
 
 end Tilt
diff --git a/Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean b/Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean
index 86d0de6b04f7ea..b48d7cf28c1579 100644
--- a/Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean
+++ b/Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean
@@ -1214,10 +1214,10 @@ theorem orderMonoidIso_embed [v.Compatible] {Γ' : Type*} [LinearOrderedCommGrou
     (w : Valuation R Γ') [w.Compatible] (x : ValueGroupWithZero R) (h : w.IsEquiv v) :
     h.orderMonoidIso
     (embed w x) = embed v x := by
-simp only [embed, ← Valuation.restrict_def, coe_mk, ZeroHom.coe_mk]
-induction x using ValueGroupWithZero.ind with
-| mk r s =>
-  simp
+  simp only [embed, ← Valuation.restrict_def, coe_mk, ZeroHom.coe_mk]
+  induction x using ValueGroupWithZero.ind with
+  | mk r s =>
+    simp
 
 /-- If a valuation `v` is compatible with the valuative relation, then `ValueGroupWithZero R`
 is isomorphic to the image group (with zero) of `v` as an ordered group with zero. -/
diff --git a/Mathlib/Tactic/ArithMult/Init.lean b/Mathlib/Tactic/ArithMult/Init.lean
index 4c95026124c1a6..4afdad3dd49e0f 100644
--- a/Mathlib/Tactic/ArithMult/Init.lean
+++ b/Mathlib/Tactic/ArithMult/Init.lean
@@ -16,6 +16,4 @@ This module defines the `IsMultiplicative` Aesop rule set which is used by the
 they're declared is imported, so we must put this declaration into its own file.
 -/
 
-public meta section
-
 declare_aesop_rule_sets [IsMultiplicative]
diff --git a/Mathlib/Tactic/Bound/Init.lean b/Mathlib/Tactic/Bound/Init.lean
index 8168cf288aefd4..f2a48a6687e866 100644
--- a/Mathlib/Tactic/Bound/Init.lean
+++ b/Mathlib/Tactic/Bound/Init.lean
@@ -16,6 +16,4 @@ This module defines the `Bound` Aesop rule set which is used by the
 they're declared is imported, so we must put this declaration into its own file.
 -/
 
-public meta section
-
 declare_aesop_rule_sets [Bound]
diff --git a/Mathlib/Tactic/Continuity/Init.lean b/Mathlib/Tactic/Continuity/Init.lean
index e988564a6b947d..19e4f9da717012 100644
--- a/Mathlib/Tactic/Continuity/Init.lean
+++ b/Mathlib/Tactic/Continuity/Init.lean
@@ -16,6 +16,4 @@ This module defines the `Continuous` Aesop rule set which is used by the
 they're declared is imported, so we must put this declaration into its own file.
 -/
 
-public meta section
-
 declare_aesop_rule_sets [Continuous]
diff --git a/Mathlib/Tactic/DefEqAbuse.lean b/Mathlib/Tactic/DefEqAbuse.lean
index edb6ba26d1af18..e5f0546c1573f8 100644
--- a/Mathlib/Tactic/DefEqAbuse.lean
+++ b/Mathlib/Tactic/DefEqAbuse.lean
@@ -308,7 +308,7 @@ Comparison is whitespace-insensitive to handle cases where LHS and RHS are seman
 but rendered with different line breaks or spacing.
 TODO: once https://github.com/leanprover/lean4/pull/12698 is available, refactor to use
 `TraceData.result?` and compare the LHS/RHS `Expr`s structurally instead of string-matching. -/
-private def isIdenticalSidesStr (raw : String) : Bool :=
+def isIdenticalSidesStr (raw : String) : Bool :=
   if let [lhsRaw, rhs] := raw.splitOn " =?= " then
     -- Strip the leading status emoji/word (first whitespace-delimited token).
     let lhs := match lhsRaw.splitOn " " with
@@ -324,7 +324,7 @@ private def isIdenticalSidesStr (raw : String) : Bool :=
 Each level adds more detail to pretty-printed expressions.
 We prefer symmetric options (`pp.universes`, `pp.explicit`) over `pp.analyze`,
 which is context-dependent and can add annotations to only one side. -/
-private def ppEscalations : List (Options → Options) :=
+def ppEscalations : List (Options → Options) :=
   [ fun o => o.setBool `pp.universes true
   , fun o => o.setBool `pp.explicit true
   ]
diff --git a/Mathlib/Tactic/Finiteness/Attr.lean b/Mathlib/Tactic/Finiteness/Attr.lean
index bb64d9e46af3de..226794663ee9b0 100644
--- a/Mathlib/Tactic/Finiteness/Attr.lean
+++ b/Mathlib/Tactic/Finiteness/Attr.lean
@@ -10,6 +10,4 @@ public import Aesop.Frontend
 
 /-! # Finiteness tactic attribute -/
 
-public meta section
-
 declare_aesop_rule_sets [finiteness]
diff --git a/Mathlib/Tactic/Linter/DirectoryDependency.lean b/Mathlib/Tactic/Linter/DirectoryDependency.lean
index bef329dd005e8f..33c1ac5d33b6a3 100644
--- a/Mathlib/Tactic/Linter/DirectoryDependency.lean
+++ b/Mathlib/Tactic/Linter/DirectoryDependency.lean
@@ -620,7 +620,7 @@ open DirectoryDependency
 
 /-- Check if one of the imports `imports` to `mainModule` is forbidden by `forbiddenImportDirs`;
 if so, return an error describing how the import transitively arises. -/
-private def checkBlocklist (env : Environment) (mainModule : Name) (imports : Array Name) : Option MessageData := Id.run do
+def checkBlocklist (env : Environment) (mainModule : Name) (imports : Array Name) : Option MessageData := Id.run do
   match forbiddenImportDirs.findAny mainModule imports with
   | some (n₁, n₂) => do
     if let some imported := n₂.prefixToName imports then
diff --git a/Mathlib/Tactic/Linter/HashCommandLinter.lean b/Mathlib/Tactic/Linter/HashCommandLinter.lean
index c8b650c5c99d36..fab26473aa53a6 100644
--- a/Mathlib/Tactic/Linter/HashCommandLinter.lean
+++ b/Mathlib/Tactic/Linter/HashCommandLinter.lean
@@ -46,7 +46,7 @@ open Command in
 /-- Exactly like `withSetOptionIn`, but recursively discards nested uses of `in`.
 Intended to be used in the `hashCommand` linter, where we want to enter `set_option` `in` commands.
 -/
-private partial def withSetOptionIn' (cmd : CommandElab) : CommandElab := fun stx => do
+partial def withSetOptionIn' (cmd : CommandElab) : CommandElab := fun stx => do
   if stx.getKind == ``Lean.Parser.Command.in then
     if stx[0].getKind == ``Lean.Parser.Command.set_option then
       let (opts, _) ← Elab.elabSetOption stx[0][1] stx[0][3]
@@ -58,7 +58,7 @@ private partial def withSetOptionIn' (cmd : CommandElab) : CommandElab := fun st
     cmd stx
 
 /-- `allowed_commands` is the `HashSet` of `#`-commands that are allowed in 'Mathlib'. -/
-private abbrev allowed_commands : Std.HashSet String := { "#adaptation_note" }
+abbrev allowed_commands : Std.HashSet String := { "#adaptation_note" }
 
 /-- Checks that no command beginning with `#` is present in 'Mathlib',
 except for the ones in `allowed_commands`.
diff --git a/Mathlib/Tactic/Linter/MinImports.lean b/Mathlib/Tactic/Linter/MinImports.lean
index ae2a42c439c518..01648ac8527692 100644
--- a/Mathlib/Tactic/Linter/MinImports.lean
+++ b/Mathlib/Tactic/Linter/MinImports.lean
@@ -52,7 +52,7 @@ structure ImportState where
 /--
 `minImportsRef` keeps track of cumulative imports across multiple commands, using `ImportState`.
 -/
-private initialize minImportsRef : IO.Ref ImportState ← IO.mkRef {}
+initialize minImportsRef : IO.Ref ImportState ← IO.mkRef {}
 
 /-- `#reset_min_imports` sets to empty the current list of cumulative imports. -/
 elab "#reset_min_imports" : command => minImportsRef.set {}
@@ -125,7 +125,7 @@ def minImportsLinter : Linter where run := withSetOptionIn fun stx ↦ do
     -- when the linter reaches the end of the file or `#exit`, it gives a report
     if #[``Parser.Command.eoi, ``Lean.Parser.Command.exit].contains stx.getKind then
       let explicitImportsInFile : NameSet :=
-        .ofArray ((env.imports.map (·.module)).erase `Init)
+        .ofArray ((env.imports.map (·.module)).filter (!isInitImport ·))
       let newImps := importsSoFar \ explicitImportsInFile
       let currentlyUnneededImports := explicitImportsInFile \ importsSoFar
       -- we read the current file, to do a custom parsing of the imports:
@@ -146,7 +146,7 @@ def minImportsLinter : Linter where run := withSetOptionIn fun stx ↦ do
         logWarningAt ((impMods.raw.find? (·.isOfKind `import)).getD default)
           m!"-- missing imports\n{"\n".intercalate withImport.toList}"
     let id ← getId stx
-    let newImports := getIrredundantImports env (← getAllImports stx id)
+    let newImports := (getIrredundantImports env (← getAllImports stx id)).filter (!isInitImport ·)
     let tot := (newImports.append importsSoFar)
     let redundant := env.findRedundantImports tot.toArray
     let currImports := tot \ redundant
diff --git a/Mathlib/Tactic/Linter/PrivateModule.lean b/Mathlib/Tactic/Linter/PrivateModule.lean
index 08905121646445..bf5a2aa6a32502 100644
--- a/Mathlib/Tactic/Linter/PrivateModule.lean
+++ b/Mathlib/Tactic/Linter/PrivateModule.lean
@@ -26,6 +26,9 @@ the file.
 Note that private declarations from the current module are exactly those which satisfy
 `isPrivateName`, whether private due to an explicit `private` or due to not being made `public`.
 
+Since initializers have downstream effects regardless of whether they're `private` or `public`, any
+module which registers an initializer is considered non-private.
+
 We also do not count declarations which satisfy `isReservedName` as public declarations *from the
 current module*. While they might indeed be public, the declarations associated with reserved names
 are generated automatically and lazily, sometimes in downstream modules from the one in which the
@@ -46,8 +49,7 @@ See also the type `Lean.ReservedNameAction`, invocations of `registerReservedNam
 
 Note that metaprograms should not add public declarations when run in private scopes. Doing so would
 likely be a bug in the metaprogram. As such, we do not perform further checks for automatically
-generated declarations such as those detected by `isAutoDecl` or `isInternalDetail`, which would
-wrongly exclude e.g. public declarations generated by `initialize`.
+generated declarations such as those detected by `isAutoDecl` or `isInternalDetail`.
 -/
 
 meta section
@@ -75,19 +77,22 @@ def privateModule : Linter where run stx := do
   if stx.isOfKind ``Parser.Command.eoi then
     unless getLinterValue linter.privateModule (← getLinterOptions) do
       return
-    if (← getEnv).header.isModule then
+    if (← getEnv).header.isModule
+      -- If there are new initializers, this module has a downstream effect and is not private.
+      && (regularInitAttr.ext.getState (← getEnv)).1.isEmpty
       -- Don't lint an imports-only module:
-      if !(← getEnv).constants.map₂.isEmpty then
-        -- Exit if any declaration from the current module is public:
-        for (decl, _) in (← getEnv).constants.map₂ do
-          -- Ignore both private and reserved names; see implementation notes
-          if !isPrivateName decl && !isReservedName (← getEnv) decl then return
-        -- Lint if all names are private:
-        let topOfFileRef := Syntax.atom (.synthetic ⟨0⟩ ⟨0⟩) ""
-        logLint linter.privateModule topOfFileRef
-          "The current module only contains private declarations.\n\n\
-          Consider adding `@[expose] public section` at the beginning of the module, \
-          or selectively marking declarations as `public`."
+      && !(← getEnv).constants.map₂.isEmpty
+    then
+      -- Exit if any declaration from the current module is public:
+      for (decl, _) in (← getEnv).constants.map₂ do
+        -- Ignore both private and reserved names; see implementation notes
+        if !isPrivateName decl && !isReservedName (← getEnv) decl then return
+      -- Lint if all names are private:
+      let topOfFileRef := Syntax.atom (.synthetic ⟨0⟩ ⟨0⟩) ""
+      logLint linter.privateModule topOfFileRef
+        "The current module only contains private declarations.\n\n\
+        Consider adding `@[expose] public section` at the beginning of the module, \
+        or selectively marking declarations as `public`."
 
 initialize addLinter privateModule
 
diff --git a/Mathlib/Tactic/Measurability/Init.lean b/Mathlib/Tactic/Measurability/Init.lean
index 85e8ae3add56fb..20debd09a5bf8b 100644
--- a/Mathlib/Tactic/Measurability/Init.lean
+++ b/Mathlib/Tactic/Measurability/Init.lean
@@ -16,6 +16,4 @@ This module defines the `Measurable` Aesop rule set which is used by the
 they're declared is imported, so we must put this declaration into its own file.
 -/
 
-public meta section
-
 declare_aesop_rule_sets [Measurable]
diff --git a/Mathlib/Tactic/MinImports.lean b/Mathlib/Tactic/MinImports.lean
index 9d5f781fece6ed..732ae93bb3ddda 100644
--- a/Mathlib/Tactic/MinImports.lean
+++ b/Mathlib/Tactic/MinImports.lean
@@ -64,6 +64,13 @@ open Lean Elab Command
 
 namespace Mathlib.Command.MinImports
 
+/-- Returns `true` if `n` is `Init` or a descendant of `Init`. These imports are always available
+in ordinary Mathlib files, so they are omitted from user-facing `#min_imports` output. -/
+partial def isInitImport : Name → Bool
+  | `Init => true
+  | .str p _ => isInitImport p
+  | _ => false
+
 /-- `getSyntaxNodeKinds stx` takes a `Syntax` input `stx` and returns the `NameSet` of all the
 `SyntaxNodeKinds` and all the identifiers contained in `stx`. -/
 partial
@@ -251,7 +258,7 @@ It is used to provide the internally generated name for "nameless" `instance`s.
 -/
 def minImpsCore (stx id : Syntax) : CommandElabM Unit := do
     let tot := getIrredundantImports (← getEnv) (← getAllImports stx id)
-    let fileNames := tot.toArray.qsort Name.lt
+    let fileNames := (tot.toArray.filter (!isInitImport ·)).qsort Name.lt
     logInfoAt (← getRef) m!"{"\n".intercalate (fileNames.map (s!"public import {·}")).toList}"
 
 /-- `#min_imports in cmd` scans the syntax `cmd` and the declaration obtained by elaborating `cmd`
diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean b/Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean
index dd08bd9caf1a31..495ccb223bb43c 100644
--- a/Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean
+++ b/Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean
@@ -269,7 +269,7 @@ end CompleteSpace
 section Pi
 
 variable {ι : Type*} {X : α → Type*} [∀ x, CommMonoid (X x)] [∀ x, TopologicalSpace (X x)]
-{L : SummationFilter ι}
+  {L : SummationFilter ι}
 
 @[to_additive]
 theorem Pi.hasProd {f : ι → ∀ x, X x} {g : ∀ x, X x} :
diff --git a/Mathlib/Topology/Algebra/InfiniteSum/GroupCompletion.lean b/Mathlib/Topology/Algebra/InfiniteSum/GroupCompletion.lean
index 226f4e4d1ab33f..dbc911b2b241b8 100644
--- a/Mathlib/Topology/Algebra/InfiniteSum/GroupCompletion.lean
+++ b/Mathlib/Topology/Algebra/InfiniteSum/GroupCompletion.lean
@@ -17,7 +17,7 @@ public section
 open UniformSpace.Completion
 
 variable {α β : Type*} [AddCommGroup α] [UniformSpace α] [IsUniformAddGroup α]
-{L : SummationFilter β}
+  {L : SummationFilter β}
 
 /-- A function `f` has a sum in a uniform additive group `α` if and only if it has that sum in the
 completion of `α`. -/
diff --git a/Mathlib/Topology/Sheaves/Init.lean b/Mathlib/Topology/Sheaves/Init.lean
index 053c3cdee10982..f5fc267eee2827 100644
--- a/Mathlib/Topology/Sheaves/Init.lean
+++ b/Mathlib/Topology/Sheaves/Init.lean
@@ -16,7 +16,5 @@ visible once the file in which they're declared is imported, so we must put this
 declaration into its own file.
 -/
 
-public section
-
 /- to prove subset relations -/
 declare_aesop_rule_sets [Restrict]
diff --git a/MathlibTest/BasicFiles/Init.lean b/MathlibTest/BasicFiles/Init.lean
index 59ca2efa0b844f..4cbb559c20d688 100644
--- a/MathlibTest/BasicFiles/Init.lean
+++ b/MathlibTest/BasicFiles/Init.lean
@@ -33,7 +33,7 @@ import Mathlib.Init
 proof_wanted please_prove_this : True
 
 -- Guard against the shake tool modifying our imports
-/-- info: [public import Init, import Mathlib.Init] -/
+/-- info: [public import Init, public meta import Init, import Mathlib.Init] -/
 #guard_msgs in
 run_elab Lean.logInfo m!"{(← Lean.MonadEnv.getEnv).imports}"
 
diff --git a/MathlibTest/BasicFiles/Tactic.lean b/MathlibTest/BasicFiles/Tactic.lean
index 3368b3c7823a2c..3944dcda6da406 100644
--- a/MathlibTest/BasicFiles/Tactic.lean
+++ b/MathlibTest/BasicFiles/Tactic.lean
@@ -8,6 +8,6 @@ import Mathlib.Tactic
 #find_syntax "test_find_syntax" approx
 
 -- Guard against the shake tool modifying our imports
-/-- info: [public import Init, import Mathlib.Tactic] -/
+/-- info: [public import Init, public meta import Init, import Mathlib.Tactic] -/
 #guard_msgs in
 run_elab Lean.logInfo m!"{(← Lean.MonadEnv.getEnv).imports}"
diff --git a/MathlibTest/BasicFiles/TacticBasic.lean b/MathlibTest/BasicFiles/TacticBasic.lean
index f19fa468ff29b1..f1e44b1e8b7eb5 100644
--- a/MathlibTest/BasicFiles/TacticBasic.lean
+++ b/MathlibTest/BasicFiles/TacticBasic.lean
@@ -5,6 +5,6 @@ import Mathlib.Tactic.Basic
 /-! Checks that some utilities are available already when importing `Mathlib.Tactic.Basic`. -/
 
 -- Guard against the shake tool modifying our imports
-/-- info: [public import Init, import Mathlib.Tactic.Basic] -/
+/-- info: [public import Init, public meta import Init, import Mathlib.Tactic.Basic] -/
 #guard_msgs in
 run_elab Lean.logInfo m!"{(← Lean.MonadEnv.getEnv).imports}"
diff --git a/MathlibTest/BasicFiles/TacticCommon.lean b/MathlibTest/BasicFiles/TacticCommon.lean
index 7c9190b296c047..3ae7c274824d68 100644
--- a/MathlibTest/BasicFiles/TacticCommon.lean
+++ b/MathlibTest/BasicFiles/TacticCommon.lean
@@ -32,6 +32,6 @@ theorem test_count_heartbeats : True := trivial
 theorem test_print_sorries : True := sorry
 
 -- Guard against the shake tool modifying our imports
-/-- info: [public import Init, import Mathlib.Tactic.Common] -/
+/-- info: [public import Init, public meta import Init, import Mathlib.Tactic.Common] -/
 #guard_msgs in
 run_elab Lean.logInfo m!"{(← Lean.MonadEnv.getEnv).imports}"
diff --git a/MathlibTest/DocPrime.lean b/MathlibTest/DocPrime.lean
index 7411651cca5259..bc217c8686bc65 100644
--- a/MathlibTest/DocPrime.lean
+++ b/MathlibTest/DocPrime.lean
@@ -60,6 +60,9 @@ Note: This linter can be disabled with `set_option linter.docPrime false`
 @[simp]
 theorem thm_with_attr_no_doc' : True := .intro
 
+class Dummy where
+  field : True
+
 /--
 warning: `inst_no_doc'` is missing a doc-string, please add one.
 Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
@@ -67,7 +70,7 @@ Declarations whose name ends with a `'` are expected to contain an explanation f
 Note: This linter can be disabled with `set_option linter.docPrime false`
 -/
 #guard_msgs in
-instance inst_no_doc' : True := .intro
+instance inst_no_doc' : Dummy := ⟨.intro⟩
 
 /--
 warning: `abbrev_no_doc'` is missing a doc-string, please add one.
@@ -91,6 +94,6 @@ def def_no_doc' : True := .intro
 namespace Foo'
 
 example : True := .intro
-instance : True := .intro
+instance : Dummy := ⟨.intro⟩
 
 end Foo'
diff --git a/MathlibTest/EmptyLine.lean b/MathlibTest/EmptyLine.lean
index 41a11e48d8e824..637a9d5ad5b0e5 100644
--- a/MathlibTest/EmptyLine.lean
+++ b/MathlibTest/EmptyLine.lean
@@ -159,31 +159,31 @@ example : True := by  -- The following empty line is not reported, since the com
 warning: Please, write a comment here or remove this line, but do not place empty lines within commands!
 Context:
                        ↓
-  ⏎example : True := by⏎⏎-- Here I start⏎⏎
+  ⏎example : True := by⏎⏎  -- Here I start⏎⏎
 
 Note: This linter can be disabled with `set_option linter.style.emptyLine false`
 ---
 warning: Please, write a comment here or remove this line, but do not place empty lines within commands!
 Context:
-         ↓
-  ⏎--stop⏎⏎trivial⏎⏎
+           ↓
+  ⏎  --stop⏎⏎  trivial⏎⏎
 
 Note: This linter can be disabled with `set_option linter.style.emptyLine false`
 -/
 #guard_msgs in
 example : True := by
 
--- Here I start
+  -- Here I start
 
-/-
+  /-
 
--/
+  -/
 
---stop
+  --stop
 
-trivial -- also a comment
+  trivial -- also a comment
 
--- with a line break
+  -- with a line break
 
 -- Check that `where` fields allow empty lines.
 structure F where
diff --git a/MathlibTest/LintStyle.lean b/MathlibTest/LintStyle.lean
index 88d0be9a340d75..e6cd6fb7f83b58 100644
--- a/MathlibTest/LintStyle.lean
+++ b/MathlibTest/LintStyle.lean
@@ -201,7 +201,6 @@ set_option linter.style.cdot true
 set_option allowUnsafeReducibility true in
 attribute [instance_reducible] Int.add
 
-set_option linter.globalAttributeIn false in
 /--
 warning: Please, use '·' (typed as `\.`) instead of '.' as 'cdot'.
 
@@ -216,7 +215,6 @@ warning: Please, use '·' (typed as `\.`) instead of '.' as 'cdot'.
 Note: This linter can be disabled with `set_option linter.style.cdot false`
 -/
 #guard_msgs in
-attribute [instance] Int.add in
 instance : Inhabited Nat where
   default := by
     . have := 0
@@ -276,7 +274,6 @@ example : True := by
 end cdotLinter
 set_option linter.style.dollarSyntax true
 
-set_option linter.globalAttributeIn false in
 /--
 warning: Please use '<|' instead of '$' for the pipe operator.
 
@@ -287,8 +284,8 @@ warning: Please use '<|' instead of '$' for the pipe operator.
 Note: This linter can be disabled with `set_option linter.style.dollarSyntax false`
 -/
 #guard_msgs in
-attribute [instance] Int.add in
-instance (f g : Nat → Nat) : Inhabited Nat where
+@[reducible]
+def test (f g : Nat → Nat) : Inhabited Nat where
   default := by
     · have := 0
       · have : Nat := f $ g $ 0
diff --git a/MathlibTest/PrivateModuleLinter/initialize.lean b/MathlibTest/PrivateModuleLinter/initialize.lean
index 7d5b5a0db2e050..2b8a212c1dd662 100644
--- a/MathlibTest/PrivateModuleLinter/initialize.lean
+++ b/MathlibTest/PrivateModuleLinter/initialize.lean
@@ -2,11 +2,11 @@ module
 
 import Mathlib.Tactic.Linter.PrivateModule
 
-set_option linter.privateModule true
-
 open Lean
 
--- Should not fire, since `initialize` creates a genuinely public declaration.
+set_option linter.privateModule true
+
+-- Should not fire, since `initialize` has effects downstream despite creating a private decl here.
 initialize pure ()
 
 /- Check that we have indeed created a declaration, and aren't not linting just due to being an
diff --git a/MathlibTest/globalAttributeIn.lean b/MathlibTest/globalAttributeIn.lean
index 37f273b69bc93b..56ced2d39e8426 100644
--- a/MathlibTest/globalAttributeIn.lean
+++ b/MathlibTest/globalAttributeIn.lean
@@ -8,33 +8,14 @@ import Mathlib.Tactic.Linter.GlobalAttributeIn
 
 /-! Tests for the `globalAttributeIn` linter. -/
 
--- Test disabling the linter.
-set_option linter.globalAttributeIn false
-
 -- After https://github.com/leanprover/lean4/pull/12263,
 -- we need to add `instance_reducible` before we can add `instance` to `Int.add`.
 set_option allowUnsafeReducibility true in
 attribute [instance_reducible] Int.add
 
-set_option autoImplicit false in
-attribute [instance] Int.add in
-instance : Inhabited Int where
-  default := 0
-
-set_option linter.globalAttributeIn true
-
-set_option linter.globalAttributeIn false in
-attribute [instance] Int.add in
-instance : Inhabited Int where
-  default := 0
-
--- Global instances with `in`, are linted, as they are a footgun.
-
 /--
-warning: Despite the `in`, the attribute 'instance 1100' is added globally to 'Int.add'
+error: Despite the `in`, the attribute instance 1100 is added globally to Int.add
 please remove the `in` or make this a `local instance 1100`
-
-Note: This linter can be disabled with `set_option linter.globalAttributeIn false`
 -/
 #guard_msgs in
 set_option autoImplicit false in
@@ -44,10 +25,8 @@ instance : Inhabited Int where
   default := 0
 
 /--
-warning: Despite the `in`, the attribute 'instance' is added globally to 'Int.add'
+error: Despite the `in`, the attribute instance is added globally to Int.add
 please remove the `in` or make this a `local instance`
-
-Note: This linter can be disabled with `set_option linter.globalAttributeIn false`
 -/
 #guard_msgs in
 attribute [instance] Int.add in
@@ -55,10 +34,8 @@ instance : Inhabited Int where
   default := 0
 
 /--
-warning: Despite the `in`, the attribute 'simp' is added globally to 'Int.add'
+error: Despite the `in`, the attribute simp is added globally to Int.add
 please remove the `in` or make this a `local simp`
-
-Note: This linter can be disabled with `set_option linter.globalAttributeIn false`
 -/
 #guard_msgs in
 attribute [simp] Int.add in
@@ -73,17 +50,14 @@ namespace X
 theorem foo (x y : Nat) : x = y := sorry
 
 /--
-warning: Despite the `in`, the attribute 'simp' is added globally to 'foo'
+error: Despite the `in`, the attribute simp is added globally to foo
 please remove the `in` or make this a `local simp`
-
-Note: This linter can be disabled with `set_option linter.globalAttributeIn false`
 ---
-warning: Despite the `in`, the attribute 'ext' is added globally to 'foo'
+error: Despite the `in`, the attribute ext is added globally to foo
 please remove the `in` or make this a `local ext`
-
-Note: This linter can be disabled with `set_option linter.globalAttributeIn false`
 -/
 #guard_msgs in
+set_option warning.simp.varHead false in
 attribute [simp, local simp, ext, scoped instance, -simp, -ext] foo in
 def bar := False
 
diff --git a/lake-manifest.json b/lake-manifest.json
index ca0e4c0d66b879..5714e5948fbf7c 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,14 +1,14 @@
 {"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover-community/plausible",
+ [{"url": "https://github.com/Kha/plausible",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "f449eabb8f7e3feef0366856c20e28a6d2c97ee3",
+   "scope": "",
+   "rev": "1e454fed5528d2df0f45708f6b9e8e519c47fc5a",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "push-nuzuuroszpvz",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "86503d416c875fdcf3b6b6c54c22581e96c6bda7",
+   "rev": "cdab3938ccabbdb044be6896e251b5814bec932e",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,20 +65,20 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "bf597c77bf9b8e66720d724928207f5911533113",
+   "rev": "4b591181697264394a76288a163fd1d47621c96e",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.30.0-rc1",
+   "inputRev": "nightly-testing",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "f7d0ca7c926cdde0562af20394dd25d028b839a5",
+   "rev": "13567aed1ac4f12aea9484178e07e51f8c9f7658",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.30.0-rc1",
+   "inputRev": "v4.30.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "mathlib",
diff --git a/lakefile.lean b/lakefile.lean
index 5f11ec894a69ad..babb657761237b 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -6,7 +6,7 @@ open Lake DSL
 ## Mathlib dependencies on upstream projects
 -/
 
-require "leanprover-community" / "batteries" @ git "v4.30.0-rc1"
+require "leanprover-community" / "batteries" @ git "nightly-testing"
 require "leanprover-community" / "Qq" @ git "nightly-testing"
 require "leanprover-community" / "aesop" @ git "nightly-testing"
 require "leanprover-community" / "proofwidgets" @ git "v0.0.97"
@@ -15,7 +15,7 @@ require "leanprover-community" / "proofwidgets" @ git "v0.0.97"
     Please report this issue on the Lean Zulip."
 require "leanprover-community" / "importGraph" @ git "main"
 require "leanprover-community" / "LeanSearchClient" @ git "main"
-require "leanprover-community" / "plausible" @ git "main"
+require plausible from git "https://github.com/Kha/plausible" @ "push-nuzuuroszpvz"
 
 
 /-!
diff --git a/lean-toolchain b/lean-toolchain
index 54caac41bddf21..844e3659d22483 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2026-04-07
+leanprover/lean4:nightly-2026-04-16
diff --git a/scripts/create_deprecated_modules.lean b/scripts/create_deprecated_modules.lean
index 3b0d79fd3b8ebf..d17459a8128f45 100644
--- a/scripts/create_deprecated_modules.lean
+++ b/scripts/create_deprecated_modules.lean
@@ -5,6 +5,7 @@ Authors: Damiano Testa
 -/
 
 --import Mathlib.Init
+import Std.Time.Format
 import Std.Time.Zoned
 import Lean.Meta.Tactic.TryThis
 -- a comment here to test `keepTrailing
@@ -49,8 +50,12 @@ It returns just the imports of `fileContent`, including trailing comments if `ke
 -/
 def getHeader (fname fileContent : String) (keepTrailing : Bool) : IO String := do
   let (stx, _) ← Parser.parseHeader (Parser.mkInputContext fileContent fname)
-  let stx := if keepTrailing then stx.raw else stx.raw.unsetTrailing
-  let some substring := stx.getSubstring? | throw <| .userError "No substring: we have a problem!"
+  let imports := stx.raw.getArg 2  -- extract just the imports list
+  let imports := if keepTrailing then imports else imports.unsetTrailing
+  -- Use `withLeading := false` to exclude leading comments (e.g. copyright header) that the
+  -- parser now attaches to the first token (see leanprover/lean4#12662).
+  let some substring := imports.getSubstring? (withLeading := false) |
+    throw <| .userError "No substring: we have a problem!"
   return substring.toString
 
 /--
@@ -374,13 +379,7 @@ the deprecations later on.
 -- #find_deleted_files 0
 
 /--
-info: /-
-Copyright (c) 2025 Damiano Testa. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Damiano Testa
--/
-
---import Mathlib.Init
+info: import Std.Time.Format
 import Std.Time.Zoned
 import Lean.Meta.Tactic.TryThis
 -/
@@ -391,13 +390,7 @@ run_cmd
   logInfo head
 
 /--
-info: /-
-Copyright (c) 2025 Damiano Testa. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Damiano Testa
--/
-
---import Mathlib.Init
+info: import Std.Time.Format
 import Std.Time.Zoned
 import Lean.Meta.Tactic.TryThis
 -- a comment here to test `keepTrailing
diff --git a/scripts/nolints.json b/scripts/nolints.json
index 60e690f82c2121..28f12584330383 100644
--- a/scripts/nolints.json
+++ b/scripts/nolints.json
@@ -224,4 +224,9 @@
  ["docBlame", "Mathlib.Tactic.Coherence.LiftObj.lift"],
  ["docBlame", "Mathlib.Tactic.GCongr.ForwardExt.eval"],
  ["docBlame", "Mathlib.Tactic.Monotonicity.mono.side"],
- ["docBlame", "Mathlib.Tactic.Sat.buildReify.mkPS"]]
+ ["docBlame", "Mathlib.Tactic.Sat.buildReify.mkPS"],
+ ["docBlame", "Lean.Meta.RefinedDiscrTree.instInhabitedPartialMatch.default"],
+ ["docBlame", "Mathlib.Linter.Flexible.instInhabitedStained.default"],
+ ["docBlame", "Mathlib.Linter.instInhabitedImportState.default"],
+ ["docBlame", "Mathlib.Linter.TextBased.instInhabitedStyleError.default"],
+ ["docBlame", "Mathlib.Linter.instInhabitedFormatError.default"]]