Merge remote-tracking branch 'origin/master' into bhargava-factorial

* origin/master: (80 commits)
  chore(CategoryTheory): remove data produced by tactic block (#20565)
  feat: `|∫ a, f a ∂μ| ≤ ∫ a, |f a| ∂μ` (#20540)
  feat: the Boolean subalgebra generated by the lattice generated by a set (#20440)
  feat: misc. lemmas about moments, tilted measures (#20150)
  chore(Algebra/Lie): make IsNilpotent and IsSolvable independent of scalars (#20556)
  feat(Combinatorics/SimpleGraph/Path): add `IsPath.getVert_injOn` (#19373)
  feat(Combinatorics/SimpleGraph): add lemmas about `spanningCoe` (#19377)
  chore: scope 'on' notation to Function (#20562)
  chore: disable docPrime linter (#20559)
  chore: deprecate MulRingNorm._ in favour of AbsoluteValue._ (#20557)
  fix(scripts/bench_summary): input jobID as a Nat, rather than a String (#20539)
  chore: move results about `DivisionMonoid` + `HasDistribNeg` (#20551)
  feat(NumberTheory/NumberField/Embeddings): definition of totally real field (#20542)
  chore(Noetherian/Artinian): generalize to Semiring (#20534)
  chore: protect `Filter.nhds_{iInf,inf}` (#20530)
  chore(AlgebraicTopology): move SplitSimplicialObject.lean (#20511)
  chore: extract 3 new files out of MeasureSpace (#20509)
  feat(RingTheory): Jacobian criterion for smoothness of local algebras (#20326)
  doc(RingTheory/Flat): add reference to Lambek's paper (#20266)
  feat(NumberTheory/AbelSummation): add more results (#19942)
  chore(Multilinear/Basic): generalize the `SMul` instance (#20536)
  feat(FDeriv/Equiv): generalize `HasFDerivAt.of_local_left_inverse` (#20516)
  feat(ContDiff): add `iteratedFDeriv_comp` (#20472)
  feat(LowerUpperTopology): add lemmas (#20465)
  feat(ContDiff): weaken some assumptions (#20368)
  fix(scripts/technical-debt-metric): avoid division by 0 (#20537)
  chore(Algebra/Ring): Clean up in SumsOfSquares and Semireal/Defs (#20528)
  feat(FTaylorSeries): add lemmas about `dist` between 0th and 1st derivs (#20089)
  feat: results on inner regularity of finite measures (#19780)
  chore: to_additive various results on groups, group actions (#20547)
  feat(Probability/Kernel): `Kernel.sectL` and `sectR` (#15466)
  chore(CategoryTheory/Limits/Fubini): relax universes constraints and weaken hypotheses (#20553)
  perf: remove `@[simp]` on `Fintype.card_of{IsEmpty,Subsingleton}` (#20524)
  fix(HashCommandLinter): remove unnecessary, broken workaround for tests (#20529)
  chore(Ideal/Basic): dependent generalization of `Ideal.pi` (#20535)
  feat(RingTheory): being unramified is a local property (#20323)
  chore(BooleanSubalgebra): use `IsSublattice` in `closure_sdiff_sup_induction` (#20439)
  feat(Order/SuccPred/CompleteLinearOrder): `⨆ a < x, succ a = x` (#19970)
  chore(*): replace `no_index (ofNat n)` with `ofNat(n)` everywhere (#20521)
  feat(CategoryTheory/Triangulated/Adjunction): the right adjoint of a triangulated functor is triangulated (#20255)
  chore(Order/SuccPred/LinearLocallyFinite): change data-creating instances to defs (#20235)
  chore: don't import algebra in `Data.Finset.Basic` (#19779)
  feat: initial segment commutes with `Iio` (#20503)
  chore(Measure/Pi): move parts to `MeasurableSpace/` (#20215)
  chore: smile more often (#20436)
  chore(Algebra/Category/MonCat/ForgetCorepresentable, Algebra/Group/Equiv/Basic): move definitions and add symmetric version (#20416)
  feat(GroupTheory/QuotientGroup): group correspondence theorem (#20007)
  doc: change "module homomorphism" to "linear map" (#20481)
  perf: improves the performance of the `Repr (Equiv.Perm α)` instance (1/4) (#20519)
  fix: do not keep only the first line of hints (#19756)
  ...

.github/build.in.yml

@@ -15,7 +15,8 @@ env:
 concurrency:
   # label each workflow run; only the latest with each label will run
   # workflows on master get more expressive labels
-  group: ${{ github.workflow }}-${{ github.ref }}.${{(github.ref == 'refs/heads/master' && github.run_id) || ''}}
+  group: ${{ github.workflow }}-${{ github.ref }}.
+    ${{ ( contains(fromJSON( '["refs/heads/master", "refs/heads/staging"]'), github.ref ) && github.run_id) || ''}}
   # cancel any running workflow with the same label
   cancel-in-progress: true
 

.github/workflows/bors.yml

@@ -25,7 +25,8 @@ env:
 concurrency:
   # label each workflow run; only the latest with each label will run
   # workflows on master get more expressive labels
-  group: ${{ github.workflow }}-${{ github.ref }}.${{(github.ref == 'refs/heads/master' && github.run_id) || ''}}
+  group: ${{ github.workflow }}-${{ github.ref }}.
+    ${{ ( contains(fromJSON( '["refs/heads/master", "refs/heads/staging"]'), github.ref ) && github.run_id) || ''}}
   # cancel any running workflow with the same label
   cancel-in-progress: true
 

.github/workflows/build.yml

@@ -32,7 +32,8 @@ env:
 concurrency:
   # label each workflow run; only the latest with each label will run
   # workflows on master get more expressive labels
-  group: ${{ github.workflow }}-${{ github.ref }}.${{(github.ref == 'refs/heads/master' && github.run_id) || ''}}
+  group: ${{ github.workflow }}-${{ github.ref }}.
+    ${{ ( contains(fromJSON( '["refs/heads/master", "refs/heads/staging"]'), github.ref ) && github.run_id) || ''}}
   # cancel any running workflow with the same label
   cancel-in-progress: true
 

.github/workflows/build_fork.yml

@@ -29,7 +29,8 @@ env:
 concurrency:
   # label each workflow run; only the latest with each label will run
   # workflows on master get more expressive labels
-  group: ${{ github.workflow }}-${{ github.ref }}.${{(github.ref == 'refs/heads/master' && github.run_id) || ''}}
+  group: ${{ github.workflow }}-${{ github.ref }}.
+    ${{ ( contains(fromJSON( '["refs/heads/master", "refs/heads/staging"]'), github.ref ) && github.run_id) || ''}}
   # cancel any running workflow with the same label
   cancel-in-progress: true
 

Archive/Sensitivity.lean

@@ -368,7 +368,7 @@ open Classical in
 subspace of `V (m+1)` spanned by the corresponding basis vectors non-trivially
 intersects the range of `g m`. -/
 theorem exists_eigenvalue (H : Set (Q m.succ)) (hH : Card H ≥ 2 ^ m + 1) :
-    ∃ y ∈ Span (e '' H) ⊓ range (g m), y ≠ (0 : _) := by
+    ∃ y ∈ Span (e '' H) ⊓ range (g m), y ≠ 0 := by
   let W := Span (e '' H)
   let img := range (g m)
   suffices 0 < dim (W ⊓ img) by
@@ -408,7 +408,7 @@ theorem huang_degree_theorem (H : Set (Q m.succ)) (hH : Card H ≥ 2 ^ m + 1) :
     rw [Finsupp.mem_support_iff] at p_in
     rw [Set.mem_toFinset]
     exact (dualBases_e_ε _).mem_of_mem_span y_mem_H p p_in
-  obtain ⟨q, H_max⟩ : ∃ q : Q m.succ, ∀ q' : Q m.succ, |(ε q' : _) y| ≤ |ε q y| :=
+  obtain ⟨q, H_max⟩ : ∃ q : Q m.succ, ∀ q' : Q m.succ, |(ε q' :) y| ≤ |ε q y| :=
     Finite.exists_max _
   have H_q_pos : 0 < |ε q y| := by
     contrapose! y_ne

Counterexamples/Girard.lean

@@ -41,7 +41,7 @@ theorem girard.{u} (pi : (Type u → Type u) → Type u)
   let τ (T : Set (Set U)) : U := lam (G T)
   let σ (S : U) : Set (Set U) := app S U τ
   have στ : ∀ {s S}, s ∈ σ (τ S) ↔ {x | τ (σ x) ∈ s} ∈ S := fun {s S} =>
-    iff_of_eq (congr_arg (fun f : F U => s ∈ f τ) (beta (G S) U) : _)
+    iff_of_eq (congr_arg (fun f : F U => s ∈ f τ) (beta (G S) U) :)
   let ω : Set (Set U) := {p | ∀ x, p ∈ σ x → x ∈ p}
   let δ (S : Set (Set U)) := ∀ p, p ∈ S → τ S ∈ p
   have : δ ω := fun _p d => d (τ ω) <| στ.2 fun x h => d (τ (σ x)) (στ.2 h)

Mathlib.lean

@@ -689,6 +689,7 @@ import Mathlib.Algebra.Order.Group.Instances
 import Mathlib.Algebra.Order.Group.Int
 import Mathlib.Algebra.Order.Group.Lattice
 import Mathlib.Algebra.Order.Group.MinMax
+import Mathlib.Algebra.Order.Group.Multiset
 import Mathlib.Algebra.Order.Group.Nat
 import Mathlib.Algebra.Order.Group.Opposite
 import Mathlib.Algebra.Order.Group.OrderIso
@@ -1081,6 +1082,7 @@ import Mathlib.AlgebraicTopology.SimplicialCategory.SimplicialObject
 import Mathlib.AlgebraicTopology.SimplicialNerve
 import Mathlib.AlgebraicTopology.SimplicialObject.Basic
 import Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal
+import Mathlib.AlgebraicTopology.SimplicialObject.Split
 import Mathlib.AlgebraicTopology.SimplicialSet.Basic
 import Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
 import Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
@@ -1090,7 +1092,6 @@ import Mathlib.AlgebraicTopology.SimplicialSet.Nerve
 import Mathlib.AlgebraicTopology.SimplicialSet.Path
 import Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
 import Mathlib.AlgebraicTopology.SingularSet
-import Mathlib.AlgebraicTopology.SplitSimplicialObject
 import Mathlib.AlgebraicTopology.TopologicalSimplex
 import Mathlib.Analysis.Analytic.Basic
 import Mathlib.Analysis.Analytic.CPolynomial
@@ -2212,6 +2213,7 @@ import Mathlib.CategoryTheory.Subterminal
 import Mathlib.CategoryTheory.Sums.Associator
 import Mathlib.CategoryTheory.Sums.Basic
 import Mathlib.CategoryTheory.Thin
+import Mathlib.CategoryTheory.Triangulated.Adjunction
 import Mathlib.CategoryTheory.Triangulated.Basic
 import Mathlib.CategoryTheory.Triangulated.Functor
 import Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
@@ -2456,6 +2458,7 @@ import Mathlib.Data.DFinsupp.NeLocus
 import Mathlib.Data.DFinsupp.Notation
 import Mathlib.Data.DFinsupp.Order
 import Mathlib.Data.DFinsupp.Sigma
+import Mathlib.Data.DFinsupp.Small
 import Mathlib.Data.DFinsupp.Submonoid
 import Mathlib.Data.DFinsupp.WellFounded
 import Mathlib.Data.DList.Instances
@@ -3761,10 +3764,12 @@ import Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable
 import Mathlib.MeasureTheory.MeasurableSpace.Instances
 import Mathlib.MeasureTheory.MeasurableSpace.Invariants
 import Mathlib.MeasureTheory.MeasurableSpace.NCard
+import Mathlib.MeasureTheory.MeasurableSpace.Pi
 import Mathlib.MeasureTheory.MeasurableSpace.PreorderRestrict
 import Mathlib.MeasureTheory.MeasurableSpace.Prod
 import Mathlib.MeasureTheory.Measure.AEDisjoint
 import Mathlib.MeasureTheory.Measure.AEMeasurable
+import Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
 import Mathlib.MeasureTheory.Measure.AddContent
 import Mathlib.MeasureTheory.Measure.Comap
 import Mathlib.MeasureTheory.Measure.Complex
@@ -3794,6 +3799,7 @@ import Mathlib.MeasureTheory.Measure.Lebesgue.Integral
 import Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
 import Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
 import Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
+import Mathlib.MeasureTheory.Measure.Map
 import Mathlib.MeasureTheory.Measure.MeasureSpace
 import Mathlib.MeasureTheory.Measure.MeasureSpaceDef
 import Mathlib.MeasureTheory.Measure.MutuallySingular
@@ -3802,7 +3808,9 @@ import Mathlib.MeasureTheory.Measure.OpenPos
 import Mathlib.MeasureTheory.Measure.Portmanteau
 import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
 import Mathlib.MeasureTheory.Measure.Prod
+import Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
 import Mathlib.MeasureTheory.Measure.Regular
+import Mathlib.MeasureTheory.Measure.RegularityCompacts
 import Mathlib.MeasureTheory.Measure.Restrict
 import Mathlib.MeasureTheory.Measure.SeparableMeasure
 import Mathlib.MeasureTheory.Measure.Stieltjes
@@ -3893,6 +3901,7 @@ import Mathlib.NumberTheory.EulerProduct.ExpLog
 import Mathlib.NumberTheory.FLT.Basic
 import Mathlib.NumberTheory.FLT.Four
 import Mathlib.NumberTheory.FLT.MasonStothers
+import Mathlib.NumberTheory.FLT.Polynomial
 import Mathlib.NumberTheory.FLT.Three
 import Mathlib.NumberTheory.FactorisationProperties
 import Mathlib.NumberTheory.Fermat
@@ -4387,6 +4396,8 @@ import Mathlib.RingTheory.EisensteinCriterion
 import Mathlib.RingTheory.EssentialFiniteness
 import Mathlib.RingTheory.Etale.Basic
 import Mathlib.RingTheory.Etale.Field
+import Mathlib.RingTheory.Etale.Kaehler
+import Mathlib.RingTheory.Etale.Pi
 import Mathlib.RingTheory.EuclideanDomain
 import Mathlib.RingTheory.Extension
 import Mathlib.RingTheory.Filtration
@@ -4641,6 +4652,7 @@ import Mathlib.RingTheory.RingHom.Integral
 import Mathlib.RingTheory.RingHom.Locally
 import Mathlib.RingTheory.RingHom.StandardSmooth
 import Mathlib.RingTheory.RingHom.Surjective
+import Mathlib.RingTheory.RingHom.Unramified
 import Mathlib.RingTheory.RingHomProperties
 import Mathlib.RingTheory.RingInvo
 import Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed
@@ -4657,6 +4669,7 @@ import Mathlib.RingTheory.SimpleRing.Field
 import Mathlib.RingTheory.SimpleRing.Matrix
 import Mathlib.RingTheory.Smooth.Basic
 import Mathlib.RingTheory.Smooth.Kaehler
+import Mathlib.RingTheory.Smooth.Local
 import Mathlib.RingTheory.Smooth.Pi
 import Mathlib.RingTheory.Smooth.StandardSmooth
 import Mathlib.RingTheory.Support
@@ -4690,6 +4703,7 @@ import Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
 import Mathlib.RingTheory.Unramified.Basic
 import Mathlib.RingTheory.Unramified.Field
 import Mathlib.RingTheory.Unramified.Finite
+import Mathlib.RingTheory.Unramified.Locus
 import Mathlib.RingTheory.Unramified.Pi
 import Mathlib.RingTheory.Valuation.AlgebraInstances
 import Mathlib.RingTheory.Valuation.Basic
@@ -5396,6 +5410,7 @@ import Mathlib.Topology.Order.Hom.Basic
 import Mathlib.Topology.Order.Hom.Esakia
 import Mathlib.Topology.Order.IntermediateValue
 import Mathlib.Topology.Order.IsLUB
+import Mathlib.Topology.Order.IsLocallyClosed
 import Mathlib.Topology.Order.Lattice
 import Mathlib.Topology.Order.LawsonTopology
 import Mathlib.Topology.Order.LeftRight

Mathlib/Algebra/AddConstMap/Basic.lean

@@ -87,7 +87,7 @@ theorem map_add_one [AddMonoidWithOne G] [Add H] [AddConstMapClass F G H 1 b]
 @[scoped simp]
 theorem map_add_ofNat' [AddMonoidWithOne G] [AddMonoid H] [AddConstMapClass F G H 1 b]
     (f : F) (x : G) (n : ℕ) [n.AtLeastTwo] :
-    f (x + no_index (OfNat.ofNat n)) = f x + (OfNat.ofNat n : ℕ) • b :=
+    f (x + ofNat(n)) = f x + (OfNat.ofNat n : ℕ) • b :=
   map_add_nat' f x n
 
 theorem map_add_nat [AddMonoidWithOne G] [AddMonoidWithOne H] [AddConstMapClass F G H 1 1]
@@ -181,7 +181,7 @@ theorem map_sub_nat' [AddGroupWithOne G] [AddGroup H] [AddConstMapClass F G H 1
 @[scoped simp]
 theorem map_sub_ofNat' [AddGroupWithOne G] [AddGroup H] [AddConstMapClass F G H 1 b]
     (f : F) (x : G) (n : ℕ) [n.AtLeastTwo] :
-    f (x - no_index (OfNat.ofNat n)) = f x - OfNat.ofNat n • b :=
+    f (x - ofNat(n)) = f x - OfNat.ofNat n • b :=
   map_sub_nat' f x n
 
 @[scoped simp]

Mathlib/Algebra/Algebra/NonUnitalHom.lean

@@ -474,7 +474,7 @@ lemma coe_restrictScalars' (f : A →ₙₐ[S] B) : (f.restrictScalars R : A →
 
 theorem restrictScalars_injective :
     Function.Injective (restrictScalars R : (A →ₙₐ[S] B) → A →ₙₐ[R] B) :=
-  fun _ _ h ↦ ext (congr_fun h : _)
+  fun _ _ h ↦ ext (congr_fun h :)
 
 end NonUnitalAlgHom
 

Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

@@ -467,7 +467,7 @@ theorem coe_codRestrict (f : F) (S : NonUnitalSubalgebra R B) (hf : ∀ x, f x 
 
 theorem injective_codRestrict (f : F) (S : NonUnitalSubalgebra R B) (hf : ∀ x : A, f x ∈ S) :
     Function.Injective (NonUnitalAlgHom.codRestrict f S hf) ↔ Function.Injective f :=
-  ⟨fun H _x _y hxy => H <| Subtype.eq hxy, fun H _x _y hxy => H (congr_arg Subtype.val hxy : _)⟩
+  ⟨fun H _x _y hxy => H <| Subtype.eq hxy, fun H _x _y hxy => H (congr_arg Subtype.val hxy :)⟩
 
 /-- Restrict the codomain of an `NonUnitalAlgHom` `f` to `f.range`.
 

Mathlib/Algebra/Algebra/Operations.lean

@@ -144,10 +144,6 @@ theorem smul_mono_left (h : I ≤ J) : I • N ≤ J • N :=
 instance : CovariantClass (Submodule R A) (Submodule R M) HSMul.hSMul LE.le :=
   ⟨fun _ _ => smul_mono le_rfl⟩
 
-@[deprecated smul_mono_right (since := "2024-03-31")]
-protected theorem smul_mono_right (h : N ≤ P) : I • N ≤ I • P :=
-  _root_.smul_mono_right I h
-
 variable (I J N P)
 
 @[simp]
@@ -180,10 +176,6 @@ protected theorem smul_assoc {B} [Semiring B] [Module R B] [Module A B] [Module
       (fun j hj n hn ↦ (smul_assoc r j n).symm ▸ smul_mem_smul (smul_mem_smul hr hj) hn)
       fun m₁ m₂ ↦ (smul_add r m₁ m₂) ▸ add_mem)
 
-@[deprecated smul_inf_le (since := "2024-03-31")]
-protected theorem smul_inf_le (M₁ M₂ : Submodule R M) :
-    I • (M₁ ⊓ M₂) ≤ I • M₁ ⊓ I • M₂ := smul_inf_le _ _ _
-
 theorem smul_iSup {ι : Sort*} {I : Submodule R A} {t : ι → Submodule R M} :
     I • (⨆ i, t i)= ⨆ i, I • t i :=
   toAddSubmonoid_injective <| by
@@ -196,11 +188,6 @@ theorem iSup_smul {ι : Sort*} {t : ι → Submodule R A} {N : Submodule R M} :
     (by simp_rw [zero_smul]; apply zero_mem) fun x y ↦ by simp_rw [add_smul]; apply add_mem)
     (iSup_le fun i ↦ Submodule.smul_mono_left <| le_iSup _ i)
 
-@[deprecated smul_iInf_le (since := "2024-03-31")]
-protected theorem smul_iInf_le {ι : Sort*} {I : Submodule R A} {t : ι → Submodule R M} :
-    I • iInf t ≤ ⨅ i, I • t i :=
-  smul_iInf_le
-
 protected theorem one_smul : (1 : Submodule R A) • N = N := by
   refine le_antisymm (smul_le.mpr fun r hr m hm ↦ ?_) fun m hm ↦ ?_
   · obtain ⟨r, rfl⟩ := hr

Mathlib/Algebra/Algebra/RestrictScalars.lean

@@ -124,7 +124,7 @@ instance RestrictScalars.opModule [Module Sᵐᵒᵖ M] : Module Rᵐᵒᵖ (Res
 
 instance RestrictScalars.isCentralScalar [Module S M] [Module Sᵐᵒᵖ M] [IsCentralScalar S M] :
     IsCentralScalar R (RestrictScalars R S M) where
-  op_smul_eq_smul r _x := (op_smul_eq_smul (algebraMap R S r) (_ : M) : _)
+  op_smul_eq_smul r _x := (op_smul_eq_smul (algebraMap R S r) (_ : M) :)
 
 /-- The `R`-algebra homomorphism from the original coefficient algebra `S` to endomorphisms
 of `RestrictScalars R S M`.

Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

@@ -520,7 +520,7 @@ theorem coe_codRestrict (f : A →ₐ[R] B) (S : Subalgebra R B) (hf : ∀ x, f
 
 theorem injective_codRestrict (f : A →ₐ[R] B) (S : Subalgebra R B) (hf : ∀ x, f x ∈ S) :
     Function.Injective (f.codRestrict S hf) ↔ Function.Injective f :=
-  ⟨fun H _x _y hxy => H <| Subtype.eq hxy, fun H _x _y hxy => H (congr_arg Subtype.val hxy : _)⟩
+  ⟨fun H _x _y hxy => H <| Subtype.eq hxy, fun H _x _y hxy => H (congr_arg Subtype.val hxy :)⟩
 
 /-- Restrict the codomain of an `AlgHom` `f` to `f.range`.
 
@@ -819,7 +819,7 @@ noncomputable def botEquivOfInjective (h : Function.Injective (algebraMap R A))
     (⊥ : Subalgebra R A) ≃ₐ[R] R :=
   AlgEquiv.symm <|
     AlgEquiv.ofBijective (Algebra.ofId R _)
-      ⟨fun _x _y hxy => h (congr_arg Subtype.val hxy : _), fun ⟨_y, x, hx⟩ => ⟨x, Subtype.eq hx⟩⟩
+      ⟨fun _x _y hxy => h (congr_arg Subtype.val hxy :), fun ⟨_y, x, hx⟩ => ⟨x, Subtype.eq hx⟩⟩
 
 /-- The bottom subalgebra is isomorphic to the field. -/
 @[simps! symm_apply]
@@ -995,7 +995,7 @@ instance isScalarTower_left [SMul α β] [SMul A α] [SMul A β] [IsScalarTower
 instance isScalarTower_mid {R S T : Type*} [CommSemiring R] [Semiring S] [AddCommMonoid T]
     [Algebra R S] [Module R T] [Module S T] [IsScalarTower R S T] (S' : Subalgebra R S) :
     IsScalarTower R S' T :=
-  ⟨fun _x y _z => (smul_assoc _ (y : S) _ : _)⟩
+  ⟨fun _x y _z => smul_assoc _ (y : S) _⟩
 
 instance [SMul A α] [FaithfulSMul A α] (S : Subalgebra R A) : FaithfulSMul S α :=
   inferInstanceAs (FaithfulSMul S.toSubsemiring α)

Mathlib/Algebra/Algebra/Subalgebra/Tower.lean

@@ -58,7 +58,7 @@ variable [Algebra R A] [IsScalarTower R S A]
 
 instance subalgebra' (S₀ : Subalgebra R S) : IsScalarTower R S₀ A :=
   @IsScalarTower.of_algebraMap_eq R S₀ A _ _ _ _ _ _ fun _ ↦
-    (IsScalarTower.algebraMap_apply R S A _ : _)
+    (IsScalarTower.algebraMap_apply R S A _ :)
 
 end Semiring
 

Mathlib/Algebra/Algebra/Tower.lean

@@ -200,7 +200,7 @@ theorem coe_restrictScalars' (f : A →ₐ[S] B) : (restrictScalars R f : A →
 
 theorem restrictScalars_injective :
     Function.Injective (restrictScalars R : (A →ₐ[S] B) → A →ₐ[R] B) := fun _ _ h =>
-  AlgHom.ext (AlgHom.congr_fun h : _)
+  AlgHom.ext (AlgHom.congr_fun h :)
 
 end AlgHom
 
@@ -223,7 +223,7 @@ theorem coe_restrictScalars' (f : A ≃ₐ[S] B) : (restrictScalars R f : A →
 
 theorem restrictScalars_injective :
     Function.Injective (restrictScalars R : (A ≃ₐ[S] B) → A ≃ₐ[R] B) := fun _ _ h =>
-  AlgEquiv.ext (AlgEquiv.congr_fun h : _)
+  AlgEquiv.ext (AlgEquiv.congr_fun h :)
 
 end AlgEquiv
 

Mathlib/Algebra/Associated/Basic.lean

@@ -581,7 +581,6 @@ theorem mk_le_mk_of_dvd {a b : M} : a ∣ b → Associates.mk a ≤ Associates.m
 
 theorem mk_le_mk_iff_dvd {a b : M} : Associates.mk a ≤ Associates.mk b ↔ a ∣ b := mk_dvd_mk
 
-@[deprecated (since := "2024-03-16")] alias mk_le_mk_iff_dvd_iff := mk_le_mk_iff_dvd
 
 @[simp]
 theorem isPrimal_mk {a : M} : IsPrimal (Associates.mk a) ↔ IsPrimal a := by
@@ -591,7 +590,6 @@ theorem isPrimal_mk {a : M} : IsPrimal (Associates.mk a) ↔ IsPrimal a := by
     exact ⟨a₁, a₂ * u, h₁, Units.mul_right_dvd.mpr h₂, mul_assoc _ _ _⟩
   · exact ⟨a₁, a₂, h₁, h₂, congr_arg _ eq⟩
 
-@[deprecated (since := "2024-03-16")] alias isPrimal_iff := isPrimal_mk
 
 @[simp]
 theorem decompositionMonoid_iff : DecompositionMonoid (Associates M) ↔ DecompositionMonoid M := by

Mathlib/Algebra/BigOperators/Group/Multiset.lean

@@ -5,7 +5,8 @@ Authors: Mario Carneiro
 -/
 import Mathlib.Algebra.BigOperators.Group.List
 import Mathlib.Algebra.Group.Prod
-import Mathlib.Data.Multiset.Basic
+import Mathlib.Algebra.Order.Group.Multiset
+import Mathlib.Algebra.Order.Sub.Unbundled.Basic
 
 /-!
 # Sums and products over multisets

Mathlib/Algebra/BigOperators/GroupWithZero/Action.lean

@@ -3,11 +3,11 @@ Copyright (c) 2020 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
+import Mathlib.Algebra.BigOperators.Finprod
 import Mathlib.Algebra.BigOperators.Group.Finset
 import Mathlib.Algebra.GroupWithZero.Action.Defs
+import Mathlib.Algebra.Order.Group.Multiset
 import Mathlib.Data.Finset.Basic
-import Mathlib.Data.Multiset.Basic
-import Mathlib.Algebra.BigOperators.Finprod
 
 /-!
 # Lemmas about group actions on big operators