refactor(Combinatorics/SimpleGraph/InducedCopy): hoist Embedding.toSubgraph API to the top

Moves the `namespace Embedding` block (containing `toSubgraph`, `toSubgraph_isInduced`, and
`range_toSubgraph`) out of `section UnlabeledEmbeddingCount` to its own block immediately after the
`SimpleGraph` namespace opens, with a section heading `Embedding to subgraph`.

This mirrors `Copy.lean`'s structure (where `Copy.toSubgraph` and `range_toSubgraph` live in the
early `section Copy` / `namespace Copy` block alongside the type's core API, separately from the
count sections). The previous placement nested the core embedding-image API inside the unlabelled
count section, which made it harder to find when navigating the file.

Pure code motion: no statement, proof, or attribute changes.

Author: FordUniver

Mathlib/Combinatorics/SimpleGraph/InducedCopy.lean

@@ -57,6 +57,38 @@ variable {V V' W W' X : Type*}
   {H : SimpleGraph W} {H' : SimpleGraph W'}
   {I : SimpleGraph X}
 
+/-!
+### Embedding to subgraph
+
+For a graph embedding `f : G ↪g H`, the image is an induced subgraph of `H` isomorphic to `G`.
+This packages the image as a `H.Subgraph`, together with the inducedness and isomorphism
+characterisations needed downstream.
+-/
+
+namespace Embedding
+
+/-- The induced subgraph corresponding to an embedding. -/
+abbrev toSubgraph (f : G ↪g H) : H.Subgraph := f.toCopy.toSubgraph
+
+@[simp] lemma toSubgraph_isInduced (f : G ↪g H) : (toSubgraph f).IsInduced := by
+  simp [toSubgraph, Copy.toSubgraph, Subgraph.IsInduced, Relation.map_apply_apply, f.injective]
+
+@[simp] lemma range_toSubgraph :
+    Set.range (toSubgraph : (G ↪g H) → H.Subgraph) =
+      {H' : H.Subgraph | H'.IsInduced ∧ Nonempty (G ≃g H'.coe)} := by
+  ext H'
+  simp only [Set.mem_range, Set.mem_setOf_eq]
+  constructor
+  · rintro ⟨f, rfl⟩
+    exact ⟨toSubgraph_isInduced f, ⟨f.toCopy.isoToSubgraph⟩⟩
+  · rintro ⟨hInd, ⟨e⟩⟩
+    refine ⟨(ofIsInduced H' hInd).comp e.toEmbedding, ?_⟩
+    have h : ((ofIsInduced H' hInd).comp e.toEmbedding).toHom =
+        H'.hom.comp e.toHom := by ext; simp
+    simp [toSubgraph, Copy.toSubgraph, h, Subgraph.map_comp]
+
+end Embedding
+
 /-!
 ### Induced containment
 
@@ -249,30 +281,6 @@ abbrev UnlabeledEmbedding (G : SimpleGraph V) (H : SimpleGraph W) : Type _ :=
 
 instance [Finite W] : Finite (G.UnlabeledEmbedding H) := Subtype.finite
 
-namespace Embedding
-
-/-- The induced subgraph corresponding to an embedding. -/
-abbrev toSubgraph (f : G ↪g H) : H.Subgraph := f.toCopy.toSubgraph
-
-@[simp] lemma toSubgraph_isInduced (f : G ↪g H) : (toSubgraph f).IsInduced := by
-  simp [toSubgraph, Copy.toSubgraph, Subgraph.IsInduced, Relation.map_apply_apply, f.injective]
-
-@[simp] lemma range_toSubgraph :
-    Set.range (toSubgraph : (G ↪g H) → H.Subgraph) =
-      {H' : H.Subgraph | H'.IsInduced ∧ Nonempty (G ≃g H'.coe)} := by
-  ext H'
-  simp only [Set.mem_range, Set.mem_setOf_eq]
-  constructor
-  · rintro ⟨f, rfl⟩
-    exact ⟨toSubgraph_isInduced f, ⟨f.toCopy.isoToSubgraph⟩⟩
-  · rintro ⟨hInd, ⟨e⟩⟩
-    refine ⟨(ofIsInduced H' hInd).comp e.toEmbedding, ?_⟩
-    have h : ((ofIsInduced H' hInd).comp e.toEmbedding).toHom =
-        H'.hom.comp e.toHom := by ext; simp
-    simp [toSubgraph, Copy.toSubgraph, h, Subgraph.map_comp]
-
-end Embedding
-
 /-- `H.unlabeledEmbeddingCount G` is the number of induced `SimpleGraph.Subgraph`s of `H`
 isomorphic to `G`.
 See `SimpleGraph.embeddingCount` for the number of induced labeled copies. -/