[CONFLICT] Sync upstream mathlib4 (2026-05-12)

.github/actions/get-mathlib-ci/action.yml

@@ -10,7 +10,11 @@ inputs:
     # Default pinned commit used by workflows unless they explicitly override.
     # Update this ref as needed to pick up changes to mathlib-ci scripts
     # This is also updated automatically by .github/workflows/update_dependencies.yml
+<<<<<<< HEAD
     default: b6def9edd1c39de8602b8c177c66e9416e5dbc60
+=======
+    default: 455d84939bba1fbe157ff2c1469a0c258372d05c
+>>>>>>> upstream/master
   path:
     description: Checkout destination path.
     required: false

Mathlib.lean

@@ -5635,7 +5635,6 @@ public import Mathlib.NumberTheory.Harmonic.Int
 public import Mathlib.NumberTheory.Harmonic.ZetaAsymp
 public import Mathlib.NumberTheory.Height.Basic
 public import Mathlib.NumberTheory.Height.MvPolynomial
-public import Mathlib.NumberTheory.Height.Northcott
 public import Mathlib.NumberTheory.Height.NumberField
 public import Mathlib.NumberTheory.Height.Projectivization
 public import Mathlib.NumberTheory.JacobiSum.Basic
@@ -6042,6 +6041,7 @@ public import Mathlib.Order.Monotone.Odd
 public import Mathlib.Order.Monotone.Union
 public import Mathlib.Order.Nat
 public import Mathlib.Order.NonemptyFiniteChains
+public import Mathlib.Order.Northcott
 public import Mathlib.Order.Notation
 public import Mathlib.Order.Nucleus
 public import Mathlib.Order.OmegaCompletePartialOrder

Mathlib/Analysis/InnerProductSpace/Adjoint.lean

@@ -171,8 +171,8 @@ theorem _root_.LinearMap.IsSymmetric.clm_adjoint_eq {A : E →L[𝕜] E} (hA : A
     A† = A := by
   rwa [eq_comm, eq_adjoint_iff A A]
 
-theorem adjoint_id : (ContinuousLinearMap.id 𝕜 E)† = ContinuousLinearMap.id 𝕜 E := by
-  simp
+lemma adjoint_id : (.id 𝕜 E)† = .id 𝕜 E := by simp
+lemma adjoint_one : (1 : E →L[𝕜] E)† = 1 := by simp
 
 theorem _root_.Submodule.adjoint_subtypeL (U : Submodule 𝕜 E) [CompleteSpace U] :
     U.subtypeL† = U.orthogonalProjection := by
@@ -256,6 +256,8 @@ theorem star_eq_adjoint (A : E →L[𝕜] E) : star A = A† :=
 theorem isSelfAdjoint_iff' {A : E →L[𝕜] E} : IsSelfAdjoint A ↔ A† = A :=
   Iff.rfl
 
+@[simp] lemma id_mem_unitary : .id 𝕜 E ∈ unitary (E →L[𝕜] E) := one_mem _
+
 theorem norm_adjoint_comp_self (A : E →L[𝕜] F) :
     ‖A† ∘L A‖ = ‖A‖ * ‖A‖ := by
   refine le_antisymm ?_ ?_
@@ -584,8 +586,8 @@ theorem IsSymmetric.adjoint_eq {A : E →ₗ[𝕜] E} (hA : A.IsSymmetric) :
     A.adjoint = A := by
   rwa [eq_comm, eq_adjoint_iff A A]
 
-theorem adjoint_id : (LinearMap.id (R := 𝕜) (M := E)).adjoint = LinearMap.id := by
-  simp
+lemma adjoint_id : (.id : E →ₗ[𝕜] E).adjoint = .id := by simp
+lemma adjoint_one : (1 : E →ₗ[𝕜] E).adjoint = 1 := by simp
 
 /-- 7.6(b) from [axler2024].
 See `ContinuousLinearMap.orthogonal_ker` for the infinite-dimensional version. -/
@@ -692,6 +694,8 @@ theorem isSymmetric_iff_isSelfAdjoint (A : E →ₗ[𝕜] E) : IsSymmetric A ↔
   rw [isSelfAdjoint_iff', IsSymmetric, ← LinearMap.eq_adjoint_iff]
   exact eq_comm
 
+@[simp] lemma id_mem_unitary : .id ∈ unitary (E →ₗ[𝕜] E) := one_mem _
+
 theorem isAdjointPair_inner (A : E →ₗ[𝕜] F) :
     IsAdjointPair (innerₛₗ 𝕜 (E := E)).flip
       (innerₛₗ 𝕜 (E := F)).flip A A.adjoint := by

Mathlib/Analysis/InnerProductSpace/Symmetric.lean

@@ -80,8 +80,8 @@ theorem IsSymmetric.apply_clm {T : E →L[𝕜] E} (hT : IsSymmetric (T : E →
 protected theorem IsSymmetric.zero : (0 : E →ₗ[𝕜] E).IsSymmetric := fun x y =>
   (inner_zero_right x : ⟪x, 0⟫ = 0).symm ▸ (inner_zero_left y : ⟪0, y⟫ = 0)
 
-@[simp]
-protected theorem IsSymmetric.id : (LinearMap.id : E →ₗ[𝕜] E).IsSymmetric := fun _ _ => rfl
+@[simp] protected lemma IsSymmetric.id : (.id : E →ₗ[𝕜] E).IsSymmetric := fun _ _ ↦ rfl
+@[simp] protected lemma IsSymmetric.one : (1 : E →ₗ[𝕜] E).IsSymmetric := fun _ _ ↦ rfl
 
 @[aesop safe apply]
 theorem IsSymmetric.add {T S : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (hS : S.IsSymmetric) :

Mathlib/CategoryTheory/Monoidal/Mod.lean

@@ -147,9 +147,6 @@ alias IsMod_Hom.smul_hom := IsModHom.smul_hom
 
 attribute [to_additive existing (attr := reassoc (attr := simp))] IsModHom.smul_hom
 
-set_option linter.existingAttributeWarning false in
-attribute [to_additive existing] IsModHom.smul_hom_assoc
-
 variable {M N O : D} [ModObj A M] [ModObj A N] [ModObj A O]
 
 @[to_additive]

Mathlib/CategoryTheory/Monoidal/Mon.lean

@@ -103,10 +103,7 @@ variable {M X Y : C} [MonObj M]
 @[inherit_doc] scoped notation "η" => MonObj.one
 @[inherit_doc] scoped notation "η[" M "]" => MonObj.one (X := M)
 
-attribute [reassoc (attr := simp)] one_mul mul_one mul_assoc
-attribute [reassoc (attr := simp)] AddMonObj.zero_add AddMonObj.add_zero AddMonObj.add_assoc
-set_option linter.existingAttributeWarning false in
-attribute [to_additive existing] one_mul_assoc mul_one_assoc mul_assoc_assoc
+attribute [to_additive existing (attr := reassoc (attr := simp))] one_mul mul_one mul_assoc
 
 /-- Transfer `MonObj` along an isomorphism. -/
 -- Note: The simps lemmas are not tagged simp because their `#discr_tree_simp_key` are too generic.

Mathlib/GroupTheory/Descent.lean

@@ -8,7 +8,7 @@ module
 public import Mathlib.Data.Real.Basic
 public import Mathlib.GroupTheory.Finiteness
 public import Mathlib.GroupTheory.Index
-public import Mathlib.NumberTheory.Height.Northcott
+public import Mathlib.Order.Northcott
 
 import Mathlib.Data.Set.Finite.Lemmas
 import Mathlib.Tactic.FieldSimp

Mathlib/GroupTheory/Perm/Fin.lean

@@ -92,12 +92,15 @@ theorem finRotate_succ_eq_decomposeFin {n : ℕ} :
       swap_apply_of_ne_of_ne (Nat.succ_ne_zero _) (Nat.succ_succ_ne_one _)]
 
 @[simp]
-theorem sign_finRotate (n : ℕ) : Perm.sign (finRotate (n + 1)) = (-1) ^ n := by
-  induction n with
+theorem sign_finRotate (n : ℕ) : Perm.sign (finRotate n) = (-1) ^ (n - 1) := by
+  cases n with
   | zero => simp
-  | succ n ih =>
-    rw [finRotate_succ_eq_decomposeFin]
-    simp [ih, pow_succ]
+  | succ n =>
+    induction n with
+    | zero => simp
+    | succ n ih =>
+      rw [finRotate_succ_eq_decomposeFin]
+      simp [ih, pow_succ]
 
 @[simp]
 theorem support_finRotate {n : ℕ} : support (finRotate (n + 2)) = Finset.univ := by

Mathlib/GroupTheory/SpecificGroups/Alternating.lean

@@ -105,7 +105,7 @@ theorem IsThreeCycle.mem_alternatingGroup {f : Perm α} (h : IsThreeCycle f) :
 
 theorem finRotate_bit1_mem_alternatingGroup {n : ℕ} :
     finRotate (2 * n + 1) ∈ alternatingGroup (Fin (2 * n + 1)) := by
-  rw [mem_alternatingGroup, sign_finRotate, pow_mul, pow_two, Int.units_mul_self, one_pow]
+  simp [mem_alternatingGroup]
 
 end Equiv.Perm
 

Mathlib/NumberTheory/ArithmeticFunction/LFunction.lean

@@ -6,7 +6,7 @@ Authors: Thomas Browning
 module
 
 public import Mathlib.NumberTheory.ArithmeticFunction.Defs
-public import Mathlib.NumberTheory.Height.Northcott
+public import Mathlib.Order.Northcott
 public import Mathlib.RingTheory.PowerSeries.Basic
 public import Mathlib.RingTheory.PowerSeries.PiTopology
 public import Mathlib.RingTheory.PowerSeries.Substitution

Mathlib/RingTheory/Ideal/Quotient/HasFiniteQuotients.lean

@@ -6,7 +6,7 @@ Authors: Xavier Roblot
 module
 
 public import Mathlib.Data.ZMod.QuotientRing
-public import Mathlib.NumberTheory.Height.Northcott
+public import Mathlib.Order.Northcott
 public import Mathlib.RingTheory.DedekindDomain.Basic
 public import Mathlib.RingTheory.IntegralDomain
 public import Mathlib.RingTheory.Ideal.Norm.AbsNorm

Mathlib/Tactic/CategoryTheory/Reassoc.lean

@@ -138,14 +138,11 @@ def reassocExpr' (pf : Expr) : TermElabM Expr := do
         Term.registerSyntheticMVarWithCurrRef inst (.typeClass none)
   return e
 
-initialize registerBuiltinAttribute {
-  name := `reassoc
-  descr := ""
-  applicationTime := .afterCompilation
-  add := fun src ref kind => match ref with
+private def reassocImpl (src : Name) (ref : Syntax) (kind : AttributeKind) : AttrM Name :=
+  match ref with
   | `(attr| reassoc $[$toDual:toDualOpt]? $optAttr) => MetaM.run' do
-    if (kind != AttributeKind.global) then
-      throwError "`reassoc` can only be used as a global attribute"
+    unless kind == AttributeKind.global do
+      throwAttrMustBeGlobal `reassoc kind
     let toDual := toDual.isSome || (Translate.findTranslation? (← getEnv) ToDual.data src).isSome
     let tgt := src.appendAfter "_assoc"
     addRelatedDecl src tgt ref optAttr fun value levels => do
@@ -157,7 +154,17 @@ initialize registerBuiltinAttribute {
     if toDual then
       liftCommandElabM <| Command.elabCommand <| ←
         `(command| attribute [to_dual none] $(mkIdent tgt))
-  | _ => throwUnsupportedSyntax }
+    return tgt
+  | _ => throwUnsupportedSyntax
+
+initialize
+  registerGeneratingAttr `reassoc ((#[·]) <$> reassocImpl · · ·)
+  registerBuiltinAttribute {
+    name := `reassoc
+    descr := ""
+    applicationTime := .afterCompilation
+    add := (discard <| reassocImpl · · ·)
+    }
 
 /--
 `reassoc_of% t`, where `t` is

Mathlib/Tactic/Translate/Core.lean

@@ -883,17 +883,20 @@ def warnParametricAttr {β : Type} [Inhabited β] (stx : Syntax) (attr : Paramet
 /-- `translateLemmas names argInfo desc t` runs `t` on all elements of `names`
 and adds translations between the generated lemmas (the output of `t`).
 `names` must be non-empty. -/
-def translateLemmas {m : Type → Type} [Monad m] [MonadError m] [MonadLiftT CoreM m]
+def translateLemmas
     (t : TranslateData) (names : Array Name) (reorder : Reorder) (relevantArg : RelevantArg)
-    (desc : String) (ref : Syntax) (runAttr : Name → m (Array Name)) : m Unit := do
+    (desc : String) (ref : Syntax) (runAttr : Name → CoreM (Array Name)) : CoreM Unit := do
   let auxLemmas ← names.mapM runAttr
   let nLemmas := auxLemmas[0]!.size
   for nm in names, lemmas in auxLemmas do
     unless lemmas.size == nLemmas do
       throwError "{names[0]!} and {nm} do not generate the same number of {desc}."
   for srcLemmas in auxLemmas, tgtLemmas in auxLemmas.eraseIdx! 0 do
     for srcLemma in srcLemmas, tgtLemma in tgtLemmas do
-      insertTranslation t srcLemma tgtLemma reorder relevantArg ref
+      -- Only add a translation if one doesn't already exist.
+      -- This happens if `srcLemma` is the `_assoc` lemma from `to_dual (attr := reassoc)`.
+      if (findTranslation? (← getEnv) t srcLemma).isNone then
+        insertTranslation t srcLemma tgtLemma reorder relevantArg ref
 
 /-- Return the provided target name or autogenerate one if one was not provided. -/
 def targetName (t : TranslateData) (cfg : Config) (src : Name) : CoreM Name := do

upstream_sha

@@ -1 +1 @@
-686c76b39dab044f7548552a8cfa9d01633ae3aa
+1b6d4054371387401ef58e4593a47b0317e8862b