bump to nightly-2024-02-09-08

mathlib commit leanprover-community/mathlib@65a1391

Mathbin/CategoryTheory/Closed/Monoidal.lean

@@ -429,7 +429,7 @@ theorem ofEquiv_curry_def (F : MonoidalFunctor C D) [IsEquivalence F.toFunctor]
       (F.1.1.Adjunction.homEquiv Y ((ihom _).obj _))
         (MonoidalClosed.curry
           (F.1.1.inv.Adjunction.homEquiv (F.1.1.obj X ⊗ F.1.1.obj Y) Z
-            ((compInvIso (F.commTensorLeft X)).Hom.app Y ≫ f))) :=
+            ((CategoryTheory.Iso.compInvIso (F.commTensorLeft X)).Hom.app Y ≫ f))) :=
   rfl
 #align category_theory.monoidal_closed.of_equiv_curry_def CategoryTheory.MonoidalClosed.ofEquiv_curry_def
 -/
@@ -445,7 +445,7 @@ theorem ofEquiv_uncurry_def (F : MonoidalFunctor C D) [IsEquivalence F.toFunctor
     [h : MonoidalClosed D] {X Y Z : C}
     (f : Y ⟶ (@ihom _ _ _ X <| (MonoidalClosed.ofEquiv F).1 X).obj Z) :
     @MonoidalClosed.uncurry _ _ _ _ _ _ ((MonoidalClosed.ofEquiv F).1 _) f =
-      (compInvIso (F.commTensorLeft X)).inv.app Y ≫
+      (CategoryTheory.Iso.compInvIso (F.commTensorLeft X)).inv.app Y ≫
         (F.1.1.inv.Adjunction.homEquiv (F.1.1.obj X ⊗ F.1.1.obj Y) Z).symm
           (MonoidalClosed.uncurry
             ((F.1.1.Adjunction.homEquiv Y ((ihom (F.1.1.obj X)).obj (F.1.1.obj Z))).symm f)) :=

Mathbin/CategoryTheory/Functor/InvIsos.lean

@@ -29,38 +29,38 @@ variable {A : Type u₁} [Category.{v₁} A] {B : Type u₂} [Category.{v₂} B]
 
 variable {F : A ⥤ C} {G : A ⥤ B} {H : B ⥤ C}
 
-#print CategoryTheory.compInvIso /-
+#print CategoryTheory.Iso.compInvIso /-
 /-- Construct an isomorphism `F ⋙ H.inv ≅ G` from an isomorphism `F ≅ G ⋙ H`. -/
 @[simps]
-def compInvIso [h : IsEquivalence H] (i : F ≅ G ⋙ H) : F ⋙ H.inv ≅ G :=
+def CategoryTheory.Iso.compInvIso [h : IsEquivalence H] (i : F ≅ G ⋙ H) : F ⋙ H.inv ≅ G :=
   isoWhiskerRight i H.inv ≪≫
     associator G H H.inv ≪≫ isoWhiskerLeft G h.unitIso.symm ≪≫ eqToIso (Functor.comp_id G)
-#align category_theory.comp_inv_iso CategoryTheory.compInvIso
+#align category_theory.comp_inv_iso CategoryTheory.Iso.compInvIso
 -/
 
-#print CategoryTheory.isoCompInv /-
+#print CategoryTheory.Iso.isoCompInv /-
 /-- Construct an isomorphism `G ≅ F ⋙ H.inv` from an isomorphism `G ⋙ H ≅ F`. -/
 @[simps]
-def isoCompInv [h : IsEquivalence H] (i : G ⋙ H ≅ F) : G ≅ F ⋙ H.inv :=
-  (compInvIso i.symm).symm
-#align category_theory.iso_comp_inv CategoryTheory.isoCompInv
+def CategoryTheory.Iso.isoCompInv [h : IsEquivalence H] (i : G ⋙ H ≅ F) : G ≅ F ⋙ H.inv :=
+  (CategoryTheory.Iso.compInvIso i.symm).symm
+#align category_theory.iso_comp_inv CategoryTheory.Iso.isoCompInv
 -/
 
-#print CategoryTheory.invCompIso /-
+#print CategoryTheory.Iso.invCompIso /-
 /-- Construct an isomorphism `G.inv ⋙ F ≅ H` from an isomorphism `F ≅ G ⋙ H`. -/
 @[simps]
-def invCompIso [h : IsEquivalence G] (i : F ≅ G ⋙ H) : G.inv ⋙ F ≅ H :=
+def CategoryTheory.Iso.invCompIso [h : IsEquivalence G] (i : F ≅ G ⋙ H) : G.inv ⋙ F ≅ H :=
   isoWhiskerLeft G.inv i ≪≫
     (associator G.inv G H).symm ≪≫ isoWhiskerRight h.counitIso H ≪≫ eqToIso (Functor.id_comp H)
-#align category_theory.inv_comp_iso CategoryTheory.invCompIso
+#align category_theory.inv_comp_iso CategoryTheory.Iso.invCompIso
 -/
 
-#print CategoryTheory.isoInvComp /-
+#print CategoryTheory.Iso.isoInvComp /-
 /-- Construct an isomorphism `H ≅ G.inv ⋙ F` from an isomorphism `G ⋙ H ≅ F`. -/
 @[simps]
-def isoInvComp [h : IsEquivalence G] (i : G ⋙ H ≅ F) : H ≅ G.inv ⋙ F :=
-  (invCompIso i.symm).symm
-#align category_theory.iso_inv_comp CategoryTheory.isoInvComp
+def CategoryTheory.Iso.isoInvComp [h : IsEquivalence G] (i : G ⋙ H ≅ F) : H ≅ G.inv ⋙ F :=
+  (CategoryTheory.Iso.invCompIso i.symm).symm
+#align category_theory.iso_inv_comp CategoryTheory.Iso.isoInvComp
 -/
 
 end CategoryTheory

Mathbin/Combinatorics/HalesJewett.lean

@@ -312,6 +312,7 @@ private theorem exists_mono_in_high_dimension' :
       -- By choice of `ι`, `C'` either has `r` color-focused lines or a monochromatic line.
       specialize hι C'
       rcases hι with (⟨s, sr⟩ | _)
+      -- By above, we are done if `C'` has a monochromatic line.
       on_goal 2 => exact Or.inr (mono_of_mono hι)
       -- Here we assume `C'` has `r` color focused lines. We split into cases depending on whether one of
       -- these `r` lines has the same color as the focus point.

Mathbin/Data/Nat/Basic.lean

@@ -1183,12 +1183,12 @@ instance decidableForallFin {n : ℕ} (P : Fin n → Prop) [H : DecidablePred P]
 #align nat.decidable_forall_fin Nat.decidableForallFin
 -/
 
-#print Nat.decidableBallLe /-
-instance decidableBallLe (n : ℕ) (P : ∀ k ≤ n, Prop) [H : ∀ n h, Decidable (P n h)] :
+#print Nat.decidableBallLE /-
+instance decidableBallLE (n : ℕ) (P : ∀ k ≤ n, Prop) [H : ∀ n h, Decidable (P n h)] :
     Decidable (∀ n h, P n h) :=
   decidable_of_iff (∀ (k) (h : k < succ n), P k (le_of_lt_succ h))
     ⟨fun a k h => a k (lt_succ_of_le h), fun a k h => a k _⟩
-#align nat.decidable_ball_le Nat.decidableBallLe
+#align nat.decidable_ball_le Nat.decidableBallLE
 -/
 
 #print Nat.decidableExistsLT /-
@@ -1201,11 +1201,11 @@ instance decidableExistsLT {P : ℕ → Prop} [h : DecidablePred P] :
 #align nat.decidable_exists_lt Nat.decidableExistsLT
 -/
 
-#print Nat.decidableExistsLe /-
-instance decidableExistsLe {P : ℕ → Prop} [h : DecidablePred P] :
+#print Nat.decidableExistsLE /-
+instance decidableExistsLE {P : ℕ → Prop} [h : DecidablePred P] :
     DecidablePred fun n => ∃ m : ℕ, m ≤ n ∧ P m := fun n =>
   decidable_of_iff (∃ m, m < n + 1 ∧ P m) (exists_congr fun x => and_congr_left' lt_succ_iff)
-#align nat.decidable_exists_le Nat.decidableExistsLe
+#align nat.decidable_exists_le Nat.decidableExistsLE
 -/
 
 end Nat

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "e752d2063b323bf5192d2dca577afa3cb3008677",
+   "rev": "2a1b7546b2df0f8e65a70d3b228c30d91752acc4",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,7 +13,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "1c88406514a636d241903e2e288d21dc6d861e01",
+   "rev": "190ec9abbc4cd43b1b6a1401722c0b54418a98b0",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "6beed82dcfbb7731d173cd517675df27d62ad0f4",
+   "rev": "4746cab6320a0d87ec951105ccd42e656fb15e89",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -49,7 +49,7 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "8079d2d1d0e073bde42eab159c24f4c2d0d3a871",
+   "rev": "d95fb9ca08220089beb3ab486d0879edaad3f497",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,19 +58,19 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "963467adad9608bd1e7e7723d362a689588aa09c",
+   "rev": "62126e3cbdb13e8ddd676b456cea999cd2e274bf",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "963467adad9608bd1e7e7723d362a689588aa09c",
+   "inputRev": "62126e3cbdb13e8ddd676b456cea999cd2e274bf",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/lean3port.git",
    "type": "git",
    "subDir": null,
-   "rev": "d5b75516d0373192cd2a90dbd740bd6edc9b7c1c",
+   "rev": "e91b66d7b1208456370ec4fa1666a6828b997c8f",
    "name": "lean3port",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "d5b75516d0373192cd2a90dbd740bd6edc9b7c1c",
+   "inputRev": "e91b66d7b1208456370ec4fa1666a6828b997c8f",
    "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-02-08-08"
+def tag : String := "nightly-2024-02-09-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"@"d5b75516d0373192cd2a90dbd740bd6edc9b7c1c"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"e91b66d7b1208456370ec4fa1666a6828b997c8f"
 
 @[default_target]
 lean_lib Mathbin where