cleanups

datokrat · datokrat · commit 83622cf5650a · 2026-06-25T15:08:53.000+02:00
diff --git a/Mathlib/Algebra/Category/MonCat/FilteredColimits.lean b/Mathlib/Algebra/Category/MonCat/FilteredColimits.lean
@@ -234,8 +234,6 @@ noncomputable def colimitCocone : Cocone F where
   pt := colimit.{v, u} F
   ι := { app := coconeMorphism F }
 
-set_option linter.tacticCheckInstances true in
-
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 /-- Given a cocone `t` of `F`, the induced monoid homomorphism from the colimit to the cocone point.
diff --git a/Mathlib/Algebra/Lie/DirectSum.lean b/Mathlib/Algebra/Lie/DirectSum.lean
@@ -90,8 +90,7 @@ set_option backward.isDefEq.respectTransparency false in
 /-- The projection map onto one component, as a morphism of Lie modules. -/
 def lieModuleComponent (j : ι) : (⨁ i, M i) →ₗ⁅R,L⁆ M j :=
   { component R ι M j with
-    map_lie' := fun {x m} => by
-      simp [component, lapply] }
+    map_lie' := fun {x m} => by simp [component, lapply] }
 
 end Modules
 
@@ -165,8 +164,7 @@ set_option backward.isDefEq.respectTransparency false in
 def lieAlgebraComponent (j : ι) : (⨁ i, L i) →ₗ⁅R⁆ L j :=
   { component R ι L j with
     toFun := component R ι L j
-    map_lie' := fun {x y} => by
-      simp [component, lapply] }
+    map_lie' := fun {x y} => by simp [component, lapply] }
 
 -- Note(kmill): `ext` cannot generate an iff theorem here since `x` and `y` do not determine `R`.
 @[ext (iff := false)]
diff --git a/Mathlib/Algebra/Order/Antidiag/Pi.lean b/Mathlib/Algebra/Order/Antidiag/Pi.lean
@@ -93,7 +93,6 @@ def finAntidiagonal.aux (d : ℕ) (n : μ) : {s : Finset (Fin d → μ) // ∀ f
           exact ⟨_, _, hf, _, rfl, Fin.cons_self_tail f⟩ }
 
 set_option backward.isDefEq.respectTransparency false in
-set_option backward.proofsInPublic true in
 /-- `finAntidiagonal d n` is the type of `d`-tuples with sum `n`.
 
 TODO: deduplicate with the less general `Finset.Nat.antidiagonalTuple`. -/
diff --git a/Mathlib/Algebra/Order/Module/HahnEmbedding.lean b/Mathlib/Algebra/Order/Module/HahnEmbedding.lean
@@ -197,7 +197,6 @@ noncomputable
 def hahnCoeff : seed.baseDomain →ₗ[K] (⨁ _ : FiniteArchimedeanClass M, R) :=
   (DirectSum.lmap seed.coeff') ∘ₗ (DirectSum.decomposeLinearEquiv _).toLinearMap
 
-set_option linter.auxLemma false in -- TODO
 theorem hahnCoeff_apply {x : seed.baseDomain} {f : Π₀ c, seed.stratum c}
     (h : x.val = f.sum fun c ↦ (seed.stratum c).subtype) (c : FiniteArchimedeanClass M) :
     seed.hahnCoeff x c = seed.coeff c (f c) := by
diff --git a/Mathlib/Algebra/Quaternion.lean b/Mathlib/Algebra/Quaternion.lean
@@ -751,9 +751,7 @@ protected instance algebra [CommSemiring S] [Algebra S R] : Algebra S ℍ[R] :=
   inferInstanceAs <| Algebra S ℍ[R,-1,0,-1]
 
 instance : Star ℍ[R] := inferInstanceAs <| Star ℍ[R,-1,0,-1]
-
 instance : StarRing ℍ[R] := inferInstanceAs <| StarRing ℍ[R,-1,0,-1]
-
 set_option backward.isDefEq.respectTransparency.types false in
 instance : IsStarNormal a := inferInstanceAs <| IsStarNormal (R := ℍ[R,-1,0,-1]) a
 
diff --git a/Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Formula.lean b/Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Formula.lean
@@ -104,15 +104,18 @@ lemma Y_sub_polynomialY : Y - W'.polynomialY = W'.negPolynomial := by
 lemma Y_sub_negPolynomial : Y - W'.negPolynomial = W'.polynomialY := by
   rw [← Y_sub_polynomialY, sub_sub_cancel]
 
+#adaptation_note
+/--
+Without this `implicit_reducible` attribute, `simpNF` gives a linter error on `slope_of_Y_eq`
+because of a nonconfluence: `negY` can be unfolded on the LHS, which prevents discharging the
+side condition of `slope_of_Y_eq` -- except if `negY` is implicit-reducible.
+So this attribute improves the confluence of `simp`.
+-/
 variable (W') in
 /-- The `Y`-coordinate of `-(x, y)` for a nonsingular affine point `(x, y)` on a Weierstrass curve
 `W`.
 
 This depends on `W`, and has argument order: `x`, `y`. -/
--- Without this `implicit_reducible` attribute, `simpNF` gives a linter error on `slope_of_Y_eq`
--- because of a nonconfluence: `negY` can be unfolded on the LHS, which prevents discharging the
--- side condition of `slope_of_Y_eq` -- except if `negY` is implicit-reducible.
--- So this attribute improves the confluence of `simp`.
 @[simp, implicit_reducible]
 def negY (x y : R) : R :=
   -y - W'.a₁ * x - W'.a₃
diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/Skeleton.lean b/Mathlib/AlgebraicTopology/SimplicialSet/Skeleton.lean
@@ -313,7 +313,8 @@ lemma ι_t_ι_eq_ι_l_b_ι (c : Cell i d) :
 lemma ι_l (c : Cell i d) : c.ιSigmaBoundary ≫ l i d = ∂Δ[d].ι ≫ c.ιSigmaStdSimplex := by
   simp
 
-/-
+#adaptation_note
+/--
 Now that `Cofan.mk` and `Discrete.functor` are implicit-reducible and
 `backward.isDefEq.implicitBump` is enabled, the simp lemma `colimit.ι_desc_assoc` is applicable.
 Previously, we had to use `by simp [Sigma.ι_desc_assoc]`, now `by simp` suffices.
diff --git a/Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean b/Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean
@@ -540,7 +540,8 @@ variable {X Y : CostructuredArrow S T} (f : X ⟶ Y)
 /-- The morphism that is part of a morphism of costructured arrows. -/
 abbrev Hom.left : X.left ⟶ Y.left := CommaMorphism.left f
 
-/-
+#adaptation_note
+/--
 The combination of `implicitBump` and making `Functor.const` implicit-reducible makes this former
 `simp` lemma redundant, so no `simp` annotation.
 -/
diff --git a/Mathlib/CategoryTheory/Functor/Const.lean b/Mathlib/CategoryTheory/Functor/Const.lean
@@ -39,8 +39,6 @@ def const : C ⥤ J ⥤ C where
       map := fun _ => 𝟙 X }
   map f := { app := fun _ => f }
 
-attribute [defeq, simp] const_obj_obj
-
 namespace const
 
 open Opposite
diff --git a/Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean b/Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean
@@ -918,15 +918,3 @@ end
 end Functor
 
 end CategoryTheory
-
-/-
-TODO: Fixing linter errors was nontrivial.
-For `#lint` to trigger, I had to disable the module-wide
-`set_option backward.defeqAttrib.useBackward true`.
-Even then, lemmas didn't seem to involve defeq abuse.
-However, when I split the `simp` into multiple parts, the `tacticCheckInstances` linter
-started reporting defeq abuse.
-Should it actually check after every single simp lemma application?
-
-Also had to make `NatTrans.id` implicit-reducible.
--/
diff --git a/Mathlib/CategoryTheory/Limits/Cones.lean b/Mathlib/CategoryTheory/Limits/Cones.lean
@@ -162,11 +162,15 @@ attribute [simp] Cone.w Cone.w_assoc -- `Cocone.w` and `Cocone.w_assoc` are redu
 set_option backward.isDefEq.respectTransparency.types false in
 attribute [elementwise] Cone.w
 
--- TODO: cleanup
-theorem Cocone.w_apply.{uF, w} {J : Type u₁}
-    [Category.{v₁, u₁} J] {C : Type u₃}
-    [Category.{v₃, u₃} C] {F : J ⥤ C} (c : Cocone F) {j j' : J} (f : j' ⟶ j) {F' : C → C → Type uF}
-    {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F' X Y) (carrier X) (carrier Y)}
+#adaptation_note
+/--
+This lemma can be derived by `simp`, so `[elementwise]` does errors out.
+For symmetry reasons, it seems good to have the dual of `Cone.w_apply`, though,
+so we provide it by hand now.
+-/
+theorem Cocone.w_apply.{uF, w} {F : J ⥤ C} (c : Cocone F) {j j' : J} (f : j' ⟶ j)
+    {F' : C → C → Type uF} {carrier : C → Type w}
+    {instFunLike : (X Y : C) → FunLike (F' X Y) (carrier X) (carrier Y)}
     [inst : ConcreteCategory C F'] (x : carrier (F.obj j')) :
     (ConcreteCategory.hom (c.ι.app j)) ((ConcreteCategory.hom (F.map f)) x) =
       (ConcreteCategory.hom (c.ι.app j')) x := by
diff --git a/Mathlib/CategoryTheory/Limits/Types/Filtered.lean b/Mathlib/CategoryTheory/Limits/Types/Filtered.lean
@@ -83,6 +83,14 @@ noncomputable def isColimitOf (t : Cocone F) (hsurj : ∀ x : t.pt, ∃ i xi, x
 
 variable [IsFilteredOrEmpty J]
 
+#adaptation_note
+/--
+Note that the body of `isColimitOf'` locally enables `respectTransparency true` for a subterm.
+The underlying reason is that there is one corner case where `respectTransparency true` unfolds
+*more*, and we need that here.
+The intended fix is to get rid of the outer `respectTransparency false`. After that, the inner
+`respectTransparency true` is redundant and can be removed, too.
+-/
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 /-- Recognizing filtered colimits of types. The injectivity condition here is
diff --git a/Mathlib/CategoryTheory/Skeletal.lean b/Mathlib/CategoryTheory/Skeletal.lean
@@ -226,6 +226,7 @@ variable (C D)
 preorder with nice definitional properties, but is only really appropriate for thin categories.
 If your original category is not thin, you probably want to be using `Skeleton` instead of this.
 -/
+@[implicit_reducible]
 def ThinSkeleton : Type u₁ :=
   Quotient (isIsomorphicSetoid C)
 
diff --git a/Mathlib/CategoryTheory/Subobject/Basic.lean b/Mathlib/CategoryTheory/Subobject/Basic.lean
@@ -535,13 +535,12 @@ def lowerEquivalence {A : C} {B : D} (e : MonoOver A ≌ MonoOver B) : Subobject
     apply eqToIso
     convert! ThinSkeleton.map_iso_eq e.unitIso
     · exact ThinSkeleton.map_id_eq.symm
-    · -- TODO: `simp; rfl` is a code smell
-      simp [lower, ThinSkeleton.map_comp_eq]; rfl
+    · exact (ThinSkeleton.map_comp_eq _ _).symm
   counitIso := by
     apply eqToIso
     convert! ThinSkeleton.map_iso_eq e.counitIso
     · exact (ThinSkeleton.map_comp_eq _ _).symm
-    · simp [ThinSkeleton.map_id_eq]; rfl
+    · exact ThinSkeleton.map_id_eq.symm
 
 section Limits
 
diff --git a/Mathlib/CategoryTheory/Whiskering.lean b/Mathlib/CategoryTheory/Whiskering.lean
@@ -87,9 +87,6 @@ def whiskeringLeft : (C ⥤ D) ⥤ (D ⥤ E) ⥤ C ⥤ E where
           naturality := fun X Y f => by dsimp; rw [← H.map_comp, ← H.map_comp, ← τ.naturality] }
       naturality := fun X Y f => by ext; dsimp; rw [f.naturality] }
 
--- TODO: Is there something to learn from the necessity to do this? Should it be done automatically?
-attribute [defeq, simp] whiskeringLeft_obj_obj
-
 set_option backward.defeqAttrib.useBackward true in
 /-- Right-composition gives a functor `(D ⥤ E) ⥤ ((C ⥤ D) ⥤ (C ⥤ E))`.
 
diff --git a/Mathlib/Combinatorics/Additive/Corner/Roth.lean b/Mathlib/Combinatorics/Additive/Corner/Roth.lean
@@ -37,8 +37,7 @@ private def triangleIndices (A : Finset (G × G)) : Finset (G × G × G) :=
 
 @[simp]
 private lemma mk_mem_triangleIndices : (a, b, c) ∈ triangleIndices A ↔ (a, b) ∈ A ∧ c = a + b := by
-  simp only [triangleIndices, Prod.ext_iff, mem_map, Prod.exists,
-    eq_comm]
+  simp only [triangleIndices, Prod.ext_iff, mem_map, Prod.exists, eq_comm]
   refine ⟨?_, fun h ↦ ⟨_, _, h.1, rfl, rfl, h.2⟩⟩
   rintro ⟨_, _, h₁, rfl, rfl, h₂⟩
   exact ⟨h₁, h₂⟩
diff --git a/Mathlib/Combinatorics/SimpleGraph/Walk/Operations.lean b/Mathlib/Combinatorics/SimpleGraph/Walk/Operations.lean
@@ -28,8 +28,6 @@ Operations on walks that produce a new walk in the same graph.
 walks
 -/
 
-set_option backward.isDefEq.respectTransparency.types false
-
 @[expose] public section
 
 open Function
@@ -543,6 +541,7 @@ lemma Nil.append {p : G.Walk u v} {q : G.Walk v w} (hp : p.Nil) (hq : q.Nil) :
 lemma nil_reverse {p : G.Walk v w} : p.reverse.Nil ↔ p.Nil := by
   cases p <;> simp
 
+set_option backward.isDefEq.respectTransparency.types false in
 /-- The walk obtained by removing the first `n` darts of a walk. -/
 def drop {u v : V} (p : G.Walk u v) (n : ℕ) : G.Walk (p.getVert n) v :=
   match p, n with
@@ -585,6 +584,7 @@ lemma darts_drop (p : G.Walk u v) (n : ℕ) : (p.drop n).darts = p.darts.drop n
 lemma edges_drop (p : G.Walk u v) (n : ℕ) : (p.drop n).edges = p.edges.drop n := by
   induction p generalizing n <;> cases n <;> simp [*, drop]
 
+set_option backward.isDefEq.respectTransparency.types false in
 /-- The walk obtained by taking the first `n` darts of a walk. -/
 def take {u v : V} (p : G.Walk u v) (n : ℕ) : G.Walk u (p.getVert n) :=
   match p, n with
@@ -726,10 +726,12 @@ lemma dropLast_concat {t u v} (p : G.Walk u v) (h : G.Adj v t) :
   · rw! [concat_cons, dropLast_cons_of_not_nil] <;>
       simp [*, ← length_eq_zero_iff]
 
+set_option backward.isDefEq.respectTransparency.types false in
 lemma cons_tail_eq (p : G.Walk u v) (hp : ¬ p.Nil) :
     cons (p.adj_snd hp) p.tail = p := by
   cases p <;> simp at hp ⊢
 
+set_option backward.isDefEq.respectTransparency.types false in
 @[simp]
 lemma concat_dropLast {p : G.Walk u v} (hp : G.Adj p.penultimate v) : p.dropLast.concat hp = p := by
   induction p with
diff --git a/Mathlib/Condensed/Discrete/Colimit.lean b/Mathlib/Condensed/Discrete/Colimit.lean
@@ -37,6 +37,11 @@ variable {I : Type u} [Category.{u} I] [IsCofiltered I] {F : I ⥤ FintypeCat.{u
 abbrev locallyConstantPresheaf : Profinite.{u}ᵒᵖ ⥤ Type (u + 1) :=
   CompHausLike.LocallyConstant.functorToPresheaves.{u, u + 1}.obj X
 
+#adaptation_note
+/--
+In this declaration and `isColimitLocallyConstantPresheaf`, `coe_comp` interferes with rewriting via
+`Cone.w`, so we needed to manualy exclude it.
+-/
 set_option backward.defeqAttrib.useBackward true in
 /--
 The functor `locallyConstantPresheaf` takes cofiltered limits of finite sets with surjective
diff --git a/Mathlib/Data/Finset/NatAntidiagonal.lean b/Mathlib/Data/Finset/NatAntidiagonal.lean
@@ -125,8 +125,7 @@ theorem antidiagonal.snd_lt {n : ℕ} {kl : ℕ × ℕ} (hlk : kl ∈ antidiagon
                       ∃ a b, a + b = k ∧ a = i ∧ b + (n - k) = j :=
     fun i j ↦ by rw [exists_comm]; exact exists₂_congr (fun a b ↦ by rw [add_comm])
   rw [← map_prodComm_antidiagonal]
-  simp_rw [aux₁, ← map_filter (p := fun a : ℕ × ℕ ↦ a.2 ≤ k), antidiagonal_filter_snd_le_of_le h,
-    map_map]
+  simp_rw [aux₁, ← map_filter, antidiagonal_filter_snd_le_of_le h, map_map]
   ext ⟨i, j⟩
   simpa using aux₂ i j
 
@@ -150,7 +149,7 @@ theorem antidiagonal.snd_lt {n : ℕ} {kl : ℕ × ℕ} (hlk : kl ∈ antidiagon
                       ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j :=
     fun i j ↦ by rw [exists_comm]; exact exists₂_congr (fun a b ↦ by rw [add_comm])
   rw [← map_prodComm_antidiagonal]
-  simp_rw [aux₁, ← map_filter (p := fun a : ℕ × ℕ ↦ k ≤ a.fst), antidiagonal_filter_le_fst_of_le h,
+  simp_rw [aux₁, ← map_filter, antidiagonal_filter_le_fst_of_le h,
     map_map]
   ext ⟨i, j⟩
   simpa using aux₂ i j
diff --git a/Mathlib/Data/Finsupp/Weight.lean b/Mathlib/Data/Finsupp/Weight.lean
@@ -265,7 +265,6 @@ lemma range_single_one :
     obtain ⟨a, rfl⟩ := (Finsupp.sum_eq_one_iff _).mp hp
     use a
 
-set_option backward.isDefEq.respectTransparency false in -- TODO?
 @[simp]
 theorem degree_mapDomain {τ : Type*} (f : σ → τ) [AddCommMonoid M] (x : σ →₀ M) :
     degree (x.mapDomain f) = degree x := by
diff --git a/Mathlib/LinearAlgebra/Matrix/Block.lean b/Mathlib/LinearAlgebra/Matrix/Block.lean
@@ -247,8 +247,7 @@ theorem equiv_block_det (M : Matrix m m R) {p q : m → Prop} [DecidablePred p]
 
 -- Removed `@[simp]` attribute,
 -- as the LHS simplifies already to `M.toSquareBlock id i ⟨i, ⋯⟩ ⟨i, ⋯⟩`
-theorem det_toSquareBlock_id (M : Matrix m m R) (i : m) :
-    (M.toSquareBlock id i).det = M i i :=
+theorem det_toSquareBlock_id (M : Matrix m m R) (i : m) : (M.toSquareBlock id i).det = M i i :=
   letI : Unique { a // id a = i } := ⟨⟨⟨i, rfl⟩⟩, fun j => Subtype.ext j.property⟩
   (det_unique _).trans rfl
 
diff --git a/Mathlib/LinearAlgebra/Span/Basic.lean b/Mathlib/LinearAlgebra/Span/Basic.lean
@@ -173,11 +173,8 @@ variable [Semiring S] [SMul R S] [Module S M] [IsScalarTower R S M] (p : Submodu
 @[simps] def inclusionSpan :
     p →ₗ[R] span S (p : Set M) where
   toFun x := ⟨x, subset_span x.property⟩
-  map_add' x y := by
-    simp
-  map_smul' t x := by
-    -- TODO: same problem
-    simp only [SetLike.val_smul, RingHom.id_apply, SetLike.mk_smul_of_tower_mk (S := Submodule S M)]
+  map_add' x y := by simp
+  map_smul' t x := by simp
 
 lemma injective_inclusionSpan :
     Injective (p.inclusionSpan S) := by
diff --git a/Mathlib/Order/BourbakiWitt.lean b/Mathlib/Order/BourbakiWitt.lean
@@ -251,8 +251,10 @@ lemma ωScottContinuous.sup (hf : ωScottContinuous f) (hg : ωScottContinuous g
   apply ωScottContinuous.sSup
   rintro f (rfl | rfl | _) <;> assumption
 
-/-
-The statement of this lemma involves a very subtle form of abuse of definitional equality.
+#adaptation_note
+/--
+Why `respectTransparency.types false` here?
+The proof of this lemma involves a very subtle form of abuse of definitional equality.
 `monotone_const` is only applicable if `Top.top` (`⊤`) can be unfolded to see that it's constant.
 However, `Top.top` is semireducible.
 This mismatch is problematic because `simp` works at implicit transparency.
diff --git a/Mathlib/RingTheory/MvPowerSeries/Substitution.lean b/Mathlib/RingTheory/MvPowerSeries/Substitution.lean
@@ -472,8 +472,7 @@ theorem le_weightedOrder_subst (ha : HasSubst a) (f : MvPowerSeries σ R) :
   by_cases hfx : f.coeff x = 0
   · simp [hfx]
   rw [coeff_eq_zero_of_lt_weightedOrder w, smul_zero]
-  refine hd.trans_le (((biInf_le ⇑(Finsupp.weight (weightedOrder w ∘ a))
-    (s := fun d => (coeff d) f = 0 → False) hfx).trans ?_).trans (le_weightedOrder_prod ..))
+  refine hd.trans_le (((biInf_le _ hfx).trans ?_).trans (le_weightedOrder_prod ..))
   simp only [Finsupp.weight_apply, Finsupp.sum, Function.comp_apply]
   exact Finset.sum_le_sum fun i hi ↦ .trans (by simp) (le_weightedOrder_pow ..)
 
diff --git a/Mathlib/SetTheory/ZFC/Class.lean b/Mathlib/SetTheory/ZFC/Class.lean
@@ -283,7 +283,7 @@ theorem eq_univ_of_powerset_subset {A : Class} (hA : powerset A ⊆ A) : A = uni
         WellFounded.min_mem ZFSet.mem_wf _ hnA
           (hA fun x hx =>
             Classical.not_not.1 fun hB =>
-              WellFounded.not_lt_min ZFSet.mem_wf Aᶜ hB <| coe_apply.1 hx))
+              WellFounded.not_lt_min ZFSet.mem_wf _ hB <| coe_apply.1 hx))
 
 /-- The definite description operator, which is `{x}` if `{y | A y} = {x}` and `∅` otherwise. -/
 def iota (A : Class) : Class :=
@@ -317,12 +317,12 @@ end Class
 
 namespace ZFSet
 
+set_option backward.isDefEq.respectTransparency.types false in
 @[simp]
 theorem map_fval {f : ZFSet.{u} → ZFSet.{u}} [Definable₁ f] {x y : ZFSet.{u}}
     (h : y ∈ x) : (ZFSet.map f x ′ y : Class.{u}) = f y :=
   Class.iota_val _ _ fun z => by
-    erw [Class.toSet_of_ZFSet]
-    rw [Class.coe_apply, mem_map]
+    rw [Class.toSet_of_ZFSet, Class.coe_apply, mem_map]
     exact
       ⟨fun ⟨w, _, pr⟩ => by
         let ⟨wy, fw⟩ := ZFSet.pair_injective pr
diff --git a/Mathlib/Topology/Category/CompHausLike/Basic.lean b/Mathlib/Topology/Category/CompHausLike/Basic.lean
@@ -125,7 +125,8 @@ theorem coe_id (X : CompHausLike P) : (𝟙 X : X → X) = id :=
 
 @[simp]
 theorem coe_comp {X Y Z : CompHausLike P} (f : X ⟶ Y) (g : Y ⟶ Z) :
-    (f ≫ g : X → Z) = (g ∘ f) := rfl
+    (f ≫ g : X → Z) = (g ∘ f) :=
+  rfl
 
 section
 
diff --git a/Mathlib/Topology/Separation/CompletelyRegular.lean b/Mathlib/Topology/Separation/CompletelyRegular.lean
@@ -199,7 +199,7 @@ theorem CompletelyRegularSpace.of_isTopologicalBasis_clopens
     (h : TopologicalSpace.IsTopologicalBasis {s : Set X | IsClopen s}) :
     CompletelyRegularSpace X where
   completely_regular x K hK hx := by
-    obtain ⟨s, hs, hx, hsK⟩ := h.exists_subset_of_mem_open (u := Kᶜ) hx hK.isOpen_compl
+    obtain ⟨s, hs, hx, hsK⟩ := h.exists_subset_of_mem_open hx hK.isOpen_compl
     refine ⟨sᶜ.indicator 1, ?_, by simpa, fun x hx ↦ indicator_of_mem ?_ _⟩
     · exact hs.compl.continuous_indicator continuous_const
     · exact (mem_compl_iff s x).mpr fun hs ↦ hsK hs hx
diff --git a/Mathlib/Topology/Spectral/Prespectral.lean b/Mathlib/Topology/Spectral/Prespectral.lean
@@ -53,9 +53,9 @@ instance (priority := low) [PrespectralSpace X] : LocallyCompactSpace X where
 
 open PrespectralSpace in
 instance (priority := low) [T2Space X] [PrespectralSpace X] : TotallySeparatedSpace X :=
-  totallySeparatedSpace_iff_exists_isClopen.mpr fun _ y hxy ↦
+  totallySeparatedSpace_iff_exists_isClopen.mpr fun _ _ hxy ↦
     have ⟨U, ⟨hU₁, hU₂⟩, hxU, hyU⟩ :=
-      isTopologicalBasis.exists_subset_of_mem_open (u := {y}ᶜ) hxy isClosed_singleton.isOpen_compl
+      isTopologicalBasis.exists_subset_of_mem_open hxy isClosed_singleton.isOpen_compl
     ⟨U, ⟨hU₂.isClosed, hU₁⟩, hxU, fun h ↦ hyU h rfl⟩
 
 lemma PrespectralSpace.of_isOpenCover
diff --git a/Mathlib/Util/AddRelatedDecl.lean b/Mathlib/Util/AddRelatedDecl.lean
@@ -66,11 +66,6 @@ The check is gated by the existing core option `linter.tacticCheckInstances` and
 otherwise; following the convention of the core linter, it does *not* participate in
 `linter.all`. -/
 def warnIfImplicitIllTyped (ref : Syntax) (declName : Name) (declType : Expr) : MetaM Unit := do
-  -- `linter.tacticCheckInstances` is declared outside any `public section` of Lean Core, so we
-  -- cannot reference its option object directly. Construct an `Lean.Option Bool` whose `name`
-  -- matches the key under which `register_builtin_option` registers it: the short identifier
-  -- as written in the macro (see `Lean/Data/Options.lean:228`), not the fully qualified
-  -- declName. The reconstructed option is used both to gate the check and to tag the warning.
   let lintOpt : Lean.Option Bool :=
     { name := `linter.tacticCheckInstances, defValue := false }
   unless lintOpt.get (← getOptions) do return
diff --git a/lake-manifest.json b/lake-manifest.json
diff --git a/lakefile.lean b/lakefile.lean
