bump to nightly-2024-01-22-06

mathlib commit leanprover-community/mathlib@65a1391

Mathbin/Geometry/Manifold/PartitionOfUnity.lean

@@ -567,11 +567,11 @@ end SmoothBumpCovering
 
 variable (I)
 
-#print exists_smooth_zero_one_of_closed /-
+#print exists_smooth_zero_one_of_isClosed /-
 /-- Given two disjoint closed sets in a Hausdorff σ-compact finite dimensional manifold, there
 exists an infinitely smooth function that is equal to `0` on one of them and is equal to one on the
 other. -/
-theorem exists_smooth_zero_one_of_closed [T2Space M] [SigmaCompactSpace M] {s t : Set M}
+theorem exists_smooth_zero_one_of_isClosed [T2Space M] [SigmaCompactSpace M] {s t : Set M}
     (hs : IsClosed s) (ht : IsClosed t) (hd : Disjoint s t) :
     ∃ f : C^∞⟮I, M; 𝓘(ℝ), ℝ⟯, EqOn f 0 s ∧ EqOn f 1 t ∧ ∀ x, f x ∈ Icc (0 : ℝ) 1 :=
   by
@@ -584,7 +584,7 @@ theorem exists_smooth_zero_one_of_closed [T2Space M] [SigmaCompactSpace M] {s t
   suffices ∀ i, g i x = 0 by simp only [this, ContMDiffMap.coeFn_mk, finsum_zero, Pi.zero_apply]
   refine' fun i => f.to_smooth_partition_of_unity_zero_of_zero _
   exact nmem_support.1 (subset_compl_comm.1 (hf.support_subset i) hx)
-#align exists_smooth_zero_one_of_closed exists_smooth_zero_one_of_closed
+#align exists_smooth_zero_one_of_closed exists_smooth_zero_one_of_isClosed
 -/
 
 namespace SmoothPartitionOfUnity
@@ -618,7 +618,7 @@ theorem exists_isSubordinate {s : Set M} (hs : IsClosed s) (U : ι → Set M) (h
   rcases BumpCovering.exists_isSubordinate_of_prop (Smooth I 𝓘(ℝ)) _ hs U ho hU with ⟨f, hf, hfU⟩
   · exact ⟨f.to_smooth_partition_of_unity hf, hfU.to_smooth_partition_of_unity hf⟩
   · intro s t hs ht hd
-    rcases exists_smooth_zero_one_of_closed I hs ht hd with ⟨f, hf⟩
+    rcases exists_smooth_zero_one_of_isClosed I hs ht hd with ⟨f, hf⟩
     exact ⟨f, f.smooth, hf⟩
 #align smooth_partition_of_unity.exists_is_subordinate SmoothPartitionOfUnity.exists_isSubordinate
 -/

Mathbin/LinearAlgebra/AffineSpace/Independent.lean

@@ -660,7 +660,7 @@ theorem exists_affineIndependent (s : Set P) :
   rw [linearIndependent_set_iff_affineIndependent_vadd_union_singleton k hb₀ p] at hb₃ 
   refine' ⟨{p} ∪ Equiv.vaddConst p '' b, _, _, hb₃⟩
   · apply Set.union_subset (set.singleton_subset_iff.mpr hp)
-    rwa [← (Equiv.vaddConst p).subset_image' b s]
+    rwa [← (Equiv.vaddConst p).subset_symm_image b s]
   · rw [Equiv.coe_vaddConst_symm, ← vectorSpan_eq_span_vsub_set_right k hp] at hb₂ 
     apply AffineSubspace.ext_of_direction_eq
     · have : Submodule.span k b = Submodule.span k (insert 0 b) := by simp

Mathbin/Logic/Equiv/Set.lean

@@ -68,21 +68,21 @@ theorem Set.preimage_equiv_eq_image_symm {α β} (S : Set α) (f : β ≃ α) :
 #align set.preimage_equiv_eq_image_symm Set.preimage_equiv_eq_image_symm
 -/
 
-#print Equiv.subset_image /-
+#print Equiv.symm_image_subset /-
 @[simp]
-protected theorem subset_image {α β} (e : α ≃ β) (s : Set α) (t : Set β) :
+protected theorem symm_image_subset {α β} (e : α ≃ β) (s : Set α) (t : Set β) :
     e.symm '' t ⊆ s ↔ t ⊆ e '' s := by rw [image_subset_iff, e.image_eq_preimage]
-#align equiv.subset_image Equiv.subset_image
+#align equiv.subset_image Equiv.symm_image_subset
 -/
 
-#print Equiv.subset_image' /-
+#print Equiv.subset_symm_image /-
 @[simp]
-protected theorem subset_image' {α β} (e : α ≃ β) (s : Set α) (t : Set β) :
+protected theorem subset_symm_image {α β} (e : α ≃ β) (s : Set α) (t : Set β) :
     s ⊆ e.symm '' t ↔ e '' s ⊆ t :=
   calc
     s ⊆ e.symm '' t ↔ e.symm.symm '' s ⊆ t := by rw [e.symm.subset_image]
     _ ↔ e '' s ⊆ t := by rw [e.symm_symm]
-#align equiv.subset_image' Equiv.subset_image'
+#align equiv.subset_image' Equiv.subset_symm_image
 -/
 
 #print Equiv.symm_image_image /-

Mathbin/Order/CountableDenseLinearOrder.lean

@@ -182,7 +182,7 @@ def definedAtRight [DenselyOrdered α] [NoMinOrder α] [NoMaxOrder α] [Nonempty
     · change (a, b) ∈ f'.val.image _
       rwa [← Finset.mem_coe, Finset.coe_image, Equiv.image_eq_preimage]
     · change _ ⊆ f'.val.image _
-      rw [← Finset.coe_subset, Finset.coe_image, ← Equiv.subset_image]
+      rw [← Finset.coe_subset, Finset.coe_image, ← Equiv.symm_image_subset]
       change f.val.image _ ⊆ _ at hl 
       rwa [← Finset.coe_subset, Finset.coe_image] at hl 
 #align order.partial_iso.defined_at_right Order.PartialIso.definedAtRight

lake-manifest.json

@@ -58,19 +58,19 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "eb34a25d1bb216990c5985adbc40d4676a102d8a",
+   "rev": "7466efcfbec769a3a676842fdc02e03ec2bd0966",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "eb34a25d1bb216990c5985adbc40d4676a102d8a",
+   "inputRev": "7466efcfbec769a3a676842fdc02e03ec2bd0966",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/lean3port.git",
    "type": "git",
    "subDir": null,
-   "rev": "adc77c0937059117ab2e34dbb323e9b6fd737da1",
+   "rev": "4752295251fa81424dcd9675f21c55b47d708595",
    "name": "lean3port",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "adc77c0937059117ab2e34dbb323e9b6fd737da1",
+   "inputRev": "4752295251fa81424dcd9675f21c55b47d708595",
    "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-01-21-06"
+def tag : String := "nightly-2024-01-22-06"
 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"@"adc77c0937059117ab2e34dbb323e9b6fd737da1"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"4752295251fa81424dcd9675f21c55b47d708595"
 
 @[default_target]
 lean_lib Mathbin where