bump to nightly-2023-03-27-14

mathlib commit leanprover-community/mathlib@ce86f4e

Mathbin/Algebra/Algebra/Spectrum.lean

@@ -346,7 +346,7 @@ theorem exists_mem_of_not_isUnit_aeval_prod [IsDomain R] {p : R[X]} {a : A} (hp
   by
   rw [← Multiset.prod_toList, AlgHom.map_list_prod] at h
   replace h := mt List.prod_isUnit h
-  simp only [not_forall, exists_prop, aeval_C, Multiset.mem_toList, List.mem_map', aeval_X,
+  simp only [not_forall, exists_prop, aeval_C, Multiset.mem_toList, List.mem_map, aeval_X,
     exists_exists_and_eq_and, Multiset.mem_map, AlgHom.map_sub] at h
   rcases h with ⟨r, r_mem, r_nu⟩
   exact ⟨r, by rwa [mem_iff, ← IsUnit.sub_iff], by rwa [← is_root.def, ← mem_roots hp]⟩

Mathbin/Algebra/TrivSqZeroExt.lean

@@ -877,7 +877,7 @@ theorem snd_pow_of_smul_comm [Monoid R] [AddMonoid M] [DistribMulAction R M]
   simp_rw [Nat.pred_succ]
   refine' (List.sum_eq_card_nsmul _ (x.fst ^ n • x.snd) _).trans _
   · rintro m hm
-    simp_rw [List.mem_map', List.mem_range] at hm
+    simp_rw [List.mem_map, List.mem_range] at hm
     obtain ⟨i, hi, rfl⟩ := hm
     rw [tsub_add_cancel_of_le (nat.lt_succ_iff.mp hi)]
   · rw [List.length_map, List.length_range]

Mathbin/CategoryTheory/Monoidal/Discrete.lean

@@ -30,6 +30,7 @@ variable (M : Type u) [Monoid M]
 
 namespace CategoryTheory
 
+#print CategoryTheory.Discrete.monoidal /-
 @[to_additive Discrete.addMonoidal, simps tensor_obj_as tensor_unit_as]
 instance Discrete.monoidal : MonoidalCategory (Discrete M)
     where
@@ -40,10 +41,12 @@ instance Discrete.monoidal : MonoidalCategory (Discrete M)
   rightUnitor X := Discrete.eqToIso (mul_one X.as)
   associator X Y Z := Discrete.eqToIso (mul_assoc _ _ _)
 #align category_theory.discrete.monoidal CategoryTheory.Discrete.monoidal
-#align discrete.add_monoidal Discrete.addMonoidal
+#align category_theory.discrete.add_monoidal CategoryTheory.Discrete.addMonoidal
+-/
 
 variable {M} {N : Type u} [Monoid N]
 
+#print CategoryTheory.Discrete.monoidalFunctor /-
 /-- A multiplicative morphism between monoids gives a monoidal functor between the corresponding
 discrete monoidal categories.
 -/
@@ -57,11 +60,13 @@ def Discrete.monoidalFunctor (F : M →* N) : MonoidalFunctor (Discrete M) (Disc
   ε := Discrete.eqToHom F.map_one.symm
   μ X Y := Discrete.eqToHom (F.map_mul X.as Y.as).symm
 #align category_theory.discrete.monoidal_functor CategoryTheory.Discrete.monoidalFunctor
-#align discrete.add_monoidal_functor Discrete.addMonoidalFunctor
+#align category_theory.discrete.add_monoidal_functor CategoryTheory.Discrete.addMonoidalFunctor
+-/
 
 variable {K : Type u} [Monoid K]
 
 /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
+#print CategoryTheory.Discrete.monoidalFunctorComp /-
 /-- The monoidal natural isomorphism corresponding to composing two multiplicative morphisms.
 -/
 @[to_additive Discrete.addMonoidalFunctorComp
@@ -72,7 +77,8 @@ def Discrete.monoidalFunctorComp (F : M →* N) (G : N →* K) :
   Hom := { app := fun X => 𝟙 _ }
   inv := { app := fun X => 𝟙 _ }
 #align category_theory.discrete.monoidal_functor_comp CategoryTheory.Discrete.monoidalFunctorComp
-#align discrete.add_monoidal_functor_comp Discrete.addMonoidalFunctorComp
+#align category_theory.discrete.add_monoidal_functor_comp CategoryTheory.Discrete.addMonoidalFunctorComp
+-/
 
 end CategoryTheory
 

Mathbin/CategoryTheory/Monoidal/Linear.lean

@@ -31,6 +31,7 @@ variable (C : Type _) [Category C] [Preadditive C] [Linear R C]
 
 variable [MonoidalCategory C] [MonoidalPreadditive C]
 
+#print CategoryTheory.MonoidalLinear /-
 /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
 /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
 /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
@@ -43,6 +44,7 @@ class MonoidalLinear : Prop where
   smul_tensor' : ∀ {W X Y Z : C} (r : R) (f : W ⟶ X) (g : Y ⟶ Z), r • f ⊗ g = r • (f ⊗ g) := by
     obviously
 #align category_theory.monoidal_linear CategoryTheory.MonoidalLinear
+-/
 
 restate_axiom monoidal_linear.tensor_smul'
 
@@ -52,18 +54,40 @@ attribute [simp] monoidal_linear.tensor_smul monoidal_linear.smul_tensor
 
 variable {C} [MonoidalLinear R C]
 
+#print CategoryTheory.tensorLeft_linear /-
 instance tensorLeft_linear (X : C) : (tensorLeft X).Linear R where
 #align category_theory.tensor_left_linear CategoryTheory.tensorLeft_linear
+-/
 
+#print CategoryTheory.tensorRight_linear /-
 instance tensorRight_linear (X : C) : (tensorRight X).Linear R where
 #align category_theory.tensor_right_linear CategoryTheory.tensorRight_linear
+-/
 
+/- warning: category_theory.tensoring_left_linear -> CategoryTheory.tensoringLeft_linear is a dubious translation:
+lean 3 declaration is
+  forall (R : Type.{u1}) [_inst_1 : Semiring.{u1} R] {C : Type.{u2}} [_inst_2 : CategoryTheory.Category.{u3, u2} C] [_inst_3 : CategoryTheory.Preadditive.{u3, u2} C _inst_2] [_inst_4 : CategoryTheory.Linear.{u1, u3, u2} R _inst_1 C _inst_2 _inst_3] [_inst_5 : CategoryTheory.MonoidalCategory.{u3, u2} C _inst_2] [_inst_6 : CategoryTheory.MonoidalPreadditive.{u2, u3} C _inst_2 _inst_3 _inst_5] [_inst_7 : CategoryTheory.MonoidalLinear.{u1, u2, u3} R _inst_1 C _inst_2 _inst_3 _inst_4 _inst_5 _inst_6] (X : C), CategoryTheory.Functor.Linear.{u1, u2, u2, u3, u3} R _inst_1 C C _inst_2 _inst_2 _inst_3 _inst_3 _inst_4 _inst_4 (CategoryTheory.Functor.obj.{u3, max u2 u3, u2, max u3 u2} C _inst_2 (CategoryTheory.Functor.{u3, u3, u2, u2} C _inst_2 C _inst_2) (CategoryTheory.Functor.category.{u3, u3, u2, u2} C _inst_2 C _inst_2) (CategoryTheory.MonoidalCategory.tensoringLeft.{u3, u2} C _inst_2 _inst_5) X) (CategoryTheory.tensoringLeft_additive.{u2, u3} C _inst_2 _inst_3 _inst_5 _inst_6 X)
+but is expected to have type
+  forall (R : Type.{u1}) [_inst_1 : Semiring.{u1} R] {C : Type.{u2}} [_inst_2 : CategoryTheory.Category.{u3, u2} C] [_inst_3 : CategoryTheory.Preadditive.{u3, u2} C _inst_2] [_inst_4 : CategoryTheory.Linear.{u1, u3, u2} R _inst_1 C _inst_2 _inst_3] [_inst_5 : CategoryTheory.MonoidalCategory.{u3, u2} C _inst_2] [_inst_6 : CategoryTheory.MonoidalPreadditive.{u2, u3} C _inst_2 _inst_3 _inst_5] [_inst_7 : CategoryTheory.MonoidalLinear.{u1, u2, u3} R _inst_1 C _inst_2 _inst_3 _inst_4 _inst_5 _inst_6] (X : C), CategoryTheory.Functor.Linear.{u1, u2, u2, u3, u3} R _inst_1 C C _inst_2 _inst_2 _inst_3 _inst_3 _inst_4 _inst_4 (Prefunctor.obj.{succ u3, max (succ u2) (succ u3), u2, max u2 u3} C (CategoryTheory.CategoryStruct.toQuiver.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_2)) (CategoryTheory.Functor.{u3, u3, u2, u2} C _inst_2 C _inst_2) (CategoryTheory.CategoryStruct.toQuiver.{max u2 u3, max u2 u3} (CategoryTheory.Functor.{u3, u3, u2, u2} C _inst_2 C _inst_2) (CategoryTheory.Category.toCategoryStruct.{max u2 u3, max u2 u3} (CategoryTheory.Functor.{u3, u3, u2, u2} C _inst_2 C _inst_2) (CategoryTheory.Functor.category.{u3, u3, u2, u2} C _inst_2 C _inst_2))) (CategoryTheory.Functor.toPrefunctor.{u3, max u2 u3, u2, max u2 u3} C _inst_2 (CategoryTheory.Functor.{u3, u3, u2, u2} C _inst_2 C _inst_2) (CategoryTheory.Functor.category.{u3, u3, u2, u2} C _inst_2 C _inst_2) (CategoryTheory.MonoidalCategory.tensoringLeft.{u3, u2} C _inst_2 _inst_5)) X) (CategoryTheory.tensoringLeft_additive.{u2, u3} C _inst_2 _inst_3 _inst_5 _inst_6 X)
+Case conversion may be inaccurate. Consider using '#align category_theory.tensoring_left_linear CategoryTheory.tensoringLeft_linearₓ'. -/
 instance tensoringLeft_linear (X : C) : ((tensoringLeft C).obj X).Linear R where
 #align category_theory.tensoring_left_linear CategoryTheory.tensoringLeft_linear
 
+/- warning: category_theory.tensoring_right_linear -> CategoryTheory.tensoringRight_linear is a dubious translation:
+lean 3 declaration is
+  forall (R : Type.{u1}) [_inst_1 : Semiring.{u1} R] {C : Type.{u2}} [_inst_2 : CategoryTheory.Category.{u3, u2} C] [_inst_3 : CategoryTheory.Preadditive.{u3, u2} C _inst_2] [_inst_4 : CategoryTheory.Linear.{u1, u3, u2} R _inst_1 C _inst_2 _inst_3] [_inst_5 : CategoryTheory.MonoidalCategory.{u3, u2} C _inst_2] [_inst_6 : CategoryTheory.MonoidalPreadditive.{u2, u3} C _inst_2 _inst_3 _inst_5] [_inst_7 : CategoryTheory.MonoidalLinear.{u1, u2, u3} R _inst_1 C _inst_2 _inst_3 _inst_4 _inst_5 _inst_6] (X : C), CategoryTheory.Functor.Linear.{u1, u2, u2, u3, u3} R _inst_1 C C _inst_2 _inst_2 _inst_3 _inst_3 _inst_4 _inst_4 (CategoryTheory.Functor.obj.{u3, max u2 u3, u2, max u3 u2} C _inst_2 (CategoryTheory.Functor.{u3, u3, u2, u2} C _inst_2 C _inst_2) (CategoryTheory.Functor.category.{u3, u3, u2, u2} C _inst_2 C _inst_2) (CategoryTheory.MonoidalCategory.tensoringRight.{u3, u2} C _inst_2 _inst_5) X) (CategoryTheory.tensoringRight_additive.{u2, u3} C _inst_2 _inst_3 _inst_5 _inst_6 X)
+but is expected to have type
+  forall (R : Type.{u1}) [_inst_1 : Semiring.{u1} R] {C : Type.{u2}} [_inst_2 : CategoryTheory.Category.{u3, u2} C] [_inst_3 : CategoryTheory.Preadditive.{u3, u2} C _inst_2] [_inst_4 : CategoryTheory.Linear.{u1, u3, u2} R _inst_1 C _inst_2 _inst_3] [_inst_5 : CategoryTheory.MonoidalCategory.{u3, u2} C _inst_2] [_inst_6 : CategoryTheory.MonoidalPreadditive.{u2, u3} C _inst_2 _inst_3 _inst_5] [_inst_7 : CategoryTheory.MonoidalLinear.{u1, u2, u3} R _inst_1 C _inst_2 _inst_3 _inst_4 _inst_5 _inst_6] (X : C), CategoryTheory.Functor.Linear.{u1, u2, u2, u3, u3} R _inst_1 C C _inst_2 _inst_2 _inst_3 _inst_3 _inst_4 _inst_4 (Prefunctor.obj.{succ u3, max (succ u2) (succ u3), u2, max u2 u3} C (CategoryTheory.CategoryStruct.toQuiver.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_2)) (CategoryTheory.Functor.{u3, u3, u2, u2} C _inst_2 C _inst_2) (CategoryTheory.CategoryStruct.toQuiver.{max u2 u3, max u2 u3} (CategoryTheory.Functor.{u3, u3, u2, u2} C _inst_2 C _inst_2) (CategoryTheory.Category.toCategoryStruct.{max u2 u3, max u2 u3} (CategoryTheory.Functor.{u3, u3, u2, u2} C _inst_2 C _inst_2) (CategoryTheory.Functor.category.{u3, u3, u2, u2} C _inst_2 C _inst_2))) (CategoryTheory.Functor.toPrefunctor.{u3, max u2 u3, u2, max u2 u3} C _inst_2 (CategoryTheory.Functor.{u3, u3, u2, u2} C _inst_2 C _inst_2) (CategoryTheory.Functor.category.{u3, u3, u2, u2} C _inst_2 C _inst_2) (CategoryTheory.MonoidalCategory.tensoringRight.{u3, u2} C _inst_2 _inst_5)) X) (CategoryTheory.tensoringRight_additive.{u2, u3} C _inst_2 _inst_3 _inst_5 _inst_6 X)
+Case conversion may be inaccurate. Consider using '#align category_theory.tensoring_right_linear CategoryTheory.tensoringRight_linearₓ'. -/
 instance tensoringRight_linear (X : C) : ((tensoringRight C).obj X).Linear R where
 #align category_theory.tensoring_right_linear CategoryTheory.tensoringRight_linear
 
+/- warning: category_theory.monoidal_linear_of_faithful -> CategoryTheory.monoidalLinearOfFaithful is a dubious translation:
+lean 3 declaration is
+  forall (R : Type.{u1}) [_inst_1 : Semiring.{u1} R] {C : Type.{u2}} [_inst_2 : CategoryTheory.Category.{u3, u2} C] [_inst_3 : CategoryTheory.Preadditive.{u3, u2} C _inst_2] [_inst_4 : CategoryTheory.Linear.{u1, u3, u2} R _inst_1 C _inst_2 _inst_3] [_inst_5 : CategoryTheory.MonoidalCategory.{u3, u2} C _inst_2] [_inst_6 : CategoryTheory.MonoidalPreadditive.{u2, u3} C _inst_2 _inst_3 _inst_5] [_inst_7 : CategoryTheory.MonoidalLinear.{u1, u2, u3} R _inst_1 C _inst_2 _inst_3 _inst_4 _inst_5 _inst_6] {D : Type.{u4}} [_inst_8 : CategoryTheory.Category.{u5, u4} D] [_inst_9 : CategoryTheory.Preadditive.{u5, u4} D _inst_8] [_inst_10 : CategoryTheory.Linear.{u1, u5, u4} R _inst_1 D _inst_8 _inst_9] [_inst_11 : CategoryTheory.MonoidalCategory.{u5, u4} D _inst_8] [_inst_12 : CategoryTheory.MonoidalPreadditive.{u4, u5} D _inst_8 _inst_9 _inst_11] (F : CategoryTheory.MonoidalFunctor.{u5, u3, u4, u2} D _inst_8 _inst_11 C _inst_2 _inst_5) [_inst_13 : CategoryTheory.Faithful.{u5, u3, u4, u2} D _inst_8 C _inst_2 (CategoryTheory.LaxMonoidalFunctor.toFunctor.{u5, u3, u4, u2} D _inst_8 _inst_11 C _inst_2 _inst_5 (CategoryTheory.MonoidalFunctor.toLaxMonoidalFunctor.{u5, u3, u4, u2} D _inst_8 _inst_11 C _inst_2 _inst_5 F))] [_inst_14 : CategoryTheory.Functor.Additive.{u4, u2, u5, u3} D C _inst_8 _inst_2 _inst_9 _inst_3 (CategoryTheory.LaxMonoidalFunctor.toFunctor.{u5, u3, u4, u2} D _inst_8 _inst_11 C _inst_2 _inst_5 (CategoryTheory.MonoidalFunctor.toLaxMonoidalFunctor.{u5, u3, u4, u2} D _inst_8 _inst_11 C _inst_2 _inst_5 F))] [_inst_15 : CategoryTheory.Functor.Linear.{u1, u4, u2, u5, u3} R _inst_1 D C _inst_8 _inst_2 _inst_9 _inst_3 _inst_10 _inst_4 (CategoryTheory.LaxMonoidalFunctor.toFunctor.{u5, u3, u4, u2} D _inst_8 _inst_11 C _inst_2 _inst_5 (CategoryTheory.MonoidalFunctor.toLaxMonoidalFunctor.{u5, u3, u4, u2} D _inst_8 _inst_11 C _inst_2 _inst_5 F)) _inst_14], CategoryTheory.MonoidalLinear.{u1, u4, u5} R _inst_1 D _inst_8 _inst_9 _inst_10 _inst_11 _inst_12
+but is expected to have type
+  forall (R : Type.{u3}) [_inst_1 : Semiring.{u3} R] {C : Type.{u1}} [_inst_2 : CategoryTheory.Category.{u2, u1} C] [_inst_3 : CategoryTheory.Preadditive.{u2, u1} C _inst_2] [_inst_4 : CategoryTheory.Linear.{u3, u2, u1} R _inst_1 C _inst_2 _inst_3] [_inst_5 : CategoryTheory.MonoidalCategory.{u2, u1} C _inst_2] [_inst_6 : CategoryTheory.MonoidalPreadditive.{u1, u2} C _inst_2 _inst_3 _inst_5] [_inst_7 : CategoryTheory.MonoidalLinear.{u3, u1, u2} R _inst_1 C _inst_2 _inst_3 _inst_4 _inst_5 _inst_6] {D : Type.{u5}} [_inst_8 : CategoryTheory.Category.{u4, u5} D] [_inst_9 : CategoryTheory.Preadditive.{u4, u5} D _inst_8] [_inst_10 : CategoryTheory.Linear.{u3, u4, u5} R _inst_1 D _inst_8 _inst_9] [_inst_11 : CategoryTheory.MonoidalCategory.{u4, u5} D _inst_8] [_inst_12 : CategoryTheory.MonoidalPreadditive.{u5, u4} D _inst_8 _inst_9 _inst_11] (F : CategoryTheory.MonoidalFunctor.{u4, u2, u5, u1} D _inst_8 _inst_11 C _inst_2 _inst_5) [_inst_13 : CategoryTheory.Faithful.{u4, u2, u5, u1} D _inst_8 C _inst_2 (CategoryTheory.LaxMonoidalFunctor.toFunctor.{u4, u2, u5, u1} D _inst_8 _inst_11 C _inst_2 _inst_5 (CategoryTheory.MonoidalFunctor.toLaxMonoidalFunctor.{u4, u2, u5, u1} D _inst_8 _inst_11 C _inst_2 _inst_5 F))] [_inst_14 : CategoryTheory.Functor.Additive.{u5, u1, u4, u2} D C _inst_8 _inst_2 _inst_9 _inst_3 (CategoryTheory.LaxMonoidalFunctor.toFunctor.{u4, u2, u5, u1} D _inst_8 _inst_11 C _inst_2 _inst_5 (CategoryTheory.MonoidalFunctor.toLaxMonoidalFunctor.{u4, u2, u5, u1} D _inst_8 _inst_11 C _inst_2 _inst_5 F))] [_inst_15 : CategoryTheory.Functor.Linear.{u3, u5, u1, u4, u2} R _inst_1 D C _inst_8 _inst_2 _inst_9 _inst_3 _inst_10 _inst_4 (CategoryTheory.LaxMonoidalFunctor.toFunctor.{u4, u2, u5, u1} D _inst_8 _inst_11 C _inst_2 _inst_5 (CategoryTheory.MonoidalFunctor.toLaxMonoidalFunctor.{u4, u2, u5, u1} D _inst_8 _inst_11 C _inst_2 _inst_5 F)) _inst_14], CategoryTheory.MonoidalLinear.{u3, u5, u4} R _inst_1 D _inst_8 _inst_9 _inst_10 _inst_11 _inst_12
+Case conversion may be inaccurate. Consider using '#align category_theory.monoidal_linear_of_faithful CategoryTheory.monoidalLinearOfFaithfulₓ'. -/
 /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
 /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
 /-- A faithful linear monoidal functor to a linear monoidal category