Merge master into nightly-testing

Author: leanprover-community-mathlib4-bot

Mathlib.lean

@@ -5308,6 +5308,7 @@ import Mathlib.RingTheory.LocalRing.ResidueField.Basic
 import Mathlib.RingTheory.LocalRing.ResidueField.Defs
 import Mathlib.RingTheory.LocalRing.ResidueField.Fiber
 import Mathlib.RingTheory.LocalRing.ResidueField.Ideal
+import Mathlib.RingTheory.LocalRing.ResidueField.Instances
 import Mathlib.RingTheory.LocalRing.RingHom.Basic
 import Mathlib.RingTheory.LocalRing.Subring
 import Mathlib.RingTheory.Localization.Algebra

Mathlib/Algebra/Star/NonUnitalSubalgebra.lean

@@ -602,7 +602,6 @@ variable {R}
 
 /-- The `NonUnitalStarSubalgebra` obtained from `S : NonUnitalSubalgebra R A` by taking the
 smallest non-unital subalgebra containing both `S` and `star S`. -/
-@[simps!]
 def starClosure (S : NonUnitalSubalgebra R A) : NonUnitalStarSubalgebra R A where
   toNonUnitalSubalgebra := S ⊔ star S
   star_mem' := @fun a (ha : a ∈ S ⊔ star S) => show star a ∈ S ⊔ star S by
@@ -611,9 +610,11 @@ def starClosure (S : NonUnitalSubalgebra R A) : NonUnitalStarSubalgebra R A wher
     simp only [Set.sup_eq_union, star_adjoin_comm, Set.union_star, coe_star, star_star,
       Set.union_comm]
 
+@[simp]
 theorem coe_starClosure (S : NonUnitalSubalgebra R A) :
     (S.starClosure : Set A) = (S ⊔ star S : NonUnitalSubalgebra R A) := rfl
 
+@[simp]
 theorem mem_starClosure (S : NonUnitalSubalgebra R A) {x : A} :
     x ∈ S.starClosure ↔ x ∈ S ⊔ star S := Iff.rfl
 

Mathlib/Algebra/Star/Subalgebra.lean

@@ -368,17 +368,18 @@ theorem star_adjoin_comm (s : Set A) : star (Algebra.adjoin R s) = Algebra.adjoi
 
 /-- The `StarSubalgebra` obtained from `S : Subalgebra R A` by taking the smallest subalgebra
 containing both `S` and `star S`. -/
-@[simps!]
 def starClosure (S : Subalgebra R A) : StarSubalgebra R A where
   toSubalgebra := S ⊔ star S
   star_mem' := fun {a} ha => by
     simp only [Subalgebra.mem_carrier, ← (@Algebra.gi R A _ _ _).l_sup_u _ _] at *
     rw [← mem_star_iff _ a, star_adjoin_comm, sup_comm]
     simpa using ha
 
+@[simp]
 theorem coe_starClosure (S : Subalgebra R A) :
     (S.starClosure : Set A) = (S ⊔ star S : Subalgebra R A) := rfl
 
+@[simp]
 theorem mem_starClosure (S : Subalgebra R A) {x : A} :
     x ∈ S.starClosure ↔ x ∈ S ⊔ star S := Iff.rfl
 

Mathlib/Analysis/Convex/Cone/Closure.lean

@@ -17,7 +17,7 @@ defining maps between proper cones. The current API is basic and should be exten
 
 namespace ConvexCone
 
-variable {𝕜 : Type*} [Semiring 𝕜] [PartialOrder 𝕜] [IsOrderedRing 𝕜]
+variable {𝕜 : Type*} [Semiring 𝕜] [PartialOrder 𝕜]
 variable {E : Type*} [AddCommMonoid E] [TopologicalSpace E] [ContinuousAdd E] [SMul 𝕜 E]
   [ContinuousConstSMul 𝕜 E]
 
@@ -53,7 +53,7 @@ variable {E : Type*} [AddCommMonoid E] [TopologicalSpace E] [ContinuousAdd E] [M
   [ContinuousConstSMul 𝕜 E]
 
 lemma toConvexCone_closure_pointed (K : PointedCone 𝕜 E) : (K : ConvexCone 𝕜 E).closure.Pointed :=
-  subset_closure <| PointedCone.toConvexCone_pointed _
+  subset_closure <| PointedCone.pointed_toConvexCone _
 
 /-- The closure of a pointed cone inside a topological space as a pointed cone. This
 construction is mainly used for defining maps between proper cones. -/

Mathlib/Analysis/Convex/Cone/InnerDual.lean

@@ -266,7 +266,7 @@ theorem hyperplane_separation (K : ProperCone ℝ H) {f : H →L[ℝ] F} {b : F}
     intro h
     contrapose! h
     -- as `b ∉ K.map f`, there is a hyperplane `y` separating `b` from `K.map f`
-    let C := PointedCone.toConvexCone (𝕜 := ℝ) (E := F) (K.map f)
+    let C := PointedCone.toConvexCone (R := ℝ) (E := F) (K.map f)
     obtain ⟨y, hxy, hyb⟩ :=
       @ConvexCone.hyperplane_separation_of_nonempty_of_isClosed_of_notMem
       _ _ _ _ C (K.map f).nonempty (K.map f).isClosed b h

Mathlib/CategoryTheory/Monoidal/Action/Basic.lean

@@ -100,7 +100,6 @@ scoped notation "λₗ["J"]" => MonoidalLeftActionStruct.actionUnitIso (C := J)
 end MonoidalLeftAction
 
 open scoped MonoidalLeftAction in
-
 /-- A `MonoidalLeftAction C D` is is the data of:
 - For every object `c : C` and `d : D`, an object `c ⊙ₗ d` of `D`.
 - For every morphism `f : (c : C) ⟶ c'` and every `d : D`, a morphism