bump to nightly-2023-06-10-01

mathlib commit leanprover-community/mathlib@7e5137f

Mathbin/Algebra/Lie/CartanSubalgebra.lean

@@ -35,6 +35,7 @@ variable {R : Type u} {L : Type v}
 
 variable [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L)
 
+#print LieSubmodule.IsUcsLimit /-
 /-- Given a Lie module `M` of a Lie algebra `L`, `lie_submodule.is_ucs_limit` is the proposition
 that a Lie submodule `N ⊆ M` is the limiting value for the upper central series.
 
@@ -44,25 +45,31 @@ def LieSubmodule.IsUcsLimit {M : Type _} [AddCommGroup M] [Module R M] [LieRingM
     [LieModule R L M] (N : LieSubmodule R L M) : Prop :=
   ∃ k, ∀ l, k ≤ l → (⊥ : LieSubmodule R L M).ucs l = N
 #align lie_submodule.is_ucs_limit LieSubmodule.IsUcsLimit
+-/
 
 namespace LieSubalgebra
 
+#print LieSubalgebra.IsCartanSubalgebra /-
 /-- A Cartan subalgebra is a nilpotent, self-normalizing subalgebra. -/
 class IsCartanSubalgebra : Prop where
   nilpotent : LieAlgebra.IsNilpotent R H
   self_normalizing : H.normalizer = H
 #align lie_subalgebra.is_cartan_subalgebra LieSubalgebra.IsCartanSubalgebra
+-/
 
 instance [H.IsCartanSubalgebra] : LieAlgebra.IsNilpotent R H :=
   IsCartanSubalgebra.nilpotent
 
+#print LieSubalgebra.normalizer_eq_self_of_isCartanSubalgebra /-
 @[simp]
 theorem normalizer_eq_self_of_isCartanSubalgebra (H : LieSubalgebra R L) [H.IsCartanSubalgebra] :
     H.toLieSubmodule.normalizer = H.toLieSubmodule := by
   rw [← LieSubmodule.coe_toSubmodule_eq_iff, coe_normalizer_eq_normalizer,
     is_cartan_subalgebra.self_normalizing, coe_to_lie_submodule]
 #align lie_subalgebra.normalizer_eq_self_of_is_cartan_subalgebra LieSubalgebra.normalizer_eq_self_of_isCartanSubalgebra
+-/
 
+#print LieSubalgebra.ucs_eq_self_of_isCartanSubalgebra /-
 @[simp]
 theorem ucs_eq_self_of_isCartanSubalgebra (H : LieSubalgebra R L) [H.IsCartanSubalgebra] (k : ℕ) :
     H.toLieSubmodule.ucs k = H.toLieSubmodule :=
@@ -71,7 +78,9 @@ theorem ucs_eq_self_of_isCartanSubalgebra (H : LieSubalgebra R L) [H.IsCartanSub
   · simp
   · simp [ih]
 #align lie_subalgebra.ucs_eq_self_of_is_cartan_subalgebra LieSubalgebra.ucs_eq_self_of_isCartanSubalgebra
+-/
 
+#print LieSubalgebra.isCartanSubalgebra_iff_isUcsLimit /-
 theorem isCartanSubalgebra_iff_isUcsLimit : H.IsCartanSubalgebra ↔ H.toLieSubmodule.IsUcsLimit :=
   by
   constructor
@@ -98,6 +107,7 @@ theorem isCartanSubalgebra_iff_isUcsLimit : H.IsCartanSubalgebra ↔ H.toLieSubm
           rw [← LieSubalgebra.coe_to_submodule_eq_iff, ← LieSubalgebra.coe_normalizer_eq_normalizer,
             hk', LieSubalgebra.coe_toLieSubmodule] }
 #align lie_subalgebra.is_cartan_subalgebra_iff_is_ucs_limit LieSubalgebra.isCartanSubalgebra_iff_isUcsLimit
+-/
 
 end LieSubalgebra
 

Mathbin/Analysis/SpecialFunctions/ImproperIntegrals.lean

@@ -32,6 +32,7 @@ open Real Set Filter MeasureTheory intervalIntegral
 
 open scoped Topology
 
+#print integrableOn_exp_Iic /-
 theorem integrableOn_exp_Iic (c : ℝ) : IntegrableOn exp (Iic c) :=
   by
   refine'
@@ -41,7 +42,9 @@ theorem integrableOn_exp_Iic (c : ℝ) : IntegrableOn exp (Iic c) :=
   simp_rw [norm_of_nonneg (exp_pos _).le, integral_exp, sub_le_self_iff]
   exact (exp_pos _).le
 #align integrable_on_exp_Iic integrableOn_exp_Iic
+-/
 
+#print integral_exp_Iic /-
 theorem integral_exp_Iic (c : ℝ) : (∫ x : ℝ in Iic c, exp x) = exp c :=
   by
   refine'
@@ -50,18 +53,23 @@ theorem integral_exp_Iic (c : ℝ) : (∫ x : ℝ in Iic c, exp x) = exp c :=
   simp_rw [integral_exp, show 𝓝 (exp c) = 𝓝 (exp c - 0) by rw [sub_zero]]
   exact tendsto_exp_at_bot.const_sub _
 #align integral_exp_Iic integral_exp_Iic
+-/
 
+#print integral_exp_Iic_zero /-
 theorem integral_exp_Iic_zero : (∫ x : ℝ in Iic 0, exp x) = 1 :=
   exp_zero ▸ integral_exp_Iic 0
 #align integral_exp_Iic_zero integral_exp_Iic_zero
+-/
 
 theorem integral_exp_neg_Ioi (c : ℝ) : (∫ x : ℝ in Ioi c, exp (-x)) = exp (-c) := by
   simpa only [integral_comp_neg_Ioi] using integral_exp_Iic (-c)
 #align integral_exp_neg_Ioi integral_exp_neg_Ioi
 
+#print integral_exp_neg_Ioi_zero /-
 theorem integral_exp_neg_Ioi_zero : (∫ x : ℝ in Ioi 0, exp (-x)) = 1 := by
   simpa only [neg_zero, exp_zero] using integral_exp_neg_Ioi 0
 #align integral_exp_neg_Ioi_zero integral_exp_neg_Ioi_zero
+-/
 
 /-- If `0 < c`, then `(λ t : ℝ, t ^ a)` is integrable on `(c, ∞)` for all `a < -1`. -/
 theorem integrableOn_Ioi_rpow_of_lt {a : ℝ} (ha : a < -1) {c : ℝ} (hc : 0 < c) :

Mathbin/FieldTheory/IsAlgClosed/Basic.lean

@@ -48,6 +48,7 @@ open Polynomial
 
 variable (k : Type u) [Field k]
 
+#print IsAlgClosed /-
 /-- Typeclass for algebraically closed fields.
 
 To show `polynomial.splits p f` for an arbitrary ring homomorphism `f`,
@@ -56,6 +57,7 @@ see `is_alg_closed.splits_codomain` and `is_alg_closed.splits_domain`.
 class IsAlgClosed : Prop where
   Splits : ∀ p : k[X], p.Splits <| RingHom.id k
 #align is_alg_closed IsAlgClosed
+-/
 
 /-- Every polynomial splits in the field extension `f : K →+* k` if `k` is algebraically closed.
 
@@ -78,9 +80,11 @@ namespace IsAlgClosed
 
 variable {k}
 
+#print IsAlgClosed.exists_root /-
 theorem exists_root [IsAlgClosed k] (p : k[X]) (hp : p.degree ≠ 0) : ∃ x, IsRoot p x :=
   exists_root_of_splits _ (IsAlgClosed.splits p) hp
 #align is_alg_closed.exists_root IsAlgClosed.exists_root
+-/
 
 theorem exists_pow_nat_eq [IsAlgClosed k] (x : k) {n : ℕ} (hn : 0 < n) : ∃ z, z ^ n = x :=
   by
@@ -182,16 +186,20 @@ class IsAlgClosure (R : Type u) (K : Type v) [CommRing R] [Field K] [Algebra R K
   algebraic : Algebra.IsAlgebraic R K
 #align is_alg_closure IsAlgClosure
 
+#print isAlgClosure_iff /-
 theorem isAlgClosure_iff (K : Type v) [Field K] [Algebra k K] :
     IsAlgClosure k K ↔ IsAlgClosed K ∧ Algebra.IsAlgebraic k K :=
   ⟨fun h => ⟨h.1, h.2⟩, fun h => ⟨h.1, h.2⟩⟩
 #align is_alg_closure_iff isAlgClosure_iff
+-/
 
+#print IsAlgClosure.normal /-
 instance (priority := 100) IsAlgClosure.normal (R K : Type _) [Field R] [Field K] [Algebra R K]
     [IsAlgClosure R K] : Normal R K :=
   ⟨IsAlgClosure.algebraic, fun _ =>
     @IsAlgClosed.splits_codomain _ _ _ (IsAlgClosure.alg_closed R) _ _ _⟩
 #align is_alg_closure.normal IsAlgClosure.normal
+-/
 
 instance (priority := 100) IsAlgClosure.separable (R K : Type _) [Field R] [Field K] [Algebra R K]
     [IsAlgClosure R K] [CharZero R] : IsSeparable R K :=
@@ -287,17 +295,20 @@ theorem exists_maximal_subfieldWithHom : ∃ E : SubfieldWithHom K L M hL, ∀ N
   exists_maximal_of_chains_bounded maximal_subfieldWithHom_chain_bounded fun _ _ _ => le_trans
 #align lift.subfield_with_hom.exists_maximal_subfield_with_hom lift.SubfieldWithHom.exists_maximal_subfieldWithHom
 
+#print lift.SubfieldWithHom.maximalSubfieldWithHom /-
 /-- The maximal `subfield_with_hom`. We later prove that this is equal to `⊤`. -/
 noncomputable def maximalSubfieldWithHom : SubfieldWithHom K L M hL :=
   Classical.choose (exists_maximal_subfieldWithHom M hL)
 #align lift.subfield_with_hom.maximal_subfield_with_hom lift.SubfieldWithHom.maximalSubfieldWithHom
+-/
 
 theorem maximalSubfieldWithHom_is_maximal :
     ∀ N : SubfieldWithHom K L M hL,
       maximalSubfieldWithHom M hL ≤ N → N ≤ maximalSubfieldWithHom M hL :=
   Classical.choose_spec (exists_maximal_subfieldWithHom M hL)
 #align lift.subfield_with_hom.maximal_subfield_with_hom_is_maximal lift.SubfieldWithHom.maximalSubfieldWithHom_is_maximal
 
+#print lift.SubfieldWithHom.maximalSubfieldWithHom_eq_top /-
 theorem maximalSubfieldWithHom_eq_top : (maximalSubfieldWithHom M hL).carrier = ⊤ :=
   by
   rw [eq_top_iff]
@@ -332,6 +343,7 @@ theorem maximalSubfieldWithHom_eq_top : (maximalSubfieldWithHom M hL).carrier =
   refine' (maximal_subfield_with_hom_is_maximal M hL O' hO').fst _
   exact Algebra.subset_adjoin (Set.mem_singleton x)
 #align lift.subfield_with_hom.maximal_subfield_with_hom_eq_top lift.SubfieldWithHom.maximalSubfieldWithHom_eq_top
+-/
 
 end SubfieldWithHom
 

Mathbin/FieldTheory/IsAlgClosed/Classification.lean

@@ -103,12 +103,12 @@ variable {κ : Type _} (w : κ → L)
 
 variable (hv : AlgebraicIndependent R v)
 
-theorem isAlgClosureOfTranscendenceBasis [IsAlgClosed K] (hv : IsTranscendenceBasis R v) :
+theorem isAlgClosure_of_transcendence_basis [IsAlgClosed K] (hv : IsTranscendenceBasis R v) :
     IsAlgClosure (Algebra.adjoin R (Set.range v)) K :=
   letI := RingHom.domain_nontrivial (algebraMap R K)
   { alg_closed := by infer_instance
     algebraic := hv.is_algebraic }
-#align is_alg_closed.is_alg_closure_of_transcendence_basis IsAlgClosed.isAlgClosureOfTranscendenceBasis
+#align is_alg_closed.is_alg_closure_of_transcendence_basis IsAlgClosed.isAlgClosure_of_transcendence_basis
 
 variable (hw : AlgebraicIndependent R w)
 

lake-manifest.json

@@ -10,15 +10,15 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "0102c373279828fdf308d6717e821fe4f9100e08",
+    "rev": "12254373b7d9f35ca209ccababaa3fca26734c4d",
     "name": "lean3port",
-    "inputRev?": "0102c373279828fdf308d6717e821fe4f9100e08"}},
+    "inputRev?": "12254373b7d9f35ca209ccababaa3fca26734c4d"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "fdc28c986f83996f43dc8ffa24ff58ca5b7f34df",
+    "rev": "d9c7687babc5560d7bf36019338cc88017cfe6a2",
     "name": "mathlib",
-    "inputRev?": "fdc28c986f83996f43dc8ffa24ff58ca5b7f34df"}},
+    "inputRev?": "d9c7687babc5560d7bf36019338cc88017cfe6a2"}},
   {"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-09-23"
+def tag : String := "nightly-2023-06-10-01"
 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"@"0102c373279828fdf308d6717e821fe4f9100e08"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"12254373b7d9f35ca209ccababaa3fca26734c4d"
 
 @[default_target]
 lean_lib Mathbin where