bump to nightly-2023-02-27-16

mathlib commit leanprover-community/mathlib@eb0cb45

Mathbin/Algebra/Lie/DirectSum.lean

@@ -245,11 +245,11 @@ def toLieAlgebra [DecidableEq ι] (L' : Type w₁) [LieRing L'] [LieAlgebra R L'
         ext (j x)
         exact this j i x y
       intro i j y x
-      simp only [lie_of R, lie_algebra_of_apply, LieHom.coe_to_linearMap, to_add_monoid_of,
+      simp only [lie_of R, lie_algebra_of_apply, LieHom.coe_toLinearMap, to_add_monoid_of,
         coe_to_module_eq_coe_to_add_monoid, LinearMap.toAddMonoidHom_coe]
       rcases eq_or_ne i j with (h | h)
       · have h' : f j (h.rec_on y) = f i y := Eq.drec (Eq.refl _) h
-        simp only [h, h', LieHom.coe_to_linearMap, dif_pos, LieHom.map_lie, to_add_monoid_of,
+        simp only [h, h', LieHom.coe_toLinearMap, dif_pos, LieHom.map_lie, to_add_monoid_of,
           LinearMap.toAddMonoidHom_coe]
       · simp only [h, hf j i h.symm x y, dif_neg, not_false_iff, AddMonoidHom.map_zero] }
 #align direct_sum.to_lie_algebra DirectSum.toLieAlgebra

Mathbin/Algebra/Lie/IdealOperations.lean

@@ -373,7 +373,7 @@ theorem comap_bracket_eq {J₁ J₂ : LieIdeal R L'} (h : f.IsIdealMorphism) :
     LieSubmodule.sup_coe_to_submodule, f.ker_coe_submodule, ← Submodule.comap_map_eq,
     LieSubmodule.lieIdeal_oper_eq_linear_span, LieSubmodule.lieIdeal_oper_eq_linear_span,
     LinearMap.map_span]
-  congr ; simp only [LieHom.coe_to_linearMap, Set.mem_setOf_eq]; ext y
+  congr ; simp only [LieHom.coe_toLinearMap, Set.mem_setOf_eq]; ext y
   constructor
   · rintro ⟨⟨x₁, hx₁⟩, ⟨x₂, hx₂⟩, hy⟩
     rw [← hy]

Mathbin/Algebra/Lie/OfAssociative.lean

@@ -320,7 +320,7 @@ theorem LieSubalgebra.ad_comp_incl_eq (K : LieSubalgebra R L) (x : K) :
     (ad R L ↑x).comp (K.incl : K →ₗ[R] L) = (K.incl : K →ₗ[R] L).comp (ad R K x) :=
   by
   ext y
-  simp only [ad_apply, LieHom.coe_to_linearMap, LieSubalgebra.coe_incl, LinearMap.coe_comp,
+  simp only [ad_apply, LieHom.coe_toLinearMap, LieSubalgebra.coe_incl, LinearMap.coe_comp,
     LieSubalgebra.coe_bracket, Function.comp_apply]
 #align lie_subalgebra.ad_comp_incl_eq LieSubalgebra.ad_comp_incl_eq
 

Mathbin/Algebra/Lie/Subalgebra.lean

@@ -810,7 +810,7 @@ variable [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlge
 
 /-- An injective Lie algebra morphism is an equivalence onto its range. -/
 noncomputable def ofInjective (f : L₁ →ₗ⁅R⁆ L₂) (h : Function.Injective f) : L₁ ≃ₗ⁅R⁆ f.range :=
-  { LinearEquiv.ofInjective (f : L₁ →ₗ[R] L₂) <| by rwa [LieHom.coe_to_linearMap] with
+  { LinearEquiv.ofInjective (f : L₁ →ₗ[R] L₂) <| by rwa [LieHom.coe_toLinearMap] with
     map_lie' := fun x y => by
       apply SetCoe.ext
       simpa }

Mathbin/Algebra/Lie/Submodule.lean

@@ -1135,7 +1135,7 @@ theorem coe_map_of_surjective (h : Function.Surjective f) :
         have hy' : ∃ x : L, x ∈ I ∧ f x = y := by simpa [hy]
         obtain ⟨z₂, hz₂, rfl⟩ := hy'
         obtain ⟨z₁, rfl⟩ := h x
-        simp only [LieHom.coe_to_linearMap, SetLike.mem_coe, Set.mem_image,
+        simp only [LieHom.coe_toLinearMap, SetLike.mem_coe, Set.mem_image,
           LieSubmodule.mem_coeSubmodule, Submodule.mem_carrier, Submodule.map_coe]
         use ⁅z₁, z₂⁆
         exact ⟨I.lie_mem hz₂, f.map_lie z₁ z₂⟩ }

Mathbin/Algebra/Lie/TensorProduct.lean

@@ -208,7 +208,7 @@ def toModuleHom : L ⊗[R] M →ₗ⁅R,L⁆ M :=
 @[simp]
 theorem toModuleHom_apply (x : L) (m : M) : toModuleHom R L M (x ⊗ₜ m) = ⁅x, m⁆ := by
   simp only [to_module_hom, TensorProduct.LieModule.liftLie_apply, to_endomorphism_apply_apply,
-    LieHom.coe_to_linearMap, LieModuleHom.coe_mk, LinearMap.coe_mk, LinearMap.toFun_eq_coe]
+    LieHom.coe_toLinearMap, LieModuleHom.coe_mk, LinearMap.coe_mk, LinearMap.toFun_eq_coe]
 #align lie_module.to_module_hom_apply LieModule.toModuleHom_apply
 
 end LieModule

Mathbin/Algebra/Lie/UniversalEnveloping.lean

@@ -101,17 +101,17 @@ def lift : (L →ₗ⁅R⁆ A) ≃ (UniversalEnvelopingAlgebra R L →ₐ[R] A)
       ⟨TensorAlgebra.lift R (f : L →ₗ[R] A), by
         intro a b h; induction' h with x y
         simp only [LieRing.of_associative_ring_bracket, map_add, TensorAlgebra.lift_ι_apply,
-          LieHom.coe_to_linearMap, LieHom.map_lie, map_mul, sub_add_cancel]⟩
+          LieHom.coe_toLinearMap, LieHom.map_lie, map_mul, sub_add_cancel]⟩
   invFun F := (F : UniversalEnvelopingAlgebra R L →ₗ⁅R⁆ A).comp (ι R)
   left_inv f := by
     ext
-    simp only [ι, mk_alg_hom, TensorAlgebra.lift_ι_apply, LieHom.coe_to_linearMap,
+    simp only [ι, mk_alg_hom, TensorAlgebra.lift_ι_apply, LieHom.coe_toLinearMap,
       LinearMap.toFun_eq_coe, LinearMap.coe_comp, LieHom.coe_comp, AlgHom.coe_to_lieHom,
       LieHom.coe_mk, Function.comp_apply, AlgHom.toLinearMap_apply,
       RingQuot.liftAlgHom_mkAlgHom_apply]
   right_inv F := by
     ext
-    simp only [ι, mk_alg_hom, TensorAlgebra.lift_ι_apply, LieHom.coe_to_linearMap,
+    simp only [ι, mk_alg_hom, TensorAlgebra.lift_ι_apply, LieHom.coe_toLinearMap,
       LinearMap.toFun_eq_coe, LinearMap.coe_comp, LieHom.coe_linearMap_comp,
       AlgHom.comp_toLinearMap, Function.comp_apply, AlgHom.toLinearMap_apply,
       RingQuot.liftAlgHom_mkAlgHom_apply, AlgHom.coe_to_lieHom, LieHom.coe_mk]

Mathbin/Algebra/Lie/Weights.lean

@@ -255,12 +255,12 @@ def IsWeight (χ : LieCharacter R H) : Prop :=
 
 /-- For a non-trivial nilpotent Lie module over a nilpotent Lie algebra, the zero character is a
 weight with respect to the `⊤` Lie subalgebra. -/
-theorem isWeightZeroOfNilpotent [Nontrivial M] [LieAlgebra.IsNilpotent R L] [IsNilpotent R L M] :
+theorem isWeight_zero_of_nilpotent [Nontrivial M] [LieAlgebra.IsNilpotent R L] [IsNilpotent R L M] :
     IsWeight (⊤ : LieSubalgebra R L) M 0 :=
   by
   rw [is_weight, LieHom.coe_zero, zero_weight_space_eq_top_of_nilpotent]
   exact top_ne_bot
-#align lie_module.is_weight_zero_of_nilpotent LieModule.isWeightZeroOfNilpotent
+#align lie_module.is_weight_zero_of_nilpotent LieModule.isWeight_zero_of_nilpotent
 
 /-- A (nilpotent) Lie algebra acts nilpotently on the zero weight space of a Noetherian Lie
 module. -/
@@ -321,15 +321,15 @@ theorem rootSpace_comap_eq_weightSpace (χ : H → R) :
     (∀ y : H, ∃ k : ℕ, (f y ^ k).comp (H.incl : H →ₗ[R] L) x = 0) ↔
       ∀ y : H, ∃ k : ℕ, (H.incl : H →ₗ[R] L).comp (g y ^ k) x = 0
     by
-    simp only [LieHom.coe_to_linearMap, LieSubalgebra.coe_incl, Function.comp_apply,
+    simp only [LieHom.coe_toLinearMap, LieSubalgebra.coe_incl, Function.comp_apply,
       LinearMap.coe_comp, Submodule.coe_eq_zero] at this
     simp only [mem_weight_space, mem_pre_weight_space, LieSubalgebra.coe_incl',
       LieSubmodule.mem_comap, this]
   have hfg : ∀ y : H, (f y).comp (H.incl : H →ₗ[R] L) = (H.incl : H →ₗ[R] L).comp (g y) :=
     by
     rintro ⟨y, hy⟩
     ext ⟨z, hz⟩
-    simp only [Submodule.coe_sub, to_endomorphism_apply_apply, LieHom.coe_to_linearMap,
+    simp only [Submodule.coe_sub, to_endomorphism_apply_apply, LieHom.coe_toLinearMap,
       LinearMap.one_apply, LieSubalgebra.coe_incl, LieSubalgebra.coe_bracket_of_module,
       LieSubalgebra.coe_bracket, LinearMap.smul_apply, Function.comp_apply,
       Submodule.coe_smul_of_tower, LinearMap.coe_comp, LinearMap.sub_apply]