bump to nightly-2023-07-01-19

mathlib commit leanprover-community/mathlib@9240e8b

Mathbin/Algebra/Category/Module/Adjunctions.lean

@@ -72,7 +72,7 @@ instance : IsRightAdjoint (forget (ModuleCat.{u} R)) :=
 
 end
 
-namespace Free
+namespace free
 
 variable [CommRing R]
 
@@ -180,7 +180,7 @@ instance : LaxMonoidal.{u} (free R).obj
 instance : IsIso (LaxMonoidal.ε (free R).obj) :=
   ⟨⟨Finsupp.lapply PUnit.unit, ⟨by ext; simp, by ext ⟨⟩ ⟨⟩; simp⟩⟩⟩
 
-end Free
+end free
 
 variable [CommRing R]
 

Mathbin/Algebra/Category/Mon/Adjunctions.lean

@@ -30,6 +30,7 @@ universe u
 
 open CategoryTheory
 
+#print adjoinOne /-
 /-- The functor of adjoining a neutral element `one` to a semigroup.
  -/
 @[to_additive "The functor of adjoining a neutral element `zero` to a semigroup", simps]
@@ -41,15 +42,19 @@ def adjoinOne : SemigroupCat.{u} ⥤ MonCat.{u}
   map_comp' X Y Z := WithOne.map_comp
 #align adjoin_one adjoinOne
 #align adjoin_zero adjoinZero
+-/
 
+#print hasForgetToSemigroup /-
 @[to_additive hasForgetToAddSemigroup]
 instance hasForgetToSemigroup : HasForget₂ MonCat SemigroupCat
     where forget₂ :=
     { obj := fun M => SemigroupCat.of M
       map := fun M N => MonoidHom.toMulHom }
 #align has_forget_to_Semigroup hasForgetToSemigroup
 #align has_forget_to_AddSemigroup hasForgetToAddSemigroup
+-/
 
+#print adjoinOneAdj /-
 /-- The adjoin_one-forgetful adjunction from `Semigroup` to `Mon`.-/
 @[to_additive "The adjoin_one-forgetful adjunction from `AddSemigroup` to `AddMon`"]
 def adjoinOneAdj : adjoinOne ⊣ forget₂ MonCat.{u} SemigroupCat.{u} :=
@@ -65,7 +70,9 @@ def adjoinOneAdj : adjoinOne ⊣ forget₂ MonCat.{u} SemigroupCat.{u} :=
         · simp }
 #align adjoin_one_adj adjoinOneAdj
 #align adjoin_zero_adj adjoinZeroAdj
+-/
 
+#print free /-
 /-- The free functor `Type u ⥤ Mon` sending a type `X` to the free monoid on `X`. -/
 def free : Type u ⥤ MonCat.{u}
     where
@@ -74,13 +81,16 @@ def free : Type u ⥤ MonCat.{u}
   map_id' := by intros; ext1; rfl
   map_comp' := by intros; ext1; rfl
 #align free free
+-/
 
+#print adj /-
 /-- The free-forgetful adjunction for monoids. -/
 def adj : free ⊣ forget MonCat.{u} :=
   Adjunction.mkOfHomEquiv
     { homEquiv := fun X G => FreeMonoid.lift.symm
       homEquiv_naturality_left_symm := fun X Y G f g => by ext1; rfl }
 #align adj adj
+-/
 
 instance : IsRightAdjoint (forget MonCat.{u}) :=
   ⟨_, adj⟩

Mathbin/CategoryTheory/Groupoid/FreeGroupoid.lean

@@ -52,7 +52,7 @@ namespace CategoryTheory
 
 namespace Groupoid
 
-namespace Free
+namespace free
 
 universe u v u' v' u'' v''
 
@@ -257,7 +257,7 @@ theorem freeGroupoidFunctor_comp (φ : V ⥤q V') (φ' : V' ⥤q V'') :
 
 end Functoriality
 
-end Free
+end free
 
 end Groupoid
 

Mathbin/FieldTheory/PrimitiveElement.lean

@@ -222,7 +222,7 @@ theorem exists_primitive_element : ∃ α : E, F⟮⟯ = ⊤ :=
   by
   rcases isEmpty_or_nonempty (Fintype F) with (F_inf | ⟨⟨F_finite⟩⟩)
   · let P : IntermediateField F E → Prop := fun K => ∃ α : E, F⟮⟯ = K
-    have base : P ⊥ := ⟨0, adjoin_zero⟩
+    have base : P ⊥ := ⟨0, adjoinZero⟩
     have ih : ∀ (K : IntermediateField F E) (x : E), P K → P (K⟮⟯.restrictScalars F) :=
       by
       intro K β hK

Mathbin/Geometry/Manifold/DerivationBundle.lean

@@ -31,29 +31,37 @@ variable (𝕜 : Type _) [NontriviallyNormedField 𝕜] {E : Type _} [NormedAddC
 
 open scoped Manifold
 
+#print smoothFunctionsAlgebra /-
 -- the following two instances prevent poorly understood type class inference timeout problems
 instance smoothFunctionsAlgebra : Algebra 𝕜 C^∞⟮I, M; 𝕜⟯ := by infer_instance
 #align smooth_functions_algebra smoothFunctionsAlgebra
+-/
 
+#print smooth_functions_tower /-
 instance smooth_functions_tower : IsScalarTower 𝕜 C^∞⟮I, M; 𝕜⟯ C^∞⟮I, M; 𝕜⟯ := by infer_instance
 #align smooth_functions_tower smooth_functions_tower
+-/
 
+#print PointedSmoothMap /-
 /-- Type synonym, introduced to put a different `has_smul` action on `C^n⟮I, M; 𝕜⟯`
 which is defined as `f • r = f(x) * r`. -/
 @[nolint unused_arguments]
 def PointedSmoothMap (x : M) :=
   C^n⟮I, M; 𝕜⟯
 #align pointed_smooth_map PointedSmoothMap
+-/
 
 scoped[Derivation] notation "C^" n "⟮" I ", " M "; " 𝕜 "⟯⟨" x "⟩" => PointedSmoothMap 𝕜 I M n x
 
 variable {𝕜 M}
 
 namespace PointedSmoothMap
 
+#print PointedSmoothMap.funLike /-
 instance funLike {x : M} : FunLike C^∞⟮I, M; 𝕜⟯⟨x⟩ M fun _ => 𝕜 :=
   ContMDiffMap.funLike
 #align pointed_smooth_map.fun_like PointedSmoothMap.funLike
+-/
 
 instance {x : M} : CommRing C^∞⟮I, M; 𝕜⟯⟨x⟩ :=
   SmoothMap.commRing
@@ -72,19 +80,25 @@ instance {x : M} : IsScalarTower 𝕜 C^∞⟮I, M; 𝕜⟯⟨x⟩ C^∞⟮I, M;
 
 variable {I}
 
+#print PointedSmoothMap.evalAlgebra /-
 /-- `smooth_map.eval_ring_hom` gives rise to an algebra structure of `C^∞⟮I, M; 𝕜⟯` on `𝕜`. -/
 instance evalAlgebra {x : M} : Algebra C^∞⟮I, M; 𝕜⟯⟨x⟩ 𝕜 :=
   (SmoothMap.evalRingHom x : C^∞⟮I, M; 𝕜⟯⟨x⟩ →+* 𝕜).toAlgebra
 #align pointed_smooth_map.eval_algebra PointedSmoothMap.evalAlgebra
+-/
 
+#print PointedSmoothMap.eval /-
 /-- With the `eval_algebra` algebra structure evaluation is actually an algebra morphism. -/
 def eval (x : M) : C^∞⟮I, M; 𝕜⟯ →ₐ[C^∞⟮I, M; 𝕜⟯⟨x⟩] 𝕜 :=
   Algebra.ofId C^∞⟮I, M; 𝕜⟯⟨x⟩ 𝕜
 #align pointed_smooth_map.eval PointedSmoothMap.eval
+-/
 
+#print PointedSmoothMap.smul_def /-
 theorem smul_def (x : M) (f : C^∞⟮I, M; 𝕜⟯⟨x⟩) (k : 𝕜) : f • k = f x * k :=
   rfl
 #align pointed_smooth_map.smul_def PointedSmoothMap.smul_def
+-/
 
 instance (x : M) : IsScalarTower 𝕜 C^∞⟮I, M; 𝕜⟯⟨x⟩ 𝕜
     where smul_assoc k f h := by
@@ -94,42 +108,51 @@ end PointedSmoothMap
 
 open scoped Derivation
 
+#print PointDerivation /-
 /-- The derivations at a point of a manifold. Some regard this as a possible definition of the
 tangent space -/
 @[reducible]
 def PointDerivation (x : M) :=
   Derivation 𝕜 C^∞⟮I, M; 𝕜⟯⟨x⟩ 𝕜
 #align point_derivation PointDerivation
+-/
 
 section
 
 variable (I) {M} (X Y : Derivation 𝕜 C^∞⟮I, M; 𝕜⟯ C^∞⟮I, M; 𝕜⟯) (f g : C^∞⟮I, M; 𝕜⟯) (r : 𝕜)
 
+#print SmoothFunction.evalAt /-
 /-- Evaluation at a point gives rise to a `C^∞⟮I, M; 𝕜⟯`-linear map between `C^∞⟮I, M; 𝕜⟯` and `𝕜`.
  -/
 def SmoothFunction.evalAt (x : M) : C^∞⟮I, M; 𝕜⟯ →ₗ[C^∞⟮I, M; 𝕜⟯⟨x⟩] 𝕜 :=
   (PointedSmoothMap.eval x).toLinearMap
 #align smooth_function.eval_at SmoothFunction.evalAt
+-/
 
 namespace Derivation
 
 variable {I}
 
+#print Derivation.evalAt /-
 /-- The evaluation at a point as a linear map. -/
 def evalAt (x : M) : Derivation 𝕜 C^∞⟮I, M; 𝕜⟯ C^∞⟮I, M; 𝕜⟯ →ₗ[𝕜] PointDerivation I x :=
   (SmoothFunction.evalAt I x).compDer
 #align derivation.eval_at Derivation.evalAt
+-/
 
+#print Derivation.evalAt_apply /-
 theorem evalAt_apply (x : M) : evalAt x X f = (X f) x :=
   rfl
 #align derivation.eval_at_apply Derivation.evalAt_apply
+-/
 
 end Derivation
 
 variable {I} {E' : Type _} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type _}
   [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type _} [TopologicalSpace M']
   [ChartedSpace H' M']
 
+#print hfdifferential /-
 /-- The heterogeneous differential as a linear map. Instead of taking a function as an argument this
 differential takes `h : f x = y`. It is particularly handy to deal with situations where the points
 on where it has to be evaluated are equal but not definitionally equal. -/
@@ -148,40 +171,49 @@ def hfdifferential {f : C^∞⟮I, M; I', M'⟯} {x : M} {y : M'} (h : f x = y)
   map_smul' k v := rfl
   map_add' v w := rfl
 #align hfdifferential hfdifferential
+-/
 
+#print fdifferential /-
 /-- The homogeneous differential as a linear map. -/
 def fdifferential (f : C^∞⟮I, M; I', M'⟯) (x : M) :
     PointDerivation I x →ₗ[𝕜] PointDerivation I' (f x) :=
   hfdifferential (rfl : f x = f x)
 #align fdifferential fdifferential
+-/
 
 -- Standard notation for the differential. The abbreviation is `MId`.
 scoped[Manifold] notation "𝒅" => fdifferential
 
 -- Standard notation for the differential. The abbreviation is `MId`.
 scoped[Manifold] notation "𝒅ₕ" => hfdifferential
 
+#print apply_fdifferential /-
 @[simp]
 theorem apply_fdifferential (f : C^∞⟮I, M; I', M'⟯) {x : M} (v : PointDerivation I x)
     (g : C^∞⟮I', M'; 𝕜⟯) : 𝒅 f x v g = v (g.comp f) :=
   rfl
 #align apply_fdifferential apply_fdifferential
+-/
 
+#print apply_hfdifferential /-
 @[simp]
 theorem apply_hfdifferential {f : C^∞⟮I, M; I', M'⟯} {x : M} {y : M'} (h : f x = y)
     (v : PointDerivation I x) (g : C^∞⟮I', M'; 𝕜⟯) : 𝒅ₕ h v g = 𝒅 f x v g :=
   rfl
 #align apply_hfdifferential apply_hfdifferential
+-/
 
 variable {E'' : Type _} [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H'' : Type _}
   [TopologicalSpace H''] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type _} [TopologicalSpace M'']
   [ChartedSpace H'' M'']
 
+#print fdifferential_comp /-
 @[simp]
 theorem fdifferential_comp (g : C^∞⟮I', M'; I'', M''⟯) (f : C^∞⟮I, M; I', M'⟯) (x : M) :
     𝒅 (g.comp f) x = (𝒅 g (f x)).comp (𝒅 f x) :=
   rfl
 #align fdifferential_comp fdifferential_comp
+-/
 
 end
 

Mathbin/GroupTheory/Subsemigroup/Center.lean

@@ -96,12 +96,10 @@ theorem add_mem_center [Distrib M] {a b : M} (ha : a ∈ Set.center M) (hb : b 
 #align set.add_mem_center Set.add_mem_center
 -/
 
-#print Set.neg_mem_center /-
 @[simp]
 theorem neg_mem_center [Ring M] {a : M} (ha : a ∈ Set.center M) : -a ∈ Set.center M := fun c => by
   rw [← neg_mul_comm, ha (-c), neg_mul_comm]
-#align set.neg_mem_center Set.neg_mem_center
--/
+#align set.neg_mem_center Set.neg_mem_centerₓ
 
 #print Set.subset_center_units /-
 @[to_additive subset_add_center_add_units]

Mathbin/LinearAlgebra/Dimension.lean

@@ -1084,7 +1084,7 @@ theorem rank_self : Module.rank R R = 1 := by
 
 end StrongRankCondition
 
-section Free
+section free
 
 variable [Ring K] [StrongRankCondition K]
 
@@ -1256,7 +1256,7 @@ def finDimVectorspaceEquiv (n : ℕ) (hn : Module.rank K V = n) : V ≃ₗ[K] Fi
 #align fin_dim_vectorspace_equiv finDimVectorspaceEquiv
 -/
 
-end Free
+end free
 
 section DivisionRing
 

Mathbin/RingTheory/NonUnitalSubsemiring/Basic.lean

@@ -1120,13 +1120,11 @@ variable {F : Type _} [NonUnitalNonAssocSemiring T] [NonUnitalRingHomClass F R S
 
 open NonUnitalSubsemiringClass NonUnitalSubsemiring
 
-#print NonUnitalRingHom.codRestrict /-
 /-- Restriction of a non-unital ring homomorphism to a non-unital subsemiring of the codomain. -/
 def codRestrict (f : F) (s : NonUnitalSubsemiring S) (h : ∀ x, f x ∈ s) : R →ₙ+* s :=
   { (f : R →ₙ* S).codRestrict s.toSubsemigroup h, (f : R →+ S).codRestrict s.toAddSubmonoid h with
     toFun := fun n => ⟨f n, h n⟩ }
-#align non_unital_ring_hom.cod_restrict NonUnitalRingHom.codRestrict
--/
+#align non_unital_ring_hom.cod_restrict NonUnitalRingHom.codRestrictₓ
 
 #print NonUnitalRingHom.srangeRestrict /-
 /-- Restriction of a non-unital ring homomorphism to its range interpreted as a

lake-manifest.json

@@ -10,15 +10,15 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "5bf7e2341ef468d74c6058dc46a076cdb18d26bc",
+    "rev": "e60dce33645383b5df74d984fb3efb16025f52fb",
     "name": "lean3port",
-    "inputRev?": "5bf7e2341ef468d74c6058dc46a076cdb18d26bc"}},
+    "inputRev?": "e60dce33645383b5df74d984fb3efb16025f52fb"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "44c828ca5b12983ef1d4eea5c54f95c2ef52cb36",
+    "rev": "d055df4832d11e9a165ef37c1bd0de6b867165bb",
     "name": "mathlib",
-    "inputRev?": "44c828ca5b12983ef1d4eea5c54f95c2ef52cb36"}},
+    "inputRev?": "d055df4832d11e9a165ef37c1bd0de6b867165bb"}},
   {"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-01-17"
+def tag : String := "nightly-2023-07-01-19"
 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"@"5bf7e2341ef468d74c6058dc46a076cdb18d26bc"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"e60dce33645383b5df74d984fb3efb16025f52fb"
 
 @[default_target]
 lean_lib Mathbin where