chore: try to use fast_instance in basic definitions

Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

@@ -90,7 +90,7 @@ lemma toSubmodule_injective : (toSubmodule : NonUnitalSubalgebra R A → Submodu
 lemma toSubmodule_inj {s t : NonUnitalSubalgebra R A} : s.toSubmodule = t.toSubmodule ↔ s = t :=
   toSubmodule_injective.eq_iff
 
-instance : PartialOrder (NonUnitalSubalgebra R A) := .ofSetLike (NonUnitalSubalgebra R A) A
+instance : PartialOrder (NonUnitalSubalgebra R A) := fast_instance% .ofSetLike (NonUnitalSubalgebra R A) A
 
 /-- The actual `NonUnitalSubalgebra` obtained from an element of a type satisfying
 `NonUnitalSubsemiringClass` and `SMulMemClass`. -/

Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

@@ -46,7 +46,7 @@ instance : SetLike (Subalgebra R A) A where
   coe s := s.carrier
   coe_injective' p q h := by cases p; cases q; congr; exact SetLike.coe_injective' h
 
-instance : PartialOrder (Subalgebra R A) := .ofSetLike (Subalgebra R A) A
+instance : PartialOrder (Subalgebra R A) := fast_instance% .ofSetLike (Subalgebra R A) A
 
 initialize_simps_projections Subalgebra (carrier → coe, as_prefix coe)
 

Mathlib/Algebra/Field/Subfield/Defs.lean

@@ -149,7 +149,7 @@ instance : SetLike (Subfield K) K where
   coe s := s.carrier
   coe_injective' p q h := by cases p; cases q; congr; exact SetLike.ext' h
 
-instance : PartialOrder (Subfield K) := .ofSetLike (Subfield K) K
+instance : PartialOrder (Subfield K) := fast_instance% .ofSetLike (Subfield K) K
 
 instance : SubfieldClass (Subfield K) K where
   add_mem {s} := s.add_mem'

Mathlib/Algebra/Group/Subgroup/Defs.lean

@@ -320,7 +320,7 @@ instance : SetLike (Subgroup G) G where
     obtain ⟨⟨⟨hq, _⟩, _⟩, _⟩ := q
     congr
 
-@[to_additive] instance : PartialOrder (Subgroup G) := .ofSetLike (Subgroup G) G
+@[to_additive] instance : PartialOrder (Subgroup G) := fast_instance% .ofSetLike (Subgroup G) G
 
 initialize_simps_projections Subgroup (carrier → coe, as_prefix coe)
 initialize_simps_projections AddSubgroup (carrier → coe, as_prefix coe)

Mathlib/Algebra/Group/Submonoid/Defs.lean

@@ -139,7 +139,7 @@ instance : SetLike (Submonoid M) M where
   coe s := s.carrier
   coe_injective' := SetLike.coe_injective.comp toSubsemigroup_injective
 
-@[to_additive] instance : PartialOrder (Submonoid M) := .ofSetLike (Submonoid M) M
+@[to_additive] instance : PartialOrder (Submonoid M) := fast_instance% .ofSetLike (Submonoid M) M
 
 initialize_simps_projections Submonoid (carrier → coe, as_prefix coe)
 initialize_simps_projections AddSubmonoid (carrier → coe, as_prefix coe)

Mathlib/Algebra/Group/Submonoid/Saturation.lean

@@ -122,7 +122,7 @@ instance : SetLike (SaturatedSubmonoid M) M where
   coe_injective' _ _ h := toSubmonoid_injective <| SetLike.coe_injective h
 
 @[to_additive]
-instance : PartialOrder (SaturatedSubmonoid M) := .ofSetLike ..
+instance : PartialOrder (SaturatedSubmonoid M) := fast_instance% .ofSetLike ..
 
 @[to_additive]
 lemma ext' {s₁ s₂ : SaturatedSubmonoid M} (h : ∀ x, x ∈ s₁ ↔ x ∈ s₂) : s₁ = s₂ :=

Mathlib/Algebra/Group/Subsemigroup/Defs.lean

@@ -98,7 +98,7 @@ namespace Subsemigroup
 instance : SetLike (Subsemigroup M) M :=
   ⟨Subsemigroup.carrier, fun p q h => by cases p; cases q; congr⟩
 
-@[to_additive] instance : PartialOrder (Subsemigroup M) := .ofSetLike (Subsemigroup M) M
+@[to_additive] instance : PartialOrder (Subsemigroup M) := fast_instance% .ofSetLike (Subsemigroup M) M
 
 initialize_simps_projections Subsemigroup (carrier → coe, as_prefix coe)
 initialize_simps_projections AddSubsemigroup (carrier → coe, as_prefix coe)

Mathlib/Algebra/Lie/Subalgebra.lean

@@ -68,7 +68,7 @@ instance : SetLike (LieSubalgebra R L) L where
     congr
     exact SetLike.coe_injective' h
 
-instance : PartialOrder (LieSubalgebra R L) := .ofSetLike (LieSubalgebra R L) L
+instance : PartialOrder (LieSubalgebra R L) := fast_instance% .ofSetLike (LieSubalgebra R L) L
 
 instance : AddSubgroupClass (LieSubalgebra R L) L where
   add_mem := Submodule.add_mem _

Mathlib/Algebra/Lie/Submodule.lean

@@ -55,7 +55,7 @@ instance : SetLike (LieSubmodule R L M) M where
   coe s := s.carrier
   coe_injective' N O h := by cases N; cases O; congr; exact SetLike.coe_injective' h
 
-instance : PartialOrder (LieSubmodule R L M) := .ofSetLike (LieSubmodule R L M) M
+instance : PartialOrder (LieSubmodule R L M) := fast_instance% .ofSetLike (LieSubmodule R L M) M
 
 instance : AddSubgroupClass (LieSubmodule R L M) M where
   add_mem {N} _ _ := N.add_mem'

Mathlib/Algebra/Module/Submodule/Defs.lean

@@ -55,7 +55,7 @@ instance setLike : SetLike (Submodule R M) M where
   coe s := s.carrier
   coe_injective' p q h := by cases p; cases q; congr; exact SetLike.coe_injective' h
 
-instance : PartialOrder (Submodule R M) := .ofSetLike (Submodule R M) M
+instance : PartialOrder (Submodule R M) := fast_instance% .ofSetLike (Submodule R M) M
 
 initialize_simps_projections Submodule (carrier → coe, as_prefix coe)
 

Mathlib/Algebra/Order/Group/Cone.lean

@@ -57,7 +57,7 @@ instance GroupCone.instSetLike (G : Type*) [CommGroup G] : SetLike (GroupCone G)
   coe_injective' p q h := by cases p; cases q; congr; exact SetLike.ext' h
 
 @[to_additive]
-instance (G : Type*) [CommGroup G] : PartialOrder (GroupCone G) := .ofSetLike (GroupCone G) G
+instance (G : Type*) [CommGroup G] : PartialOrder (GroupCone G) := fast_instance% .ofSetLike (GroupCone G) G
 
 @[to_additive]
 instance GroupCone.instGroupConeClass (G : Type*) [CommGroup G] :

Mathlib/Algebra/Order/Ring/Cone.lean

@@ -38,7 +38,7 @@ instance RingCone.instSetLike (R : Type*) [Ring R] : SetLike (RingCone R) R wher
   coe C := C.carrier
   coe_injective' p q h := by cases p; cases q; congr; exact SetLike.ext' h
 
-instance (R : Type*) [Ring R] : PartialOrder (RingCone R) := .ofSetLike (RingCone R) R
+instance (R : Type*) [Ring R] : PartialOrder (RingCone R) := fast_instance% .ofSetLike (RingCone R) R
 
 instance RingCone.instRingConeClass (R : Type*) [Ring R] :
     RingConeClass (RingCone R) R where

Mathlib/Algebra/Order/Ring/Ordering/Defs.lean

@@ -56,7 +56,7 @@ instance : SetLike (RingPreordering R) R where
   coe P := P.carrier
   coe_injective' p q h := by cases p; cases q; congr; exact SetLike.ext' h
 
-instance : PartialOrder (RingPreordering R) := .ofSetLike (RingPreordering R) R
+instance : PartialOrder (RingPreordering R) := fast_instance% .ofSetLike (RingPreordering R) R
 
 initialize_simps_projections RingPreordering (carrier → coe, as_prefix coe)
 

Mathlib/Algebra/Ring/Subring/Defs.lean

@@ -187,7 +187,7 @@ lemma toAddSubgroup_injective : (toAddSubgroup : Subring R → AddSubgroup R).In
 lemma toSubmonoid_injective : (fun s : Subring R => s.toSubmonoid).Injective :=
   fun _ _ h ↦ SetLike.ext (SetLike.ext_iff.mp h :)
 
-instance : PartialOrder (Subring R) := .ofSetLike (Subring R) R
+instance : PartialOrder (Subring R) := fast_instance% .ofSetLike (Subring R) R
 
 initialize_simps_projections Subring (carrier → coe, as_prefix coe)
 

Mathlib/Algebra/Ring/Subsemiring/Defs.lean

@@ -142,7 +142,7 @@ instance : SetLike (Subsemiring R) R where
   coe s := s.carrier
   coe_injective' p q h := by cases p; cases q; congr; exact SetLike.coe_injective' h
 
-instance : PartialOrder (Subsemiring R) := .ofSetLike (Subsemiring R) R
+instance : PartialOrder (Subsemiring R) := fast_instance% .ofSetLike (Subsemiring R) R
 
 initialize_simps_projections Subsemiring (carrier → coe, as_prefix coe)
 

Mathlib/Algebra/Star/NonUnitalSubalgebra.lean

@@ -119,7 +119,7 @@ instance instSetLike : SetLike (NonUnitalStarSubalgebra R A) A where
   coe {s} := s.carrier
   coe_injective' p q h := by cases p; cases q; congr; exact SetLike.coe_injective h
 
-instance : PartialOrder (NonUnitalStarSubalgebra R A) := .ofSetLike (NonUnitalStarSubalgebra R A) A
+instance : PartialOrder (NonUnitalStarSubalgebra R A) := fast_instance% .ofSetLike (NonUnitalStarSubalgebra R A) A
 
 /-- The actual `NonUnitalStarSubalgebra` obtained from an element of a type satisfying
 `NonUnitalSubsemiringClass`, `SMulMemClass` and `StarMemClass`. -/

Mathlib/Algebra/Star/Subalgebra.lean

@@ -43,7 +43,7 @@ instance setLike : SetLike (StarSubalgebra R A) A where
   coe S := S.carrier
   coe_injective' p q h := by obtain ⟨⟨⟨⟨⟨_, _⟩, _⟩, _⟩, _⟩, _⟩ := p; cases q; congr
 
-instance : PartialOrder (StarSubalgebra R A) := .ofSetLike (StarSubalgebra R A) A
+instance : PartialOrder (StarSubalgebra R A) := fast_instance% .ofSetLike (StarSubalgebra R A) A
 
 /-- The actual `StarSubalgebra` obtained from an element of a type satisfying `SubsemiringClass`,
 `SMulMemClass` and `StarMemClass`. -/

Mathlib/Analysis/Convex/Body.lean

@@ -64,7 +64,7 @@ instance : SetLike (ConvexBody V) V where
     cases L
     congr
 
-instance : PartialOrder (ConvexBody V) := .ofSetLike (ConvexBody V) V
+instance : PartialOrder (ConvexBody V) := fast_instance% .ofSetLike (ConvexBody V) V
 
 protected theorem convex (K : ConvexBody V) : Convex ℝ (K : Set V) :=
   K.convex'

Mathlib/Analysis/Convex/Cone/Basic.lean

@@ -78,7 +78,7 @@ instance : SetLike (ProperCone R E) E where
   coe C := C.carrier
   coe_injective' _ _ h := ProperCone.toPointedCone_injective <| SetLike.coe_injective h
 
-instance : PartialOrder (ProperCone R E) := .ofSetLike (ProperCone R E) E
+instance : PartialOrder (ProperCone R E) := fast_instance% .ofSetLike (ProperCone R E) E
 
 @[ext] lemma ext (h : ∀ x, x ∈ C₁ ↔ x ∈ C₂) : C₁ = C₂ := SetLike.ext h
 

Mathlib/Analysis/VonNeumannAlgebra/Basic.lean

@@ -83,7 +83,7 @@ instance instSetLike : SetLike (VonNeumannAlgebra H) (H →L[ℂ] H) where
   coe S := S.carrier
   coe_injective' S T h := by obtain ⟨⟨⟨⟨⟨⟨_, _⟩, _⟩, _⟩, _⟩, _⟩, _⟩ := S; cases T; congr
 
-instance : PartialOrder (VonNeumannAlgebra H) := .ofSetLike (VonNeumannAlgebra H) (H →L[ℂ] H)
+instance : PartialOrder (VonNeumannAlgebra H) := fast_instance% .ofSetLike (VonNeumannAlgebra H) (H →L[ℂ] H)
 
 noncomputable instance instStarMemClass : StarMemClass (VonNeumannAlgebra H) (H →L[ℂ] H) where
   star_mem {s} := s.star_mem'

Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean

@@ -173,7 +173,7 @@ instance : SetLike (Subgroupoid C) (Σ c d : C, c ⟶ d) where
   coe := toSet
   coe_injective' := fun ⟨S, _, _⟩ ⟨T, _, _⟩ h => by ext c d f; apply Set.ext_iff.1 h ⟨c, d, f⟩
 
-instance : PartialOrder (Subgroupoid C) := .ofSetLike (Subgroupoid C) (Σ c d : C, c ⟶ d)
+instance : PartialOrder (Subgroupoid C) := fast_instance% .ofSetLike (Subgroupoid C) (Σ c d : C, c ⟶ d)
 
 theorem mem_iff (S : Subgroupoid C) (F : Σ c d, c ⟶ d) : F ∈ S ↔ F.2.2 ∈ S.arrows F.1 F.2.1 :=
   Iff.rfl

Mathlib/Combinatorics/SimpleGraph/Ends/Defs.lean

@@ -54,7 +54,7 @@ instance ComponentCompl.setLike : SetLike (G.ComponentCompl K) V where
   coe := ComponentCompl.supp
   coe_injective' _ _ := ComponentCompl.supp_inj.mp
 
-instance : PartialOrder (G.ComponentCompl K) := .ofSetLike (G.ComponentCompl K) V
+instance : PartialOrder (G.ComponentCompl K) := fast_instance% .ofSetLike (G.ComponentCompl K) V
 
 @[simp]
 theorem ComponentCompl.mem_supp_iff {v : V} {C : ComponentCompl G K} :

Mathlib/Combinatorics/Young/YoungDiagram.lean

@@ -75,7 +75,7 @@ instance : SetLike YoungDiagram (ℕ × ℕ) where
   coe y := y.cells
   coe_injective' μ ν h := by rwa [YoungDiagram.ext_iff, ← Finset.coe_inj]
 
-instance : PartialOrder YoungDiagram := .ofSetLike YoungDiagram (ℕ × ℕ)
+instance : PartialOrder YoungDiagram := fast_instance% .ofSetLike YoungDiagram (ℕ × ℕ)
 
 @[simp]
 theorem mem_cells {μ : YoungDiagram} (c : ℕ × ℕ) : c ∈ μ.cells ↔ c ∈ μ :=

Mathlib/Data/Finset/Defs.lean

@@ -120,7 +120,7 @@ instance decidableMem [_h : DecidableEq α] (a : α) (s : Finset α) : Decidable
 @[simp] lemma forall_mem_not_eq {s : Finset α} {a : α} : (∀ b ∈ s, ¬ a = b) ↔ a ∉ s := by grind
 @[simp] lemma forall_mem_not_eq' {s : Finset α} {a : α} : (∀ b ∈ s, ¬ b = a) ↔ a ∉ s := by grind
 
-instance : PartialOrder (Finset α) := .ofSetLike (Finset α) α
+instance : PartialOrder (Finset α) := fast_instance% .ofSetLike (Finset α) α
 
 /-- Convert a finset to a set in the natural way. -/
 @[deprecated SetLike.coe (since := "2025-10-22")]

Mathlib/Data/Set/PowersetCard.lean

@@ -44,7 +44,7 @@ theorem mem_iff {s : Finset α} :
 
 instance : SetLike (powersetCard α n) α := SetLike.instSubtype
 
-instance : PartialOrder (Set.powersetCard α n) := .ofSetLike (Set.powersetCard α n) α
+instance : PartialOrder (Set.powersetCard α n) := fast_instance% .ofSetLike (Set.powersetCard α n) α
 
 @[simp]
 theorem coe_coe {s : powersetCard α n} :

Mathlib/Data/SetLike/Basic.lean

@@ -6,6 +6,7 @@ Authors: Eric Wieser
 module
 
 public import Mathlib.Tactic.Monotonicity.Attr
+public import Mathlib.Tactic.FastInstance
 public import Mathlib.Tactic.SetLike
 public import Mathlib.Data.Set.Basic
 
@@ -45,7 +46,7 @@ variable {X : Type*} [ObjectTypeclass X] {x : X}
 instance : SetLike (MySubobject X) X :=
   ⟨MySubobject.carrier, fun p q h => by cases p; cases q; congr!⟩
 
-instance : PartialOrder (MySubobject X) := .ofSetLike (MySubobject X) X
+instance : PartialOrder (MySubobject X) := fast_instance% .ofSetLike (MySubobject X) X
 
 @[simp] lemma mem_carrier {p : MySubobject X} : x ∈ p.carrier ↔ x ∈ (p : Set X) := Iff.rfl
 
@@ -227,14 +228,17 @@ variable (A B : Type*) [SetLike A B]
 @[reducible] def LE.ofSetLike : LE A where
   le := fun H K => ∀ ⦃x⦄, x ∈ H → x ∈ K
 
+/-- Auxiliary definition to construct the order from a `SetLike` instance by inclusion. -/
+@[reducible] def PartialOrder.ofSetLikeAux : PartialOrder A where
+  __ := LE.ofSetLike A B
+  __ := PartialOrder.lift (SetLike.coe : A → Set B) SetLike.coe_injective
+
 /-- The partial order induced from a `SetLike` instance by inclusion.
 
 A partial order defined as `.ofSetLike` will automatically make available an instance
-of `IsConcreteLE`.
--/
-@[reducible] def PartialOrder.ofSetLike : PartialOrder A where
-  __ := LE.ofSetLike A B
-  __ := PartialOrder.lift (SetLike.coe : A → Set B) SetLike.coe_injective
+of `IsConcreteLE`. -/
+@[implicit_reducible] def PartialOrder.ofSetLike : PartialOrder A :=
+  fast_instance% PartialOrder.ofSetLikeAux A B
 
 instance : letI := PartialOrder.ofSetLike A B; IsConcreteLE A B :=
   letI := PartialOrder.ofSetLike A B; { coe_subset_coe' := Iff.rfl }

Mathlib/Data/Sym/Sym2.lean

@@ -331,7 +331,7 @@ instance : SetLike (Sym2 α) α where
     simp only [mem_iff'] at hx hy hx' hy'
     aesop
 
-instance : PartialOrder (Sym2 α) := .ofSetLike (Sym2 α) α
+instance : PartialOrder (Sym2 α) := fast_instance% .ofSetLike (Sym2 α) α
 
 @[simp]
 theorem mem_iff_mem {x : α} {z : Sym2 α} : Sym2.Mem x z ↔ x ∈ z :=

Mathlib/FieldTheory/IntermediateField/Basic.lean

@@ -64,7 +64,7 @@ instance : SetLike (IntermediateField K L) L :=
     rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩
     simp ⟩
 
-instance : PartialOrder (IntermediateField K L) := .ofSetLike (IntermediateField K L) L
+instance : PartialOrder (IntermediateField K L) := fast_instance% .ofSetLike (IntermediateField K L) L
 
 protected theorem neg_mem {x : L} (hx : x ∈ S) : -x ∈ S := by
   change -x ∈ S.toSubalgebra; simpa

Mathlib/Geometry/Convex/Cone/Basic.lean

@@ -77,7 +77,7 @@ instance : SetLike (ConvexCone R M) M where
   coe := carrier
   coe_injective' C₁ C₂ h := by cases C₁; congr!
 
-instance : PartialOrder (ConvexCone R M) := .ofSetLike (ConvexCone R M) M
+instance : PartialOrder (ConvexCone R M) := fast_instance% .ofSetLike (ConvexCone R M) M
 
 @[simp, norm_cast] lemma coe_mk (s : Set M) (h₁ h₂) : ↑(mk (R := R) s h₁ h₂) = s := rfl
 

Mathlib/GroupTheory/FiniteIndexNormalSubgroup.lean

@@ -52,7 +52,7 @@ instance : SetLike (FiniteIndexNormalSubgroup G) G where
   coe_injective' _ _ h := toSubgroup_injective <| SetLike.ext' h
 
 @[to_additive]
-instance : PartialOrder (FiniteIndexNormalSubgroup G) := .ofSetLike (FiniteIndexNormalSubgroup G) G
+instance : PartialOrder (FiniteIndexNormalSubgroup G) := fast_instance% .ofSetLike (FiniteIndexNormalSubgroup G) G
 
 @[to_additive]
 instance : SubgroupClass (FiniteIndexNormalSubgroup G) G where

Mathlib/GroupTheory/GroupAction/SubMulAction.lean

@@ -212,7 +212,7 @@ variable [SMul R M]
 instance : SetLike (SubMulAction R M) M :=
   ⟨SubMulAction.carrier, fun p q h => by cases p; cases q; congr⟩
 
-@[to_additive] instance : PartialOrder (SubMulAction R M) := .ofSetLike (SubMulAction R M) M
+@[to_additive] instance : PartialOrder (SubMulAction R M) := fast_instance% .ofSetLike (SubMulAction R M) M
 
 @[to_additive]
 instance : SMulMemClass (SubMulAction R M) R M where smul_mem := smul_mem' _

Mathlib/GroupTheory/Sylow.lean

@@ -70,7 +70,7 @@ instance : SetLike (Sylow p G) G where
   coe := (↑)
   coe_injective' _ _ h := ext (SetLike.coe_injective h)
 
-instance : PartialOrder (Sylow p G) := .ofSetLike (Sylow p G) G
+instance : PartialOrder (Sylow p G) := fast_instance% .ofSetLike (Sylow p G) G
 
 instance : SubgroupClass (Sylow p G) G where
   mul_mem := Subgroup.mul_mem _

Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean

@@ -174,7 +174,7 @@ instance : SetLike (AffineSubspace k P) P where
   coe := carrier
   coe_injective' p q _ := by cases p; cases q; congr
 
-instance : PartialOrder (AffineSubspace k P) := .ofSetLike (AffineSubspace k P) P
+instance : PartialOrder (AffineSubspace k P) := fast_instance% .ofSetLike (AffineSubspace k P) P
 
 /-- A point is in an affine subspace coerced to a set if and only if it is in that affine
 subspace. -/

Mathlib/LinearAlgebra/Projectivization/Subspace.lean

@@ -60,7 +60,7 @@ instance : SetLike (Subspace K V) (ℙ K V) where
     cases B
     simp
 
-instance : PartialOrder (Subspace K V) := .ofSetLike (Subspace K V) (ℙ K V)
+instance : PartialOrder (Subspace K V) := fast_instance% .ofSetLike (Subspace K V) (ℙ K V)
 
 @[simp]
 theorem mem_carrier_iff (A : Subspace K V) (x : ℙ K V) : x ∈ A.carrier ↔ x ∈ A :=

Mathlib/ModelTheory/Definability.lean

@@ -296,7 +296,7 @@ instance instSetLike : SetLike (L.DefinableSet A α) (α → M) where
   coe := Subtype.val
   coe_injective' := Subtype.val_injective
 
-instance : PartialOrder (L.DefinableSet A α) := .ofSetLike (L.DefinableSet A α) (α → M)
+instance : PartialOrder (L.DefinableSet A α) := fast_instance% .ofSetLike (L.DefinableSet A α) (α → M)
 
 instance instTop : Top (L.DefinableSet A α) :=
   ⟨⟨⊤, definable_univ⟩⟩

Mathlib/ModelTheory/ElementarySubstructures.lean

@@ -62,7 +62,7 @@ instance instSetLike : SetLike (L.ElementarySubstructure M) M :=
   ⟨fun x => x.toSubstructure.carrier, fun ⟨⟨s, hs1⟩, hs2⟩ ⟨⟨t, ht1⟩, _⟩ _ => by
     congr⟩
 
-instance : PartialOrder (L.ElementarySubstructure M) := .ofSetLike (L.ElementarySubstructure M) M
+instance : PartialOrder (L.ElementarySubstructure M) := fast_instance% .ofSetLike (L.ElementarySubstructure M) M
 
 instance inducedStructure (S : L.ElementarySubstructure M) : L.Structure S :=
   Substructure.inducedStructure

Mathlib/ModelTheory/Substructures.lean

@@ -107,7 +107,7 @@ attribute [coe] Substructure.carrier
 instance instSetLike : SetLike (L.Substructure M) M :=
   ⟨Substructure.carrier, fun p q h => by cases p; cases q; congr⟩
 
-instance : PartialOrder (L.Substructure M) := .ofSetLike (L.Substructure M) M
+instance : PartialOrder (L.Substructure M) := fast_instance% .ofSetLike (L.Substructure M) M
 
 /-- See Note [custom simps projection] -/
 def Simps.coe (S : L.Substructure M) : Set M :=

Mathlib/ModelTheory/Types.lean

@@ -80,7 +80,7 @@ instance Sentence.instSetLike : SetLike (T.CompleteType α) L[[α]].Sentence :=
     cases q
     congr ⟩
 
-instance : PartialOrder (T.CompleteType α) := .ofSetLike (T.CompleteType α) (L[[α]].Sentence)
+instance : PartialOrder (T.CompleteType α) := fast_instance% .ofSetLike (T.CompleteType α) (L[[α]].Sentence)
 
 theorem isMaximal (p : T.CompleteType α) : IsMaximal (p : L[[α]].Theory) :=
   p.isMaximal'

Mathlib/Order/Basic.lean

@@ -8,6 +8,7 @@ module
 public import Mathlib.Data.Subtype
 public import Mathlib.Order.Defs.LinearOrder
 public import Mathlib.Order.Notation
+public import Mathlib.Tactic.FastInstance
 public import Mathlib.Tactic.Spread
 public import Mathlib.Tactic.Convert
 public import Mathlib.Tactic.Inhabit
@@ -730,7 +731,7 @@ See note [reducible non-instances]. -/
 abbrev PartialOrder.lift [PartialOrder β] (f : α → β) (inj : Injective f) : PartialOrder α :=
   letI _instLE : LE α := ⟨fun a b ↦ f a ≤ f b⟩
   letI _instLT : LT α := ⟨fun a b ↦ f a < f b⟩
-  Function.Injective.partialOrder f inj .rfl .rfl
+  fast_instance% Function.Injective.partialOrder f inj .rfl .rfl
 
 theorem compare_of_injective_eq_compareOfLessAndEq (a b : α) [LinearOrder β]
     [DecidableEq α] (f : α → β) (inj : Injective f)

Mathlib/Order/BooleanSubalgebra.lean

@@ -37,7 +37,7 @@ instance instSetLike : SetLike (BooleanSubalgebra α) α where
   coe L := L.carrier
   coe_injective' L M h := by obtain ⟨⟨_, _⟩, _⟩ := L; congr
 
-instance : PartialOrder (BooleanSubalgebra α) := .ofSetLike (BooleanSubalgebra α) α
+instance : PartialOrder (BooleanSubalgebra α) := fast_instance% .ofSetLike (BooleanSubalgebra α) α
 
 lemma coe_inj : (L : Set α) = M ↔ L = M := SetLike.coe_set_eq