bump to nightly-2023-07-10-11

mathlib commit leanprover-community/mathlib@1a51edf

Mathbin/Analysis/Normed/Group/SemiNormedGroup/Completion.lean

@@ -44,6 +44,7 @@ open UniformSpace MulOpposite CategoryTheory NormedAddGroupHom
 
 namespace SemiNormedGroupCat
 
+#print SemiNormedGroupCat.completion /-
 /-- The completion of a seminormed group, as an endofunctor on `SemiNormedGroup`. -/
 @[simps]
 def completion : SemiNormedGroupCat.{u} ⥤ SemiNormedGroupCat.{u}
@@ -53,11 +54,15 @@ def completion : SemiNormedGroupCat.{u} ⥤ SemiNormedGroupCat.{u}
   map_id' V := completion_id
   map_comp' U V W f g := (completion_comp f g).symm
 #align SemiNormedGroup.Completion SemiNormedGroupCat.completion
+-/
 
+#print SemiNormedGroupCat.completion_completeSpace /-
 instance completion_completeSpace {V : SemiNormedGroupCat} : CompleteSpace (completion.obj V) :=
   Completion.completeSpace _
 #align SemiNormedGroup.Completion_complete_space SemiNormedGroupCat.completion_completeSpace
+-/
 
+#print SemiNormedGroupCat.completion.incl /-
 /-- The canonical morphism from a seminormed group `V` to its completion. -/
 @[simps]
 def completion.incl {V : SemiNormedGroupCat} : V ⟶ completion.obj V
@@ -66,18 +71,24 @@ def completion.incl {V : SemiNormedGroupCat} : V ⟶ completion.obj V
   map_add' := Completion.coe_add
   bound' := ⟨1, fun v => by simp⟩
 #align SemiNormedGroup.Completion.incl SemiNormedGroupCat.completion.incl
+-/
 
+#print SemiNormedGroupCat.completion.norm_incl_eq /-
 theorem completion.norm_incl_eq {V : SemiNormedGroupCat} {v : V} : ‖completion.incl v‖ = ‖v‖ := by
   simp
 #align SemiNormedGroup.Completion.norm_incl_eq SemiNormedGroupCat.completion.norm_incl_eq
+-/
 
+#print SemiNormedGroupCat.completion.map_normNoninc /-
 theorem completion.map_normNoninc {V W : SemiNormedGroupCat} {f : V ⟶ W} (hf : f.NormNoninc) :
     (completion.map f).NormNoninc :=
   NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one.2 <|
     (NormedAddGroupHom.norm_completion f).le.trans <|
       NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one.1 hf
 #align SemiNormedGroup.Completion.map_norm_noninc SemiNormedGroupCat.completion.map_normNoninc
+-/
 
+#print SemiNormedGroupCat.completion.mapHom /-
 /-- Given a normed group hom `V ⟶ W`, this defines the associated morphism
 from the completion of `V` to the completion of `W`.
 The difference from the definition obtained from the functoriality of completion is in that the
@@ -86,11 +97,14 @@ def completion.mapHom (V W : SemiNormedGroupCat.{u}) :
     (V ⟶ W) →+ (completion.obj V ⟶ completion.obj W) :=
   AddMonoidHom.mk' (CategoryTheory.Functor.map completion) fun f g => f.completion_add g
 #align SemiNormedGroup.Completion.map_hom SemiNormedGroupCat.completion.mapHom
+-/
 
+#print SemiNormedGroupCat.completion.map_zero /-
 @[simp]
 theorem completion.map_zero (V W : SemiNormedGroupCat) : completion.map (0 : V ⟶ W) = 0 :=
   (completion.mapHom V W).map_zero
 #align SemiNormedGroup.Completion.map_zero SemiNormedGroupCat.completion.map_zero
+-/
 
 instance : Preadditive SemiNormedGroupCat.{u}
     where
@@ -104,6 +118,7 @@ instance : Preadditive SemiNormedGroupCat.{u}
 
 instance : Functor.Additive completion where map_add' X Y := (completion.mapHom _ _).map_add
 
+#print SemiNormedGroupCat.completion.lift /-
 /-- Given a normed group hom `f : V → W` with `W` complete, this provides a lift of `f` to
 the completion of `V`. The lemmas `lift_unique` and `lift_comp_incl` provide the api for the
 universal property of the completion. -/
@@ -113,16 +128,21 @@ def completion.lift {V W : SemiNormedGroupCat} [CompleteSpace W] [SeparatedSpace
   map_add' := f.extension.toAddMonoidHom.map_add'
   bound' := f.extension.bound'
 #align SemiNormedGroup.Completion.lift SemiNormedGroupCat.completion.lift
+-/
 
+#print SemiNormedGroupCat.completion.lift_comp_incl /-
 theorem completion.lift_comp_incl {V W : SemiNormedGroupCat} [CompleteSpace W] [SeparatedSpace W]
     (f : V ⟶ W) : completion.incl ≫ completion.lift f = f := by ext;
   apply NormedAddGroupHom.extension_coe
 #align SemiNormedGroup.Completion.lift_comp_incl SemiNormedGroupCat.completion.lift_comp_incl
+-/
 
+#print SemiNormedGroupCat.completion.lift_unique /-
 theorem completion.lift_unique {V W : SemiNormedGroupCat} [CompleteSpace W] [SeparatedSpace W]
     (f : V ⟶ W) (g : completion.obj V ⟶ W) : completion.incl ≫ g = f → g = completion.lift f :=
   fun h => (NormedAddGroupHom.extension_unique _ fun v => ((ext_iff.1 h) v).symm).symm
 #align SemiNormedGroup.Completion.lift_unique SemiNormedGroupCat.completion.lift_unique
+-/
 
 end SemiNormedGroupCat
 

lake-manifest.json

@@ -10,9 +10,9 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "492eaebaa2524b7c3933c05d5653b5507ca74528",
+    "rev": "4aca376101b0a20a9a1b01f13b4ea8b564934e91",
     "name": "lean3port",
-    "inputRev?": "492eaebaa2524b7c3933c05d5653b5507ca74528"}},
+    "inputRev?": "4aca376101b0a20a9a1b01f13b4ea8b564934e91"}},
   {"git":
    {"url": "https://github.com/mhuisi/lean4-cli.git",
     "subDir?": null,
@@ -22,9 +22,9 @@
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "02ea90a076686968ce1d3b3938193f66912f422f",
+    "rev": "278a8fe1522abc239723c43e7a7d24f3d36316ac",
     "name": "mathlib",
-    "inputRev?": "02ea90a076686968ce1d3b3938193f66912f422f"}},
+    "inputRev?": "278a8fe1522abc239723c43e7a7d24f3d36316ac"}},
   {"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-10-09"
+def tag : String := "nightly-2023-07-10-11"
 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"@"492eaebaa2524b7c3933c05d5653b5507ca74528"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"4aca376101b0a20a9a1b01f13b4ea8b564934e91"
 
 @[default_target]
 lean_lib Mathbin where