Merge master into nightly-testing

Author: leanprover-community-mathlib4-bot

Archive/Imo/Imo1998Q2.lean

@@ -176,7 +176,7 @@ theorem judge_pairs_card_lower_bound {z : ℕ} (hJ : Fintype.card J = 2 * z + 1)
   rw [h]; apply Int.le_of_ofNat_le_ofNat; simp only [Int.natCast_add, Int.natCast_mul]
   apply norm_bound_of_odd_sum
   suffices x + y = 2 * z + 1 by simp [← Int.natCast_add, this]
-  rw [Finset.filter_card_add_filter_neg_card_eq_card, ← hJ, Finset.card_univ]
+  rw [Finset.card_filter_add_card_filter_not, ← hJ, Finset.card_univ]
 
 open scoped Classical in
 theorem distinct_judge_pairs_card_lower_bound {z : ℕ} (hJ : Fintype.card J = 2 * z + 1) (c : C) :

Mathlib.lean

@@ -652,7 +652,6 @@ public import Mathlib.Algebra.Lie.Abelian
 public import Mathlib.Algebra.Lie.BaseChange
 public import Mathlib.Algebra.Lie.Basic
 public import Mathlib.Algebra.Lie.CartanExists
-public import Mathlib.Algebra.Lie.CartanMatrix
 public import Mathlib.Algebra.Lie.CartanSubalgebra
 public import Mathlib.Algebra.Lie.Character
 public import Mathlib.Algebra.Lie.Classical
@@ -680,6 +679,7 @@ public import Mathlib.Algebra.Lie.Rank
 public import Mathlib.Algebra.Lie.Semisimple.Basic
 public import Mathlib.Algebra.Lie.Semisimple.Defs
 public import Mathlib.Algebra.Lie.Semisimple.Lemmas
+public import Mathlib.Algebra.Lie.SerreConstruction
 public import Mathlib.Algebra.Lie.SkewAdjoint
 public import Mathlib.Algebra.Lie.Sl2
 public import Mathlib.Algebra.Lie.Solvable
@@ -3670,6 +3670,7 @@ public import Mathlib.Data.Matrix.Basic
 public import Mathlib.Data.Matrix.Basis
 public import Mathlib.Data.Matrix.Bilinear
 public import Mathlib.Data.Matrix.Block
+public import Mathlib.Data.Matrix.Cartan
 public import Mathlib.Data.Matrix.ColumnRowPartitioned
 public import Mathlib.Data.Matrix.Composition
 public import Mathlib.Data.Matrix.DMatrix
@@ -6247,6 +6248,7 @@ public import Mathlib.RingTheory.Smooth.NoetherianDescent
 public import Mathlib.RingTheory.Smooth.Pi
 public import Mathlib.RingTheory.Smooth.StandardSmooth
 public import Mathlib.RingTheory.Smooth.StandardSmoothCotangent
+public import Mathlib.RingTheory.Smooth.StandardSmoothOfFree
 public import Mathlib.RingTheory.Spectrum.Maximal.Basic
 public import Mathlib.RingTheory.Spectrum.Maximal.Defs
 public import Mathlib.RingTheory.Spectrum.Maximal.Localization

Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean

@@ -149,7 +149,7 @@ theorem prod_filter_mul_prod_filter_not
     (s : Finset ι) (p : ι → Prop) [DecidablePred p] [∀ x, Decidable (¬p x)] (f : ι → M) :
     (∏ x ∈ s with p x, f x) * ∏ x ∈ s with ¬p x, f x = ∏ x ∈ s, f x := by
   have := Classical.decEq ι
-  rw [← prod_union (disjoint_filter_filter_neg s s p), filter_union_filter_neg_eq]
+  rw [← prod_union (disjoint_filter_filter_not s s p), filter_union_filter_not_eq]
 
 @[to_additive]
 lemma prod_filter_not_mul_prod_filter (s : Finset ι) (p : ι → Prop) [DecidablePred p]

Mathlib/Algebra/Category/FGModuleCat/Colimits.lean

@@ -57,7 +57,7 @@ def forget₂CreatesColimit (F : J ⥤ FGModuleCat k) :
 instance : CreatesColimitsOfShape J (forget₂ (FGModuleCat k) (ModuleCat.{v} k)) where
   CreatesColimit {F} := forget₂CreatesColimit F
 
-instance (J : Type) [Category J] [FinCategory J] :
+instance (J : Type) [SmallCategory J] [FinCategory J] :
     HasColimitsOfShape J (FGModuleCat.{v} k) :=
   hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape
     (forget₂ (FGModuleCat k) (ModuleCat.{v} k))

Mathlib/Algebra/Category/FGModuleCat/Limits.lean

@@ -65,7 +65,7 @@ def forget₂CreatesLimit (F : J ⥤ FGModuleCat k) :
 instance : CreatesLimitsOfShape J (forget₂ (FGModuleCat k) (ModuleCat.{v} k)) where
   CreatesLimit {F} := forget₂CreatesLimit F
 
-instance (J : Type) [Category J] [FinCategory J] :
+instance (J : Type) [SmallCategory J] [FinCategory J] :
     HasLimitsOfShape J (FGModuleCat.{v} k) :=
   hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape
     (forget₂ (FGModuleCat k) (ModuleCat.{v} k))

Mathlib/Algebra/Category/Grp/AB.lean

@@ -23,7 +23,7 @@ universe u
 
 open CategoryTheory Limits
 
-instance {J C : Type*} [Category J] [Category C] [HasColimitsOfShape J C] [Preadditive C] :
+instance {J C : Type*} [Category* J] [Category* C] [HasColimitsOfShape J C] [Preadditive C] :
     (colim (J := J) (C := C)).Additive where
 
 variable {J : Type u} [SmallCategory J] [IsFiltered J]

Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean

@@ -212,7 +212,7 @@ namespace CategoryTheory
 
 universe v u
 
-/-- `Free R C` is a type synonym for `C`, which, given `[CommRing R]` and `[Category C]`,
+/-- `Free R C` is a type synonym for `C`, which, given `[CommRing R]` and `[Category* C]`,
 we will equip with a category structure where the morphisms are formal `R`-linear combinations
 of the morphisms in `C`.
 -/

Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

@@ -855,15 +855,15 @@ instance {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+*
   (extendRestrictScalarsAdj f).isRightAdjoint
 
 noncomputable instance preservesLimit_restrictScalars
-    {R : Type*} {S : Type*} [Ring R] [Ring S] (f : R →+* S) {J : Type*} [Category J]
+    {R : Type*} {S : Type*} [Ring R] [Ring S] (f : R →+* S) {J : Type*} [Category* J]
     (F : J ⥤ ModuleCat.{v} S) [Small.{v} (F ⋙ forget _).sections] :
     PreservesLimit F (restrictScalars f) :=
   ⟨fun {c} hc => ⟨by
     have hc' := isLimitOfPreserves (forget₂ _ AddCommGrpCat) hc
     exact isLimitOfReflects (forget₂ _ AddCommGrpCat) hc'⟩⟩
 
 instance preservesColimit_restrictScalars {R S : Type*} [Ring R] [Ring S]
-    (f : R →+* S) {J : Type*} [Category J] (F : J ⥤ ModuleCat.{v} S)
+    (f : R →+* S) {J : Type*} [Category* J] (F : J ⥤ ModuleCat.{v} S)
     [HasColimit (F ⋙ forget₂ _ AddCommGrpCat)] :
     PreservesColimit F (ModuleCat.restrictScalars.{v} f) := by
   have : HasColimit ((F ⋙ restrictScalars f) ⋙ forget₂ (ModuleCat R) AddCommGrpCat) :=

Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean

@@ -29,7 +29,7 @@ open CategoryTheory MonoidalCategory Category
 
 universe v u v₁ u₁
 
-variable {C : Type*} [Category C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
+variable {C : Type*} [Category* C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
 
 instance (X : Cᵒᵖ) : CommRing ((R ⋙ forget₂ _ RingCat).obj X) :=
   inferInstanceAs (CommRing (R.obj X))

Mathlib/Algebra/Category/ModuleCat/Topology/Basic.lean

@@ -214,7 +214,7 @@ def toCoinduced (i) : X i ⟶ coinduced f :=
 
 /-- The cocone of topological modules associated to a cocone over the underlying modules, where
 the cocone point is given the coinduced topology. This is colimiting when the given cocone is. -/
-def ofCocone {J : Type*} [Category J] {F : J ⥤ TopModuleCat R}
+def ofCocone {J : Type*} [Category* J] {F : J ⥤ TopModuleCat R}
     (c : Cocone (F ⋙ forget₂ _ (ModuleCat R))) : Cocone F where
   pt := coinduced c.ι.app
   ι :=
@@ -223,7 +223,7 @@ def ofCocone {J : Type*} [Category J] {F : J ⥤ TopModuleCat R}
 
 /-- Given a colimit cocone over the underlying modules, equipping the cocone point with
 the coinduced topology gives a colimit cocone in `TopModuleCat R`. -/
-def isColimit {J : Type*} [Category J] {F : J ⥤ TopModuleCat R}
+def isColimit {J : Type*} [Category* J] {F : J ⥤ TopModuleCat R}
     {c : Cocone (F ⋙ forget₂ _ (ModuleCat R))} (hc : IsColimit c) :
     IsColimit (ofCocone c) where
   desc s := ofHom (X := (ofCocone c).pt) ⟨(hc.desc ((forget₂ _ _).mapCocone s)).hom, by
@@ -242,11 +242,11 @@ def isColimit {J : Type*} [Category J] {F : J ⥤ TopModuleCat R}
     ext y
     exact congr($(H j).hom y)
 
-instance {J : Type*} [Category J] {F : J ⥤ TopModuleCat R}
+instance {J : Type*} [Category* J] {F : J ⥤ TopModuleCat R}
     [HasColimit (F ⋙ forget₂ _ (ModuleCat R))] : HasColimit F :=
   ⟨_, isColimit (colimit.isColimit _)⟩
 
-instance {J : Type*} [Category J] [HasColimitsOfShape J (ModuleCat.{v} R)] :
+instance {J : Type*} [Category* J] [HasColimitsOfShape J (ModuleCat.{v} R)] :
     HasColimitsOfShape J (TopModuleCat.{v} R) where
 
 instance : HasColimits (TopModuleCat.{v} R) where
@@ -275,7 +275,7 @@ open Limits
 
 /-- The cone of topological modules associated to a cone over the underlying modules, where
 the cone point is given the induced topology. This is limiting when the given cone is. -/
-def ofCone {J : Type*} [Category J] {F : J ⥤ TopModuleCat R}
+def ofCone {J : Type*} [Category* J] {F : J ⥤ TopModuleCat R}
     (c : Cone (F ⋙ forget₂ _ (ModuleCat R))) : Cone F where
   pt := induced c.π.app
   π :=
@@ -284,7 +284,7 @@ def ofCone {J : Type*} [Category J] {F : J ⥤ TopModuleCat R}
 
 /-- Given a limit cone over the underlying modules, equipping the cone point with
 the induced topology gives a limit cone in `TopModuleCat R`. -/
-def isLimit {J : Type*} [Category J] {F : J ⥤ TopModuleCat R}
+def isLimit {J : Type*} [Category* J] {F : J ⥤ TopModuleCat R}
     {c : Cone (F ⋙ forget₂ _ (ModuleCat R))} (hc : IsLimit c) :
     IsLimit (ofCone c) where
   lift s := ofHom (Y := (ofCone c).pt) ⟨(hc.lift ((forget₂ _ _).mapCone s)).hom, by
@@ -302,18 +302,18 @@ def isLimit {J : Type*} [Category J] {F : J ⥤ TopModuleCat R}
     ext y
     exact congr($(H j).hom y)
 
-instance hasLimit_of_hasLimit_forget₂ {J : Type*} [Category J] {F : J ⥤ TopModuleCat.{v} R}
+instance hasLimit_of_hasLimit_forget₂ {J : Type*} [Category* J] {F : J ⥤ TopModuleCat.{v} R}
     [HasLimit (F ⋙ forget₂ _ (ModuleCat.{v} R))] : HasLimit F :=
   ⟨_, isLimit (limit.isLimit _)⟩
 
-instance {J : Type*} [Category J] [HasLimitsOfShape J (ModuleCat.{v} R)] :
+instance {J : Type*} [Category* J] [HasLimitsOfShape J (ModuleCat.{v} R)] :
     HasLimitsOfShape J (TopModuleCat.{v} R) where
   has_limit _ := hasLimit_of_hasLimit_forget₂
 
 instance : HasLimits (TopModuleCat.{v} R) where
   has_limits_of_shape _ _ := ⟨fun _ ↦ hasLimit_of_hasLimit_forget₂⟩
 
-instance {J : Type*} [Category J] {F : J ⥤ TopModuleCat.{v} R}
+instance {J : Type*} [Category* J] {F : J ⥤ TopModuleCat.{v} R}
     [HasLimit (F ⋙ forget₂ _ (ModuleCat.{v} R))]
     [PreservesLimit (F ⋙ forget₂ _ (ModuleCat.{v} R)) (forget _)] :
     PreservesLimit F (forget₂ _ TopCat) :=
@@ -322,7 +322,7 @@ instance {J : Type*} [Category J] {F : J ⥤ TopModuleCat.{v} R}
       ((forget _).mapCone (getLimitCone (F ⋙ forget₂ _ (ModuleCat.{v} R))).1:)
       (isLimitOfPreserves (forget (ModuleCat R)) (limit.isLimit _)))
 
-instance {J : Type*} [Category J]
+instance {J : Type*} [Category* J]
     [HasLimitsOfShape J (ModuleCat.{v} R)]
     [PreservesLimitsOfShape J (forget (ModuleCat.{v} R))] :
     PreservesLimitsOfShape J (forget₂ (TopModuleCat.{v} R) TopCat) where