chore(Data/SetLike/Basic): generalise instance (leanprover-community#40025)

* Generalise the standard `IsConcreteLE` instance from `PartialOrder.ofSetLike` to `LE.ofSetLike`

Co-authored-by: artie2000 <artem.khovanov@gmail.com>

Author: artie2000

Mathlib/Data/SetLike/Basic.lean

@@ -224,10 +224,17 @@ section default
 
 variable (A B : Type*) [SetLike A B]
 
-/-- The order induced from a `SetLike` instance by inclusion. -/
+/-- The order induced from a `SetLike` instance by inclusion.
+
+An order defined as `.ofSetLike` will automatically make available an instance
+of `IsConcreteLE`.
+-/
 @[reducible] def LE.ofSetLike : LE A where
   le := fun H K => ∀ ⦃x⦄, x ∈ H → x ∈ K
 
+instance : letI := LE.ofSetLike A B; IsConcreteLE A B :=
+  letI := LE.ofSetLike A B; { coe_subset_coe' := Iff.rfl }
+
 /-- The partial order induced from a `SetLike` instance by inclusion.
 
 A partial order defined as `.ofSetLike` will automatically make available an instance
@@ -238,9 +245,6 @@ of `IsConcreteLE`.
   lt s t := letI := LE.ofSetLike A B; s ≤ t ∧ ¬t ≤ s
   __ := PartialOrder.lift (SetLike.coe : A → Set B) SetLike.coe_injective
 
-instance : letI := PartialOrder.ofSetLike A B; IsConcreteLE A B :=
-  letI := PartialOrder.ofSetLike A B; { coe_subset_coe' := Iff.rfl }
-
 end default
 
 namespace SetLike