style(Order): use where __ := x instead of := { x with } (#10588)

The former style encourages one parent per line, which is easier to review and see diffs of. It also allows a handful of `:= fun a b =>`s to be replaced with the less noisy `a b :=`.

A small number of `inferInstanceAs _ with`s were removed, as they are automatic in those places anyway.

Mathlib/Algebra/Order/Pi.lean

@@ -29,9 +29,10 @@ namespace Pi
       "The product of a family of ordered additive commutative monoids is
 an ordered additive commutative monoid."]
 instance orderedCommMonoid {ι : Type*} {Z : ι → Type*} [∀ i, OrderedCommMonoid (Z i)] :
-    OrderedCommMonoid (∀ i, Z i) :=
-  { Pi.partialOrder, Pi.commMonoid with
-    mul_le_mul_left := fun _ _ w _ i => mul_le_mul_left' (w i) _ }
+    OrderedCommMonoid (∀ i, Z i) where
+  __ := Pi.partialOrder
+  __ := Pi.commMonoid
+  mul_le_mul_left _ _ w _ := fun i => mul_le_mul_left' (w i) _
 #align pi.ordered_comm_monoid Pi.orderedCommMonoid
 #align pi.ordered_add_comm_monoid Pi.orderedAddCommMonoid
 
@@ -49,9 +50,11 @@ instance existsMulOfLe {ι : Type*} {α : ι → Type*} [∀ i, LE (α i)] [∀
       "The product of a family of canonically ordered additive monoids is
 a canonically ordered additive monoid."]
 instance {ι : Type*} {Z : ι → Type*} [∀ i, CanonicallyOrderedCommMonoid (Z i)] :
-    CanonicallyOrderedCommMonoid (∀ i, Z i) :=
-  { Pi.orderBot, Pi.orderedCommMonoid, Pi.existsMulOfLe with
-    le_self_mul := fun _ _ _ => le_self_mul }
+    CanonicallyOrderedCommMonoid (∀ i, Z i) where
+  __ := Pi.orderBot
+  __ := Pi.orderedCommMonoid
+  __ := Pi.existsMulOfLe
+  le_self_mul _ _ := fun _ => le_self_mul
 
 @[to_additive]
 instance orderedCancelCommMonoid [∀ i, OrderedCancelCommMonoid <| f i] :
@@ -72,31 +75,36 @@ instance orderedCancelCommMonoid [∀ i, OrderedCancelCommMonoid <| f i] :
 #align pi.ordered_cancel_add_comm_monoid Pi.orderedAddCancelCommMonoid
 
 @[to_additive]
-instance orderedCommGroup [∀ i, OrderedCommGroup <| f i] : OrderedCommGroup (∀ i : I, f i) :=
-  { Pi.commGroup, Pi.orderedCommMonoid with
-    npow := Monoid.npow }
+instance orderedCommGroup [∀ i, OrderedCommGroup <| f i] : OrderedCommGroup (∀ i : I, f i) where
+  __ := Pi.commGroup
+  __ := Pi.orderedCommMonoid
+  npow := Monoid.npow
 #align pi.ordered_comm_group Pi.orderedCommGroup
 #align pi.ordered_add_comm_group Pi.orderedAddCommGroup
 
-instance orderedSemiring [∀ i, OrderedSemiring (f i)] : OrderedSemiring (∀ i, f i) :=
-  { Pi.semiring,
-    Pi.partialOrder with
-    add_le_add_left := fun _ _ hab _ _ => add_le_add_left (hab _) _
-    zero_le_one := fun i => zero_le_one (α := f i)
-    mul_le_mul_of_nonneg_left := fun _ _ _ hab hc _ => mul_le_mul_of_nonneg_left (hab _) <| hc _
-    mul_le_mul_of_nonneg_right := fun _ _ _ hab hc _ => mul_le_mul_of_nonneg_right (hab _) <| hc _ }
+instance orderedSemiring [∀ i, OrderedSemiring (f i)] : OrderedSemiring (∀ i, f i) where
+  __ := Pi.semiring
+  __ := Pi.partialOrder
+  add_le_add_left _ _ hab _ := fun _ => add_le_add_left (hab _) _
+  zero_le_one := fun i => zero_le_one (α := f i)
+  mul_le_mul_of_nonneg_left _ _ _ hab hc := fun _ => mul_le_mul_of_nonneg_left (hab _) <| hc _
+  mul_le_mul_of_nonneg_right _ _ _ hab hc := fun _ => mul_le_mul_of_nonneg_right (hab _) <| hc _
 #align pi.ordered_semiring Pi.orderedSemiring
 
-instance orderedCommSemiring [∀ i, OrderedCommSemiring (f i)] : OrderedCommSemiring (∀ i, f i) :=
-  { Pi.commSemiring, Pi.orderedSemiring with }
+instance orderedCommSemiring [∀ i, OrderedCommSemiring (f i)] : OrderedCommSemiring (∀ i, f i) where
+  __ := Pi.commSemiring
+  __ := Pi.orderedSemiring
 #align pi.ordered_comm_semiring Pi.orderedCommSemiring
 
-instance orderedRing [∀ i, OrderedRing (f i)] : OrderedRing (∀ i, f i) :=
-  { Pi.ring, Pi.orderedSemiring with mul_nonneg := fun _ _ ha hb _ => mul_nonneg (ha _) (hb _) }
+instance orderedRing [∀ i, OrderedRing (f i)] : OrderedRing (∀ i, f i) where
+  __ := Pi.ring
+  __ := Pi.orderedSemiring
+  mul_nonneg _ _ ha hb := fun _ => mul_nonneg (ha _) (hb _)
 #align pi.ordered_ring Pi.orderedRing
 
-instance orderedCommRing [∀ i, OrderedCommRing (f i)] : OrderedCommRing (∀ i, f i) :=
-  { Pi.commRing, Pi.orderedRing with }
+instance orderedCommRing [∀ i, OrderedCommRing (f i)] : OrderedCommRing (∀ i, f i) where
+  __ := Pi.commRing
+  __ := Pi.orderedRing
 #align pi.ordered_comm_ring Pi.orderedCommRing
 
 end Pi

Mathlib/Order/BooleanAlgebra.lean

@@ -112,11 +112,11 @@ theorem inf_sdiff_inf (x y : α) : x \ y ⊓ (x ⊓ y) = ⊥ := by rw [inf_comm,
 #align inf_sdiff_inf inf_sdiff_inf
 
 -- see Note [lower instance priority]
-instance (priority := 100) GeneralizedBooleanAlgebra.toOrderBot : OrderBot α :=
-  { GeneralizedBooleanAlgebra.toBot with
-    bot_le := fun a => by
-      rw [← inf_inf_sdiff a a, inf_assoc]
-      exact inf_le_left }
+instance (priority := 100) GeneralizedBooleanAlgebra.toOrderBot : OrderBot α where
+  __ := GeneralizedBooleanAlgebra.toBot
+  bot_le a := by
+    rw [← inf_inf_sdiff a a, inf_assoc]
+    exact inf_le_left
 #align generalized_boolean_algebra.to_order_bot GeneralizedBooleanAlgebra.toOrderBot
 
 theorem disjoint_inf_sdiff : Disjoint (x ⊓ y) (x \ y) :=
@@ -178,32 +178,33 @@ theorem inf_sdiff_self_left : y \ x ⊓ x = ⊥ := by rw [inf_comm, inf_sdiff_se
 
 -- see Note [lower instance priority]
 instance (priority := 100) GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra :
-    GeneralizedCoheytingAlgebra α :=
-  { ‹GeneralizedBooleanAlgebra α›, GeneralizedBooleanAlgebra.toOrderBot with
-    sdiff := (· \ ·),
-    sdiff_le_iff := fun y x z =>
-      ⟨fun h =>
-        le_of_inf_le_sup_le
-          (le_of_eq
-            (calc
-              y ⊓ y \ x = y \ x := inf_of_le_right sdiff_le'
-              _ = x ⊓ y \ x ⊔ z ⊓ y \ x :=
-                by rw [inf_eq_right.2 h, inf_sdiff_self_right, bot_sup_eq]
-              _ = (x ⊔ z) ⊓ y \ x := inf_sup_right.symm))
+    GeneralizedCoheytingAlgebra α where
+  __ := ‹GeneralizedBooleanAlgebra α›
+  __ := GeneralizedBooleanAlgebra.toOrderBot
+  sdiff := (· \ ·)
+  sdiff_le_iff y x z :=
+    ⟨fun h =>
+      le_of_inf_le_sup_le
+        (le_of_eq
           (calc
-            y ⊔ y \ x = y := sup_of_le_left sdiff_le'
-            _ ≤ y ⊔ (x ⊔ z) := le_sup_left
-            _ = y \ x ⊔ x ⊔ z := by rw [← sup_assoc, ← @sdiff_sup_self' _ x y]
-            _ = x ⊔ z ⊔ y \ x := by ac_rfl),
-        fun h =>
-        le_of_inf_le_sup_le
-          (calc
-            y \ x ⊓ x = ⊥ := inf_sdiff_self_left
-            _ ≤ z ⊓ x := bot_le)
-          (calc
-            y \ x ⊔ x = y ⊔ x := sdiff_sup_self'
-            _ ≤ x ⊔ z ⊔ x := sup_le_sup_right h x
-            _ ≤ z ⊔ x := by rw [sup_assoc, sup_comm, sup_assoc, sup_idem])⟩ }
+            y ⊓ y \ x = y \ x := inf_of_le_right sdiff_le'
+            _ = x ⊓ y \ x ⊔ z ⊓ y \ x :=
+              by rw [inf_eq_right.2 h, inf_sdiff_self_right, bot_sup_eq]
+            _ = (x ⊔ z) ⊓ y \ x := inf_sup_right.symm))
+        (calc
+          y ⊔ y \ x = y := sup_of_le_left sdiff_le'
+          _ ≤ y ⊔ (x ⊔ z) := le_sup_left
+          _ = y \ x ⊔ x ⊔ z := by rw [← sup_assoc, ← @sdiff_sup_self' _ x y]
+          _ = x ⊔ z ⊔ y \ x := by ac_rfl),
+      fun h =>
+      le_of_inf_le_sup_le
+        (calc
+          y \ x ⊓ x = ⊥ := inf_sdiff_self_left
+          _ ≤ z ⊓ x := bot_le)
+        (calc
+          y \ x ⊔ x = y ⊔ x := sdiff_sup_self'
+          _ ≤ x ⊔ z ⊔ x := sup_le_sup_right h x
+          _ ≤ z ⊔ x := by rw [sup_assoc, sup_comm, sup_assoc, sup_idem])⟩
 #align generalized_boolean_algebra.to_generalized_coheyting_algebra GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra
 
 theorem disjoint_sdiff_self_left : Disjoint (y \ x) x :=
@@ -556,15 +557,17 @@ instance (priority := 100) BooleanAlgebra.toBoundedOrder [h : BooleanAlgebra α]
 /-- A bounded generalized boolean algebra is a boolean algebra. -/
 @[reducible]
 def GeneralizedBooleanAlgebra.toBooleanAlgebra [GeneralizedBooleanAlgebra α] [OrderTop α] :
-    BooleanAlgebra α :=
-  { ‹GeneralizedBooleanAlgebra α›, GeneralizedBooleanAlgebra.toOrderBot, ‹OrderTop α› with
-    compl := fun a => ⊤ \ a,
-    inf_compl_le_bot := fun _ => disjoint_sdiff_self_right.le_bot,
-    top_le_sup_compl := fun _ => le_sup_sdiff,
-    sdiff_eq := fun _ _ => by
+    BooleanAlgebra α where
+  __ := ‹GeneralizedBooleanAlgebra α›
+  __ := GeneralizedBooleanAlgebra.toOrderBot
+  __ := ‹OrderTop α›
+  compl a := ⊤ \ a
+  inf_compl_le_bot _ := disjoint_sdiff_self_right.le_bot
+  top_le_sup_compl _ := le_sup_sdiff
+  sdiff_eq _ _ := by
       -- Porting note: changed `rw` to `erw` here.
       -- https://github.com/leanprover-community/mathlib4/issues/5164
-      erw [← inf_sdiff_assoc, inf_top_eq] }
+      erw [← inf_sdiff_assoc, inf_top_eq]
 #align generalized_boolean_algebra.to_boolean_algebra GeneralizedBooleanAlgebra.toBooleanAlgebra
 
 section BooleanAlgebra
@@ -603,20 +606,21 @@ instance (priority := 100) BooleanAlgebra.toComplementedLattice : ComplementedLa
 
 -- see Note [lower instance priority]
 instance (priority := 100) BooleanAlgebra.toGeneralizedBooleanAlgebra :
-    GeneralizedBooleanAlgebra α :=
-  { ‹BooleanAlgebra α› with
-    sup_inf_sdiff := fun a b => by rw [sdiff_eq, ← inf_sup_left, sup_compl_eq_top, inf_top_eq],
-    inf_inf_sdiff := fun a b => by
-      rw [sdiff_eq, ← inf_inf_distrib_left, inf_compl_eq_bot', inf_bot_eq] }
+    GeneralizedBooleanAlgebra α where
+  __ := ‹BooleanAlgebra α›
+  sup_inf_sdiff a b := by rw [sdiff_eq, ← inf_sup_left, sup_compl_eq_top, inf_top_eq]
+  inf_inf_sdiff a b := by
+    rw [sdiff_eq, ← inf_inf_distrib_left, inf_compl_eq_bot', inf_bot_eq]
 #align boolean_algebra.to_generalized_boolean_algebra BooleanAlgebra.toGeneralizedBooleanAlgebra
 
 -- See note [lower instance priority]
-instance (priority := 100) BooleanAlgebra.toBiheytingAlgebra : BiheytingAlgebra α :=
-  { ‹BooleanAlgebra α›, GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra with
-    hnot := compl,
-    le_himp_iff := fun a b c => by rw [himp_eq, isCompl_compl.le_sup_right_iff_inf_left_le],
-    himp_bot := fun _ => _root_.himp_eq.trans bot_sup_eq,
-    top_sdiff := fun a => by rw [sdiff_eq, top_inf_eq]; rfl }
+instance (priority := 100) BooleanAlgebra.toBiheytingAlgebra : BiheytingAlgebra α where
+  __ := ‹BooleanAlgebra α›
+  __ := GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra
+  hnot := compl
+  le_himp_iff a b c := by rw [himp_eq, isCompl_compl.le_sup_right_iff_inf_left_le]
+  himp_bot _ := _root_.himp_eq.trans bot_sup_eq
+  top_sdiff a := by rw [sdiff_eq, top_inf_eq]; rfl
 #align boolean_algebra.to_biheyting_algebra BooleanAlgebra.toBiheytingAlgebra
 
 @[simp]
@@ -724,15 +728,15 @@ theorem compl_le_iff_compl_le : xᶜ ≤ y ↔ yᶜ ≤ x :=
 theorem sdiff_compl : x \ yᶜ = x ⊓ y := by rw [sdiff_eq, compl_compl]
 #align sdiff_compl sdiff_compl
 
-instance OrderDual.booleanAlgebra (α) [BooleanAlgebra α] : BooleanAlgebra αᵒᵈ :=
-  { OrderDual.distribLattice α, OrderDual.boundedOrder α with
-    compl := fun a => toDual (ofDual aᶜ),
-    sdiff :=
-      fun a b => toDual (ofDual b ⇨ ofDual a), himp := fun a b => toDual (ofDual b \ ofDual a),
-    inf_compl_le_bot := fun a => (@codisjoint_hnot_right _ _ (ofDual a)).top_le,
-    top_le_sup_compl := fun a => (@disjoint_compl_right _ _ (ofDual a)).le_bot,
-    sdiff_eq := fun _ _ => @himp_eq α _ _ _,
-    himp_eq := fun _ _ => @sdiff_eq α _ _ _, }
+instance OrderDual.booleanAlgebra (α) [BooleanAlgebra α] : BooleanAlgebra αᵒᵈ where
+  __ := OrderDual.distribLattice α
+  __ := OrderDual.boundedOrder α
+  compl a := toDual (ofDual aᶜ)
+  sdiff a b := toDual (ofDual b ⇨ ofDual a); himp := fun a b => toDual (ofDual b \ ofDual a)
+  inf_compl_le_bot a := (@codisjoint_hnot_right _ _ (ofDual a)).top_le
+  top_le_sup_compl a := (@disjoint_compl_right _ _ (ofDual a)).le_bot
+  sdiff_eq _ _ := @himp_eq α _ _ _
+  himp_eq _ _ := @sdiff_eq α _ _ _
 
 @[simp]
 theorem sup_inf_inf_compl : x ⊓ y ⊔ x ⊓ yᶜ = x := by rw [← sdiff_eq, sup_inf_sdiff _ _]
@@ -786,12 +790,13 @@ lemma himp_ne_right : x ⇨ y ≠ x ↔ x ≠ ⊤ ∨ y ≠ ⊤ := himp_eq_left.
 
 end BooleanAlgebra
 
-instance Prop.booleanAlgebra : BooleanAlgebra Prop :=
-  { Prop.heytingAlgebra, GeneralizedHeytingAlgebra.toDistribLattice with
-    compl := Not,
-    himp_eq := fun p q => propext imp_iff_or_not,
-    inf_compl_le_bot := fun p ⟨Hp, Hpc⟩ => Hpc Hp,
-    top_le_sup_compl := fun p _ => Classical.em p }
+instance Prop.booleanAlgebra : BooleanAlgebra Prop where
+  __ := Prop.heytingAlgebra
+  __ := GeneralizedHeytingAlgebra.toDistribLattice
+  compl := Not
+  himp_eq p q := propext imp_iff_or_not
+  inf_compl_le_bot p H := H.2 H.1
+  top_le_sup_compl p _ := Classical.em p
 #align Prop.boolean_algebra Prop.booleanAlgebra
 
 instance Prod.booleanAlgebra (α β) [BooleanAlgebra α] [BooleanAlgebra β] :
@@ -804,12 +809,14 @@ instance Prod.booleanAlgebra (α β) [BooleanAlgebra α] [BooleanAlgebra β] :
   top_le_sup_compl x := by constructor <;> simp
 
 instance Pi.booleanAlgebra {ι : Type u} {α : ι → Type v} [∀ i, BooleanAlgebra (α i)] :
-    BooleanAlgebra (∀ i, α i) :=
-  { Pi.sdiff, Pi.heytingAlgebra, @Pi.distribLattice ι α _ with
-    sdiff_eq := fun _ _ => funext fun _ => sdiff_eq,
-    himp_eq := fun _ _ => funext fun _ => himp_eq,
-    inf_compl_le_bot := fun _ _ => BooleanAlgebra.inf_compl_le_bot _,
-    top_le_sup_compl := fun _ _ => BooleanAlgebra.top_le_sup_compl _ }
+    BooleanAlgebra (∀ i, α i) where
+  __ := Pi.sdiff
+  __ := Pi.heytingAlgebra
+  __ := @Pi.distribLattice ι α _
+  sdiff_eq _ _ := funext fun _ => sdiff_eq
+  himp_eq _ _ := funext fun _ => himp_eq
+  inf_compl_le_bot _ _ := BooleanAlgebra.inf_compl_le_bot _
+  top_le_sup_compl _ _ := BooleanAlgebra.top_le_sup_compl _
 #align pi.boolean_algebra Pi.booleanAlgebra
 
 instance Bool.instBooleanAlgebra : BooleanAlgebra Bool where
@@ -844,11 +851,11 @@ protected def Function.Injective.generalizedBooleanAlgebra [Sup α] [Inf α] [Bo
     [GeneralizedBooleanAlgebra β] (f : α → β) (hf : Injective f)
     (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b)
     (map_bot : f ⊥ = ⊥) (map_sdiff : ∀ a b, f (a \ b) = f a \ f b) :
-    GeneralizedBooleanAlgebra α :=
-  { hf.generalizedCoheytingAlgebra f map_sup map_inf map_bot map_sdiff,
-    hf.distribLattice f map_sup map_inf with
-    sup_inf_sdiff := fun a b => hf <| by erw [map_sup, map_sdiff, map_inf, sup_inf_sdiff],
-    inf_inf_sdiff := fun a b => hf <| by erw [map_inf, map_sdiff, map_inf, inf_inf_sdiff, map_bot] }
+    GeneralizedBooleanAlgebra α where
+  __ := hf.generalizedCoheytingAlgebra f map_sup map_inf map_bot map_sdiff
+  __ := hf.distribLattice f map_sup map_inf
+  sup_inf_sdiff a b := hf <| by erw [map_sup, map_sdiff, map_inf, sup_inf_sdiff]
+  inf_inf_sdiff a b := hf <| by erw [map_inf, map_sdiff, map_inf, inf_inf_sdiff, map_bot]
 #align function.injective.generalized_boolean_algebra Function.Injective.generalizedBooleanAlgebra
 
 -- See note [reducible non-instances]
@@ -858,19 +865,17 @@ protected def Function.Injective.booleanAlgebra [Sup α] [Inf α] [Top α] [Bot
     [SDiff α] [BooleanAlgebra β] (f : α → β) (hf : Injective f)
     (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b)
     (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) (map_compl : ∀ a, f aᶜ = (f a)ᶜ)
-    (map_sdiff : ∀ a b, f (a \ b) = f a \ f b) : BooleanAlgebra α :=
-  { hf.generalizedBooleanAlgebra f map_sup map_inf map_bot map_sdiff with
-    compl := compl,
-    top := ⊤,
-    le_top := fun a => (@le_top β _ _ _).trans map_top.ge,
-    bot_le := fun a => map_bot.le.trans bot_le,
-    inf_compl_le_bot :=
-      fun a => ((map_inf _ _).trans <| by rw [map_compl, inf_compl_eq_bot, map_bot]).le,
-    top_le_sup_compl :=
-      fun a => ((map_sup _ _).trans <| by rw [map_compl, sup_compl_eq_top, map_top]).ge,
-    sdiff_eq := fun a b => by
-      refine hf ((map_sdiff _ _).trans (sdiff_eq.trans ?_))
-      rw [map_inf, map_compl] }
+    (map_sdiff : ∀ a b, f (a \ b) = f a \ f b) : BooleanAlgebra α where
+  __ := hf.generalizedBooleanAlgebra f map_sup map_inf map_bot map_sdiff
+  compl := compl
+  top := ⊤
+  le_top a := (@le_top β _ _ _).trans map_top.ge
+  bot_le a := map_bot.le.trans bot_le
+  inf_compl_le_bot a := ((map_inf _ _).trans <| by rw [map_compl, inf_compl_eq_bot, map_bot]).le
+  top_le_sup_compl a := ((map_sup _ _).trans <| by rw [map_compl, sup_compl_eq_top, map_top]).ge
+  sdiff_eq a b := by
+    refine hf ((map_sdiff _ _).trans (sdiff_eq.trans ?_))
+    rw [map_inf, map_compl]
 #align function.injective.boolean_algebra Function.Injective.booleanAlgebra
 
 end lift

Mathlib/Order/BoundedOrder.lean

@@ -622,11 +622,11 @@ theorem top_def [∀ i, Top (α' i)] : (⊤ : ∀ i, α' i) = fun _ => ⊤ :=
   rfl
 #align pi.top_def Pi.top_def
 
-instance orderTop [∀ i, LE (α' i)] [∀ i, OrderTop (α' i)] : OrderTop (∀ i, α' i) :=
-  { inferInstanceAs (Top (∀ i, α' i)) with le_top := fun _ _ => le_top }
+instance orderTop [∀ i, LE (α' i)] [∀ i, OrderTop (α' i)] : OrderTop (∀ i, α' i) where
+  le_top _ := fun _ => le_top
 
-instance orderBot [∀ i, LE (α' i)] [∀ i, OrderBot (α' i)] : OrderBot (∀ i, α' i) :=
-  { inferInstanceAs (Bot (∀ i, α' i)) with bot_le := fun _ _ => bot_le }
+instance orderBot [∀ i, LE (α' i)] [∀ i, OrderBot (α' i)] : OrderBot (∀ i, α' i) where
+  bot_le _ := fun _ => bot_le
 
 instance boundedOrder [∀ i, LE (α' i)] [∀ i, BoundedOrder (α' i)] : BoundedOrder (∀ i, α' i) where
   __ := inferInstanceAs (OrderTop (∀ i, α' i))
@@ -691,8 +691,10 @@ def OrderBot.lift [LE α] [Bot α] [LE β] [OrderBot β] (f : α → β)
 /-- Pullback a `BoundedOrder`. -/
 @[reducible]
 def BoundedOrder.lift [LE α] [Top α] [Bot α] [LE β] [BoundedOrder β] (f : α → β)
-    (map_le : ∀ a b, f a ≤ f b → a ≤ b) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) : BoundedOrder α :=
-  { OrderTop.lift f map_le map_top, OrderBot.lift f map_le map_bot with }
+    (map_le : ∀ a b, f a ≤ f b → a ≤ b) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) :
+    BoundedOrder α where
+  __ := OrderTop.lift f map_le map_top
+  __ := OrderBot.lift f map_le map_bot
 #align bounded_order.lift BoundedOrder.lift
 
 end lift
@@ -724,8 +726,9 @@ protected def orderTop [LE α] [OrderTop α] (htop : p ⊤) : OrderTop { x : α
 /-- A subtype remains a bounded order if the property holds at `⊥` and `⊤`. -/
 @[reducible]
 protected def boundedOrder [LE α] [BoundedOrder α] (hbot : p ⊥) (htop : p ⊤) :
-    BoundedOrder (Subtype p) :=
-  { Subtype.orderTop htop, Subtype.orderBot hbot with }
+    BoundedOrder (Subtype p) where
+  __ := Subtype.orderTop htop
+  __ := Subtype.orderBot hbot
 #align subtype.bounded_order Subtype.boundedOrder
 
 variable [PartialOrder α]