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/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/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/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/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/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..aaa29a83dcfec3 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/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/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/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/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/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/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/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/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/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/globalAttributeIn.lean b/MathlibTest/globalAttributeIn.lean index 37f273b69bc93b..a61961950ef7e2 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,15 +50,11 @@ 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 attribute [simp, local simp, ext, scoped instance, -simp, -ext] foo in diff --git a/lake-manifest.json b/lake-manifest.json index ca0e4c0d66b879..96cf216690b058 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f449eabb8f7e3feef0366856c20e28a6d2c97ee3", + "rev": "86210d4ad1b08b086d0bd638637a75246523dbb8", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -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..bbba35493244d0 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" diff --git a/lean-toolchain b/lean-toolchain index 54caac41bddf21..9187f2ebfc2754 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2026-04-07 +leanprover/lean4:nightly-2026-04-10 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"]]