bump to nightly-2023-03-14-10

mathlib commit leanprover-community/mathlib@2196ab3

Mathbin/Algebra/CharP/ExpChar.lean

@@ -59,7 +59,7 @@ theorem char_eq_expChar_iff (p q : ℕ) [hp : CharP R p] [hq : ExpChar R q] : p
   cases' hq with q hq_one hq_prime
   · apply iff_of_false
     · rintro rfl
-      exact one_ne_zero (hp.eq R (CharP.of_charZero R))
+      exact one_ne_zero (hp.eq R (CharP.ofCharZero R))
     · intro pprime
       rw [(CharP.eq R hp inferInstance : p = 0)] at pprime
       exact Nat.not_prime_zero pprime

Mathbin/Algebra/CharP/LocalRing.lean

@@ -70,7 +70,7 @@ theorem charP_zero_or_prime_power (R : Type _) [CommRing R] [LocalRing R] (q : 
     haveI K_char_zero : CharZero K := CharP.charP_to_charZero K
     haveI R_char_zero := RingHom.charZero (LocalRing.residue R)
     -- Finally, `r = 0` would lead to a contradiction:
-    have q_zero := CharP.eq R char_R_q (CharP.of_charZero R)
+    have q_zero := CharP.eq R char_R_q (CharP.ofCharZero R)
     exact absurd q_zero q_pos
 #align char_p_zero_or_prime_power charP_zero_or_prime_power
 

Mathbin/Algebra/CharP/MixedCharZero.lean

@@ -271,7 +271,7 @@ theorem equal_charZero_to_not_mixed_char (h : ∀ I : Ideal R, I ≠ ⊤ → Cha
   intro p p_pos
   by_contra hp_mixed_char
   rcases hp_mixed_char.char_p_quotient with ⟨I, hI_ne_top, hI_p⟩
-  replace hI_zero : CharP (R ⧸ I) 0 := @CharP.of_charZero _ _ (h I hI_ne_top)
+  replace hI_zero : CharP (R ⧸ I) 0 := @CharP.ofCharZero _ _ (h I hI_ne_top)
   exact absurd (CharP.eq (R ⧸ I) hI_p hI_zero) (ne_of_gt p_pos)
 #align equal_char_zero_to_not_mixed_char equal_charZero_to_not_mixed_char
 

Mathbin/CategoryTheory/Limits/Pi.lean

@@ -36,6 +36,7 @@ variable {J : Type v₁} [SmallCategory J]
 
 variable {F : J ⥤ ∀ i, C i}
 
+#print CategoryTheory.pi.coneCompEval /-
 /-- A cone over `F : J ⥤ Π i, C i` has as its components cones over each of the `F ⋙ pi.eval C i`.
 -/
 def coneCompEval (c : Cone F) (i : I) : Cone (F ⋙ Pi.eval C i)
@@ -45,7 +46,9 @@ def coneCompEval (c : Cone F) (i : I) : Cone (F ⋙ Pi.eval C i)
     { app := fun j => c.π.app j i
       naturality' := fun j j' f => congr_fun (c.π.naturality f) i }
 #align category_theory.pi.cone_comp_eval CategoryTheory.pi.coneCompEval
+-/
 
+#print CategoryTheory.pi.coconeCompEval /-
 /--
 A cocone over `F : J ⥤ Π i, C i` has as its components cocones over each of the `F ⋙ pi.eval C i`.
 -/
@@ -56,7 +59,9 @@ def coconeCompEval (c : Cocone F) (i : I) : Cocone (F ⋙ Pi.eval C i)
     { app := fun j => c.ι.app j i
       naturality' := fun j j' f => congr_fun (c.ι.naturality f) i }
 #align category_theory.pi.cocone_comp_eval CategoryTheory.pi.coconeCompEval
+-/
 
+#print CategoryTheory.pi.coneOfConeCompEval /-
 /--
 Given a family of cones over the `F ⋙ pi.eval C i`, we can assemble these together as a `cone F`.
 -/
@@ -69,7 +74,9 @@ def coneOfConeCompEval (c : ∀ i, Cone (F ⋙ Pi.eval C i)) : Cone F
         ext i
         exact (c i).π.naturality f }
 #align category_theory.pi.cone_of_cone_comp_eval CategoryTheory.pi.coneOfConeCompEval
+-/
 
+#print CategoryTheory.pi.coconeOfCoconeCompEval /-
 /-- Given a family of cocones over the `F ⋙ pi.eval C i`,
 we can assemble these together as a `cocone F`.
 -/
@@ -82,7 +89,9 @@ def coconeOfCoconeCompEval (c : ∀ i, Cocone (F ⋙ Pi.eval C i)) : Cocone F
         ext i
         exact (c i).ι.naturality f }
 #align category_theory.pi.cocone_of_cocone_comp_eval CategoryTheory.pi.coconeOfCoconeCompEval
+-/
 
+#print CategoryTheory.pi.coneOfConeEvalIsLimit /-
 /-- Given a family of limit cones over the `F ⋙ pi.eval C i`,
 assembling them together as a `cone F` produces a limit cone.
 -/
@@ -97,7 +106,9 @@ def coneOfConeEvalIsLimit {c : ∀ i, Cone (F ⋙ Pi.eval C i)} (P : ∀ i, IsLi
     ext i
     exact (P i).uniq (cone_comp_eval s i) (m i) fun j => congr_fun (w j) i
 #align category_theory.pi.cone_of_cone_eval_is_limit CategoryTheory.pi.coneOfConeEvalIsLimit
+-/
 
+#print CategoryTheory.pi.coconeOfCoconeEvalIsColimit /-
 /-- Given a family of colimit cocones over the `F ⋙ pi.eval C i`,
 assembling them together as a `cocone F` produces a colimit cocone.
 -/
@@ -112,11 +123,13 @@ def coconeOfCoconeEvalIsColimit {c : ∀ i, Cocone (F ⋙ Pi.eval C i)} (P : ∀
     ext i
     exact (P i).uniq (cocone_comp_eval s i) (m i) fun j => congr_fun (w j) i
 #align category_theory.pi.cocone_of_cocone_eval_is_colimit CategoryTheory.pi.coconeOfCoconeEvalIsColimit
+-/
 
 section
 
 variable [∀ i, HasLimit (F ⋙ Pi.eval C i)]
 
+#print CategoryTheory.pi.hasLimit_of_hasLimit_comp_eval /-
 /-- If we have a functor `F : J ⥤ Π i, C i` into a category of indexed families,
 and we have limits for each of the `F ⋙ pi.eval C i`,
 then `F` has a limit.
@@ -126,13 +139,15 @@ theorem hasLimit_of_hasLimit_comp_eval : HasLimit F :=
     { Cone := coneOfConeCompEval fun i => limit.cone _
       IsLimit := coneOfConeEvalIsLimit fun i => limit.isLimit _ }
 #align category_theory.pi.has_limit_of_has_limit_comp_eval CategoryTheory.pi.hasLimit_of_hasLimit_comp_eval
+-/
 
 end
 
 section
 
 variable [∀ i, HasColimit (F ⋙ Pi.eval C i)]
 
+#print CategoryTheory.pi.hasColimit_of_hasColimit_comp_eval /-
 /-- If we have a functor `F : J ⥤ Π i, C i` into a category of indexed families,
 and colimits exist for each of the `F ⋙ pi.eval C i`,
 there is a colimit for `F`.
@@ -142,6 +157,7 @@ theorem hasColimit_of_hasColimit_comp_eval : HasColimit F :=
     { Cocone := coconeOfCoconeCompEval fun i => colimit.cocone _
       IsColimit := coconeOfCoconeEvalIsColimit fun i => colimit.isColimit _ }
 #align category_theory.pi.has_colimit_of_has_colimit_comp_eval CategoryTheory.pi.hasColimit_of_hasColimit_comp_eval
+-/
 
 end
 

Mathbin/Data/Zmod/Basic.lean

@@ -458,7 +458,7 @@ end CharEq
 end UniversalProperty
 
 theorem int_coe_eq_int_coe_iff (a b : ℤ) (c : ℕ) : (a : ZMod c) = (b : ZMod c) ↔ a ≡ b [ZMOD c] :=
-  CharP.int_coe_eq_int_coe_iff (ZMod c) c a b
+  CharP.int_cast_eq_int_cast_iff (ZMod c) c a b
 #align zmod.int_coe_eq_int_coe_iff ZMod.int_coe_eq_int_coe_iff
 
 theorem int_coe_eq_int_coe_iff' (a b : ℤ) (c : ℕ) : (a : ZMod c) = (b : ZMod c) ↔ a % c = b % c :=

Mathbin/FieldTheory/Finite/Basic.lean

@@ -526,7 +526,7 @@ variable [Finite F]
 /-- In a finite field of characteristic `2`, all elements are squares. -/
 theorem isSquare_of_char_two (hF : ringChar F = 2) (a : F) : IsSquare a :=
   haveI hF' : CharP F 2 := ringChar.of_eq hF
-  isSquare_of_char_two' a
+  isSquare_of_charTwo' a
 #align finite_field.is_square_of_char_two FiniteField.isSquare_of_char_two
 
 /-- In a finite field of odd characteristic, not every element is a square. -/

Mathbin/FieldTheory/Fixed.lean

@@ -117,7 +117,7 @@ theorem smul (m : M) (x : FixedPoints.subfield M F) : m • x = x :=
 theorem smul_polynomial (m : M) (p : Polynomial (FixedPoints.subfield M F)) : m • p = p :=
   Polynomial.induction_on p (fun x => by rw [Polynomial.smul_C, smul])
     (fun p q ihp ihq => by rw [smul_add, ihp, ihq]) fun n x ih => by
-    rw [smul_mul', Polynomial.smul_C, smul, smul_pow', Polynomial.smul_x]
+    rw [smul_mul', Polynomial.smul_C, smul, smul_pow', Polynomial.smul_X]
 #align fixed_points.smul_polynomial FixedPoints.smul_polynomial
 
 instance : Algebra (FixedPoints.subfield M F) F := by infer_instance

Mathbin/Topology/Instances/Ennreal.lean

@@ -2655,7 +2655,7 @@ theorem summable_sigma_of_nonneg {β : ∀ x : α, Type _} {f : (Σx, β x) →
 lean 3 declaration is
   forall {ι : Type.{u1}} {f : ι -> Real} {c : Real}, (LE.le.{u1} (ι -> Real) (Pi.hasLe.{u1, 0} ι (fun (ᾰ : ι) => Real) (fun (i : ι) => Real.hasLe)) (OfNat.ofNat.{u1} (ι -> Real) 0 (OfNat.mk.{u1} (ι -> Real) 0 (Zero.zero.{u1} (ι -> Real) (Pi.instZero.{u1, 0} ι (fun (ᾰ : ι) => Real) (fun (i : ι) => Real.hasZero))))) f) -> (forall (u : Finset.{u1} ι), LE.le.{0} Real Real.hasLe (Finset.sum.{0, u1} Real ι Real.addCommMonoid u (fun (x : ι) => f x)) c) -> (Summable.{0, u1} Real ι Real.addCommMonoid (UniformSpace.toTopologicalSpace.{0} Real (PseudoMetricSpace.toUniformSpace.{0} Real Real.pseudoMetricSpace)) f)
 but is expected to have type
-  forall {ι : Type.{u1}} {f : ι -> Real} {c : Real}, (LE.le.{u1} (ι -> Real) (Pi.hasLe.{u1, 0} ι (fun (ᾰ : ι) => Real) (fun (i : ι) => Real.instLEReal)) (OfNat.ofNat.{u1} (ι -> Real) 0 (Zero.toOfNat0.{u1} (ι -> Real) (Pi.instZero.{u1, 0} ι (fun (a._@.Mathlib.Topology.Instances.ENNReal._hyg.26766 : ι) => Real) (fun (i : ι) => Real.instZeroReal)))) f) -> (forall (u : Finset.{u1} ι), LE.le.{0} Real Real.instLEReal (Finset.sum.{0, u1} Real ι Real.instAddCommMonoidReal u (fun (x : ι) => f x)) c) -> (Summable.{0, u1} Real ι Real.instAddCommMonoidReal (UniformSpace.toTopologicalSpace.{0} Real (PseudoMetricSpace.toUniformSpace.{0} Real Real.pseudoMetricSpace)) f)
+  forall {ι : Type.{u1}} {f : ι -> Real} {c : Real}, (LE.le.{u1} (ι -> Real) (Pi.hasLe.{u1, 0} ι (fun (ᾰ : ι) => Real) (fun (i : ι) => Real.instLEReal)) (OfNat.ofNat.{u1} (ι -> Real) 0 (Zero.toOfNat0.{u1} (ι -> Real) (Pi.instZero.{u1, 0} ι (fun (a._@.Mathlib.Topology.Instances.ENNReal._hyg.26850 : ι) => Real) (fun (i : ι) => Real.instZeroReal)))) f) -> (forall (u : Finset.{u1} ι), LE.le.{0} Real Real.instLEReal (Finset.sum.{0, u1} Real ι Real.instAddCommMonoidReal u (fun (x : ι) => f x)) c) -> (Summable.{0, u1} Real ι Real.instAddCommMonoidReal (UniformSpace.toTopologicalSpace.{0} Real (PseudoMetricSpace.toUniformSpace.{0} Real Real.pseudoMetricSpace)) f)
 Case conversion may be inaccurate. Consider using '#align summable_of_sum_le summable_of_sum_leₓ'. -/
 theorem summable_of_sum_le {ι : Type _} {f : ι → ℝ} {c : ℝ} (hf : 0 ≤ f)
     (h : ∀ u : Finset ι, (∑ x in u, f x) ≤ c) : Summable f :=

lake-manifest.json

@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "1e7117b51cfd7b837832092575afca3ef2d86768",
+    "rev": "0f23d970a4b7798361413cd8259047ed44f44389",
     "name": "lean3port",
-    "inputRev?": "1e7117b51cfd7b837832092575afca3ef2d86768"}},
+    "inputRev?": "0f23d970a4b7798361413cd8259047ed44f44389"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "d962f0faef9dff74d887486f27f6f9191049057d",
+    "rev": "92a6bf698329a97ea43a47da96889b095109d489",
     "name": "mathlib",
-    "inputRev?": "d962f0faef9dff74d887486f27f6f9191049057d"}},
+    "inputRev?": "92a6bf698329a97ea43a47da96889b095109d489"}},
   {"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-14-08"
+def tag : String := "nightly-2023-03-14-10"
 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"@"1e7117b51cfd7b837832092575afca3ef2d86768"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"0f23d970a4b7798361413cd8259047ed44f44389"
 
 @[default_target]
 lean_lib Mathbin where