bump to nightly-2023-10-30-06

mathlib commit leanprover-community/mathlib@3365b20

Mathbin/CategoryTheory/Extensive.lean

@@ -321,14 +321,14 @@ theorem hasStrictInitial_of_isUniversal [HasInitial C]
 #align category_theory.has_strict_initial_of_is_universal CategoryTheory.hasStrictInitial_of_isUniversal
 -/
 
-#print CategoryTheory.hasStrictInitialObjects_of_finitaryExtensive /-
-instance (priority := 100) hasStrictInitialObjects_of_finitaryExtensive [FinitaryExtensive C] :
+#print CategoryTheory.hasStrictInitialObjects_of_finitaryPreExtensive /-
+instance (priority := 100) hasStrictInitialObjects_of_finitaryPreExtensive [FinitaryExtensive C] :
     HasStrictInitialObjects C :=
   hasStrictInitial_of_isUniversal
     (FinitaryExtensive.vanKampen _
         ((BinaryCofan.isColimit_iff_isIso_inr initialIsInitial _).mpr
             (by dsimp; infer_instance)).some).isUniversal
-#align category_theory.has_strict_initial_objects_of_finitary_extensive CategoryTheory.hasStrictInitialObjects_of_finitaryExtensive
+#align category_theory.has_strict_initial_objects_of_finitary_extensive CategoryTheory.hasStrictInitialObjects_of_finitaryPreExtensive
 -/
 
 #print CategoryTheory.finitaryExtensive_iff_of_isTerminal /-

Mathbin/GroupTheory/IsFreeGroup.lean

@@ -72,12 +72,10 @@ def of : Generators G → G :=
 #align is_free_group.of IsFreeGroup.of
 -/
 
-#print IsFreeGroup.of_eq_freeGroup_of /-
 @[simp]
 theorem of_eq_freeGroup_of {A : Type u} : @of (FreeGroup A) _ _ = FreeGroup.of :=
   rfl
 #align is_free_group.of_eq_free_group_of IsFreeGroup.of_eq_freeGroup_of
--/
 
 variable {H : Type _} [Group H]
 
@@ -93,12 +91,10 @@ def lift : (Generators G → H) ≃ (G →* H) :=
 #align is_free_group.lift IsFreeGroup.lift
 -/
 
-#print IsFreeGroup.lift'_eq_freeGroup_lift /-
 @[simp]
 theorem lift'_eq_freeGroup_lift {A : Type u} : @lift (FreeGroup A) _ _ H _ = FreeGroup.lift :=
   rfl
 #align is_free_group.lift'_eq_free_group_lift IsFreeGroup.lift'_eq_freeGroup_lift
--/
 
 #print IsFreeGroup.lift_of /-
 @[simp]
@@ -132,10 +128,9 @@ theorem unique_lift (f : Generators G → H) : ∃! F : G →* H, ∀ a, F (of a
 #align is_free_group.unique_lift IsFreeGroup.unique_lift
 -/
 
-#print IsFreeGroup.ofLift /-
 /-- If a group satisfies the universal property of a free group, then it is a free group, where
 the universal property is expressed as in `is_free_group.lift` and its properties. -/
-def ofLift {G : Type u} [Group G] (X : Type u) (of : X → G)
+def of_lift {G : Type u} [Group G] (X : Type u) (of : X → G)
     (lift : ∀ {H : Type u} [Group H], (X → H) ≃ (G →* H))
     (lift_of : ∀ {H : Type u} [Group H], ∀ (f : X → H) (a), lift f (of a) = f a) : IsFreeGroup G
     where
@@ -152,13 +147,11 @@ def ofLift {G : Type u} [Group G] (X : Type u) (of : X → G)
         apply lift.symm.injective; ext x
         simp only [MonoidHom.coe_comp, Function.comp_apply, MonoidHom.id_apply, FreeGroup.lift.of,
           lift_of, lift_symm_of])
-#align is_free_group.of_lift IsFreeGroup.ofLift
--/
+#align is_free_group.of_lift IsFreeGroup.of_lift
 
-#print IsFreeGroup.ofUniqueLift /-
 /-- If a group satisfies the universal property of a free group, then it is a free group, where
 the universal property is expressed as in `is_free_group.unique_lift`.  -/
-noncomputable def ofUniqueLift {G : Type u} [Group G] (X : Type u) (of : X → G)
+noncomputable def of_unique_lift {G : Type u} [Group G] (X : Type u) (of : X → G)
     (h : ∀ {H : Type u} [Group H] (f : X → H), ∃! F : G →* H, ∀ a, F (of a) = f a) :
     IsFreeGroup G :=
   let lift {H : Type u} [Group H] : (X → H) ≃ (G →* H) :=
@@ -168,18 +161,15 @@ noncomputable def ofUniqueLift {G : Type u} [Group G] (X : Type u) (of : X → G
       right_inv := fun F => ((Classical.choose_spec (h (F ∘ of))).right F fun _ => rfl).symm }
   let lift_of {H : Type u} [Group H] (f : X → H) (a : X) : lift f (of a) = f a :=
     congr_fun (lift.symm_apply_apply f) a
-  ofLift X of @lift @lift_of
-#align is_free_group.of_unique_lift IsFreeGroup.ofUniqueLift
--/
+  of_lift X of @lift @lift_of
+#align is_free_group.of_unique_lift IsFreeGroup.of_unique_lift
 
-#print IsFreeGroup.ofMulEquiv /-
 /-- Being a free group transports across group isomorphisms. -/
-def ofMulEquiv {H : Type _} [Group H] (h : G ≃* H) : IsFreeGroup H
+def of_mulEquiv {H : Type _} [Group H] (h : G ≃* H) : IsFreeGroup H
     where
   Generators := Generators G
   MulEquiv := (mulEquiv G).trans h
-#align is_free_group.of_mul_equiv IsFreeGroup.ofMulEquiv
--/
+#align is_free_group.of_mul_equiv IsFreeGroup.of_mulEquiv
 
 end IsFreeGroup
 

Mathbin/GroupTheory/NielsenSchreier.lean

@@ -239,7 +239,7 @@ def functorOfMonoidHom {X} [Monoid X] (f : End (root' T) →* X) : G ⥤ Categor
     group at the root is freely generated by loops coming from generating arrows
     in the complement of the tree. -/
 def endIsFree : IsFreeGroup (End (root' T)) :=
-  IsFreeGroup.ofUniqueLift ((wideSubquiverEquivSetTotal <| wideSubquiverSymmetrify T)ᶜ : Set _)
+  IsFreeGroup.of_unique_lift ((wideSubquiverEquivSetTotal <| wideSubquiverSymmetrify T)ᶜ : Set _)
     (fun e => loopOfHom T (of e.val.Hom))
     (by
       intro X _ f
@@ -328,7 +328,7 @@ end IsFreeGroupoid
 /-- The Nielsen-Schreier theorem: a subgroup of a free group is free. -/
 instance subgroupIsFreeOfIsFree {G : Type u} [Group G] [IsFreeGroup G] (H : Subgroup G) :
     IsFreeGroup H :=
-  IsFreeGroup.ofMulEquiv (endMulEquivSubgroup H)
+  IsFreeGroup.of_mulEquiv (endMulEquivSubgroup H)
 #align subgroup_is_free_of_is_free subgroupIsFreeOfIsFree
 -/
 

lake-manifest.json

@@ -4,18 +4,18 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "8ad5fe635df49db850d9fdf019e8dcc7504749e3",
+    "rev": "e30b0f6d7c048a1ca5b652d0497d9aa5ab59572d",
     "opts": {},
     "name": "lean3port",
-    "inputRev?": "8ad5fe635df49db850d9fdf019e8dcc7504749e3",
+    "inputRev?": "e30b0f6d7c048a1ca5b652d0497d9aa5ab59572d",
     "inherited": false}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "77ccc30d9f983d3c9bfbc6a795623d404227f4e7",
+    "rev": "a988ad9300897ae7de89811e768a0b09555e6488",
     "opts": {},
     "name": "mathlib",
-    "inputRev?": "77ccc30d9f983d3c9bfbc6a795623d404227f4e7",
+    "inputRev?": "a988ad9300897ae7de89811e768a0b09555e6488",
     "inherited": true}},
   {"git":
    {"url": "https://github.com/leanprover/std4",

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-29-06"
+def tag : String := "nightly-2023-10-30-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"@"8ad5fe635df49db850d9fdf019e8dcc7504749e3"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"e30b0f6d7c048a1ca5b652d0497d9aa5ab59572d"
 
 @[default_target]
 lean_lib Mathbin where