bump to nightly-2023-03-27-16

mathlib commit leanprover-community/mathlib@ce86f4e

Mathbin/Data/List/Func.lean

@@ -493,9 +493,9 @@ theorem length_sub [Zero α] [Sub α] {xs ys : List α} :
 
 /- warning: list.func.nil_sub -> List.Func.nil_sub is a dubious translation:
 lean 3 declaration is
-  forall {α : Type.{u_1}} [_inst_1 : AddGroup.{u_1} α] (as : List.{u_1} α), Eq.{succ u_1} (List.{u_1} α) (List.Func.sub.{u_1} α (AddZeroClass.toHasZero.{u_1} α (AddMonoid.toAddZeroClass.{u_1} α (SubNegMonoid.toAddMonoid.{u_1} α (AddGroup.toSubNegMonoid.{u_1} α _inst_1)))) (SubNegMonoid.toHasSub.{u_1} α (AddGroup.toSubNegMonoid.{u_1} α _inst_1)) (List.nil.{u_1} α) as) (List.Func.neg.{u_1} α (SubNegMonoid.toHasNeg.{u_1} α (AddGroup.toSubNegMonoid.{u_1} α _inst_1)) as)
+  forall {α : Type.{u1}} [_inst_1 : AddGroup.{u1} α] (as : List.{u1} α), Eq.{succ u1} (List.{u1} α) (List.Func.sub.{u1} α (AddZeroClass.toHasZero.{u1} α (AddMonoid.toAddZeroClass.{u1} α (SubNegMonoid.toAddMonoid.{u1} α (AddGroup.toSubNegMonoid.{u1} α _inst_1)))) (SubNegMonoid.toHasSub.{u1} α (AddGroup.toSubNegMonoid.{u1} α _inst_1)) (List.nil.{u1} α) as) (List.Func.neg.{u1} α (SubNegMonoid.toHasNeg.{u1} α (AddGroup.toSubNegMonoid.{u1} α _inst_1)) as)
 but is expected to have type
-  forall {α : Type} [_inst_1 : AddGroup.{0} α] (as : List.{0} α), Eq.{1} (List.{0} α) (List.Func.sub.{0} α (NegZeroClass.toZero.{0} α (SubNegZeroMonoid.toNegZeroClass.{0} α (SubtractionMonoid.toSubNegZeroMonoid.{0} α (AddGroup.toSubtractionMonoid.{0} α _inst_1)))) (SubNegMonoid.toSub.{0} α (AddGroup.toSubNegMonoid.{0} α _inst_1)) (List.nil.{0} α) as) (List.Func.neg.{0} α (NegZeroClass.toNeg.{0} α (SubNegZeroMonoid.toNegZeroClass.{0} α (SubtractionMonoid.toSubNegZeroMonoid.{0} α (AddGroup.toSubtractionMonoid.{0} α _inst_1)))) as)
+  forall {α : Type.{u1}} [_inst_1 : AddGroup.{u1} α] (as : List.{u1} α), Eq.{succ u1} (List.{u1} α) (List.Func.sub.{u1} α (NegZeroClass.toZero.{u1} α (SubNegZeroMonoid.toNegZeroClass.{u1} α (SubtractionMonoid.toSubNegZeroMonoid.{u1} α (AddGroup.toSubtractionMonoid.{u1} α _inst_1)))) (SubNegMonoid.toSub.{u1} α (AddGroup.toSubNegMonoid.{u1} α _inst_1)) (List.nil.{u1} α) as) (List.Func.neg.{u1} α (NegZeroClass.toNeg.{u1} α (SubNegZeroMonoid.toNegZeroClass.{u1} α (SubtractionMonoid.toSubNegZeroMonoid.{u1} α (AddGroup.toSubtractionMonoid.{u1} α _inst_1)))) as)
 Case conversion may be inaccurate. Consider using '#align list.func.nil_sub List.Func.nil_subₓ'. -/
 @[simp]
 theorem nil_sub {α : Type _} [AddGroup α] (as : List α) : sub [] as = neg as :=
@@ -507,9 +507,9 @@ theorem nil_sub {α : Type _} [AddGroup α] (as : List α) : sub [] as = neg as
 
 /- warning: list.func.sub_nil -> List.Func.sub_nil is a dubious translation:
 lean 3 declaration is
-  forall {α : Type.{u_1}} [_inst_1 : AddGroup.{u_1} α] (as : List.{u_1} α), Eq.{succ u_1} (List.{u_1} α) (List.Func.sub.{u_1} α (AddZeroClass.toHasZero.{u_1} α (AddMonoid.toAddZeroClass.{u_1} α (SubNegMonoid.toAddMonoid.{u_1} α (AddGroup.toSubNegMonoid.{u_1} α _inst_1)))) (SubNegMonoid.toHasSub.{u_1} α (AddGroup.toSubNegMonoid.{u_1} α _inst_1)) as (List.nil.{u_1} α)) as
+  forall {α : Type.{u1}} [_inst_1 : AddGroup.{u1} α] (as : List.{u1} α), Eq.{succ u1} (List.{u1} α) (List.Func.sub.{u1} α (AddZeroClass.toHasZero.{u1} α (AddMonoid.toAddZeroClass.{u1} α (SubNegMonoid.toAddMonoid.{u1} α (AddGroup.toSubNegMonoid.{u1} α _inst_1)))) (SubNegMonoid.toHasSub.{u1} α (AddGroup.toSubNegMonoid.{u1} α _inst_1)) as (List.nil.{u1} α)) as
 but is expected to have type
-  forall {α : Type} [_inst_1 : AddGroup.{0} α] (as : List.{0} α), Eq.{1} (List.{0} α) (List.Func.sub.{0} α (NegZeroClass.toZero.{0} α (SubNegZeroMonoid.toNegZeroClass.{0} α (SubtractionMonoid.toSubNegZeroMonoid.{0} α (AddGroup.toSubtractionMonoid.{0} α _inst_1)))) (SubNegMonoid.toSub.{0} α (AddGroup.toSubNegMonoid.{0} α _inst_1)) as (List.nil.{0} α)) as
+  forall {α : Type.{u1}} [_inst_1 : AddGroup.{u1} α] (as : List.{u1} α), Eq.{succ u1} (List.{u1} α) (List.Func.sub.{u1} α (NegZeroClass.toZero.{u1} α (SubNegZeroMonoid.toNegZeroClass.{u1} α (SubtractionMonoid.toSubNegZeroMonoid.{u1} α (AddGroup.toSubtractionMonoid.{u1} α _inst_1)))) (SubNegMonoid.toSub.{u1} α (AddGroup.toSubNegMonoid.{u1} α _inst_1)) as (List.nil.{u1} α)) as
 Case conversion may be inaccurate. Consider using '#align list.func.sub_nil List.Func.sub_nilₓ'. -/
 @[simp]
 theorem sub_nil {α : Type _} [AddGroup α] (as : List α) : sub as [] = as :=

Mathbin/FieldTheory/Fixed.lean

@@ -301,7 +301,7 @@ instance normal : Normal (FixedPoints.subfield G F) F :=
       cases nonempty_fintype G
       rw [← minpoly_eq_minpoly, minpoly, coe_algebra_map, ← Subfield.toSubring_subtype_eq_subtype,
         Polynomial.map_toSubring _ (Subfield G F).toSubring, prodXSubSmul]
-      exact Polynomial.splits_prod _ fun _ _ => Polynomial.splits_x_sub_c _⟩
+      exact Polynomial.splits_prod _ fun _ _ => Polynomial.splits_X_sub_C _⟩
 #align fixed_points.normal FixedPoints.normal
 
 instance separable : IsSeparable (FixedPoints.subfield G F) F :=

Mathbin/FieldTheory/Galois.lean

@@ -482,7 +482,7 @@ theorem of_separable_splitting_field [sp : p.IsSplittingField F E] (hp : p.Separ
       IntermediateField.card_algHom_adjoin_integral F
         (show IsIntegral F (0 : E) from isIntegral_zero)
     rw [minpoly.zero, Polynomial.natDegree_X] at key
-    specialize key Polynomial.separable_x (Polynomial.splits_x (algebraMap F E))
+    specialize key Polynomial.separable_x (Polynomial.splits_X (algebraMap F E))
     rw [← @Subalgebra.finrank_bot F E _ _ _, ← IntermediateField.bot_toSubalgebra] at key
     refine' Eq.trans _ key
     apply Fintype.card_congr

Mathbin/FieldTheory/Normal.lean

@@ -70,7 +70,7 @@ variable (F K)
 
 instance normal_self : Normal F F :=
   ⟨fun x => isIntegral_algebraMap.IsAlgebraic F, fun x =>
-    (minpoly.eq_x_sub_C' x).symm ▸ splits_x_sub_c _⟩
+    (minpoly.eq_x_sub_C' x).symm ▸ splits_X_sub_C _⟩
 #align normal_self normal_self
 
 variable {K}

Mathbin/FieldTheory/PolynomialGaloisGroup.lean

@@ -103,19 +103,19 @@ instance uniqueGalOne : Unique (1 : F[X]).Gal :=
 #align polynomial.gal.unique_gal_one Polynomial.Gal.uniqueGalOne
 
 instance uniqueGalC (x : F) : Unique (C x).Gal :=
-  uniqueGalOfSplits _ (splits_c _ _)
+  uniqueGalOfSplits _ (splits_C _ _)
 #align polynomial.gal.unique_gal_C Polynomial.Gal.uniqueGalC
 
 instance uniqueGalX : Unique (X : F[X]).Gal :=
-  uniqueGalOfSplits _ (splits_x _)
+  uniqueGalOfSplits _ (splits_X _)
 #align polynomial.gal.unique_gal_X Polynomial.Gal.uniqueGalX
 
 instance uniqueGalXSubC (x : F) : Unique (X - C x).Gal :=
-  uniqueGalOfSplits _ (splits_x_sub_c _)
+  uniqueGalOfSplits _ (splits_X_sub_C _)
 #align polynomial.gal.unique_gal_X_sub_C Polynomial.Gal.uniqueGalXSubC
 
 instance uniqueGalXPow (n : ℕ) : Unique (X ^ n : F[X]).Gal :=
-  uniqueGalOfSplits _ (splits_x_pow _ _)
+  uniqueGalOfSplits _ (splits_X_pow _ _)
 #align polynomial.gal.unique_gal_X_pow Polynomial.Gal.uniqueGalXPow
 
 instance [h : Fact (p.Splits (algebraMap F E))] : Algebra p.SplittingField E :=

Mathbin/FieldTheory/Separable.lean

@@ -445,7 +445,7 @@ theorem eq_x_sub_c_of_separable_of_root_eq {x : F} {h : F[X]} (h_sep : h.Separab
   have h_ne_zero : h ≠ 0 := by
     rintro rfl
     exact not_separable_zero h_sep
-  apply Polynomial.eq_x_sub_c_of_splits_of_single_root i h_splits
+  apply Polynomial.eq_X_sub_C_of_splits_of_single_root i h_splits
   apply Finset.mk.inj
   · change _ = {i x}
     rw [Finset.eq_singleton_iff_unique_mem]

Mathbin/Logic/Equiv/List.lean

@@ -536,12 +536,7 @@ def listNatEquivNat : List ℕ ≃ ℕ :=
 #align equiv.list_nat_equiv_nat Equiv.listNatEquivNat
 -/
 
-/- warning: equiv.list_equiv_self_of_equiv_nat -> Equiv.listEquivSelfOfEquivNat is a dubious translation:
-lean 3 declaration is
-  forall {α : Type.{u_1}}, (Equiv.{succ u_1, 1} α Nat) -> (Equiv.{succ u_1, succ u_1} (List.{u_1} α) α)
-but is expected to have type
-  forall {α : Type}, (Equiv.{1, 1} α Nat) -> (Equiv.{1, 1} (List.{0} α) α)
-Case conversion may be inaccurate. Consider using '#align equiv.list_equiv_self_of_equiv_nat Equiv.listEquivSelfOfEquivNatₓ'. -/
+#print Equiv.listEquivSelfOfEquivNat /-
 /-- If `α` is equivalent to `ℕ`, then `list α` is equivalent to `α`. -/
 def listEquivSelfOfEquivNat {α : Type _} (e : α ≃ ℕ) : List α ≃ α :=
   calc
@@ -550,6 +545,7 @@ def listEquivSelfOfEquivNat {α : Type _} (e : α ≃ ℕ) : List α ≃ α :=
     _ ≃ α := e.symm
     
 #align equiv.list_equiv_self_of_equiv_nat Equiv.listEquivSelfOfEquivNat
+-/
 
 end Equiv
 

lake-manifest.json

@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "0050744e9092481c9ac2df379c329ca7466d1e35",
+    "rev": "fefede6cd9672e65a0b46e667d8fc5fa52f9c986",
     "name": "lean3port",
-    "inputRev?": "0050744e9092481c9ac2df379c329ca7466d1e35"}},
+    "inputRev?": "fefede6cd9672e65a0b46e667d8fc5fa52f9c986"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "b306241065fee3816854194be3b5dee27bc2d1e3",
+    "rev": "da32edd74856504ceb69ecabbf69a11fb5b1342b",
     "name": "mathlib",
-    "inputRev?": "b306241065fee3816854194be3b5dee27bc2d1e3"}},
+    "inputRev?": "da32edd74856504ceb69ecabbf69a11fb5b1342b"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,

lakefile.lean

@@ -4,7 +4,7 @@ open Lake DSL System
 -- Usually the `tag` will be of the form `nightly-2021-11-22`.
 -- If you would like to use an artifact from a PR build,
 -- it will be of the form `pr-branchname-sha`.
-def tag : String := "nightly-2023-03-27-14"
+def tag : String := "nightly-2023-03-27-16"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg : Package) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"0050744e9092481c9ac2df379c329ca7466d1e35"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"fefede6cd9672e65a0b46e667d8fc5fa52f9c986"
 
 @[default_target]
 lean_lib Mathbin where