merge bump/nightly-2025-12-13

Author: kim-em

Mathlib/Algebra/Polynomial/Factors.lean

@@ -431,23 +431,23 @@ theorem splits_mul_iff (hf₀ : f ≠ 0) (hg₀ : g ≠ 0) :
     have := ih (by aesop) hg₀ (f * g) rfl  (splits_X_sub_C_mul_iff.mp h) hn
     aesop
 
-theorem Splits.splits_of_dvd (hg : Splits g) (hg₀ : g ≠ 0) (hfg : f ∣ g) : Splits f := by
+theorem Splits.of_dvd (hg : Splits g) (hg₀ : g ≠ 0) (hfg : f ∣ g) : Splits f := by
   obtain ⟨g, rfl⟩ := hfg
   exact ((splits_mul_iff (by aesop) (by aesop)).mp hg).1
 
 @[deprecated (since := "2025-11-27")]
-alias Splits.of_dvd := Splits.splits_of_dvd
+alias Splits.splits_of_dvd := Splits.of_dvd
 
 theorem splits_prod_iff {ι : Type*} {f : ι → R[X]} {s : Finset ι} (hf : ∀ i ∈ s, f i ≠ 0) :
     (∏ x ∈ s, f x).Splits ↔ ∀ x ∈ s, (f x).Splits :=
-  ⟨fun h _ hx ↦ h.splits_of_dvd (Finset.prod_ne_zero_iff.mpr hf) (Finset.dvd_prod_of_mem f hx),
+  ⟨fun h _ hx ↦ h.of_dvd (Finset.prod_ne_zero_iff.mpr hf) (Finset.dvd_prod_of_mem f hx),
     Splits.prod⟩
 
 -- Todo: Remove or fix name once `Splits` is gone.
 theorem Splits.splits (hf : Splits f) :
     f = 0 ∨ ∀ {g : R[X]}, Irreducible g → g ∣ f → degree g ≤ 1 :=
   or_iff_not_imp_left.mpr fun hf0 _ hg hgf ↦ degree_le_of_natDegree_le <|
-    (hf.splits_of_dvd hf0 hgf).natDegree_le_one_of_irreducible hg
+    (hf.of_dvd hf0 hgf).natDegree_le_one_of_irreducible hg
 
 lemma map_sub_sprod_roots_eq_prod_map_eval
     (s : Multiset R) (g : R[X]) (hg : g.Monic) (hg' : g.Splits) :

Mathlib/Algebra/Polynomial/Splits.lean

@@ -142,17 +142,17 @@ alias Splits.def := splits_iff_splits
 alias splits_of_splits_mul := splits_mul_iff
 
 @[deprecated (since := "2025-11-25")]
-alias splits_of_splits_of_dvd := Splits.splits_of_dvd
+alias splits_of_splits_of_dvd := Splits.of_dvd
 
-@[deprecated "Use `Splits.splits_of_dvd` directly." (since := "2025-11-30")]
+@[deprecated "Use `Splits.of_dvd` directly." (since := "2025-11-30")]
 theorem splits_of_splits_gcd_left [DecidableEq K] {f g : K[X]} (hf0 : f ≠ 0)
     (hf : Splits f) : Splits (EuclideanDomain.gcd f g) :=
-  Splits.splits_of_dvd hf hf0 <| EuclideanDomain.gcd_dvd_left f g
+  Splits.of_dvd hf hf0 <| EuclideanDomain.gcd_dvd_left f g
 
-@[deprecated "Use `Splits.splits_of_dvd` directly." (since := "2025-11-30")]
+@[deprecated "Use `Splits.of_dvd` directly." (since := "2025-11-30")]
 theorem splits_of_splits_gcd_right [DecidableEq K] {f g : K[X]} (hg0 : g ≠ 0)
     (hg : Splits g) : Splits (EuclideanDomain.gcd f g) :=
-  Splits.splits_of_dvd hg hg0 <| EuclideanDomain.gcd_dvd_right f g
+  Splits.of_dvd hg hg0 <| EuclideanDomain.gcd_dvd_right f g
 
 @[deprecated (since := "2025-11-30")]
 alias degree_eq_one_of_irreducible_of_splits := Splits.degree_eq_one_of_irreducible

Mathlib/Algebra/Ring/Subsemiring/Order.lean

@@ -5,6 +5,7 @@ Authors: Damiano Testa
 -/
 module
 
+public import Mathlib.Algebra.Order.Monoid.Submonoid
 public import Mathlib.Algebra.Order.Ring.InjSurj
 public import Mathlib.Algebra.Ring.Subsemiring.Defs
 public import Mathlib.Order.Interval.Set.Defs
@@ -54,14 +55,16 @@ variable (R) in
 /-- The set of nonnegative elements in an ordered semiring, as a subsemiring. -/
 @[simps]
 def nonneg : Subsemiring R where
-  carrier := Set.Ici 0
+  __ := AddSubmonoid.nonneg R
   mul_mem' := mul_nonneg
   one_mem' := zero_le_one
-  add_mem' := add_nonneg
-  zero_mem' := le_rfl
 
 @[simp] lemma mem_nonneg {x : R} : x ∈ nonneg R ↔ 0 ≤ x := .rfl
 
+variable (R) in
+@[simp]
+theorem nonneg_toAddSubmonoid : (nonneg R).toAddSubmonoid = AddSubmonoid.nonneg R := rfl
+
 end nonneg
 
 end Subsemiring

Mathlib/AlgebraicTopology/SimplicialSet/Dimension.lean

@@ -72,14 +72,14 @@ instance (d : ℕ) [X.HasDimensionLT d] (A : X.Subcomplex) : HasDimensionLT A d
     simp [A.mem_degenerate_iff, X.degenerate_eq_top_of_hasDimensionLT d n hd]
 
 lemma le_iff_of_hasDimensionLT (A B : X.Subcomplex) (d : ℕ) [X.HasDimensionLT d] :
-    A ≤ B ↔ ∀ (i : ℕ) (_ : i < d), A.obj _ ∩ X.nonDegenerate i ⊆ B.obj (op ⦋i⦌) := by
+    A ≤ B ↔ ∀ i < d, A.obj _ ∩ X.nonDegenerate i ⊆ B.obj (op ⦋i⦌) := by
   refine ⟨fun h i hi a ⟨ha, _⟩ ↦ h _ ha, fun h ↦ ?_⟩
   rw [le_iff_contains_nonDegenerate]
   rintro n x hx
   exact h _ (X.dim_lt_of_nonDegenerate x d) ⟨hx, x.prop⟩
 
 lemma eq_top_iff_of_hasDimensionLT (A : X.Subcomplex) (d : ℕ) [X.HasDimensionLT d] :
-    A = ⊤ ↔ ∀ (i : ℕ) (_ : i < d), X.nonDegenerate i ⊆ A.obj _ := by
+    A = ⊤ ↔ ∀ i < d, X.nonDegenerate i ⊆ A.obj _ := by
   simp [← top_le_iff, le_iff_of_hasDimensionLT ⊤ A d]
 
 end Subcomplex

Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean

@@ -548,10 +548,11 @@ def eraseMiddle (c : OrderedFinpartition (n + 1)) (hc : range (c.emb 0) ≠ {0})
     rw [← Nat.add_lt_add_iff_right (k := 1)]
     convert Fin.lt_def.1 (c.parts_strictMono hij)
     · rcases eq_or_ne i (c.index 0) with rfl | hi
+      -- We do not yet replace `omega` with `lia` here, as it is measurably slower.
       · simp only [↓reduceDIte, update_self, succ_mk, cast_mk, val_pred]
         have A := c.one_lt_partSize_index_zero hc
         rw [Nat.sub_add_cancel]
-        · congr; lia
+        · congr; omega
         · rw [Order.one_le_iff_pos]
           conv_lhs => rw [show (0 : ℕ) = c.emb (c.index 0) 0 by simp [emb_zero]]
           rw [← lt_def]
@@ -562,7 +563,7 @@ def eraseMiddle (c : OrderedFinpartition (n + 1)) (hc : range (c.emb 0) ≠ {0})
         have : c.emb i ⟨c.partSize i - 1, Nat.sub_one_lt_of_lt (c.partSize_pos i)⟩
             ≠ c.emb (c.index 0) 0 := c.emb_ne_emb_of_ne hi
         simp only [c.emb_zero, ne_eq, ← val_eq_val, val_zero] at this
-        lia
+        omega
     · rcases eq_or_ne j (c.index 0) with rfl | hj
       · simp only [↓reduceDIte, update_self, succ_mk, cast_mk, val_pred]
         have A := c.one_lt_partSize_index_zero hc

Mathlib/CategoryTheory/Bicategory/InducedBicategory.lean

@@ -22,7 +22,7 @@ of 1-morphisms as well. However, this needs more thought. If one tries the naive
 replacing the map `F` below with a "functor" (between `CategoryStruct`s), one runs into the issue
 that `map_comp` and `map_id` might not be definitional equalities (which they should be in
 practice). Hence one needs to carefully carry these around, or specify `F` in a way that ensures
-they are def-eqs, perhaps constructing it from specified `MorhpismProperty`s.
+they are def-eqs, perhaps constructing it from specified `MorphismProperty`s.
 -/
 
 @[expose] public section

Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Oplax.lean

@@ -73,7 +73,7 @@ structure LaxTrans (F G : OplaxFunctor B C) where
   naturality_naturality {a b : B} {f g : a ⟶ b} (η : f ⟶ g) :
       naturality f ≫ F.map₂ η ▷ app b = app a ◁ G.map₂ η ≫ naturality g := by
     cat_disch
-  naturality_id (a : B):
+  naturality_id (a : B) :
       naturality (𝟙 a) ≫ F.mapId a ▷ app a =
         app a ◁ G.mapId a ≫ (ρ_ (app a)).hom ≫ (λ_ (app a)).inv := by
     cat_disch

Mathlib/CategoryTheory/ComposableArrows/One.lean

@@ -26,8 +26,7 @@ variable (C : Type u) [Category.{v} C]
 which sends `S` to `mk₁ (S.map' i j)` when `i`, `j` and `n`
 are such that `i ≤ j` and `j ≤ n`. -/
 @[simps]
-noncomputable def functorArrows (i j n : ℕ) (hij : i ≤ j := by lia)
-      (hj : j ≤ n := by lia) :
+noncomputable def functorArrows (i j n : ℕ) (hij : i ≤ j := by lia) (hj : j ≤ n := by lia) :
     ComposableArrows C n ⥤ ComposableArrows C 1 where
   obj S := mk₁ (S.map' i j)
   map {S S'} φ := homMk₁ (φ.app _) (φ.app _) (φ.naturality _)

Mathlib/CategoryTheory/Enriched/Ordinary/Basic.lean

@@ -231,8 +231,8 @@ open EnrichedCategory
 then `F` induces the structure of a `W`-enriched ordinary category on `TransportEnrichment F C`,
 i.e. on the same underlying category `C`. -/
 def TransportEnrichment.enrichedOrdinaryCategory
-  (e : ∀ v : V, (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v))
-  (h : ∀ v : V, ∀ f : 𝟙_ V ⟶ v, e v f = Functor.LaxMonoidal.ε F ≫ F.map f) :
+    (e : ∀ v : V, (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v))
+    (h : ∀ v : V, ∀ f : 𝟙_ V ⟶ v, e v f = Functor.LaxMonoidal.ε F ≫ F.map f) :
     EnrichedOrdinaryCategory W (TransportEnrichment F C) where
   homEquiv {X Y} := (eHomEquiv V (C := C)).trans (e (Hom (C := C) X Y))
   homEquiv_id {X} := by simpa using h _ (eId V _)

Mathlib/CategoryTheory/Functor/Flat.lean

@@ -23,7 +23,7 @@ over `X` is cofiltered for each `X`. This concept is also known as flat functors
 Remark C2.3.7, and this name is suggested by Mike Shulman in
 https://golem.ph.utexas.edu/category/2011/06/flat_functors_and_morphisms_of.html to avoid
 confusion with other notions of flatness (e.g. see the notion of flat type-valued
-functor in the file `Functor.TypeValuedFlat`).
+functor in the file `Mathlib/CategoryTheory/Functor/TypeValuedFlat.lean`).
 
 This definition is equivalent to left exact functors (functors that preserves finite limits) when
 `C` has all finite limits.