bump to nightly-2023-07-07-15

mathlib commit leanprover-community/mathlib@8905e5e

Mathbin/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean

@@ -49,27 +49,33 @@ open scoped unitInterval
 
 namespace unitInterval
 
+#print unitInterval.path01 /-
 /-- The path 0 ⟶ 1 in I -/
 def path01 : Path (0 : I) 1 where
   toFun := id
   source' := rfl
   target' := rfl
 #align unit_interval.path01 unitInterval.path01
+-/
 
+#print unitInterval.upath01 /-
 /-- The path 0 ⟶ 1 in ulift I -/
 def upath01 : Path (ULift.up 0 : ULift.{u} I) (ULift.up 1)
     where
   toFun := ULift.up
   source' := rfl
   target' := rfl
 #align unit_interval.upath01 unitInterval.upath01
+-/
 
 attribute [local instance] Path.Homotopic.setoid
 
+#print unitInterval.uhpath01 /-
 /-- The homotopy path class of 0 → 1 in `ulift I` -/
 def uhpath01 : @fromTop (TopCat.of <| ULift.{u} I) (ULift.up (0 : I)) ⟶ fromTop (ULift.up 1) :=
   ⟦upath01⟧
 #align unit_interval.uhpath01 unitInterval.uhpath01
+-/
 
 end unitInterval
 
@@ -81,33 +87,41 @@ attribute [local instance] Path.Homotopic.setoid
 
 section Casts
 
+#print ContinuousMap.Homotopy.hcast /-
 /-- Abbreviation for `eq_to_hom` that accepts points in a topological space -/
 abbrev hcast {X : TopCat} {x₀ x₁ : X} (hx : x₀ = x₁) : fromTop x₀ ⟶ fromTop x₁ :=
   eqToHom hx
 #align continuous_map.homotopy.hcast ContinuousMap.Homotopy.hcast
+-/
 
+#print ContinuousMap.Homotopy.hcast_def /-
 @[simp]
 theorem hcast_def {X : TopCat} {x₀ x₁ : X} (hx₀ : x₀ = x₁) : hcast hx₀ = eqToHom hx₀ :=
   rfl
 #align continuous_map.homotopy.hcast_def ContinuousMap.Homotopy.hcast_def
+-/
 
 variable {X₁ X₂ Y : TopCat.{u}} {f : C(X₁, Y)} {g : C(X₂, Y)} {x₀ x₁ : X₁} {x₂ x₃ : X₂}
   {p : Path x₀ x₁} {q : Path x₂ x₃} (hfg : ∀ t, f (p t) = g (q t))
 
+#print ContinuousMap.Homotopy.heq_path_of_eq_image /-
 /-- If `f(p(t) = g(q(t))` for two paths `p` and `q`, then the induced path homotopy classes
 `f(p)` and `g(p)` are the same as well, despite having a priori different types -/
-theorem hEq_path_of_eq_image : HEq ((πₘ f).map ⟦p⟧) ((πₘ g).map ⟦q⟧) := by
+theorem heq_path_of_eq_image : HEq ((πₘ f).map ⟦p⟧) ((πₘ g).map ⟦q⟧) := by
   simp only [map_eq, ← Path.Homotopic.map_lift]; apply Path.Homotopic.hpath_hext; exact hfg
-#align continuous_map.homotopy.heq_path_of_eq_image ContinuousMap.Homotopy.hEq_path_of_eq_image
+#align continuous_map.homotopy.heq_path_of_eq_image ContinuousMap.Homotopy.heq_path_of_eq_image
+-/
 
 private theorem start_path : f x₀ = g x₂ := by convert hfg 0 <;> simp only [Path.source]
 
 private theorem end_path : f x₁ = g x₃ := by convert hfg 1 <;> simp only [Path.target]
 
+#print ContinuousMap.Homotopy.eq_path_of_eq_image /-
 theorem eq_path_of_eq_image :
     (πₘ f).map ⟦p⟧ = hcast (start_path hfg) ≫ (πₘ g).map ⟦q⟧ ≫ hcast (end_path hfg).symm := by
   rw [functor.conj_eq_to_hom_iff_heq]; exact heq_path_of_eq_image hfg
 #align continuous_map.homotopy.eq_path_of_eq_image ContinuousMap.Homotopy.eq_path_of_eq_image
+-/
 
 end Casts
 
@@ -138,35 +152,46 @@ many of the paths do not have defeq starting/ending points, so we end up needing
 -/
 
 
+#print ContinuousMap.Homotopy.uliftMap /-
 /-- Interpret a homotopy `H : C(I × X, Y) as a map C(ulift I × X, Y) -/
 def uliftMap : C(TopCat.of (ULift.{u} I × X), Y) :=
   ⟨fun x => H (x.1.down, x.2),
     H.Continuous.comp ((continuous_induced_dom.comp continuous_fst).prod_mk continuous_snd)⟩
 #align continuous_map.homotopy.ulift_map ContinuousMap.Homotopy.uliftMap
+-/
 
+#print ContinuousMap.Homotopy.ulift_apply /-
 @[simp]
-theorem uLift_apply (i : ULift.{u} I) (x : X) : H.uliftMap (i, x) = H (i.down, x) :=
+theorem ulift_apply (i : ULift.{u} I) (x : X) : H.uliftMap (i, x) = H (i.down, x) :=
   rfl
-#align continuous_map.homotopy.ulift_apply ContinuousMap.Homotopy.uLift_apply
+#align continuous_map.homotopy.ulift_apply ContinuousMap.Homotopy.ulift_apply
+-/
 
+#print ContinuousMap.Homotopy.prodToProdTopI /-
 /-- An abbreviation for `prod_to_prod_Top`, with some types already in place to help the
  typechecker. In particular, the first path should be on the ulifted unit interval. -/
 abbrev prodToProdTopI {a₁ a₂ : TopCat.of (ULift I)} {b₁ b₂ : X} (p₁ : fromTop a₁ ⟶ fromTop a₂)
     (p₂ : fromTop b₁ ⟶ fromTop b₂) :=
   @CategoryTheory.Functor.map _ _ _ _ (prodToProdTop (TopCat.of <| ULift I) X) (a₁, b₁) (a₂, b₂)
     (p₁, p₂)
 #align continuous_map.homotopy.prod_to_prod_Top_I ContinuousMap.Homotopy.prodToProdTopI
+-/
 
+#print ContinuousMap.Homotopy.diagonalPath /-
 /-- The diagonal path `d` of a homotopy `H` on a path `p` -/
 def diagonalPath : fromTop (H (0, x₀)) ⟶ fromTop (H (1, x₁)) :=
   (πₘ H.uliftMap).map (prodToProdTopI uhpath01 p)
 #align continuous_map.homotopy.diagonal_path ContinuousMap.Homotopy.diagonalPath
+-/
 
+#print ContinuousMap.Homotopy.diagonalPath' /-
 /-- The diagonal path, but starting from `f x₀` and going to `g x₁` -/
 def diagonalPath' : fromTop (f x₀) ⟶ fromTop (g x₁) :=
   hcast (H.apply_zero x₀).symm ≫ H.diagonalPath p ≫ hcast (H.apply_one x₁)
 #align continuous_map.homotopy.diagonal_path' ContinuousMap.Homotopy.diagonalPath'
+-/
 
+#print ContinuousMap.Homotopy.apply_zero_path /-
 /-- Proof that `f(p) = H(0 ⟶ 0, p)`, with the appropriate casts -/
 theorem apply_zero_path :
     (πₘ f).map p =
@@ -178,7 +203,9 @@ theorem apply_zero_path :
   apply @eq_path_of_eq_image _ _ _ _ H.ulift_map _ _ _ _ _ ((Path.refl (ULift.up _)).Prod p')
   simp
 #align continuous_map.homotopy.apply_zero_path ContinuousMap.Homotopy.apply_zero_path
+-/
 
+#print ContinuousMap.Homotopy.apply_one_path /-
 /-- Proof that `g(p) = H(1 ⟶ 1, p)`, with the appropriate casts -/
 theorem apply_one_path :
     (πₘ g).map p =
@@ -190,7 +217,9 @@ theorem apply_one_path :
   apply @eq_path_of_eq_image _ _ _ _ H.ulift_map _ _ _ _ _ ((Path.refl (ULift.up _)).Prod p')
   simp
 #align continuous_map.homotopy.apply_one_path ContinuousMap.Homotopy.apply_one_path
+-/
 
+#print ContinuousMap.Homotopy.evalAt_eq /-
 /-- Proof that `H.eval_at x = H(0 ⟶ 1, x ⟶ x)`, with the appropriate casts -/
 theorem evalAt_eq (x : X) :
     ⟦H.evalAt x⟧ =
@@ -203,7 +232,9 @@ theorem evalAt_eq (x : X) :
     Path.Homotopic.map_lift]
   apply Path.Homotopic.hpath_hext; intro; rfl
 #align continuous_map.homotopy.eval_at_eq ContinuousMap.Homotopy.evalAt_eq
+-/
 
+#print ContinuousMap.Homotopy.eq_diag_path /-
 -- Finally, we show `d = f(p) ≫ H₁ = H₀ ≫ g(p)`
 theorem eq_diag_path :
     (πₘ f).map p ≫ ⟦H.evalAt x₁⟧ = H.diagonalPath' p ∧
@@ -213,6 +244,7 @@ theorem eq_diag_path :
   dsimp only [prod_to_prod_Top_I]
   constructor <;> · slice_lhs 2 5 => simp [← CategoryTheory.Functor.map_comp]; rfl
 #align continuous_map.homotopy.eq_diag_path ContinuousMap.Homotopy.eq_diag_path
+-/
 
 end ContinuousMap.Homotopy
 
@@ -226,18 +258,21 @@ attribute [local instance] Path.Homotopic.setoid
 
 variable {X Y : TopCat.{u}} {f g : C(X, Y)} (H : ContinuousMap.Homotopy f g)
 
+#print FundamentalGroupoidFunctor.homotopicMapsNatIso /-
 /-- Given a homotopy H : f ∼ g, we have an associated natural isomorphism between the induced
 functors `f` and `g` -/
 def homotopicMapsNatIso : πₘ f ⟶ πₘ g
     where
   app x := ⟦H.evalAt x⟧
   naturality' x y p := by rw [(H.eq_diag_path p).1, (H.eq_diag_path p).2]
 #align fundamental_groupoid_functor.homotopic_maps_nat_iso FundamentalGroupoidFunctor.homotopicMapsNatIso
+-/
 
 instance : IsIso (homotopicMapsNatIso H) := by apply nat_iso.is_iso_of_is_iso_app
 
 open scoped ContinuousMap
 
+#print FundamentalGroupoidFunctor.equivOfHomotopyEquiv /-
 /-- Homotopy equivalent topological spaces have equivalent fundamental groupoids. -/
 def equivOfHomotopyEquiv (hequiv : X ≃ₕ Y) : πₓ X ≌ πₓ Y :=
   by
@@ -248,6 +283,7 @@ def equivOfHomotopyEquiv (hequiv : X ≃ₕ Y) : πₓ X ≌ πₓ Y :=
   · convert as_iso (homotopic_maps_nat_iso hequiv.right_inv.some)
     exacts [(π.map_comp _ _).symm, (π.map_id Y).symm]
 #align fundamental_groupoid_functor.equiv_of_homotopy_equiv FundamentalGroupoidFunctor.equivOfHomotopyEquiv
+-/
 
 end FundamentalGroupoidFunctor
 

Mathbin/CategoryTheory/EqToHom.lean

@@ -190,18 +190,18 @@ theorem ext {F G : C ⥤ D} (h_obj : ∀ X, F.obj X = G.obj X)
 #align category_theory.functor.ext CategoryTheory.Functor.ext
 -/
 
-#print CategoryTheory.Functor.conj_eqToHom_iff_hEq /-
+#print CategoryTheory.Functor.conj_eqToHom_iff_heq /-
 /-- Two morphisms are conjugate via eq_to_hom if and only if they are heterogeneously equal. -/
-theorem conj_eqToHom_iff_hEq {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) (h : W = Y) (h' : X = Z) :
+theorem conj_eqToHom_iff_heq {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) (h : W = Y) (h' : X = Z) :
     f = eqToHom h ≫ g ≫ eqToHom h'.symm ↔ HEq f g := by cases h; cases h'; simp
-#align category_theory.functor.conj_eq_to_hom_iff_heq CategoryTheory.Functor.conj_eqToHom_iff_hEq
+#align category_theory.functor.conj_eq_to_hom_iff_heq CategoryTheory.Functor.conj_eqToHom_iff_heq
 -/
 
 #print CategoryTheory.Functor.hext /-
 /-- Proving equality between functors using heterogeneous equality. -/
 theorem hext {F G : C ⥤ D} (h_obj : ∀ X, F.obj X = G.obj X)
     (h_map : ∀ (X Y) (f : X ⟶ Y), HEq (F.map f) (G.map f)) : F = G :=
-  Functor.ext h_obj fun _ _ f => (conj_eqToHom_iff_hEq _ _ (h_obj _) (h_obj _)).2 <| h_map _ _ f
+  Functor.ext h_obj fun _ _ f => (conj_eqToHom_iff_heq _ _ (h_obj _) (h_obj _)).2 <| h_map _ _ f
 #align category_theory.functor.hext CategoryTheory.Functor.hext
 -/
 
@@ -238,38 +238,38 @@ section HEq
 -- Composition of functors and maps w.r.t. heq
 variable {E : Type u₃} [Category.{v₃} E] {F G : C ⥤ D} {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z}
 
-#print CategoryTheory.Functor.map_comp_hEq /-
-theorem map_comp_hEq (hx : F.obj X = G.obj X) (hy : F.obj Y = G.obj Y) (hz : F.obj Z = G.obj Z)
+#print CategoryTheory.Functor.map_comp_heq /-
+theorem map_comp_heq (hx : F.obj X = G.obj X) (hy : F.obj Y = G.obj Y) (hz : F.obj Z = G.obj Z)
     (hf : HEq (F.map f) (G.map f)) (hg : HEq (F.map g) (G.map g)) :
     HEq (F.map (f ≫ g)) (G.map (f ≫ g)) := by rw [F.map_comp, G.map_comp]; congr
-#align category_theory.functor.map_comp_heq CategoryTheory.Functor.map_comp_hEq
+#align category_theory.functor.map_comp_heq CategoryTheory.Functor.map_comp_heq
 -/
 
-#print CategoryTheory.Functor.map_comp_hEq' /-
-theorem map_comp_hEq' (hobj : ∀ X : C, F.obj X = G.obj X)
+#print CategoryTheory.Functor.map_comp_heq' /-
+theorem map_comp_heq' (hobj : ∀ X : C, F.obj X = G.obj X)
     (hmap : ∀ {X Y} (f : X ⟶ Y), HEq (F.map f) (G.map f)) : HEq (F.map (f ≫ g)) (G.map (f ≫ g)) :=
   by rw [functor.hext hobj fun _ _ => hmap]
-#align category_theory.functor.map_comp_heq' CategoryTheory.Functor.map_comp_hEq'
+#align category_theory.functor.map_comp_heq' CategoryTheory.Functor.map_comp_heq'
 -/
 
-#print CategoryTheory.Functor.precomp_map_hEq /-
-theorem precomp_map_hEq (H : E ⥤ C) (hmap : ∀ {X Y} (f : X ⟶ Y), HEq (F.map f) (G.map f)) {X Y : E}
+#print CategoryTheory.Functor.precomp_map_heq /-
+theorem precomp_map_heq (H : E ⥤ C) (hmap : ∀ {X Y} (f : X ⟶ Y), HEq (F.map f) (G.map f)) {X Y : E}
     (f : X ⟶ Y) : HEq ((H ⋙ F).map f) ((H ⋙ G).map f) :=
   hmap _
-#align category_theory.functor.precomp_map_heq CategoryTheory.Functor.precomp_map_hEq
+#align category_theory.functor.precomp_map_heq CategoryTheory.Functor.precomp_map_heq
 -/
 
-#print CategoryTheory.Functor.postcomp_map_hEq /-
-theorem postcomp_map_hEq (H : D ⥤ E) (hx : F.obj X = G.obj X) (hy : F.obj Y = G.obj Y)
+#print CategoryTheory.Functor.postcomp_map_heq /-
+theorem postcomp_map_heq (H : D ⥤ E) (hx : F.obj X = G.obj X) (hy : F.obj Y = G.obj Y)
     (hmap : HEq (F.map f) (G.map f)) : HEq ((F ⋙ H).map f) ((G ⋙ H).map f) := by dsimp; congr
-#align category_theory.functor.postcomp_map_heq CategoryTheory.Functor.postcomp_map_hEq
+#align category_theory.functor.postcomp_map_heq CategoryTheory.Functor.postcomp_map_heq
 -/
 
-#print CategoryTheory.Functor.postcomp_map_hEq' /-
-theorem postcomp_map_hEq' (H : D ⥤ E) (hobj : ∀ X : C, F.obj X = G.obj X)
+#print CategoryTheory.Functor.postcomp_map_heq' /-
+theorem postcomp_map_heq' (H : D ⥤ E) (hobj : ∀ X : C, F.obj X = G.obj X)
     (hmap : ∀ {X Y} (f : X ⟶ Y), HEq (F.map f) (G.map f)) : HEq ((F ⋙ H).map f) ((G ⋙ H).map f) :=
   by rw [functor.hext hobj fun _ _ => hmap]
-#align category_theory.functor.postcomp_map_heq' CategoryTheory.Functor.postcomp_map_hEq'
+#align category_theory.functor.postcomp_map_heq' CategoryTheory.Functor.postcomp_map_heq'
 -/
 
 #print CategoryTheory.Functor.hcongr_hom /-

Mathbin/Control/Traversable/Instances.lean

@@ -117,7 +117,7 @@ protected theorem naturality {α β} (f : α → F β) (x : List α) :
 open Nat
 
 instance : LawfulTraversable.{u} List :=
-  { List.lawfulMonad with
+  { List.instLawfulMonad with
     id_traverse := @List.id_traverse
     comp_traverse := @List.comp_traverse
     traverse_eq_map_id := @List.traverse_eq_map_id

Mathbin/Data/List/Basic.lean

@@ -472,6 +472,8 @@ theorem doubleton_eq [DecidableEq α] {x y : α} (h : x ≠ y) : ({x, y} : List
 /-! ### bounded quantifiers over lists -/
 
 
+/- warning: list.forall_mem_nil clashes with list.ball_nil -> List.forall_mem_nil
+Case conversion may be inaccurate. Consider using '#align list.forall_mem_nil List.forall_mem_nilₓ'. -/
 #print List.forall_mem_nil /-
 theorem forall_mem_nil (p : α → Prop) : ∀ x ∈ @nil α, p x :=
   fun.

lake-manifest.json

@@ -10,15 +10,15 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "5676d39ca647849ac60e2d8cac0c292e76728cb3",
+    "rev": "019242c8fca21dbf51fef439c8869be35cbd8048",
     "name": "lean3port",
-    "inputRev?": "5676d39ca647849ac60e2d8cac0c292e76728cb3"}},
+    "inputRev?": "019242c8fca21dbf51fef439c8869be35cbd8048"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "c4bb14cbd48da428ec1f6432e5fcd700a36ed07f",
+    "rev": "e5bc438559068652f49a35f263ffc088ce39a62c",
     "name": "mathlib",
-    "inputRev?": "c4bb14cbd48da428ec1f6432e5fcd700a36ed07f"}},
+    "inputRev?": "e5bc438559068652f49a35f263ffc088ce39a62c"}},
   {"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-07-07-13"
+def tag : String := "nightly-2023-07-07-15"
 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"@"5676d39ca647849ac60e2d8cac0c292e76728cb3"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"019242c8fca21dbf51fef439c8869be35cbd8048"
 
 @[default_target]
 lean_lib Mathbin where