bump to nightly-2023-10-18-06

mathlib commit leanprover-community/mathlib@b1abe23

Archive/Imo/Imo2005Q4.lean

@@ -100,7 +100,7 @@ theorem imo2005_q4 {k : ℕ} (hk : 0 < k) : (∀ n : ℕ, 1 ≤ n → IsCoprime
   have hp₃ : 3 ≤ p :=
     by
     have : 2 ≠ p := by rwa [Nat.coprime_primes Nat.prime_two hp] at hp₂ 
-    apply Nat.lt_of_le_and_ne hp.two_le this
+    apply Nat.lt_of_le_of_ne hp.two_le this
   -- Testing the special property of `k` for the `p - 2`th term of the sequence, we see that `p` is
   -- coprime to `a (p - 2)`.
   have : IsCoprime (↑p) (a (p - 2)) :=

Mathbin/Analysis/NormedSpace/WeakDual.lean

@@ -250,7 +250,7 @@ theorem isClosed_image_coe_of_bounded_of_closed {s : Set (WeakDual 𝕜 E)}
 #print WeakDual.isCompact_of_bounded_of_closed /-
 theorem isCompact_of_bounded_of_closed [ProperSpace 𝕜] {s : Set (WeakDual 𝕜 E)}
     (hb : Bounded (Dual.toWeakDual ⁻¹' s)) (hc : IsClosed s) : IsCompact s :=
-  (Embedding.isCompact_iff_isCompact_image FunLike.coe_injective.embedding_induced).mpr <|
+  (Embedding.isCompact_iff FunLike.coe_injective.embedding_induced).mpr <|
     ContinuousLinearMap.isCompact_image_coe_of_bounded_of_closed_image hb <|
       isClosed_image_coe_of_bounded_of_closed hb hc
 #align weak_dual.is_compact_of_bounded_of_closed WeakDual.isCompact_of_bounded_of_closed

Mathbin/Combinatorics/SimpleGraph/Regularity/Bound.lean

@@ -187,7 +187,7 @@ theorem hundred_le_m [Nonempty α] (hPα : P.parts.card * 16 ^ P.parts.card ≤
 theorem a_add_one_le_four_pow_parts_card : a + 1 ≤ 4 ^ P.parts.card :=
   by
   have h : 1 ≤ 4 ^ P.parts.card := one_le_pow_of_one_le (by norm_num) _
-  rw [step_bound, ← Nat.div_div_eq_div_mul, ← Nat.le_sub_iff_right h, tsub_le_iff_left, ←
+  rw [step_bound, ← Nat.div_div_eq_div_mul, ← Nat.le_sub_iff_add_le h, tsub_le_iff_left, ←
     Nat.add_sub_assoc h]
   exact Nat.le_pred_of_lt (Nat.lt_div_mul_add h)
 #align szemeredi_regularity.a_add_one_le_four_pow_parts_card SzemerediRegularity.a_add_one_le_four_pow_parts_card

Mathbin/Data/Fin/Basic.lean

@@ -2938,7 +2938,7 @@ theorem succAbove_predAbove {p : Fin n} {i : Fin (n + 1)} (h : i ≠ p.cast_succ
     · simp
     · simp only [Fin.mk_eq_mk, Ne.def, Fin.castSucc_mk] at h 
       simp only [pred, Fin.mk_lt_mk, not_lt]
-      exact Nat.le_pred_of_lt (Nat.lt_of_le_and_ne H (Ne.symm h))
+      exact Nat.le_pred_of_lt (Nat.lt_of_le_of_ne H (Ne.symm h))
 #align fin.succ_above_pred_above Fin.succAbove_predAbove
 -/
 

Mathbin/Data/Int/Basic.lean

@@ -652,15 +652,15 @@ theorem mul_ediv_mul_of_pos {a : ℤ} (b c : ℤ) (H : 0 < a) : a * b / (a * c)
       rw [mul_neg, Int.div_neg, Int.div_neg] <;> apply congr_arg Neg.neg <;> apply this
   fun m k b =>
   match b, k with
-  | (n : ℕ), k => congr_arg ofNat (Nat.mul_div_mul _ _ m.succ_pos)
+  | (n : ℕ), k => congr_arg ofNat (Nat.mul_div_mul_left _ _ m.succ_pos)
   | -[n+1], 0 => by rw [Int.ofNat_zero, MulZeroClass.mul_zero, Int.div_zero, Int.div_zero]
   | -[n+1], k + 1 =>
     congr_arg negSucc <|
       show (m.succ * n + m) / (m.succ * k.succ) = n / k.succ
         by
         apply Nat.div_eq_of_lt_le
         · refine' le_trans _ (Nat.le_add_right _ _)
-          rw [← Nat.mul_div_mul _ _ m.succ_pos]
+          rw [← Nat.mul_div_mul_left _ _ m.succ_pos]
           apply Nat.div_mul_le_self
         · change m.succ * n.succ ≤ _
           rw [mul_left_comm]

Mathbin/Data/Nat/Basic.lean

@@ -802,11 +802,13 @@ protected theorem mul_div_cancel_left' {a b : ℕ} (Hd : a ∣ b) : a * (b / a)
 #align nat.mul_div_cancel_left' Nat.mul_div_cancel_left'
 -/
 
+/- warning: nat.mul_div_mul_left clashes with nat.mul_div_mul -> Nat.mul_div_mul_left
+Case conversion may be inaccurate. Consider using '#align nat.mul_div_mul_left Nat.mul_div_mul_leftₓ'. -/
 #print Nat.mul_div_mul_left /-
 --TODO: Update `nat.mul_div_mul` in the core?
 /-- Alias of `nat.mul_div_mul` -/
 protected theorem mul_div_mul_left (a b : ℕ) {c : ℕ} (hc : 0 < c) : c * a / (c * b) = a / b :=
-  Nat.mul_div_mul a b hc
+  Nat.mul_div_mul_left a b hc
 #align nat.mul_div_mul_left Nat.mul_div_mul_left
 -/
 

Mathbin/Data/Nat/Choose/Multinomial.lean

@@ -99,7 +99,7 @@ theorem multinomial_insert [DecidableEq α] (h : a ∉ s) :
   rw [div_mul_div_comm ((f a).factorial_mul_factorial_dvd_factorial_add (s.sum f))
       (prod_factorial_dvd_factorial_sum _ _),
     mul_comm (f a)! (s.sum f)!, mul_assoc, mul_comm _ (s.sum f)!,
-    Nat.mul_div_mul _ _ (factorial_pos _)]
+    Nat.mul_div_mul_left _ _ (factorial_pos _)]
 #align nat.multinomial_insert Nat.multinomial_insert
 -/
 

Mathbin/Data/Nat/Order/Basic.lean

@@ -527,7 +527,7 @@ theorem div_mul_div_le_div (m n k : ℕ) : m / k * n / m ≤ n / k :=
         Nat.div_le_div_right (by rw [mul_comm] <;> exact mul_div_le_mul_div_assoc _ _ _)
       _ = n / k := by
         rw [Nat.div_div_eq_div_mul, mul_comm n, mul_comm k,
-          Nat.mul_div_mul _ _ (Nat.pos_of_ne_zero hm0)]
+          Nat.mul_div_mul_left _ _ (Nat.pos_of_ne_zero hm0)]
 #align nat.div_mul_div_le_div Nat.div_mul_div_le_div
 -/
 

Mathbin/Logic/Function/Basic.lean

@@ -956,10 +956,10 @@ def FactorsThrough (g : α → γ) (f : α → β) : Prop :=
 #align function.factors_through Function.FactorsThrough
 -/
 
-#print Function.Injective.FactorsThrough /-
-theorem Injective.FactorsThrough (hf : Injective f) (g : α → γ) : g.FactorsThrough f := fun a b h =>
+#print Function.Injective.factorsThrough /-
+theorem Injective.factorsThrough (hf : Injective f) (g : α → γ) : g.FactorsThrough f := fun a b h =>
   congr_arg g (hf h)
-#align function.injective.factors_through Function.Injective.FactorsThrough
+#align function.injective.factors_through Function.Injective.factorsThrough
 -/
 
 #print Function.extend_def /-

Mathbin/NumberTheory/FermatPsp.lean

@@ -72,7 +72,7 @@ namespace Nat.FermatPsp
 
 #print Nat.decidableProbablePrime /-
 instance decidableProbablePrime (n b : ℕ) : Decidable (ProbablePrime n b) :=
-  Nat.decidableDvd _ _
+  Nat.decidable_dvd _ _
 #align fermat_psp.decidable_probable_prime Nat.decidableProbablePrime
 -/
 

Mathbin/Topology/Algebra/Order/LiminfLimsup.lean

@@ -653,7 +653,7 @@ theorem limsup_eq_tendsto_sum_indicator_nat_atTop (s : ℕ → Set α) :
         Finset.sum_lt_sum (fun m _ => Set.indicator_nonneg (fun _ _ => zero_le_one) _)
           ⟨j - 1,
             Finset.mem_Ico.2
-              ⟨(Nat.le_sub_iff_right (le_trans ((le_add_iff_nonneg_left _).2 zero_le') hj₁)).2 hj₁,
+              ⟨(Nat.le_sub_iff_add_le (le_trans ((le_add_iff_nonneg_left _).2 zero_le') hj₁)).2 hj₁,
                 lt_of_le_of_lt (Nat.sub_le _ _) j.lt_succ_self⟩,
             _⟩
       rw [Nat.sub_add_cancel (le_trans ((le_add_iff_nonneg_left _).2 zero_le') hj₁),

Mathbin/Topology/Homeomorph.lean

@@ -344,7 +344,7 @@ protected theorem secondCountableTopology [TopologicalSpace.SecondCountableTopol
 
 #print Homeomorph.isCompact_image /-
 theorem isCompact_image {s : Set α} (h : α ≃ₜ β) : IsCompact (h '' s) ↔ IsCompact s :=
-  h.Embedding.isCompact_iff_isCompact_image.symm
+  h.Embedding.isCompact_iff.symm
 #align homeomorph.is_compact_image Homeomorph.isCompact_image
 -/
 

Mathbin/Topology/SubsetProperties.lean

@@ -1156,14 +1156,13 @@ theorem Inducing.isCompact_iff {f : α → β} (hf : Inducing f) {s : Set α} :
 #align inducing.is_compact_iff Inducing.isCompact_iff
 -/
 
-#print Embedding.isCompact_iff_isCompact_image /-
+#print Embedding.isCompact_iff /-
 /-- If `f : α → β` is an `embedding` (or more generally, an `inducing` map, see
 `inducing.is_compact_iff`), then the image `f '' s` of a set `s` is compact if and only if the set
 `s` is closed. -/
-theorem Embedding.isCompact_iff_isCompact_image {f : α → β} (hf : Embedding f) :
-    IsCompact s ↔ IsCompact (f '' s) :=
+theorem Embedding.isCompact_iff {f : α → β} (hf : Embedding f) : IsCompact s ↔ IsCompact (f '' s) :=
   hf.to_inducing.isCompact_iff.symm
-#align embedding.is_compact_iff_is_compact_image Embedding.isCompact_iff_isCompact_image
+#align embedding.is_compact_iff_is_compact_image Embedding.isCompact_iff
 -/
 
 #print ClosedEmbedding.isCompact_preimage /-
@@ -1186,16 +1185,16 @@ theorem ClosedEmbedding.tendsto_cocompact {f : α → β} (hf : ClosedEmbedding
 #align closed_embedding.tendsto_cocompact ClosedEmbedding.tendsto_cocompact
 -/
 
-#print isCompact_iff_isCompact_in_subtype /-
-theorem isCompact_iff_isCompact_in_subtype {p : α → Prop} {s : Set { a // p a }} :
+#print Subtype.isCompact_iff /-
+theorem Subtype.isCompact_iff {p : α → Prop} {s : Set { a // p a }} :
     IsCompact s ↔ IsCompact ((coe : _ → α) '' s) :=
-  embedding_subtype_val.isCompact_iff_isCompact_image
-#align is_compact_iff_is_compact_in_subtype isCompact_iff_isCompact_in_subtype
+  embedding_subtype_val.isCompact_iff
+#align is_compact_iff_is_compact_in_subtype Subtype.isCompact_iff
 -/
 
 #print isCompact_iff_isCompact_univ /-
 theorem isCompact_iff_isCompact_univ {s : Set α} : IsCompact s ↔ IsCompact (univ : Set s) := by
-  rw [isCompact_iff_isCompact_in_subtype, image_univ, Subtype.range_coe] <;> rfl
+  rw [Subtype.isCompact_iff, image_univ, Subtype.range_coe] <;> rfl
 #align is_compact_iff_is_compact_univ isCompact_iff_isCompact_univ
 -/
 

lake-manifest.json

@@ -4,18 +4,18 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "f1eae6ec09a681742597fe0665246e6d323284a6",
+    "rev": "4d8c8b13886ce2e5add885934ea7f445eb533f2c",
     "opts": {},
     "name": "lean3port",
-    "inputRev?": "f1eae6ec09a681742597fe0665246e6d323284a6",
+    "inputRev?": "4d8c8b13886ce2e5add885934ea7f445eb533f2c",
     "inherited": false}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "26eb2b0ade1d7e252d07b13ea9253f9c8652facd",
+    "rev": "4de9b983b6933d0fac3dacd97efd1744a3d5badb",
     "opts": {},
     "name": "mathlib",
-    "inputRev?": "26eb2b0ade1d7e252d07b13ea9253f9c8652facd",
+    "inputRev?": "4de9b983b6933d0fac3dacd97efd1744a3d5badb",
     "inherited": true}},
   {"git":
    {"url": "https://github.com/gebner/quote4",

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-10-17-06"
+def tag : String := "nightly-2023-10-18-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"@"f1eae6ec09a681742597fe0665246e6d323284a6"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"4d8c8b13886ce2e5add885934ea7f445eb533f2c"
 
 @[default_target]
 lean_lib Mathbin where

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.2.0-rc2
+leanprover/lean4:v4.2.0-rc3