style(Combinatorics/SimpleGraph): tidy two more namespace/order issues

* `InducedCopy.lean`: flatten the two-decl `namespace Copy` block around
  `Copy.toEmbeddingOfIsInduced` / `Copy.toEmbeddingOfIsInduced_apply` to prefixed names.
  Saves the `namespace`/`end` pair and one indentation level for two declarations.

* `Copy.lean`: move `Copy.toSubgraph_comp` up to sit between `toSubgraph_adj_iff` and
  `mem_range_of_toSubgraph_eq`. The new order is basic-to-complex:

    toSubgraph (def) → isoToSubgraph / range_toSubgraph / toSubgraph_surjOn (existing
    image API) → verts_toSubgraph / toSubgraph_adj_iff / toSubgraph_comp (basic
    "shape" facts) → mem_range_of_toSubgraph_eq / equivOfToSubgraphEq / _apply (multi-copy
    facts using classical choice).

  `toSubgraph_comp` is a one-line functoriality fact; pairing it with `verts_*` and
  `*_adj_iff` rather than burying it after the equivOfToSubgraphEq classical-choice
  scaffolding mirrors the order already used on the Embedding side in `InducedCopy.lean`.

Author: FordUniver

Mathlib/Combinatorics/SimpleGraph/Copy.lean

@@ -208,6 +208,12 @@ lemma toSubgraph_surjOn :
   rintro ⟨c, d, hcd, hc, hd⟩
   rwa [f.injective hc, f.injective hd] at hcd
 
+/-- Functoriality of `Copy.toSubgraph`: composing two copies and taking the image subgraph is the
+same as taking the image subgraph of the inner copy and mapping it through the outer. -/
+@[simp] lemma toSubgraph_comp (g : Copy H I) (f : Copy G H) :
+    (g.comp f).toSubgraph = f.toSubgraph.map g.toHom := by
+  simp [toSubgraph, Subgraph.map_comp]
+
 lemma mem_range_of_toSubgraph_eq {f f' : Copy G H} (h : f.toSubgraph = f'.toSubgraph) (v : V) :
     f v ∈ Set.range (f' : V → W) := by
   rw [← f'.verts_toSubgraph, ← congrArg Subgraph.verts h, f.verts_toSubgraph]
@@ -233,12 +239,6 @@ noncomputable def equivOfToSubgraphEq {f f' : Copy G H} (h : f.toSubgraph = f'.t
     (v : V) : f' (equivOfToSubgraphEq h v) = f v :=
   (mem_range_of_toSubgraph_eq h v).choose_spec
 
-/-- Functoriality of `Copy.toSubgraph`: composing two copies and taking the image subgraph is the
-same as taking the image subgraph of the inner copy and mapping it through the outer. -/
-@[simp] lemma toSubgraph_comp (g : Copy H I) (f : Copy G H) :
-    (g.comp f).toSubgraph = f.toSubgraph.map g.toHom := by
-  simp [toSubgraph, Subgraph.map_comp]
-
 instance [Subsingleton (V → W)] : Subsingleton (G.Copy H) := DFunLike.coe_injective.subsingleton
 
 instance [Fintype {f : G →g H // Injective f}] : Fintype (G.Copy H) :=

Mathlib/Combinatorics/SimpleGraph/InducedCopy.lean

@@ -122,11 +122,9 @@ end Embedding
 
 /-! ### Promoting a copy with induced image to an embedding -/
 
-namespace Copy
-
 /-- A copy whose image subgraph is induced canonically promotes to an embedding,
 providing the converse direction to `Embedding.toSubgraph` / `Embedding.toSubgraph_isInduced`. -/
-@[expose] def toEmbeddingOfIsInduced (f : Copy G H) (hInd : f.toSubgraph.IsInduced) :
+@[expose] def Copy.toEmbeddingOfIsInduced (f : Copy G H) (hInd : f.toSubgraph.IsInduced) :
     Embedding G H where
   toFun := f
   inj' := f.injective
@@ -136,11 +134,9 @@ providing the converse direction to `Embedding.toSubgraph` / `Embedding.toSubgra
            (f.verts_toSubgraph ▸ Set.mem_range_self b) hAdj,
      fun hAdj ↦ f.toHom.map_adj hAdj⟩
 
-@[simp] lemma toEmbeddingOfIsInduced_apply (f : Copy G H) (hInd : f.toSubgraph.IsInduced)
+@[simp] lemma Copy.toEmbeddingOfIsInduced_apply (f : Copy G H) (hInd : f.toSubgraph.IsInduced)
     (v : V) : f.toEmbeddingOfIsInduced hInd v = f v := rfl
 
-end Copy
-
 /-!
 ### Induced containment