bump to nightly-2023-03-21-20

mathlib commit leanprover-community/mathlib@290a7ba

Mathbin/Algebra/Algebra/Subalgebra/Basic.lean

@@ -2300,27 +2300,27 @@ theorem smul_def [SMul A α] {S : Subalgebra R A} (g : S) (m : α) : g • m = (
   rfl
 #align subalgebra.smul_def Subalgebra.smul_def
 
-/- warning: subalgebra.smul_comm_class_left -> Subalgebra.sMulCommClass_left is a dubious translation:
+/- warning: subalgebra.smul_comm_class_left -> Subalgebra.smulCommClass_left is a dubious translation:
 lean 3 declaration is
   forall {R : Type.{u1}} {A : Type.{u2}} [_inst_1 : CommSemiring.{u1} R] [_inst_2 : Semiring.{u2} A] [_inst_3 : Algebra.{u1, u2} R A _inst_1 _inst_2] {α : Type.{u3}} {β : Type.{u4}} [_inst_6 : SMul.{u2, u4} A β] [_inst_7 : SMul.{u3, u4} α β] [_inst_8 : SMulCommClass.{u2, u3, u4} A α β _inst_6 _inst_7] (S : Subalgebra.{u1, u2} R A _inst_1 _inst_2 _inst_3), SMulCommClass.{u2, u3, u4} (coeSort.{succ u2, succ (succ u2)} (Subalgebra.{u1, u2} R A _inst_1 _inst_2 _inst_3) Type.{u2} (SetLike.hasCoeToSort.{u2, u2} (Subalgebra.{u1, u2} R A _inst_1 _inst_2 _inst_3) A (Subalgebra.setLike.{u1, u2} R A _inst_1 _inst_2 _inst_3)) S) α β (Subalgebra.hasSmul.{u1, u2, u4} R A _inst_1 _inst_2 _inst_3 β _inst_6 S) _inst_7
 but is expected to have type
   forall {R : Type.{u1}} {A : Type.{u2}} [_inst_1 : CommSemiring.{u1} R] [_inst_2 : Semiring.{u2} A] [_inst_3 : Algebra.{u1, u2} R A _inst_1 _inst_2] {α : Type.{u3}} {β : Type.{u4}} [_inst_6 : SMul.{u2, u4} A β] [_inst_7 : SMul.{u3, u4} α β] [_inst_8 : SMulCommClass.{u2, u3, u4} A α β _inst_6 _inst_7] (S : Subalgebra.{u1, u2} R A _inst_1 _inst_2 _inst_3), SMulCommClass.{u2, u3, u4} (Subtype.{succ u2} A (fun (x : A) => Membership.mem.{u2, u2} A (Subalgebra.{u1, u2} R A _inst_1 _inst_2 _inst_3) (SetLike.instMembership.{u2, u2} (Subalgebra.{u1, u2} R A _inst_1 _inst_2 _inst_3) A (Subalgebra.instSetLikeSubalgebra.{u1, u2} R A _inst_1 _inst_2 _inst_3)) x S)) α β (Subalgebra.instSMulSubtypeMemSubalgebraInstMembershipInstSetLikeSubalgebra.{u1, u2, u4} R A _inst_1 _inst_2 _inst_3 β _inst_6 S) _inst_7
-Case conversion may be inaccurate. Consider using '#align subalgebra.smul_comm_class_left Subalgebra.sMulCommClass_leftₓ'. -/
-instance sMulCommClass_left [SMul A β] [SMul α β] [SMulCommClass A α β] (S : Subalgebra R A) :
+Case conversion may be inaccurate. Consider using '#align subalgebra.smul_comm_class_left Subalgebra.smulCommClass_leftₓ'. -/
+instance smulCommClass_left [SMul A β] [SMul α β] [SMulCommClass A α β] (S : Subalgebra R A) :
     SMulCommClass S α β :=
   S.toSubsemiring.smulCommClass_left
-#align subalgebra.smul_comm_class_left Subalgebra.sMulCommClass_left
+#align subalgebra.smul_comm_class_left Subalgebra.smulCommClass_left
 
-/- warning: subalgebra.smul_comm_class_right -> Subalgebra.sMulCommClass_right is a dubious translation:
+/- warning: subalgebra.smul_comm_class_right -> Subalgebra.smulCommClass_right is a dubious translation:
 lean 3 declaration is
   forall {R : Type.{u1}} {A : Type.{u2}} [_inst_1 : CommSemiring.{u1} R] [_inst_2 : Semiring.{u2} A] [_inst_3 : Algebra.{u1, u2} R A _inst_1 _inst_2] {α : Type.{u3}} {β : Type.{u4}} [_inst_6 : SMul.{u3, u4} α β] [_inst_7 : SMul.{u2, u4} A β] [_inst_8 : SMulCommClass.{u3, u2, u4} α A β _inst_6 _inst_7] (S : Subalgebra.{u1, u2} R A _inst_1 _inst_2 _inst_3), SMulCommClass.{u3, u2, u4} α (coeSort.{succ u2, succ (succ u2)} (Subalgebra.{u1, u2} R A _inst_1 _inst_2 _inst_3) Type.{u2} (SetLike.hasCoeToSort.{u2, u2} (Subalgebra.{u1, u2} R A _inst_1 _inst_2 _inst_3) A (Subalgebra.setLike.{u1, u2} R A _inst_1 _inst_2 _inst_3)) S) β _inst_6 (Subalgebra.hasSmul.{u1, u2, u4} R A _inst_1 _inst_2 _inst_3 β _inst_7 S)
 but is expected to have type
   forall {R : Type.{u1}} {A : Type.{u2}} [_inst_1 : CommSemiring.{u1} R] [_inst_2 : Semiring.{u2} A] [_inst_3 : Algebra.{u1, u2} R A _inst_1 _inst_2] {α : Type.{u3}} {β : Type.{u4}} [_inst_6 : SMul.{u3, u4} α β] [_inst_7 : SMul.{u2, u4} A β] [_inst_8 : SMulCommClass.{u3, u2, u4} α A β _inst_6 _inst_7] (S : Subalgebra.{u1, u2} R A _inst_1 _inst_2 _inst_3), SMulCommClass.{u3, u2, u4} α (Subtype.{succ u2} A (fun (x : A) => Membership.mem.{u2, u2} A (Subalgebra.{u1, u2} R A _inst_1 _inst_2 _inst_3) (SetLike.instMembership.{u2, u2} (Subalgebra.{u1, u2} R A _inst_1 _inst_2 _inst_3) A (Subalgebra.instSetLikeSubalgebra.{u1, u2} R A _inst_1 _inst_2 _inst_3)) x S)) β _inst_6 (Subalgebra.instSMulSubtypeMemSubalgebraInstMembershipInstSetLikeSubalgebra.{u1, u2, u4} R A _inst_1 _inst_2 _inst_3 β _inst_7 S)
-Case conversion may be inaccurate. Consider using '#align subalgebra.smul_comm_class_right Subalgebra.sMulCommClass_rightₓ'. -/
-instance sMulCommClass_right [SMul α β] [SMul A β] [SMulCommClass α A β] (S : Subalgebra R A) :
+Case conversion may be inaccurate. Consider using '#align subalgebra.smul_comm_class_right Subalgebra.smulCommClass_rightₓ'. -/
+instance smulCommClass_right [SMul α β] [SMul A β] [SMulCommClass α A β] (S : Subalgebra R A) :
     SMulCommClass α S β :=
   S.toSubsemiring.smulCommClass_right
-#align subalgebra.smul_comm_class_right Subalgebra.sMulCommClass_right
+#align subalgebra.smul_comm_class_right Subalgebra.smulCommClass_right
 
 /- warning: subalgebra.is_scalar_tower_left -> Subalgebra.isScalarTower_left is a dubious translation:
 lean 3 declaration is

Mathbin/Analysis/Complex/Basic.lean

@@ -468,8 +468,7 @@ section ComplexOrder
 open ComplexOrder
 
 theorem eq_coe_norm_of_nonneg {z : ℂ} (hz : 0 ≤ z) : z = ↑‖z‖ := by
-  rw [eq_re_of_real_le hz, IsROrC.norm_of_real,
-    Real.norm_of_nonneg (Complex.ComplexOrder.le_def.2 hz).1]
+  rw [eq_re_of_real_le hz, IsROrC.norm_of_real, Real.norm_of_nonneg (Complex.le_def.2 hz).1]
 #align complex.eq_coe_norm_of_nonneg Complex.eq_coe_norm_of_nonneg
 
 end ComplexOrder

Mathbin/Analysis/NormedSpace/Star/ContinuousFunctionalCalculus.lean

@@ -107,8 +107,8 @@ theorem spectrum_star_mul_self_of_isStarNormal :
     rw [gelfand_transform_apply_apply ℂ _ (star a' * a') φ, map_mul φ, map_star φ]
     rw [Complex.eq_coe_norm_of_nonneg star_mul_self_nonneg, ← map_star, ← map_mul]
     exact
-      ⟨Complex.ComplexOrder.zero_le_real.2 (norm_nonneg _),
-        Complex.ComplexOrder.real_le_real.2 (AlgHom.norm_apply_le_self φ (star a' * a'))⟩
+      ⟨Complex.zero_le_real.2 (norm_nonneg _),
+        Complex.real_le_real.2 (AlgHom.norm_apply_le_self φ (star a' * a'))⟩
 #align spectrum_star_mul_self_of_is_star_normal spectrum_star_mul_self_of_isStarNormal
 
 variable {a}
@@ -165,9 +165,7 @@ theorem elementalStarAlgebra.isUnit_of_isUnit_of_isStarNormal (h : IsUnit a) :
       by
       replace hz := Set.image_subset _ (spectrum_star_mul_self_of_isStarNormal a) hz
       rwa [Set.image_const_sub_Icc, sub_self, sub_zero] at hz
-    refine'
-      lt_of_le_of_ne
-        (Complex.ComplexOrder.real_le_real.1 <| Complex.eq_coe_norm_of_nonneg h₃.1 ▸ h₃.2) _
+    refine' lt_of_le_of_ne (Complex.real_le_real.1 <| Complex.eq_coe_norm_of_nonneg h₃.1 ▸ h₃.2) _
     · intro hz'
       replace hz' := congr_arg (fun x : ℝ≥0 => ((x : ℝ) : ℂ)) hz'
       simp only [coe_nnnorm] at hz'

Mathbin/CategoryTheory/Limits/Constructions/ZeroObjects.lean

@@ -191,13 +191,13 @@ def coprodZeroIso (X : C) : X ⨿ (0 : C) ≅ X :=
 #align category_theory.limits.coprod_zero_iso CategoryTheory.Limits.coprodZeroIso
 -/
 
-#print CategoryTheory.Limits.inr_coprod_zeroiso_hom /-
+#print CategoryTheory.Limits.inr_coprodZeroIso_hom /-
 @[simp]
-theorem inr_coprod_zeroiso_hom (X : C) : coprod.inl ≫ (coprodZeroIso X).Hom = 𝟙 X :=
+theorem inr_coprodZeroIso_hom (X : C) : coprod.inl ≫ (coprodZeroIso X).Hom = 𝟙 X :=
   by
   dsimp [coprod_zero_iso, binary_cofan_zero_right]
   simp
-#align category_theory.limits.inr_coprod_zeroiso_hom CategoryTheory.Limits.inr_coprod_zeroiso_hom
+#align category_theory.limits.inr_coprod_zeroiso_hom CategoryTheory.Limits.inr_coprodZeroIso_hom
 -/
 
 #print CategoryTheory.Limits.coprodZeroIso_inv /-