feat(Topology): use OrderHomClass for CompactExhaustion (#6461)

Also rename `is_compact'` field to `isCompact'`.

Author: urkud

Mathlib/Topology/SubsetProperties.lean

@@ -1443,7 +1443,7 @@ structure CompactExhaustion (X : Type*) [TopologicalSpace X] where
   /-- The sequence of compact sets that form a compact exhaustion. -/
   toFun : ℕ → Set X
   /-- The sets in the compact exhaustion are in fact compact. -/
-  is_compact' : ∀ n, IsCompact (toFun n)
+  isCompact' : ∀ n, IsCompact (toFun n)
   /-- The sets in the compact exhaustion form a sequence:
     each set is contained in the interior of the next. -/
   subset_interior_succ' : ∀ n, toFun n ⊆ interior (toFun (n + 1))
@@ -1453,29 +1453,33 @@ structure CompactExhaustion (X : Type*) [TopologicalSpace X] where
 
 namespace CompactExhaustion
 
--- porting note: todo: use `FunLike`?
-instance : CoeFun (CompactExhaustion α) fun _ => ℕ → Set α :=
-  ⟨toFun⟩
+instance : @RelHomClass (CompactExhaustion α) ℕ (Set α) LE.le HasSubset.Subset where
+  coe := toFun
+  coe_injective' | ⟨_, _, _, _⟩, ⟨_, _, _, _⟩, rfl => rfl
+  map_rel f _ _ h := monotone_nat_of_le_succ
+    (fun n ↦ (f.subset_interior_succ' n).trans interior_subset) h
 
 variable (K : CompactExhaustion α)
 
+@[simp]
+theorem toFun_eq_coe : K.toFun = K := rfl
+
 protected theorem isCompact (n : ℕ) : IsCompact (K n) :=
-  K.is_compact' n
+  K.isCompact' n
 #align compact_exhaustion.is_compact CompactExhaustion.isCompact
 
 theorem subset_interior_succ (n : ℕ) : K n ⊆ interior (K (n + 1)) :=
   K.subset_interior_succ' n
 #align compact_exhaustion.subset_interior_succ CompactExhaustion.subset_interior_succ
 
-theorem subset_succ (n : ℕ) : K n ⊆ K (n + 1) :=
-  Subset.trans (K.subset_interior_succ n) interior_subset
-#align compact_exhaustion.subset_succ CompactExhaustion.subset_succ
-
 @[mono]
 protected theorem subset ⦃m n : ℕ⦄ (h : m ≤ n) : K m ⊆ K n :=
-  show K m ≤ K n from monotone_nat_of_le_succ K.subset_succ h
+  OrderHomClass.mono K h
 #align compact_exhaustion.subset CompactExhaustion.subset
 
+theorem subset_succ (n : ℕ) : K n ⊆ K (n + 1) := K.subset n.le_succ
+#align compact_exhaustion.subset_succ CompactExhaustion.subset_succ
+
 theorem subset_interior ⦃m n : ℕ⦄ (h : m < n) : K m ⊆ interior (K n) :=
   Subset.trans (K.subset_interior_succ m) <| interior_mono <| K.subset h
 #align compact_exhaustion.subset_interior CompactExhaustion.subset_interior
@@ -1504,7 +1508,7 @@ theorem mem_iff_find_le {x : α} {n : ℕ} : x ∈ K n ↔ K.find x ≤ n :=
 /-- Prepend the empty set to a compact exhaustion `K n`. -/
 def shiftr : CompactExhaustion α where
   toFun n := Nat.casesOn n ∅ K
-  is_compact' n := Nat.casesOn n isCompact_empty K.isCompact
+  isCompact' n := Nat.casesOn n isCompact_empty K.isCompact
   subset_interior_succ' n := Nat.casesOn n (empty_subset _) K.subset_interior_succ
   iUnion_eq' := iUnion_eq_univ_iff.2 fun x => ⟨K.find x + 1, K.mem_find x⟩
 #align compact_exhaustion.shiftr CompactExhaustion.shiftr