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 constructive copy `def`s that
need cross-module reduction: `Copy.toEmbedding`, `Copy.id`, `Copy.ofLE`,
`Copy.topEmbedding`.

The noncomputable counting defs `copyCount`/`subCount` remain non-exposed;
the cross-module unfolding API they need is added in the immediately
following `chore/copy-nat-card` PR, paired with the switch from
`Fintype.card` to `Nat.card` which makes the unfolding lemmas trivial.

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