chore(Combinatorics.SimpleGraph.Copy): replace file-wide @[expose] with selective exposure

Replace `@[expose] public section` with a plain `public section` and
restore selective `@[expose]` on only the declarations that need
cross-module reduction:

* `Copy.toEmbedding`, `Copy.id`, `Copy.ofLE`, `Copy.topEmbedding` — the
  small constructive copy `def`s, kept transparent so consumers can
  elaborate against them by reducing.
* `copyCount`, `subCount` — the noncomputable counts. These need to be
  exposed so downstream files (e.g. the upcoming `InducedCopy.lean` in
  feat/ind-copy-count) can prove bridging inequalities like
  `embCount_le_copyCount` and `indSubCount_le_subCount` directly via
  `Nat.card_le_card_of_injective`.

Also:

* Inline the `@[simps!]` projections of `Copy.topEmbedding` into a manual
  `@[simp] lemma topEmbedding_apply` (and similarly for `Copy.toEmbedding`).
  The auto-generated `simps` form attached to `@[simps!]` was opaque to
  cross-module simp; the manual form is small enough to ship as a one-line
  named lemma. The body of `topEmbedding` is also tightened from
  `fun {v w} ↦ ⟨fun h ↦ by simpa using h.ne, _⟩` to
  `fun {_ _} ↦ ⟨fun h ↦ f.injective.ne_iff.mp h.ne, _⟩`.
* `IsIndContained` switches from `def` to `abbrev`, since the body
  `Nonempty (G ↪g H)` is small and downstream Lean elaboration benefits
  from automatic unfolding here.

Author: FordUniver

Mathlib/Combinatorics/SimpleGraph/Copy.lean

@@ -75,7 +75,7 @@ Argument *order* follows mathlib's two conventions, one for each category:
 * Add densities `copyDensity G H`, `subDensity G H`, and `homDensity G H`.
 -/
 
-@[expose] public section
+public section
 
 open Finset Function
 open Fintype (card)
@@ -139,10 +139,12 @@ def mapNeighborSet (f : Copy G H) (a : V) :
     exact f.injective h
 
 /-- A copy gives rise to an embedding of vertex types. -/
-def toEmbedding (f : Copy G H) : V ↪ W := ⟨f, f.injective⟩
+@[expose] def toEmbedding (f : Copy G H) : V ↪ W := ⟨f, f.injective⟩
+
+@[simp] lemma toEmbedding_apply (f : Copy G H) (a : V) : f.toEmbedding a = f a := rfl
 
 /-- The identity copy from a simple graph to itself. -/
-@[refl] def id (G : SimpleGraph V) : Copy G G := ⟨Hom.id, Function.injective_id⟩
+@[expose, refl] def id (G : SimpleGraph V) : Copy G G := ⟨Hom.id, Function.injective_id⟩
 
 @[simp, norm_cast] lemma coe_id : ⇑(id G) = _root_.id := rfl
 
@@ -157,7 +159,8 @@ theorem comp_apply (g : Copy H I) (f : Copy G H) (a : V) : g.comp f a = g (f a)
   RelHom.comp_apply g.toHom f.toHom a
 
 /-- The copy from a subgraph to the supergraph. -/
-def ofLE (G₁ G₂ : SimpleGraph V) (h : G₁ ≤ G₂) : Copy G₁ G₂ := ⟨Hom.ofLE h, Function.injective_id⟩
+@[expose] def ofLE (G₁ G₂ : SimpleGraph V) (h : G₁ ≤ G₂) : Copy G₁ G₂ :=
+    ⟨Hom.ofLE h, Function.injective_id⟩
 
 @[simp, norm_cast]
 theorem coe_comp (g : Copy H I) (f : Copy G H) : ⇑(g.comp f) = g ∘ f := by ext; simp
@@ -214,10 +217,12 @@ instance [Fintype {f : G →g H // Injective f}] : Fintype (G.Copy H) :=
   }
 
 /-- A copy of `⊤` gives rise to an embedding of `⊤`. -/
-@[simps!]
-def topEmbedding (f : Copy (⊤ : SimpleGraph V) H) : (⊤ : SimpleGraph V) ↪g H :=
+@[expose] def topEmbedding (f : Copy (⊤ : SimpleGraph V) H) : (⊤ : SimpleGraph V) ↪g H :=
   { f.toEmbedding with
-    map_rel_iff' := fun {v w} ↦ ⟨fun h ↦ by simpa using h.ne, f.toHom.map_adj⟩}
+    map_rel_iff' := fun {_ _} ↦ ⟨fun h ↦ f.injective.ne_iff.mp h.ne, f.toHom.map_adj⟩ }
+
+@[simp] lemma topEmbedding_apply (f : Copy (⊤ : SimpleGraph V) H) (v : V) :
+    f.topEmbedding v = f v := rfl
 
 end Copy
 
@@ -404,7 +409,7 @@ We denote "`G` is inducingly contained in `H`" by `G ⊴ H` (`\trianglelefteq`).
 
 /-- A simple graph `G` is inducingly contained in a simple graph `H` if there exists an induced
 subgraph of `H` isomorphic to `G`. This is denoted by `G ⊴ H`. -/
-def IsIndContained (G : SimpleGraph V) (H : SimpleGraph W) : Prop := Nonempty (G ↪g H)
+abbrev IsIndContained (G : SimpleGraph V) (H : SimpleGraph W) : Prop := Nonempty (G ↪g H)
 
 @[inherit_doc] scoped infixl:50 " ⊴ " => SimpleGraph.IsIndContained
 
@@ -497,7 +502,7 @@ variable [Fintype V] [Fintype W]
 /-- `H.copyCount G` is the number of labeled copies of `G` in `H`, i.e. the number of injective
 graph homomorphisms from `G` to `H`. See `SimpleGraph.subCount` for the number of unlabeled
 copies. -/
-noncomputable def copyCount (H : SimpleGraph W) (G : SimpleGraph V) : ℕ := by
+@[expose] noncomputable def copyCount (H : SimpleGraph W) (G : SimpleGraph V) : ℕ := by
   classical exact Fintype.card (Copy G H)
 
 @[deprecated (since := "2026-04-30")] alias labelledCopyCount := copyCount
@@ -532,7 +537,7 @@ abbrev Sub (G : SimpleGraph V) (H : SimpleGraph W) : Type _ :=
 
 /-- `H.subCount G` is the number of `SimpleGraph.Subgraph`s of `H` isomorphic to `G`. See
 `SimpleGraph.copyCount` for the number of labeled copies. -/
-noncomputable def subCount (H : SimpleGraph W) (G : SimpleGraph V) : ℕ := by
+@[expose] noncomputable def subCount (H : SimpleGraph W) (G : SimpleGraph V) : ℕ := by
   classical exact Fintype.card (G.Sub H)
 
 @[simp] lemma subCount_eq_zero : H.subCount G = 0 ↔ G.Free H := by