bump to nightly-2023-05-23-18

mathlib commit leanprover-community/mathlib@75e7fca

Mathbin/FieldTheory/Fixed.lean

@@ -310,7 +310,7 @@ instance separable : IsSeparable (FixedPoints.subfield G F) F :=
     -- this was a plain rw when we were using unbundled subrings
     erw [← minpoly_eq_minpoly, ← Polynomial.separable_map (FixedPoints.subfield G F).Subtype,
       minpoly, Polynomial.map_toSubring _ (Subfield G F).toSubring]
-    exact Polynomial.separable_prod_x_sub_c_iff.2 (injective_of_quotient_stabilizer G x)⟩
+    exact Polynomial.separable_prod_X_sub_C_iff.2 (injective_of_quotient_stabilizer G x)⟩
 #align fixed_points.separable FixedPoints.separable
 
 instance : FiniteDimensional (subfield G F) F :=

Mathbin/FieldTheory/Galois.lean

@@ -481,7 +481,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/MeasureTheory/Function/StronglyMeasurable/Basic.lean

@@ -612,7 +612,7 @@ end CommMonoid
 theorem isSeparable_range {m : MeasurableSpace α} [TopologicalSpace β] (hf : StronglyMeasurable f) :
     TopologicalSpace.IsSeparable (range f) :=
   by
-  have : is_separable (closure (⋃ n, range (hf.approx n))) :=
+  have : IsSeparable (closure (⋃ n, range (hf.approx n))) :=
     (is_separable_Union fun n => (simple_func.finite_range (hf.approx n)).IsSeparable).closure
   apply this.mono
   rintro _ ⟨x, rfl⟩
@@ -728,7 +728,7 @@ theorem Embedding.comp_stronglyMeasurable_iff {m : MeasurableSpace α} [Topologi
           exact mem_range_self x }
     have : Measurable (G ∘ f) := Measurable.subtype_mk H.measurable
     exact hG.measurable_embedding.measurable_comp_iff.1 this
-  · have : is_separable (g ⁻¹' range (g ∘ f)) := hg.is_separable_preimage H.is_separable_range
+  · have : IsSeparable (g ⁻¹' range (g ∘ f)) := hg.is_separable_preimage H.is_separable_range
     convert this
     ext x
     simp [hg.inj.eq_iff]
@@ -743,7 +743,7 @@ theorem stronglyMeasurable_of_tendsto {ι : Type _} {m : MeasurableSpace α} [To
   refine' stronglyMeasurable_iff_measurable_separable.2 ⟨_, _⟩
   · exact measurable_of_tendsto_metrizable' u (fun i => (hf i).Measurable) limUnder
   · rcases u.exists_seq_tendsto with ⟨v, hv⟩
-    have : is_separable (closure (⋃ i, range (f (v i)))) :=
+    have : IsSeparable (closure (⋃ i, range (f (v i)))) :=
       (is_separable_Union fun i => (hf (v i)).isSeparable_range).closure
     apply this.mono
     rintro _ ⟨x, rfl⟩
@@ -1691,7 +1691,7 @@ theorem aeStronglyMeasurable_of_tendsto_ae {ι : Type _} [PseudoMetrizableSpace
   refine' aeStronglyMeasurable_iff_aEMeasurable_separable.2 ⟨_, _⟩
   · exact aemeasurable_of_tendsto_metrizable_ae _ (fun n => (hf n).AEMeasurable) limUnder
   · rcases u.exists_seq_tendsto with ⟨v, hv⟩
-    have : ∀ n : ℕ, ∃ t : Set β, is_separable t ∧ f (v n) ⁻¹' t ∈ μ.ae := fun n =>
+    have : ∀ n : ℕ, ∃ t : Set β, IsSeparable t ∧ f (v n) ⁻¹' t ∈ μ.ae := fun n =>
       (aeStronglyMeasurable_iff_aEMeasurable_separable.1 (hf (v n))).2
     choose t t_sep ht using this
     refine' ⟨closure (⋃ i, t i), (is_separable_Union fun i => t_sep i).closure, _⟩
@@ -1727,7 +1727,7 @@ theorem sum_measure [PseudoMetrizableSpace β] {m : MeasurableSpace α} {μ : ι
   refine'
     aeStronglyMeasurable_iff_aEMeasurable_separable.2
       ⟨AEMeasurable.sum_measure fun i => (h i).AEMeasurable, _⟩
-  have A : ∀ i : ι, ∃ t : Set β, is_separable t ∧ f ⁻¹' t ∈ (μ i).ae := fun i =>
+  have A : ∀ i : ι, ∃ t : Set β, IsSeparable t ∧ f ⁻¹' t ∈ (μ i).ae := fun i =>
     (aeStronglyMeasurable_iff_aEMeasurable_separable.1 (h i)).2
   choose t t_sep ht using A
   refine' ⟨⋃ i, t i, is_separable_Union t_sep, _⟩
@@ -2088,7 +2088,7 @@ theorem stronglyMeasurable_uncurry_of_continuous_of_stronglyMeasurable {α β ι
         rfl
       rw [this, measurable_swap_iff]
       exact measurable_from_prod_countable fun j => (h j).Measurable
-    · have : is_separable (⋃ i : (t_sf n).range, range (u i)) :=
+    · have : IsSeparable (⋃ i : (t_sf n).range, range (u i)) :=
         is_separable_Union fun i => (h i).isSeparable_range
       apply this.mono
       rintro _ ⟨⟨i, x⟩, rfl⟩

Mathbin/MeasureTheory/Integral/IntegrableOn.lean

@@ -552,7 +552,7 @@ theorem ContinuousOn.aeStronglyMeasurable [TopologicalSpace α] [TopologicalSpac
   cases h.out
   · let f' : s → β := s.restrict f
     have A : Continuous f' := continuousOn_iff_continuous_restrict.1 hf
-    have B : is_separable (univ : Set s) := is_separable_of_separable_space _
+    have B : IsSeparable (univ : Set s) := is_separable_of_separable_space _
     convert is_separable.image B A using 1
     ext x
     simp

Mathbin/Topology/Bases.lean

@@ -627,7 +627,7 @@ theorem IsSeparable.image {β : Type _} [TopologicalSpace β] {s : Set α} (hs :
 #print TopologicalSpace.isSeparable_of_separableSpace_subtype /-
 theorem isSeparable_of_separableSpace_subtype (s : Set α) [SeparableSpace s] : IsSeparable s :=
   by
-  have : is_separable ((coe : s → α) '' (univ : Set s)) :=
+  have : IsSeparable ((coe : s → α) '' (univ : Set s)) :=
     (is_separable_of_separable_space _).image continuous_subtype_val
   simpa only [image_univ, Subtype.range_coe_subtype]
 #align topological_space.is_separable_of_separable_space_subtype TopologicalSpace.isSeparable_of_separableSpace_subtype

lake-manifest.json

@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "8a66df4148e57e828d77e906891aa3664b386f05",
+    "rev": "1da898dbf4b43e1f8061d427d2fb50c9d978c5b8",
     "name": "lean3port",
-    "inputRev?": "8a66df4148e57e828d77e906891aa3664b386f05"}},
+    "inputRev?": "1da898dbf4b43e1f8061d427d2fb50c9d978c5b8"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "5a3910475d832ead3e4353d488ab2e4857391832",
+    "rev": "c82f1498dd4fb62b632ffc706e300eed7d72ad0a",
     "name": "mathlib",
-    "inputRev?": "5a3910475d832ead3e4353d488ab2e4857391832"}},
+    "inputRev?": "c82f1498dd4fb62b632ffc706e300eed7d72ad0a"}},
   {"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-05-23-16"
+def tag : String := "nightly-2023-05-23-18"
 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"@"8a66df4148e57e828d77e906891aa3664b386f05"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"1da898dbf4b43e1f8061d427d2fb50c9d978c5b8"
 
 @[default_target]
 lean_lib Mathbin where