bump to nightly-2024-03-18-08

mathlib commit leanprover-community/mathlib@65a1391

Mathbin/Analysis/PSeries.lean

@@ -258,7 +258,7 @@ theorem Real.summable_one_div_int_pow {p : ℕ} : (Summable fun n : ℤ => 1 / (
   by
   refine'
     ⟨fun h => real.summable_one_div_nat_pow.mp (h.comp_injective Nat.cast_injective), fun h =>
-      summable_int_of_summable_nat (real.summable_one_div_nat_pow.mpr h)
+      Summable.of_nat_of_neg (real.summable_one_div_nat_pow.mpr h)
         (((real.summable_one_div_nat_pow.mpr h).hMul_left <| 1 / (-1) ^ p).congr fun n => _)⟩
   conv_rhs => rw [Int.cast_neg, neg_eq_neg_one_mul, mul_pow, ← div_div]
   conv_lhs => rw [mul_div, mul_one]
@@ -270,7 +270,7 @@ theorem Real.summable_one_div_int_pow {p : ℕ} : (Summable fun n : ℤ => 1 / (
 theorem Real.summable_abs_int_rpow {b : ℝ} (hb : 1 < b) : Summable fun n : ℤ => |(n : ℝ)| ^ (-b) :=
   by
   refine'
-    summable_int_of_summable_nat (_ : Summable fun n : ℕ => |(n : ℝ)| ^ _)
+    Summable.of_nat_of_neg (_ : Summable fun n : ℕ => |(n : ℝ)| ^ _)
       (_ : Summable fun n : ℕ => |((-n : ℤ) : ℝ)| ^ _)
   on_goal 2 => simp_rw [Int.cast_neg, Int.cast_ofNat, abs_neg]
   all_goals

Mathbin/Data/Analysis/Topology.lean

@@ -196,7 +196,7 @@ protected theorem isOpen [TopologicalSpace α] (F : Realizer α) (s : F.σ) : Is
 theorem ext' [T : TopologicalSpace α] {σ : Type _} {F : Ctop α σ}
     (H : ∀ a s, s ∈ 𝓝 a ↔ ∃ b, a ∈ F b ∧ F b ⊆ s) : F.toTopsp = T :=
   by
-  refine' eq_of_nhds_eq_nhds fun x => _
+  refine' TopologicalSpace.ext_nhds fun x => _
   ext s
   rw [mem_nhds_to_topsp, H]
 #align ctop.realizer.ext' Ctop.Realizer.ext'

Mathbin/MeasureTheory/Constructions/Polish.lean

@@ -1003,7 +1003,7 @@ just be added as an instance soon after the definition of `polish_space`.-/
 private theorem second_countable_of_polish [h : PolishSpace α] : SecondCountableTopology α :=
   h.second_countable
 
-attribute [-instance] polishSpace_of_complete_second_countable
+attribute [-instance] PolishSpace.of_separableSpace_completeSpace_metrizable
 
 attribute [local instance] second_countable_of_polish
 

Mathbin/NumberTheory/ModularForms/JacobiTheta/Basic.lean

@@ -64,7 +64,7 @@ theorem exists_summable_bound_exp_mul_sq {R : ℝ} (hR : 0 < R) :
   by
   let y := rexp (-π * R)
   have h : y < 1 := exp_lt_one_iff.mpr (mul_neg_of_neg_of_pos (neg_lt_zero.mpr pi_pos) hR)
-  refine' ⟨fun n => y ^ n.natAbs, summable_int_of_summable_nat _ _, fun τ hτ n => _⟩; pick_goal 3
+  refine' ⟨fun n => y ^ n.natAbs, Summable.of_nat_of_neg _ _, fun τ hτ n => _⟩; pick_goal 3
   · refine' (norm_exp_mul_sq_le (hR.trans_le hτ) n).trans _
     refine' pow_le_pow_left (exp_pos _).le (real.exp_le_exp.mpr _) _
     rwa [mul_le_mul_left_of_neg (neg_lt_zero.mpr pi_pos)]
@@ -136,7 +136,7 @@ theorem jacobiTheta_S_smul (τ : ℍ) :
 theorem hasSum_nat_jacobiTheta {z : ℂ} (hz : 0 < im z) :
     HasSum (fun n : ℕ => cexp (π * I * (n + 1) ^ 2 * z)) ((jacobiTheta z - 1) / 2) :=
   by
-  have := (summable_exp_mul_sq hz).HasSum.sum_nat_of_sum_int
+  have := (summable_exp_mul_sq hz).HasSum.nat_add_neg
   rw [← @hasSum_nat_add_iff' ℂ _ _ _ _ 1] at this
   simp_rw [Finset.sum_range_one, Int.cast_neg, Int.cast_ofNat, Nat.cast_zero, neg_zero,
     Int.cast_zero, sq (0 : ℂ), MulZeroClass.mul_zero, MulZeroClass.zero_mul, neg_sq, ← mul_two,

Mathbin/NumberTheory/ZetaValues.lean

@@ -290,7 +290,7 @@ theorem hasSum_one_div_nat_pow_mul_fourier {k : ℕ} (hk : 2 ≤ k) {x : ℝ} (h
     HasSum (fun n : ℕ => 1 / (n : ℂ) ^ k * (fourier n (x : 𝕌) + (-1) ^ k * fourier (-n) (x : 𝕌)))
       (-(2 * π * I) ^ k / k ! * bernoulliFun k x) :=
   by
-  convert (hasSum_one_div_pow_mul_fourier_mul_bernoulliFun hk hx).sum_nat_of_sum_int
+  convert (hasSum_one_div_pow_mul_fourier_mul_bernoulliFun hk hx).nat_add_neg
   · ext1 n
     rw [Int.cast_neg, mul_add, ← mul_assoc]
     conv_rhs => rw [neg_eq_neg_one_mul, mul_pow, ← div_div]

Mathbin/Topology/Algebra/Group/Basic.lean

@@ -1058,7 +1058,7 @@ theorem continuous_of_continuousAt_one {M hom : Type _} [MulOneClass M] [Topolog
 theorem TopologicalGroup.ext {G : Type _} [Group G] {t t' : TopologicalSpace G}
     (tg : @TopologicalGroup G t _) (tg' : @TopologicalGroup G t' _)
     (h : @nhds G t 1 = @nhds G t' 1) : t = t' :=
-  eq_of_nhds_eq_nhds fun x => by
+  TopologicalSpace.ext_nhds fun x => by
     rw [← @nhds_translation_mul_inv G t _ _ x, ← @nhds_translation_mul_inv G t' _ _ x, ← h]
 #align topological_group.ext TopologicalGroup.ext
 #align topological_add_group.ext TopologicalAddGroup.ext

Mathbin/Topology/Algebra/InfiniteSum/Basic.lean

@@ -487,10 +487,12 @@ theorem Summable.compl_add {s : Set β} (hs : Summable (f ∘ coe : sᶜ → α)
 #align summable.compl_add Summable.compl_add
 -/
 
+#print Summable.even_add_odd /-
 theorem Summable.even_add_odd {f : ℕ → α} (he : Summable fun k => f (2 * k))
     (ho : Summable fun k => f (2 * k + 1)) : Summable f :=
   (he.HasSum.even_add_odd ho.HasSum).Summable
 #align summable.even_add_odd Summable.even_add_odd
+-/
 
 #print HasSum.sigma /-
 theorem HasSum.sigma [RegularSpace α] {γ : β → Type _} {f : (Σ b : β, γ b) → α} {g : β → α} {a : α}
@@ -1279,36 +1281,37 @@ theorem HasSum.int_rec {b : α} {f g : ℕ → α} (hf : HasSum f a) (hg : HasSu
 #align has_sum.int_rec HasSum.int_rec
 -/
 
-#print HasSum.nonneg_add_neg /-
-theorem HasSum.nonneg_add_neg {b : α} {f : ℤ → α} (hnonneg : HasSum (fun n : ℕ => f n) a)
+#print HasSum.of_nat_of_neg_add_one /-
+theorem HasSum.of_nat_of_neg_add_one {b : α} {f : ℤ → α} (hnonneg : HasSum (fun n : ℕ => f n) a)
     (hneg : HasSum (fun n : ℕ => f (-n.succ)) b) : HasSum f (a + b) :=
   by
   simp_rw [← Int.negSucc_coe] at hneg
   convert hnonneg.int_rec hneg using 1
   ext (i | j) <;> rfl
-#align has_sum.nonneg_add_neg HasSum.nonneg_add_neg
+#align has_sum.nonneg_add_neg HasSum.of_nat_of_neg_add_one
 -/
 
-#print HasSum.pos_add_zero_add_neg /-
-theorem HasSum.pos_add_zero_add_neg {b : α} {f : ℤ → α} (hpos : HasSum (fun n : ℕ => f (n + 1)) a)
-    (hneg : HasSum (fun n : ℕ => f (-n.succ)) b) : HasSum f (a + f 0 + b) :=
+#print HasSum.of_add_one_of_neg_add_one /-
+theorem HasSum.of_add_one_of_neg_add_one {b : α} {f : ℤ → α}
+    (hpos : HasSum (fun n : ℕ => f (n + 1)) a) (hneg : HasSum (fun n : ℕ => f (-n.succ)) b) :
+    HasSum f (a + f 0 + b) :=
   haveI : ∀ g : ℕ → α, HasSum (fun k => g (k + 1)) a → HasSum g (a + g 0) := by intro g hg;
     simpa using (hasSum_nat_add_iff _).mp hg
-  (this (fun n => f n) hpos).nonneg_add_neg hneg
-#align has_sum.pos_add_zero_add_neg HasSum.pos_add_zero_add_neg
+  (this (fun n => f n) hpos).of_nat_of_neg_add_one hneg
+#align has_sum.pos_add_zero_add_neg HasSum.of_add_one_of_neg_add_one
 -/
 
-#print summable_int_of_summable_nat /-
-theorem summable_int_of_summable_nat {f : ℤ → α} (hp : Summable fun n : ℕ => f n)
+#print Summable.of_nat_of_neg /-
+theorem Summable.of_nat_of_neg {f : ℤ → α} (hp : Summable fun n : ℕ => f n)
     (hn : Summable fun n : ℕ => f (-n)) : Summable f :=
-  (HasSum.nonneg_add_neg hp.HasSum <| Summable.hasSum <| (summable_nat_add_iff 1).mpr hn).Summable
-#align summable_int_of_summable_nat summable_int_of_summable_nat
+  (HasSum.of_nat_of_neg_add_one hp.HasSum <|
+      Summable.hasSum <| (summable_nat_add_iff 1).mpr hn).Summable
+#align summable_int_of_summable_nat Summable.of_nat_of_neg
 -/
 
-#print HasSum.sum_nat_of_sum_int /-
-theorem HasSum.sum_nat_of_sum_int {α : Type _} [AddCommMonoid α] [TopologicalSpace α]
-    [ContinuousAdd α] {a : α} {f : ℤ → α} (hf : HasSum f a) :
-    HasSum (fun n : ℕ => f n + f (-n)) (a + f 0) :=
+#print HasSum.nat_add_neg /-
+theorem HasSum.nat_add_neg {α : Type _} [AddCommMonoid α] [TopologicalSpace α] [ContinuousAdd α]
+    {a : α} {f : ℤ → α} (hf : HasSum f a) : HasSum (fun n : ℕ => f n + f (-n)) (a + f 0) :=
   by
   apply (hf.add (hasSum_ite_eq (0 : ℤ) (f 0))).hasSum_of_sum_eq fun u => _
   refine' ⟨u.image Int.natAbs, fun v' hv' => _⟩
@@ -1353,7 +1356,7 @@ theorem HasSum.sum_nat_of_sum_int {α : Type _} [AddCommMonoid α] [TopologicalS
     _ = ∑ b in v', f b + ∑ b in v', f (-b) := by
       simp only [sum_image, Nat.cast_inj, imp_self, imp_true_iff, neg_inj]
     _ = ∑ b in v', (f b + f (-b)) := sum_add_distrib.symm
-#align has_sum.sum_nat_of_sum_int HasSum.sum_nat_of_sum_int
+#align has_sum.sum_nat_of_sum_int HasSum.nat_add_neg
 -/
 
 end Nat

Mathbin/Topology/Bases.lean

@@ -562,8 +562,8 @@ theorem isTopologicalBasis_pi {ι : Type _} {X : ι → Type _} [∀ i, Topologi
 #align is_topological_basis_pi isTopologicalBasis_pi
 -/
 
-#print isTopologicalBasis_iInf /-
-theorem isTopologicalBasis_iInf {β : Type _} {ι : Type _} {X : ι → Type _}
+#print IsTopologicalBasis.iInf_induced /-
+theorem IsTopologicalBasis.iInf_induced {β : Type _} {ι : Type _} {X : ι → Type _}
     [t : ∀ i, TopologicalSpace (X i)] {T : ∀ i, Set (Set (X i))}
     (cond : ∀ i, IsTopologicalBasis (T i)) (f : ∀ i, β → X i) :
     @IsTopologicalBasis β (⨅ i, induced (f i) (t i))
@@ -592,7 +592,7 @@ theorem isTopologicalBasis_iInf {β : Type _} {ι : Type _} {X : ι → Type _}
     ext1
     rw [Set.preimage_iInter]
     rfl
-#align is_topological_basis_infi isTopologicalBasis_iInf
+#align is_topological_basis_infi IsTopologicalBasis.iInf_induced
 -/
 
 #print isTopologicalBasis_singletons /-

Mathbin/Topology/Category/Top/Limits/Cofiltered.lean

@@ -68,7 +68,7 @@ theorem isTopologicalBasis_cofiltered_limit (T : ∀ j, Set (Set (F.obj j)))
       refine' ⟨j, V, hV, rfl⟩
   -- Using `D`, we can apply the characterization of the topological basis of a
   -- topology defined as an infimum...
-  convert isTopologicalBasis_iInf hT fun j (x : D.X) => D.π.app j x
+  convert IsTopologicalBasis.iInf_induced hT fun j (x : D.X) => D.π.app j x
   ext U0
   constructor
   · rintro ⟨j, V, hV, rfl⟩

Mathbin/Topology/MetricSpace/Polish.lean

@@ -85,13 +85,13 @@ class UpgradedPolishSpace (α : Type _) extends MetricSpace α, SecondCountableT
 #align upgraded_polish_space UpgradedPolishSpace
 -/
 
-#print polishSpace_of_complete_second_countable /-
-instance (priority := 100) polishSpace_of_complete_second_countable [m : MetricSpace α]
-    [h : SecondCountableTopology α] [h' : CompleteSpace α] : PolishSpace α
+#print PolishSpace.of_separableSpace_completeSpace_metrizable /-
+instance (priority := 100) PolishSpace.of_separableSpace_completeSpace_metrizable
+    [m : MetricSpace α] [h : SecondCountableTopology α] [h' : CompleteSpace α] : PolishSpace α
     where
   second_countable := h
   complete := ⟨m, rfl, h'⟩
-#align polish_space_of_complete_second_countable polishSpace_of_complete_second_countable
+#align polish_space_of_complete_second_countable PolishSpace.of_separableSpace_completeSpace_metrizable
 -/
 
 #print polishSpaceMetric /-
@@ -210,14 +210,12 @@ theorem IsClosed.polishSpace {α : Type _} [TopologicalSpace α] [PolishSpace α
 #align is_closed.polish_space IsClosed.polishSpace
 -/
 
-#print PolishSpace.AuxCopy /-
 /-- A sequence of type synonyms of a given type `α`, useful in the proof of
 `exists_polish_space_forall_le` to endow each copy with a different topology. -/
 @[nolint unused_arguments has_nonempty_instance]
 def AuxCopy (α : Type _) {ι : Type _} (i : ι) : Type _ :=
   α
 #align polish_space.aux_copy PolishSpace.AuxCopy
--/
 
 #print PolishSpace.exists_polishSpace_forall_le /-
 /-- Given a Polish space, and countably many finer Polish topologies, there exists another Polish

Mathbin/Topology/Order.lean

@@ -387,12 +387,12 @@ theorem le_of_nhds_le_nhds {t₁ t₂ : TopologicalSpace α} (h : ∀ x, @nhds 
 #align le_of_nhds_le_nhds le_of_nhds_le_nhds
 -/
 
-#print eq_of_nhds_eq_nhds /-
-theorem eq_of_nhds_eq_nhds {t₁ t₂ : TopologicalSpace α} (h : ∀ x, @nhds α t₁ x = @nhds α t₂ x) :
-    t₁ = t₂ :=
+#print TopologicalSpace.ext_nhds /-
+theorem TopologicalSpace.ext_nhds {t₁ t₂ : TopologicalSpace α}
+    (h : ∀ x, @nhds α t₁ x = @nhds α t₂ x) : t₁ = t₂ :=
   le_antisymm (le_of_nhds_le_nhds fun x => le_of_eq <| h x)
     (le_of_nhds_le_nhds fun x => le_of_eq <| (h x).symm)
-#align eq_of_nhds_eq_nhds eq_of_nhds_eq_nhds
+#align eq_of_nhds_eq_nhds TopologicalSpace.ext_nhds
 -/
 
 #print eq_bot_of_singletons_open /-
@@ -1126,7 +1126,7 @@ theorem nhds_induced [T : TopologicalSpace α] (f : β → α) (a : β) :
 theorem induced_iff_nhds_eq [tα : TopologicalSpace α] [tβ : TopologicalSpace β] (f : β → α) :
     tβ = tα.induced f ↔ ∀ b, 𝓝 b = comap f (𝓝 <| f b) :=
   ⟨fun h a => h.symm ▸ nhds_induced f a, fun h =>
-    eq_of_nhds_eq_nhds fun x => by rw [h, nhds_induced]⟩
+    TopologicalSpace.ext_nhds fun x => by rw [h, nhds_induced]⟩
 #align induced_iff_nhds_eq induced_iff_nhds_eq
 -/
 

Mathbin/Topology/Order/Basic.lean

@@ -1214,7 +1214,7 @@ theorem induced_orderTopology' {α : Type u} {β : Type v} [Preorder α] [ta : T
     @OrderTopology _ (induced f ta) _ :=
   by
   letI := induced f ta
-  refine' ⟨eq_of_nhds_eq_nhds fun a => _⟩
+  refine' ⟨TopologicalSpace.ext_nhds fun a => _⟩
   rw [nhds_induced, nhds_generate_from, nhds_eq_order (f a)]
   apply le_antisymm
   · refine' le_iInf fun s => le_iInf fun hs => le_principal_iff.2 _
@@ -1265,7 +1265,7 @@ instance orderTopology_of_ordConnected {α : Type u} [ta : TopologicalSpace α]
     [OrderTopology α] {t : Set α} [ht : OrdConnected t] : OrderTopology t :=
   by
   letI := induced (coe : t → α) ta
-  refine' ⟨eq_of_nhds_eq_nhds fun a => _⟩
+  refine' ⟨TopologicalSpace.ext_nhds fun a => _⟩
   rw [nhds_induced, nhds_generate_from, nhds_eq_order (a : α)]
   apply le_antisymm
   · refine' le_iInf fun s => le_iInf fun hs => le_principal_iff.2 _
@@ -2271,7 +2271,7 @@ theorem nhds_eq_iInf_abs_sub (a : α) : 𝓝 a = ⨅ r > 0, 𝓟 {b | |a - b| <
 theorem orderTopology_of_nhds_abs {α : Type _} [TopologicalSpace α] [LinearOrderedAddCommGroup α]
     (h_nhds : ∀ a : α, 𝓝 a = ⨅ r > 0, 𝓟 {b | |a - b| < r}) : OrderTopology α :=
   by
-  refine' ⟨eq_of_nhds_eq_nhds fun a => _⟩
+  refine' ⟨TopologicalSpace.ext_nhds fun a => _⟩
   rw [h_nhds]
   letI := Preorder.topology α; letI : OrderTopology α := ⟨rfl⟩
   exact (nhds_eq_iInf_abs_sub a).symm

Mathbin/Topology/UniformSpace/Basic.lean

@@ -1527,7 +1527,7 @@ instance : Inf (UniformSpace α) :=
             refl := le_inf u₁.refl u₂.refl
             symm := u₁.symm.inf u₂.symm
             comp := (lift'_inf_le _ _ _).trans <| inf_le_inf u₁.comp u₂.comp }) <|
-      eq_of_nhds_eq_nhds fun a => by
+      TopologicalSpace.ext_nhds fun a => by
         simpa only [nhds_inf, nhds_eq_comap_uniformity] using comap_inf.symm⟩
 
 instance : CompleteLattice (UniformSpace α) :=
@@ -1725,7 +1725,7 @@ theorem UniformSpace.toTopologicalSpace_top : @UniformSpace.toTopologicalSpace 
 theorem UniformSpace.toTopologicalSpace_iInf {ι : Sort _} {u : ι → UniformSpace α} :
     (iInf u).toTopologicalSpace = ⨅ i, (u i).toTopologicalSpace :=
   by
-  refine' eq_of_nhds_eq_nhds fun a => _
+  refine' TopologicalSpace.ext_nhds fun a => _
   simp only [nhds_iInf, nhds_eq_uniformity, iInf_uniformity]
   exact lift'_infi_of_map_univ (ball_inter _) preimage_univ
 #align to_topological_space_infi UniformSpace.toTopologicalSpace_iInf

lake-manifest.json

@@ -58,19 +58,19 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "1a1dffdd3d023000aecf7e6940843980dcce9170",
+   "rev": "6d1dffa1281a6e231f594e4c49ec01bc3ad9974e",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "1a1dffdd3d023000aecf7e6940843980dcce9170",
+   "inputRev": "6d1dffa1281a6e231f594e4c49ec01bc3ad9974e",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/lean3port.git",
    "type": "git",
    "subDir": null,
-   "rev": "df422fe3a075ec0fd32a2c541ae69f7d40460159",
+   "rev": "f1ece73bb42398637048a17f8c9172036c2a9035",
    "name": "lean3port",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "df422fe3a075ec0fd32a2c541ae69f7d40460159",
+   "inputRev": "f1ece73bb42398637048a17f8c9172036c2a9035",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "mathlib3port",

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-2024-03-17-08"
+def tag : String := "nightly-2024-03-18-08"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"df422fe3a075ec0fd32a2c541ae69f7d40460159"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"f1ece73bb42398637048a17f8c9172036c2a9035"
 
 @[default_target]
 lean_lib Mathbin where