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

Remove `@[expose] public section`; add `@[expose]` selectively to `toEmbedding`,
`id`, `ofLE`, and `topEmbedding`, which have exported `rfl`-proved `@[simp]` lemmas.
Change `IsIndContained` from `def` to `abbrev` for elaborator transparency.
Replace `@[simps!]` on `topEmbedding` with an explicit `topEmbedding_apply` lemma.
Add missing `toEmbedding_apply` simp lemma for API symmetry with `toHom_apply`.

Author: FordUniver

Mathlib/Combinatorics/SimpleGraph/Copy.lean

@@ -59,7 +59,7 @@ The following notation is declared in scope `SimpleGraph`:
 * Make `copyCount`/`labeledCopyCount` computable (not necessarily efficiently).
 -/
 
-@[expose] public section
+public section
 
 open Finset Function
 open Fintype (card)
@@ -125,10 +125,12 @@ def mapNeighborSet (f : Copy A B) (a : α) :
     exact f.injective h
 
 /-- A copy gives rise to an embedding of vertex types. -/
-def toEmbedding (f : Copy A B) : α ↪ β := ⟨f, f.injective⟩
+@[expose] def toEmbedding (f : Copy A B) : α ↪ β := ⟨f, f.injective⟩
+
+@[simp] lemma toEmbedding_apply (f : Copy A B) (a : α) : 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
 
@@ -143,7 +145,8 @@ theorem comp_apply (g : Copy B C) (f : Copy A B) (a : α) : 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 B C) (f : Copy A B) : ⇑(g.comp f) = g ∘ f := by ext; simp
@@ -200,10 +203,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 α) G) : (⊤ : SimpleGraph α) ↪g G :=
+@[expose] def topEmbedding (f : Copy (⊤ : SimpleGraph α) G) : (⊤ : SimpleGraph α) ↪g G :=
   { 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 α) G) (v : α) :
+    f.topEmbedding v = f v := rfl
 
 end Copy
 
@@ -385,7 +390,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