use where

YaelDillies · YaelDillies · commit d0976fbd8352 · 2025-01-08T11:26:38.000Z
diff --git a/Mathlib/Algebra/Ring/Subring/Defs.lean b/Mathlib/Algebra/Ring/Subring/Defs.lean
@@ -167,7 +167,7 @@ instance : SubringClass (Subring R) R where
 initialize_simps_projections Subring (carrier → coe, as_prefix coe)
 
 /-- Turn a `Subring` into a `NonUnitalSubring` by forgetting that it contains `1`. -/
-def toNonUnitalSubring (S : Subring R) : NonUnitalSubring R := { S with }
+def toNonUnitalSubring (S : Subring R) : NonUnitalSubring R where __ := S
 
 @[simp]
 theorem mem_toSubsemiring {s : Subring R} {x : R} : x ∈ s.toSubsemiring ↔ x ∈ s := Iff.rfl
diff --git a/Mathlib/Algebra/Ring/Subsemiring/Defs.lean b/Mathlib/Algebra/Ring/Subsemiring/Defs.lean
@@ -140,8 +140,7 @@ instance : SubsemiringClass (Subsemiring R) R where
 initialize_simps_projections Subsemiring (carrier → coe, as_prefix coe)
 
 /-- Turn a `Subsemiring` into a `NonUnitalSubsemiring` by forgetting that it contains `1`. -/
-def toNonUnitalSubsemiring (S : Subsemiring R) : NonUnitalSubsemiring R :=
-  { S with }
+def toNonUnitalSubsemiring (S : Subsemiring R) : NonUnitalSubsemiring R where __ := S
 
 @[simp]
 theorem mem_toSubmonoid {s : Subsemiring R} {x : R} : x ∈ s.toSubmonoid ↔ x ∈ s :=
