feat(Combinatorics/SimpleGraph): extract apply_mem_verts_toSubgraph for Copy + Embedding

`f v ∈ f.toSubgraph.verts` is a basic membership fact about `Copy.toSubgraph` —
combining `verts_toSubgraph` (`f.toSubgraph.verts = Set.range f`) with the obvious
`v ∈ Set.range f`. It was inlined twice as `f.verts_toSubgraph ▸ Set.mem_range_self _`
inside `Copy.toEmbeddingOfIsInduced`. Extract and use the named lemma; mirror on the
Embedding side.

Author: FordUniver

Mathlib/Combinatorics/SimpleGraph/Copy.lean

@@ -201,6 +201,9 @@ lemma toSubgraph_surjOn :
 @[simp] lemma verts_toSubgraph (f : Copy G H) : f.toSubgraph.verts = Set.range f := by
   simp [toSubgraph, Subgraph.map_verts, Set.image_univ]
 
+lemma apply_mem_verts_toSubgraph (f : Copy G H) (v : V) : f v ∈ f.toSubgraph.verts :=
+  f.verts_toSubgraph ▸ Set.mem_range_self v
+
 @[simp] lemma toSubgraph_adj_iff (f : Copy G H) {a b : V} :
     f.toSubgraph.Adj (f a) (f b) ↔ G.Adj a b := by
   simp only [toSubgraph, Subgraph.map_adj, Subgraph.top_adj, Relation.map_apply]

Mathlib/Combinatorics/SimpleGraph/InducedCopy.lean

@@ -83,6 +83,9 @@ abbrev toSubgraph (f : Embedding G H) : H.Subgraph := f.toCopy.toSubgraph
 @[simp] lemma verts_toSubgraph (f : Embedding G H) : f.toSubgraph.verts = Set.range f :=
   f.toCopy.verts_toSubgraph
 
+lemma apply_mem_verts_toSubgraph (f : Embedding G H) (v : V) : f v ∈ f.toSubgraph.verts :=
+  f.toCopy.apply_mem_verts_toSubgraph v
+
 @[simp] lemma toSubgraph_adj_iff (f : Embedding G H) {a b : V} :
     f.toSubgraph.Adj (f a) (f b) ↔ G.Adj a b :=
   f.toCopy.toSubgraph_adj_iff
@@ -130,8 +133,7 @@ providing the converse direction to `Embedding.toSubgraph` / `Embedding.toSubgra
   inj' := f.injective
   map_rel_iff' {a b} :=
     ⟨fun hAdj ↦ f.toSubgraph_adj_iff.mp <|
-      hInd (f.verts_toSubgraph ▸ Set.mem_range_self a)
-           (f.verts_toSubgraph ▸ Set.mem_range_self b) hAdj,
+      hInd (f.apply_mem_verts_toSubgraph a) (f.apply_mem_verts_toSubgraph b) hAdj,
      fun hAdj ↦ f.toHom.map_adj hAdj⟩
 
 @[simp] lemma Copy.toEmbeddingOfIsInduced_apply (f : Copy G H) (hInd : f.toSubgraph.IsInduced)