bump to nightly-2023-11-06-06

mathlib commit leanprover-community/mathlib@65a1391

Mathbin/Combinatorics/Composition.lean

@@ -414,7 +414,7 @@ theorem sizeUpTo_index_le (j : Fin n) : c.sizeUpTo (c.index j) ≤ j :=
   have i₁_succ : i₁.succ = i := Nat.succ_pred_eq_of_pos i_pos
   have := Nat.find_min (c.index_exists j.2) i₁_lt_i
   simp [lt_trans i₁_lt_i (c.index j).2, i₁_succ] at this 
-  exact Nat.lt_le_antisymm H this
+  exact Nat.lt_le_asymm H this
 #align composition.size_up_to_index_le Composition.sizeUpTo_index_le
 -/
 

Mathbin/Combinatorics/SimpleGraph/Clique.lean

@@ -354,7 +354,7 @@ theorem CliqueFree.anti (h : G ≤ H) : H.CliqueFree n → G.CliqueFree n :=
 theorem cliqueFree_of_card_lt [Fintype α] (hc : card α < n) : G.CliqueFree n :=
   by
   by_contra h
-  refine' Nat.lt_le_antisymm hc _
+  refine' Nat.lt_le_asymm hc _
   rw [clique_free_iff, not_isEmpty_iff] at h 
   simpa using Fintype.card_le_of_embedding h.some.to_embedding
 #align simple_graph.clique_free_of_card_lt SimpleGraph.cliqueFree_of_card_lt

Mathbin/Combinatorics/SimpleGraph/Coloring.lean

@@ -452,7 +452,7 @@ theorem chromaticNumber_eq_card_of_forall_surj [Fintype α] (C : G.Coloring α)
     change Function.Surjective (f ∘ C') at h 
     have h1 : Function.Surjective f := Function.Surjective.of_comp h
     have h2 := Fintype.card_le_of_surjective _ h1
-    exact Nat.lt_le_antisymm hc h2
+    exact Nat.lt_le_asymm hc h2
 #align simple_graph.chromatic_number_eq_card_of_forall_surj SimpleGraph.chromaticNumber_eq_card_of_forall_surj
 -/
 
@@ -568,7 +568,7 @@ protected theorem Colorable.cliqueFree {n m : ℕ} (hc : G.Colorable n) (hm : n
   by_contra h
   simp only [clique_free, is_n_clique_iff, Classical.not_forall, Classical.not_not] at h 
   obtain ⟨s, h, rfl⟩ := h
-  exact Nat.lt_le_antisymm hm (h.card_le_of_colorable hc)
+  exact Nat.lt_le_asymm hm (h.card_le_of_colorable hc)
 #align simple_graph.colorable.clique_free SimpleGraph.Colorable.cliqueFree
 -/
 

Mathbin/Data/Nat/Prime.lean

@@ -855,7 +855,7 @@ theorem coprime_or_dvd_of_prime {p} (pp : Prime p) (i : ℕ) : Coprime p i ∨ p
 
 #print Nat.coprime_of_lt_prime /-
 theorem coprime_of_lt_prime {n p} (n_pos : 0 < n) (hlt : n < p) (pp : Prime p) : Coprime p n :=
-  (coprime_or_dvd_of_prime pp n).resolve_right fun h => lt_le_antisymm hlt (le_of_dvd n_pos h)
+  (coprime_or_dvd_of_prime pp n).resolve_right fun h => lt_le_asymm hlt (le_of_dvd n_pos h)
 #align nat.coprime_of_lt_prime Nat.coprime_of_lt_prime
 -/
 

Mathbin/NumberTheory/Fermat4.lean

@@ -111,7 +111,7 @@ theorem coprime_of_minimal {a b c : ℤ} (h : Minimal a b c) : IsCoprime a b :=
   obtain ⟨c1, rfl⟩ := hpc
   have hf : Fermat42 a1 b1 c1 :=
     (Fermat42.mul (int.coe_nat_ne_zero.mpr (Nat.Prime.ne_zero hp))).mpr h.1
-  apply Nat.le_lt_antisymm (h.2 _ _ _ hf)
+  apply Nat.le_lt_asymm (h.2 _ _ _ hf)
   rw [Int.natAbs_mul, lt_mul_iff_one_lt_left, Int.natAbs_pow, Int.natAbs_ofNat]
   · exact Nat.one_lt_pow _ _ zero_lt_two (Nat.Prime.one_lt hp)
   · exact Nat.pos_of_ne_zero (Int.natAbs_ne_zero_of_ne_zero (NeZero hf))

lake-manifest.json

@@ -4,26 +4,18 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "3f9df728de9b6fef40a11c6db4ec44342816cbc8",
+    "rev": "f04b3b878062fa768a214094655381421a9f75a7",
     "opts": {},
     "name": "lean3port",
-    "inputRev?": "3f9df728de9b6fef40a11c6db4ec44342816cbc8",
+    "inputRev?": "f04b3b878062fa768a214094655381421a9f75a7",
     "inherited": false}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "e853cefc93e6f1f11de861ed05b95973d3b4f397",
+    "rev": "5f84b04fbc1600f1ca5b6e466cc318ba177810a5",
     "opts": {},
     "name": "mathlib",
-    "inputRev?": "e853cefc93e6f1f11de861ed05b95973d3b4f397",
-    "inherited": true}},
-  {"git":
-   {"url": "https://github.com/leanprover/std4",
-    "subDir?": null,
-    "rev": "9bfbd2a12ee9cf2e159a8a6b4d1ef6c149728f66",
-    "opts": {},
-    "name": "std",
-    "inputRev?": "main",
+    "inputRev?": "5f84b04fbc1600f1ca5b6e466cc318ba177810a5",
     "inherited": true}},
   {"git":
    {"url": "https://github.com/leanprover-community/quote4",
@@ -56,5 +48,13 @@
     "opts": {},
     "name": "aesop",
     "inputRev?": "master",
+    "inherited": true}},
+  {"git":
+   {"url": "https://github.com/leanprover/std4",
+    "subDir?": null,
+    "rev": "efa34980940840cde7f70451da58c0bd3c5eeb67",
+    "opts": {},
+    "name": "std",
+    "inputRev?": "main",
     "inherited": true}}],
  "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-2023-11-05-06"
+def tag : String := "nightly-2023-11-06-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"@"3f9df728de9b6fef40a11c6db4ec44342816cbc8"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"f04b3b878062fa768a214094655381421a9f75a7"
 
 @[default_target]
 lean_lib Mathbin where