Merge branch 'nightly-testing' of github.com:leanprover-community/mat…

…hlib4 into nightly-testing

Mathlib.lean

@@ -85,6 +85,7 @@ import Mathlib.Algebra.Category.Grp.Abelian
 import Mathlib.Algebra.Category.Grp.Adjunctions
 import Mathlib.Algebra.Category.Grp.Basic
 import Mathlib.Algebra.Category.Grp.Biproducts
+import Mathlib.Algebra.Category.Grp.ChosenFiniteProducts
 import Mathlib.Algebra.Category.Grp.Colimits
 import Mathlib.Algebra.Category.Grp.EnoughInjectives
 import Mathlib.Algebra.Category.Grp.EpiMono
@@ -1129,6 +1130,7 @@ import Mathlib.AlgebraicTopology.Quasicategory.Basic
 import Mathlib.AlgebraicTopology.Quasicategory.Nerve
 import Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
 import Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
+import Mathlib.AlgebraicTopology.RelativeCellComplex.Basic
 import Mathlib.AlgebraicTopology.SimplexCategory
 import Mathlib.AlgebraicTopology.SimplicialCategory.Basic
 import Mathlib.AlgebraicTopology.SimplicialCategory.SimplicialObject
@@ -2167,6 +2169,7 @@ import Mathlib.CategoryTheory.MorphismProperty.Limits
 import Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
 import Mathlib.CategoryTheory.MorphismProperty.Representable
 import Mathlib.CategoryTheory.MorphismProperty.Retract
+import Mathlib.CategoryTheory.MorphismProperty.RetractArgument
 import Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
 import Mathlib.CategoryTheory.NatIso
 import Mathlib.CategoryTheory.NatTrans
@@ -3852,8 +3855,9 @@ import Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
 import Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
 import Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
 import Mathlib.MeasureTheory.Function.LpSeminorm.Trim
-import Mathlib.MeasureTheory.Function.LpSpace
+import Mathlib.MeasureTheory.Function.LpSpace.Basic
 import Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving
+import Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions
 import Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
 import Mathlib.MeasureTheory.Function.LpSpace.DomAct.Continuous
 import Mathlib.MeasureTheory.Function.SimpleFunc
@@ -4888,6 +4892,7 @@ import Mathlib.RingTheory.Spectrum.Prime.Jacobson
 import Mathlib.RingTheory.Spectrum.Prime.Module
 import Mathlib.RingTheory.Spectrum.Prime.Noetherian
 import Mathlib.RingTheory.Spectrum.Prime.Polynomial
+import Mathlib.RingTheory.Spectrum.Prime.RingHom
 import Mathlib.RingTheory.Spectrum.Prime.TensorProduct
 import Mathlib.RingTheory.Spectrum.Prime.Topology
 import Mathlib.RingTheory.Support

Mathlib/Algebra/Category/AlgebraCat/Limits.lean

@@ -100,9 +100,6 @@ def limitCone : Cone F where
 def limitConeIsLimit : IsLimit (limitCone.{v, w} F) := by
   refine
     IsLimit.ofFaithful (forget (AlgebraCat R)) (Types.Small.limitConeIsLimit.{v, w} _)
-      -- Porting note: in mathlib3 the function term
-      -- `fun v => ⟨fun j => ((forget (AlgebraCat R)).mapCone s).π.app j v`
-      -- was provided by unification, and the last argument `(fun s => _)` was `(fun s => rfl)`.
       (fun s => ofHom
         { toFun := _, map_one' := ?_, map_mul' := ?_, map_zero' := ?_, map_add' := ?_,
           commutes' := ?_ })

Mathlib/Algebra/Category/Grp/Biproducts.lean

@@ -34,22 +34,11 @@ instance : HasFiniteBiproducts AddCommGrp :=
 /-- Construct limit data for a binary product in `AddCommGrp`, using
 `AddCommGrp.of (G × H)`.
 -/
-@[simps cone_pt isLimit_lift]
+@[simps! cone_pt isLimit_lift]
 def binaryProductLimitCone (G H : AddCommGrp.{u}) : Limits.LimitCone (pair G H) where
-  cone :=
-    { pt := AddCommGrp.of (G × H)
-      π :=
-        { app := fun j =>
-            Discrete.casesOn j fun j =>
-              WalkingPair.casesOn j (ofHom (AddMonoidHom.fst G H)) (ofHom (AddMonoidHom.snd G H))
-          naturality := by rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩ ⟨⟨⟨⟩⟩⟩ <;> rfl } }
-  isLimit :=
-    { lift := fun s => ofHom <|
-        AddMonoidHom.prod (s.π.app ⟨WalkingPair.left⟩).hom (s.π.app ⟨WalkingPair.right⟩).hom
-      fac := by rintro s (⟨⟩ | ⟨⟩) <;> rfl
-      uniq := fun s m w => by
-        simp_rw [← w ⟨WalkingPair.left⟩, ← w ⟨WalkingPair.right⟩]
-        rfl }
+  cone := BinaryFan.mk (ofHom (AddMonoidHom.fst G H)) (ofHom (AddMonoidHom.snd G H))
+  isLimit := BinaryFan.IsLimit.mk _ (fun l r => ofHom (AddMonoidHom.prod l.hom r.hom))
+    (fun _ _ => rfl) (fun _ _ => rfl) (by aesop_cat)
 
 @[simp]
 theorem binaryProductLimitCone_cone_π_app_left (G H : AddCommGrp.{u}) :

Mathlib/Algebra/Category/Grp/ChosenFiniteProducts.lean

@@ -0,0 +1,122 @@
+/-
+Copyright (c) 2025 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+import Mathlib.Algebra.Category.Grp.Biproducts
+import Mathlib.Algebra.Category.Grp.Zero
+import Mathlib.CategoryTheory.Monoidal.Types.Basic
+
+/-!
+# Chosen finite products in `Grp` and friends
+-/
+
+open CategoryTheory Limits MonoidalCategory
+
+universe u
+
+namespace Grp
+
+/-- Construct limit data for a binary product in `Grp`, using `Grp.of (G × H)` -/
+@[simps! cone_pt isLimit_lift]
+def binaryProductLimitCone (G H : Grp.{u}) : LimitCone (pair G H) where
+  cone := BinaryFan.mk (ofHom (MonoidHom.fst G H)) (ofHom (MonoidHom.snd G H))
+  isLimit := BinaryFan.IsLimit.mk _ (fun l r => ofHom (MonoidHom.prod l.hom r.hom))
+    (fun _ _ => rfl) (fun _ _ => rfl) (by aesop_cat)
+
+/-- We choose `Grp.of (G × H)` as the product of `G` and `H` and `Grp.of PUnit` as
+the terminal object. -/
+noncomputable instance chosenFiniteProductsGrp : ChosenFiniteProducts Grp.{u} where
+  product G H := binaryProductLimitCone G H
+  terminal := ⟨_, (isZero_of_subsingleton (Grp.of PUnit.{u + 1})).isTerminal⟩
+
+attribute [local instance] Functor.monoidalOfChosenFiniteProducts
+
+theorem tensorObj_eq (G H : Grp.{u}) : (G ⊗ H) = of (G × H) := rfl
+
+@[simp]
+theorem μ_forget_apply {G H : Grp.{u}} (p : G) (q : H) :
+    Functor.LaxMonoidal.μ (forget Grp.{u}) G H (p, q) = (p, q) := by
+  apply Prod.ext
+  · exact congrFun (Functor.Monoidal.μ_fst (forget Grp.{u}) G H) (p, q)
+  · exact congrFun (Functor.Monoidal.μ_snd (forget Grp.{u}) G H) (p, q)
+
+end Grp
+
+namespace AddGrp
+
+/-- Construct limit data for a binary product in `AddGrp`, using `AddGrp.of (G × H)` -/
+@[simps! cone_pt isLimit_lift]
+def binaryProductLimitCone (G H : AddGrp.{u}) : LimitCone (pair G H) where
+  cone := BinaryFan.mk (ofHom (AddMonoidHom.fst G H)) (ofHom (AddMonoidHom.snd G H))
+  isLimit := BinaryFan.IsLimit.mk _ (fun l r => ofHom (AddMonoidHom.prod l.hom r.hom))
+    (fun _ _ => rfl) (fun _ _ => rfl) (by aesop_cat)
+
+/-- We choose `AddGrp.of (G × H)` as the product of `G` and `H` and `AddGrp.of PUnit` as
+the terminal object. -/
+noncomputable instance chosenFiniteProductsAddGrp : ChosenFiniteProducts AddGrp.{u} where
+  product G H := binaryProductLimitCone G H
+  terminal := ⟨_, (isZero_of_subsingleton (AddGrp.of PUnit.{u + 1})).isTerminal⟩
+
+attribute [local instance] Functor.monoidalOfChosenFiniteProducts
+
+theorem tensorObj_eq (G H : AddGrp.{u}) : (G ⊗ H) = of (G × H) := rfl
+
+@[simp]
+theorem μ_forget_apply {G H : AddGrp.{u}} (p : G) (q : H) :
+    Functor.LaxMonoidal.μ (forget AddGrp.{u}) G H (p, q) = (p, q) := by
+  apply Prod.ext
+  · exact congrFun (Functor.Monoidal.μ_fst (forget AddGrp.{u}) G H) (p, q)
+  · exact congrFun (Functor.Monoidal.μ_snd (forget AddGrp.{u}) G H) (p, q)
+
+end AddGrp
+
+namespace CommGrp
+
+/-- Construct limit data for a binary product in `CommGrp`, using `CommGrp.of (G × H)` -/
+@[simps! cone_pt isLimit_lift]
+def binaryProductLimitCone (G H : CommGrp.{u}) : LimitCone (pair G H) where
+  cone := BinaryFan.mk (ofHom (MonoidHom.fst G H)) (ofHom (MonoidHom.snd G H))
+  isLimit := BinaryFan.IsLimit.mk _ (fun l r => ofHom (MonoidHom.prod l.hom r.hom))
+    (fun _ _ => rfl) (fun _ _ => rfl) (by aesop_cat)
+
+/-- We choose `CommGrp.of (G × H)` as the product of `G` and `H` and `CommGrp.of PUnit` as
+the terminal object. -/
+noncomputable instance chosenFiniteProductsCommGrp : ChosenFiniteProducts CommGrp.{u} where
+  product G H := binaryProductLimitCone G H
+  terminal := ⟨_, (isZero_of_subsingleton (CommGrp.of PUnit.{u + 1})).isTerminal⟩
+
+attribute [local instance] Functor.monoidalOfChosenFiniteProducts
+
+theorem tensorObj_eq (G H : CommGrp.{u}) : (G ⊗ H) = of (G × H) := rfl
+
+@[simp]
+theorem μ_forget_apply {G H : CommGrp.{u}} (p : G) (q : H) :
+    Functor.LaxMonoidal.μ (forget CommGrp.{u}) G H (p, q) = (p, q) := by
+  apply Prod.ext
+  · exact congrFun (Functor.Monoidal.μ_fst (forget CommGrp.{u}) G H) (p, q)
+  · exact congrFun (Functor.Monoidal.μ_snd (forget CommGrp.{u}) G H) (p, q)
+
+end CommGrp
+
+namespace AddCommGrp
+
+/-- We choose `AddCommGrp.of (G × H)` as the product of `G` and `H` and `AddGrp.of PUnit` as
+the terminal object. -/
+noncomputable def chosenFiniteProductsAddCommGrp : ChosenFiniteProducts AddCommGrp.{u} where
+  product G H := binaryProductLimitCone G H
+  terminal := ⟨_, (isZero_of_subsingleton (AddCommGrp.of PUnit.{u + 1})).isTerminal⟩
+
+attribute [local instance] chosenFiniteProductsAddCommGrp
+attribute [local instance] Functor.monoidalOfChosenFiniteProducts
+
+theorem tensorObj_eq (G H : AddCommGrp.{u}) : (G ⊗ H) = of (G × H) := rfl
+
+@[simp]
+theorem μ_forget_apply {G H : AddCommGrp.{u}} (p : G) (q : H) :
+    Functor.LaxMonoidal.μ (forget AddCommGrp.{u}) G H (p, q) = (p, q) := by
+  apply Prod.ext
+  · exact congrFun (Functor.Monoidal.μ_fst (forget AddCommGrp.{u}) G H) (p, q)
+  · exact congrFun (Functor.Monoidal.μ_snd (forget AddCommGrp.{u}) G H) (p, q)
+
+end AddCommGrp

Mathlib/Algebra/Category/ModuleCat/Basic.lean

@@ -206,20 +206,11 @@ instance : Inhabited (ModuleCat R) :=
 definitional equality issues. -/
 lemma forget_obj {M : ModuleCat.{v} R} : (forget (ModuleCat.{v} R)).obj M = M := rfl
 
-/- Not a `@[simp]` lemma since the LHS is a categorical arrow and the RHS is a plain function. -/
+@[simp]
 lemma forget_map {M N : ModuleCat.{v} R} (f : M ⟶ N) :
     (forget (ModuleCat.{v} R)).map f = f :=
   rfl
 
--- Porting note:
--- One might hope these two instances would not be needed,
--- as we already have `AddCommGroup M` and `Module R M`,
--- but sometimes we seem to need these when rewriting by lemmas about generic concrete categories.
-instance {M : ModuleCat.{v} R} : AddCommGroup ((forget (ModuleCat R)).obj M) :=
-  (inferInstance : AddCommGroup M)
-instance {M : ModuleCat.{v} R} : Module R ((forget (ModuleCat R)).obj M) :=
-  (inferInstance : Module R M)
-
 instance hasForgetToAddCommGroup : HasForget₂ (ModuleCat R) AddCommGrp where
   forget₂ :=
     { obj := fun M => AddCommGrp.of M

Mathlib/Algebra/Category/ModuleCat/Presheaf.lean

@@ -97,7 +97,7 @@ lemma comp_app {M₁ M₂ M₃ : PresheafOfModules R} (f : M₁ ⟶ M₂) (g : M
 
 lemma naturality_apply (f : M₁ ⟶ M₂) {X Y : Cᵒᵖ} (g : X ⟶ Y) (x : M₁.obj X) :
     Hom.app f Y (M₁.map g x) = M₂.map g (Hom.app f X x) :=
-  congr_fun ((forget _).congr_map (Hom.naturality f g)) x
+  CategoryTheory.congr_fun (Hom.naturality f g) x
 
 /-- Constructor for isomorphisms in the category of presheaves of modules. -/
 @[simps!]
@@ -190,7 +190,7 @@ def homMk (φ : M₁.presheaf ⟶ M₂.presheaf)
       map_smul' := hφ X }
   naturality := fun f ↦ by
     ext x
-    exact congr_fun ((forget _).congr_map (φ.naturality f)) x
+    exact CategoryTheory.congr_fun (φ.naturality f) x
 
 instance : Zero (M₁ ⟶ M₂) where
   zero := { app := fun _ ↦ 0 }

Mathlib/Algebra/Category/ModuleCat/Sheaf.lean

@@ -211,13 +211,13 @@ noncomputable def homEquivOfIsLocallyBijective : (M₂ ⟶ N) ≃ (M₁ ⟶ N) w
           ((PresheafOfModules.toPresheaf R).map ψ)
         simp only [← hφ, Equiv.symm_apply_apply]
         replace hφ : ∀ (Z : Cᵒᵖ) (x : M₁.obj Z), φ.app Z (f.app Z x) = ψ.app Z x :=
-          fun Z x ↦ congr_fun ((forget _).congr_map (congr_app hφ Z)) x
+          fun Z x ↦ CategoryTheory.congr_fun (congr_app hφ Z) x
         intro X r y
         apply hN.isSeparated _ _
           (Presheaf.imageSieve_mem J ((toPresheaf R).map f) y)
         rintro Y p ⟨x : M₁.obj _, hx : f.app _ x = M₂.map p.op y⟩
         have hφ' : ∀ (z : M₂.obj X), φ.app _ (M₂.map p.op z) =
-            N.map p.op (φ.app _ z) := congr_fun ((forget _).congr_map (φ.naturality p.op))
+            N.map p.op (φ.app _ z) := CategoryTheory.congr_fun (φ.naturality p.op)
         change N.map p.op (φ.app X (r • y)) = N.map p.op (r • φ.app X y)
         rw [← hφ', M₂.map_smul, ← hx, ← (f.app _).hom.map_smul, hφ, (ψ.app _).hom.map_smul,
           ← hφ, hx, N.map_smul, hφ'])

Mathlib/Algebra/Category/ModuleCat/Sheaf/ChangeOfRings.lean

@@ -55,7 +55,7 @@ noncomputable def restrictHomEquivOfIsLocallySurjective
     apply hM₂.isSeparated _ _ (Presheaf.imageSieve_mem J α r')
     rintro Y p ⟨r : R.obj _, hr⟩
     have hg : ∀ (z : M₁.obj X), g.app _ (M₁.map p.op z) = M₂.map p.op (g.app X z) :=
-      fun z ↦ congr_fun ((forget _).congr_map (g.naturality p.op)) z
+      fun z ↦ CategoryTheory.congr_fun (g.naturality p.op) z
     change M₂.map p.op (g.app X (r' • m)) = M₂.map p.op (r' • show M₂.obj X from g.app X m)
     dsimp at hg ⊢
     rw [← hg, M₂.map_smul, ← hg, ← hr]

Mathlib/Algebra/Category/ModuleCat/Tannaka.lean

@@ -35,8 +35,8 @@ def ringEquivEndForget₂ (R : Type u) [Ring R] :
     intro φ
     apply NatTrans.ext
     ext M (x : M)
-    have w := congr_fun ((forget _).congr_map
-      (φ.naturality (ModuleCat.ofHom (LinearMap.toSpanSingleton R M x)))) (1 : R)
+    have w := CategoryTheory.congr_fun
+      (φ.naturality (ModuleCat.ofHom (LinearMap.toSpanSingleton R M x))) (1 : R)
     exact w.symm.trans (congr_arg (φ.app M) (one_smul R x))
   map_add' := by
     intros

Mathlib/Algebra/Category/MonCat/FilteredColimits.lean

@@ -294,7 +294,7 @@ def colimitCoconeIsColimit : IsColimit (colimitCocone.{v, u} F) where
     (F ⋙ forget MonCat)).fac ((forget MonCat).mapCocone t) j) x
   uniq t m h := MonCat.ext fun y => congr_fun
       ((Types.TypeMax.colimitCoconeIsColimit (F ⋙ forget MonCat)).uniq ((forget MonCat).mapCocone t)
-        ((forget MonCat).map m)
+        ⇑(ConcreteCategory.hom m)
         fun j => funext fun x => ConcreteCategory.congr_hom (h j) x) y
 
 @[to_additive]
@@ -370,7 +370,7 @@ def colimitCoconeIsColimit : IsColimit (colimitCocone.{v, u} F) where
     ConcreteCategory.coe_ext <|
       (Types.TypeMax.colimitCoconeIsColimit.{v, u} (F ⋙ forget CommMonCat.{max v u})).uniq
         ((forget CommMonCat.{max v u}).mapCocone t)
-        ((forget CommMonCat.{max v u}).map m) fun j => funext fun x =>
+        ⇑(ConcreteCategory.hom m) fun j => funext fun x =>
           CategoryTheory.congr_fun (h j) x
 
 @[to_additive forget₂AddMonPreservesFilteredColimits]

Mathlib/Algebra/Homology/ImageToKernel.lean

@@ -57,11 +57,12 @@ theorem imageToKernel_arrow (w : f ≫ g = 0) :
   simp [imageToKernel]
 
 @[simp]
-lemma imageToKernel_arrow_apply [HasForget V] (w : f ≫ g = 0)
-    (x : (forget V).obj (Subobject.underlying.obj (imageSubobject f))) :
+lemma imageToKernel_arrow_apply {FV : V → V → Type*} {CV : V → Type*}
+    [∀ X Y, FunLike (FV X Y) (CV X) (CV Y)] [ConcreteCategory V FV] (w : f ≫ g = 0)
+    (x : ToType (Subobject.underlying.obj (imageSubobject f))) :
     (kernelSubobject g).arrow (imageToKernel f g w x) =
       (imageSubobject f).arrow x := by
-  rw [← CategoryTheory.comp_apply, imageToKernel_arrow]
+  rw [← ConcreteCategory.comp_apply, imageToKernel_arrow]
 
 -- This is less useful as a `simp` lemma than it initially appears,
 -- as it "loses" the information the morphism factors through the image.