[auto-sync] Merge upstream mathlib4 into master (PR #76)

Auto-merged by sync_finalize after CI success.

Author: winstonyin-ax

Mathlib.lean

@@ -2253,6 +2253,7 @@ public import Mathlib.Analysis.Normed.Operator.LinearIsometry
 public import Mathlib.Analysis.Normed.Operator.Mul
 public import Mathlib.Analysis.Normed.Operator.NNNorm
 public import Mathlib.Analysis.Normed.Operator.NormedSpace
+public import Mathlib.Analysis.Normed.Operator.Perturbation.StrictByFinite
 public import Mathlib.Analysis.Normed.Operator.Prod
 public import Mathlib.Analysis.Normed.Order.Basic
 public import Mathlib.Analysis.Normed.Order.Hom.Basic
@@ -3869,6 +3870,7 @@ public import Mathlib.Data.Fin.Basic
 public import Mathlib.Data.Fin.Embedding
 public import Mathlib.Data.Fin.Fin2
 public import Mathlib.Data.Fin.FlagRange
+public import Mathlib.Data.Fin.Init
 public import Mathlib.Data.Fin.Parity
 public import Mathlib.Data.Fin.Pigeonhole
 public import Mathlib.Data.Fin.Rev
@@ -4053,7 +4055,8 @@ public import Mathlib.Data.Int.Sqrt
 public import Mathlib.Data.Int.Star
 public import Mathlib.Data.Int.SuccPred
 public import Mathlib.Data.Int.WithZero
-public import Mathlib.Data.LawfulXor
+public import Mathlib.Data.LawfulXor.Basic
+public import Mathlib.Data.LawfulXor.Equiv
 public import Mathlib.Data.List.AList
 public import Mathlib.Data.List.Basic
 public import Mathlib.Data.List.Chain
@@ -5664,6 +5667,7 @@ public import Mathlib.MeasureTheory.VectorMeasure.SetIntegral
 public import Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
 public import Mathlib.MeasureTheory.VectorMeasure.Variation.Defs
 public import Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation
+public import Mathlib.MeasureTheory.VectorMeasure.Variation.SignedMeasure
 public import Mathlib.MeasureTheory.VectorMeasure.WithDensity
 public import Mathlib.MeasureTheory.VectorMeasure.WithDensityVec
 public import Mathlib.ModelTheory.Algebra.Field.Basic
@@ -6829,6 +6833,7 @@ public import Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
 public import Mathlib.RingTheory.MvPolynomial.Tower
 public import Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
 public import Mathlib.RingTheory.MvPowerSeries.Basic
+public import Mathlib.RingTheory.MvPowerSeries.Derivative
 public import Mathlib.RingTheory.MvPowerSeries.Equiv
 public import Mathlib.RingTheory.MvPowerSeries.Evaluation
 public import Mathlib.RingTheory.MvPowerSeries.Expand

Mathlib/Algebra/DirectSum/Basic.lean

@@ -38,7 +38,6 @@ Note: `open DirectSum` will enable the notation `⨁ i, β i` for `DirectSum ι
 @[implicit_reducible]
 def DirectSum [∀ i, AddCommMonoid (β i)] : Type _ :=
   Π₀ i, β i
-deriving AddCommMonoid, Inhabited, DFunLike
 
 set_option backward.inferInstanceAs.wrap.data false in
 deriving instance CoeFun for DirectSum
@@ -58,14 +57,21 @@ scoped[DirectSum] notation3 "⨁ "(...)", "r:(scoped f => DirectSum _ f) => r
 --   | `(⨁ ($x:ident) ($y:ident), $p) => `(DirectSum _ (fun $x ↦ fun $y ↦ $p))
 -- end
 
+namespace DirectSum
+
+variable {ι β}
+
+-- This instance exists to avoid nsmul and zsmul diamonds.
+instance {R : Type u} [Semiring R] [∀ i, AddCommMonoid (β i)] [∀ i, Module R (β i)] :
+    SMul R (⨁ i, β i) := inferInstanceAs <| SMul R (Π₀ (i : ι), β i)
+
+deriving instance AddCommMonoid, Inhabited, DFunLike for DirectSum
+
 instance [DecidableEq ι] [∀ i, AddCommMonoid (β i)] [∀ i, DecidableEq (β i)] :
     DecidableEq (DirectSum ι β) :=
   inferInstanceAs <| DecidableEq (Π₀ i, β i)
 
-namespace DirectSum
-
-variable {ι}
-
+variable (β) in
 /-- Coercion from a `DirectSum` to a pi type is an `AddMonoidHom`. -/
 def coeFnAddMonoidHom [∀ i, AddCommMonoid (β i)] : (⨁ i, β i) →+ (Π i, β i) where
   toFun x := x
@@ -83,8 +89,6 @@ variable [∀ i, AddCommGroup (β i)]
 instance : AddCommGroup (DirectSum ι β) :=
   inferInstanceAs (AddCommGroup (Π₀ i, β i))
 
-variable {β}
-
 @[simp]
 theorem sub_apply (g₁ g₂ : ⨁ i, β i) (i : ι) : (g₁ - g₂) i = g₁ i - g₂ i :=
   rfl
@@ -100,8 +104,6 @@ variable [∀ i, AddCommMonoid (β i)]
 theorem zero_apply (i : ι) : (0 : ⨁ i, β i) i = 0 :=
   rfl
 
-variable {β}
-
 @[simp]
 theorem add_apply (g₁ g₂ : ⨁ i, β i) (i : ι) : (g₁ + g₂) i = g₁ i + g₂ i :=
   rfl

Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean

@@ -66,13 +66,12 @@ variable (F G)
 of a family of morphisms `F.X p ⟶ G.X q` whenever `p + n = q`, i.e. for all
 triplets in `HomComplex.Triplet n`. -/
 def Cochain := ∀ (T : Triplet n), F.X T.p ⟶ G.X T.q
-deriving AddCommGroup
-
-instance : Module R (Cochain F G n) :=
-  inferInstanceAs <| Module R (∀ _, _)
 
 namespace Cochain
 
+-- The `SMul` instance exists to avoid a zsmul diamond.
+deriving instance SMul R, AddCommGroup, Module R for Cochain F G n
+
 variable {F G n}
 
 /-- A practical constructor for cochains. -/
@@ -579,10 +578,6 @@ def cocycle : AddSubgroup (Cochain F G n) :=
 /-- The type of `n`-cocycles, as a subtype of `Cochain F G n`. -/
 def Cocycle : Type v := cocycle F G n
 
-instance : AddCommGroup (Cocycle F G n) := by
-  dsimp only [Cocycle]
-  infer_instance
-
 namespace Cocycle
 
 variable {F G}
@@ -607,6 +602,9 @@ instance : SMul R (Cocycle F G n) where
 
 variable (F G n)
 
+instance : AddCommGroup (Cocycle F G n) :=
+  inferInstanceAs <| AddCommGroup (cocycle F G n)
+
 @[simp]
 lemma coe_zero : (↑(0 : Cocycle F G n) : Cochain F G n) = 0 := by rfl
 

Mathlib/Algebra/MonoidAlgebra/Defs.lean

@@ -468,9 +468,12 @@ instance one : One R[M] where one := single 1 1
 @[to_additive (dont_translate := R) one_def]
 lemma one_def : (1 : R[M]) = single 1 1 := rfl
 
-@[to_additive (attr := simp) (dont_translate := R)]
+@[to_additive (attr := simp) (dont_translate := R) coeff_one_zero]
 lemma coeff_one_one : (1 : R[M]).coeff 1 = 1 := by simp [one_def]
 
+@[deprecated (since := "2026-07-15")]
+alias _root_.AddMonoidAlgebra.coeff_zero_zero := AddMonoidAlgebra.coeff_one_zero
+
 end One
 
 section Mul

Mathlib/Algebra/Polynomial/Degree/Defs.lean

@@ -20,7 +20,7 @@ public import Mathlib.Order.SuccPred.WithBot
 * `Polynomial.degree`: the degree of a polynomial, where `0` has degree `⊥`
 * `Polynomial.natDegree`: the degree of a polynomial, where `0` has degree `0`
 * `Polynomial.leadingCoeff`: the leading coefficient of a polynomial
-* `Polynomial.Monic`: a polynomial is monic if its leading coefficient is 0
+* `Polynomial.Monic`: a polynomial is monic if its leading coefficient is 1
 * `Polynomial.nextCoeff`: the next coefficient after the leading coefficient
 
 ## Main results

Mathlib/AlgebraicGeometry/Sites/AffineEtale.lean

@@ -5,8 +5,9 @@ Authors: Christian Merten, Joël Riou
 -/
 module
 
-public import Mathlib.Algebra.Category.ModuleCat.AB
-public import Mathlib.Algebra.Category.ModuleCat.FilteredColimits
+-- these `ModuleCat` instances are only used by the `example` below, which `shake` cannot see
+public import Mathlib.Algebra.Category.ModuleCat.AB  -- shake: keep
+public import Mathlib.Algebra.Category.ModuleCat.FilteredColimits  -- shake: keep
 public import Mathlib.AlgebraicGeometry.Sites.Affine
 public import Mathlib.AlgebraicGeometry.Sites.Etale
 public import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf

Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean

@@ -52,14 +52,18 @@ def FormalMultilinearSeries (𝕜 : Type*) (E : Type*) (F : Type*) [Semiring 
   ∀ n : ℕ, E [×n]→L[𝕜] F
 deriving Inhabited
 
+-- This instance exists to avoid an nsmul diamond.
+instance (𝕜') [Semiring 𝕜'] [Module 𝕜' F] [ContinuousConstSMul 𝕜' F] [SMulCommClass 𝕜 𝕜' F] :
+    SMul 𝕜' (FormalMultilinearSeries 𝕜 E F) where
+  smul k x n := k • x n
+
 section AddCommMonoid
 
 /-- Copy `Pi.addCommMonoid`, ensuring the pointwise operations hold by defeq. -/
-instance : AddCommMonoid (FormalMultilinearSeries 𝕜 E F) where
+instance : AddCommMonoid (FormalMultilinearSeries 𝕜 E F) := fast_instance% {
   __ := Pi.addCommMonoid
   zero _ := 0
-  add x y n := x n + y n
-  nsmul k x n := k • x n
+  add x y n := x n + y n }
 
 end AddCommMonoid
 

Mathlib/Analysis/Normed/Lp/lpSpace.lean

@@ -343,10 +343,13 @@ the same ambient group, which permits lemma statements like `lp.monotone` (below
 @[nolint unusedArguments]
 def PreLp (E : α → Type*) [∀ i, NormedAddCommGroup (E i)] : Type _ :=
   ∀ i, E i
-deriving AddCommGroup
 
 namespace PreLp
 
+-- The `SMul` instance exists to avoid a zsmul diamond.
+variable [NormedRing 𝕜] [∀ i, Module 𝕜 (E i)] in
+deriving instance SMul 𝕜, AddCommGroup for PreLp E
+
 @[simp] lemma add_apply {x y : PreLp E} {i : α} : (x + y) i = x i + y i := rfl
 @[simp] lemma zero_apply {i : α} : (0 : PreLp E) i = 0 := rfl
 @[simp] lemma sub_apply {x y : PreLp E} {i : α} : (x - y) i = x i - y i := rfl