bump to nightly-2023-06-08-11

mathlib commit leanprover-community/mathlib@31c24aa

Mathbin/Algebra/Lie/Normalizer.lean

@@ -50,6 +50,7 @@ namespace LieSubmodule
 
 variable (N : LieSubmodule R L M) {N₁ N₂ : LieSubmodule R L M}
 
+#print LieSubmodule.normalizer /-
 /-- The normalizer of a Lie submodule. -/
 def normalizer : LieSubmodule R L M
     where
@@ -59,6 +60,7 @@ def normalizer : LieSubmodule R L M
   smul_mem' t m hm x := by rw [lie_smul]; exact N.smul_mem' t (hm x)
   lie_mem x m hm y := by rw [leibniz_lie]; exact N.add_mem' (hm ⁅y, x⁆) (N.lie_mem (hm y))
 #align lie_submodule.normalizer LieSubmodule.normalizer
+-/
 
 @[simp]
 theorem mem_normalizer (m : M) : m ∈ N.normalizer ↔ ∀ x : L, ⁅x, m⁆ ∈ N :=
@@ -110,6 +112,7 @@ namespace LieSubalgebra
 
 variable (H : LieSubalgebra R L)
 
+#print LieSubalgebra.normalizer /-
 /-- Regarding a Lie subalgebra `H ⊆ L` as a module over itself, its normalizer is in fact a Lie
 subalgebra. -/
 def normalizer : LieSubalgebra R L :=
@@ -119,26 +122,33 @@ def normalizer : LieSubalgebra R L :=
       rw [coe_bracket_of_module, mem_to_lie_submodule, leibniz_lie, ← lie_skew y, ← sub_eq_add_neg]
       exact H.sub_mem (hz ⟨_, hy x⟩) (hy ⟨_, hz x⟩) }
 #align lie_subalgebra.normalizer LieSubalgebra.normalizer
+-/
 
+#print LieSubalgebra.mem_normalizer_iff' /-
 theorem mem_normalizer_iff' (x : L) : x ∈ H.normalizer ↔ ∀ y : L, y ∈ H → ⁅y, x⁆ ∈ H := by
   rw [Subtype.forall']; rfl
 #align lie_subalgebra.mem_normalizer_iff' LieSubalgebra.mem_normalizer_iff'
+-/
 
+#print LieSubalgebra.mem_normalizer_iff /-
 theorem mem_normalizer_iff (x : L) : x ∈ H.normalizer ↔ ∀ y : L, y ∈ H → ⁅x, y⁆ ∈ H :=
   by
   rw [mem_normalizer_iff']
   refine' forall₂_congr fun y hy => _
   rw [← lie_skew, neg_mem_iff]
 #align lie_subalgebra.mem_normalizer_iff LieSubalgebra.mem_normalizer_iff
+-/
 
 theorem le_normalizer : H ≤ H.normalizer :=
   H.toLieSubmodule.le_normalizer
 #align lie_subalgebra.le_normalizer LieSubalgebra.le_normalizer
 
+#print LieSubalgebra.coe_normalizer_eq_normalizer /-
 theorem coe_normalizer_eq_normalizer :
     (H.toLieSubmodule.normalizer : Submodule R L) = H.normalizer :=
   rfl
 #align lie_subalgebra.coe_normalizer_eq_normalizer LieSubalgebra.coe_normalizer_eq_normalizer
+-/
 
 variable {H}
 
@@ -157,12 +167,14 @@ theorem lie_mem_sup_of_mem_normalizer {x y z : L} (hx : x ∈ H.normalizer) (hy
   exacts [(H.mem_normalizer_iff' x).mp hx v hv, (H.mem_normalizer_iff x).mp hx w hw]
 #align lie_subalgebra.lie_mem_sup_of_mem_normalizer LieSubalgebra.lie_mem_sup_of_mem_normalizer
 
+#print LieSubalgebra.ideal_in_normalizer /-
 /-- A Lie subalgebra is an ideal of its normalizer. -/
 theorem ideal_in_normalizer {x y : L} (hx : x ∈ H.normalizer) (hy : y ∈ H) : ⁅x, y⁆ ∈ H :=
   by
   rw [← lie_skew, neg_mem_iff]
   exact hx ⟨y, hy⟩
 #align lie_subalgebra.ideal_in_normalizer LieSubalgebra.ideal_in_normalizer
+-/
 
 /-- A Lie subalgebra `H` is an ideal of any Lie subalgebra `K` containing `H` and contained in the
 normalizer of `H`. -/
@@ -175,6 +187,7 @@ theorem exists_nested_lieIdeal_ofLe_normalizer {K : LieSubalgebra R L} (h₁ : H
 
 variable (H)
 
+#print LieSubalgebra.normalizer_eq_self_iff /-
 theorem normalizer_eq_self_iff :
     H.normalizer = H ↔ (LieModule.maxTrivSubmodule R H <| L ⧸ H.toLieSubmodule) = ⊥ :=
   by
@@ -195,6 +208,7 @@ theorem normalizer_eq_self_iff :
       exact (H.mem_normalizer_iff' x).mp hx z hz
     simpa using h y hy
 #align lie_subalgebra.normalizer_eq_self_iff LieSubalgebra.normalizer_eq_self_iff
+-/
 
 end LieSubalgebra
 

Mathbin/Algebra/Lie/UniversalEnveloping.lean

@@ -50,6 +50,7 @@ local notation "ιₜ" => TensorAlgebra.ι R
 
 namespace UniversalEnvelopingAlgebra
 
+#print UniversalEnvelopingAlgebra.Rel /-
 /-- The quotient by the ideal generated by this relation is the universal enveloping algebra.
 
 Note that we have avoided using the more natural expression:
@@ -58,16 +59,19 @@ so that our construction needs only the semiring structure of the tensor algebra
 inductive Rel : TensorAlgebra R L → TensorAlgebra R L → Prop
   | lie_compat (x y : L) : Rel (ιₜ ⁅x, y⁆ + ιₜ y * ιₜ x) (ιₜ x * ιₜ y)
 #align universal_enveloping_algebra.rel UniversalEnvelopingAlgebra.Rel
+-/
 
 end UniversalEnvelopingAlgebra
 
 /- ./././Mathport/Syntax/Translate/Command.lean:43:9: unsupported derive handler algebra[algebra] R -/
+#print UniversalEnvelopingAlgebra /-
 /-- The universal enveloping algebra of a Lie algebra. -/
 def UniversalEnvelopingAlgebra :=
   RingQuot (UniversalEnvelopingAlgebra.Rel R L)
 deriving Inhabited, Ring,
   «./././Mathport/Syntax/Translate/Command.lean:43:9: unsupported derive handler algebra[algebra] R»
 #align universal_enveloping_algebra UniversalEnvelopingAlgebra
+-/
 
 namespace UniversalEnvelopingAlgebra
 

Mathbin/Algebra/Star/Order.lean

@@ -55,27 +55,31 @@ class StarOrderedRing (R : Type u) [NonUnitalSemiring R] [PartialOrder R] extend
 
 namespace StarOrderedRing
 
+#print StarOrderedRing.toOrderedAddCommMonoid /-
 -- see note [lower instance priority]
 instance (priority := 100) toOrderedAddCommMonoid [NonUnitalSemiring R] [PartialOrder R]
     [StarOrderedRing R] : OrderedAddCommMonoid R :=
   { show NonUnitalSemiring R by infer_instance, show PartialOrder R by infer_instance,
     show StarOrderedRing R by infer_instance with }
 #align star_ordered_ring.to_ordered_add_comm_monoid StarOrderedRing.toOrderedAddCommMonoid
+-/
 
 -- see note [lower instance priority]
-instance (priority := 100) to_existsAddOfLE [NonUnitalSemiring R] [PartialOrder R]
+instance (priority := 100) toExistsAddOfLE [NonUnitalSemiring R] [PartialOrder R]
     [StarOrderedRing R] : ExistsAddOfLE R
     where exists_add_of_le a b h :=
     match (le_iff _ _).mp h with
     | ⟨p, _, hp⟩ => ⟨p, hp⟩
-#align star_ordered_ring.to_has_exists_add_of_le StarOrderedRing.to_existsAddOfLE
+#align star_ordered_ring.to_has_exists_add_of_le StarOrderedRing.toExistsAddOfLE
 
+#print StarOrderedRing.toOrderedAddCommGroup /-
 -- see note [lower instance priority]
 instance (priority := 100) toOrderedAddCommGroup [NonUnitalRing R] [PartialOrder R]
     [StarOrderedRing R] : OrderedAddCommGroup R :=
   { show NonUnitalRing R by infer_instance, show PartialOrder R by infer_instance,
     show StarOrderedRing R by infer_instance with }
 #align star_ordered_ring.to_ordered_add_comm_group StarOrderedRing.toOrderedAddCommGroup
+-/
 
 -- set note [reducible non-instances]
 /-- To construct a `star_ordered_ring` instance it suffices to show that `x ≤ y` if and only if

Mathbin/Analysis/SpecialFunctions/PolarCoord.lean

@@ -114,6 +114,7 @@ theorem hasFDerivAt_polarCoord_symm (p : ℝ × ℝ) :
     simp only [smul_smul, add_comm, neg_mul, neg_smul, smul_neg]
 #align has_fderiv_at_polar_coord_symm hasFDerivAt_polarCoord_symm
 
+#print polarCoord_source_ae_eq_univ /-
 theorem polarCoord_source_ae_eq_univ : polarCoord.source =ᵐ[volume] univ :=
   by
   have A : polar_coord.sourceᶜ ⊆ (LinearMap.snd ℝ ℝ ℝ).ker :=
@@ -132,7 +133,9 @@ theorem polarCoord_source_ae_eq_univ : polarCoord.source =ᵐ[volume] univ :=
   simp only [ae_eq_univ]
   exact le_antisymm ((measure_mono A).trans (le_of_eq B)) bot_le
 #align polar_coord_source_ae_eq_univ polarCoord_source_ae_eq_univ
+-/
 
+#print integral_comp_polarCoord_symm /-
 theorem integral_comp_polarCoord_symm {E : Type _} [NormedAddCommGroup E] [NormedSpace ℝ E]
     [CompleteSpace E] (f : ℝ × ℝ → E) :
     (∫ p in polarCoord.target, p.1 • f (polarCoord.symm p)) = ∫ p, f p :=
@@ -165,4 +168,5 @@ theorem integral_comp_polarCoord_symm {E : Type _} [NormedAddCommGroup E] [Norme
       exact hx.1
     
 #align integral_comp_polar_coord_symm integral_comp_polarCoord_symm
+-/