bump to nightly-2023-06-05-21

mathlib commit leanprover-community/mathlib@1336155

Mathbin/Algebra/Lie/DirectSum.lean

@@ -94,6 +94,7 @@ variable (L : ι → Type w)
 
 variable [∀ i, LieRing (L i)] [∀ i, LieAlgebra R (L i)]
 
+#print DirectSum.lieRing /-
 instance lieRing : LieRing (⨁ i, L i) :=
   {
     (inferInstance :
@@ -107,20 +108,24 @@ instance lieRing : LieRing (⨁ i, L i) :=
       ext; simp only [sub_apply, zip_with_apply, add_apply, zero_apply]
       apply leibniz_lie }
 #align direct_sum.lie_ring DirectSum.lieRing
+-/
 
 @[simp]
 theorem bracket_apply (x y : ⨁ i, L i) (i : ι) : ⁅x, y⁆ i = ⁅x i, y i⁆ :=
   zipWith_apply _ _ x y i
 #align direct_sum.bracket_apply DirectSum.bracket_apply
 
+#print DirectSum.lieAlgebra /-
 instance lieAlgebra : LieAlgebra R (⨁ i, L i) :=
   { (inferInstance : Module R _) with
     lie_smul := fun c x y => by ext;
       simp only [zip_with_apply, smul_apply, bracket_apply, lie_smul] }
 #align direct_sum.lie_algebra DirectSum.lieAlgebra
+-/
 
 variable (R ι L)
 
+#print DirectSum.lieAlgebraOf /-
 /-- The inclusion of each component into the direct sum as morphism of Lie algebras. -/
 @[simps]
 def lieAlgebraOf [DecidableEq ι] (j : ι) : L j →ₗ⁅R⁆ ⨁ i, L i :=
@@ -131,7 +136,9 @@ def lieAlgebraOf [DecidableEq ι] (j : ι) : L j →ₗ⁅R⁆ ⨁ i, L i :=
       · rw [← h]; simp [of]
       · simp [of, single_eq_of_ne h] }
 #align direct_sum.lie_algebra_of DirectSum.lieAlgebraOf
+-/
 
+#print DirectSum.lieAlgebraComponent /-
 /-- The projection map onto one component, as a morphism of Lie algebras. -/
 @[simps]
 def lieAlgebraComponent (j : ι) : (⨁ i, L i) →ₗ⁅R⁆ L j :=
@@ -140,6 +147,7 @@ def lieAlgebraComponent (j : ι) : (⨁ i, L i) →ₗ⁅R⁆ L j :=
     map_lie' := fun x y => by
       simp only [component, bracket_apply, lapply_apply, LinearMap.toFun_eq_coe] }
 #align direct_sum.lie_algebra_component DirectSum.lieAlgebraComponent
+-/
 
 @[ext]
 theorem lieAlgebra_ext {x y : ⨁ i, L i}
@@ -233,17 +241,21 @@ section Ideals
 
 variable {L : Type w} [LieRing L] [LieAlgebra R L] (I : ι → LieIdeal R L)
 
+#print DirectSum.lieRingOfIdeals /-
 /-- The fact that this instance is necessary seems to be a bug in typeclass inference. See
 [this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/
 Typeclass.20resolution.20under.20binders/near/245151099). -/
 instance lieRingOfIdeals : LieRing (⨁ i, I i) :=
   DirectSum.lieRing fun i => ↥(I i)
 #align direct_sum.lie_ring_of_ideals DirectSum.lieRingOfIdeals
+-/
 
+#print DirectSum.lieAlgebraOfIdeals /-
 /-- See `direct_sum.lie_ring_of_ideals` comment. -/
 instance lieAlgebraOfIdeals : LieAlgebra R (⨁ i, I i) :=
   DirectSum.lieAlgebra fun i => ↥(I i)
 #align direct_sum.lie_algebra_of_ideals DirectSum.lieAlgebraOfIdeals
+-/
 
 end Ideals
 

lake-manifest.json

@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "e8f22251802fb8c905688bfd8d62643539711cf2",
+    "rev": "7affe0290df13338ed0a44f76f36c5b7777b72c2",
     "name": "lean3port",
-    "inputRev?": "e8f22251802fb8c905688bfd8d62643539711cf2"}},
+    "inputRev?": "7affe0290df13338ed0a44f76f36c5b7777b72c2"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "db83690ee0ac0e6c939893d18456b5871927bd40",
+    "rev": "d75993443babf361446cfe3d2ed8b4a7477c5dea",
     "name": "mathlib",
-    "inputRev?": "db83690ee0ac0e6c939893d18456b5871927bd40"}},
+    "inputRev?": "d75993443babf361446cfe3d2ed8b4a7477c5dea"}},
   {"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-06-05-18"
+def tag : String := "nightly-2023-06-05-21"
 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"@"e8f22251802fb8c905688bfd8d62643539711cf2"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"7affe0290df13338ed0a44f76f36c5b7777b72c2"
 
 @[default_target]
 lean_lib Mathbin where