chore(Combinatorics/SimpleGraph): drop @[simp] on {Copy,Embedding}.{verts_toSubgraph,toSubgraph_adj_iff}

The four lemmas don't pass the `simpNF` linter: the `verts_toSubgraph`
pair is already discharged by simp via the `@[simps]`-generated
`Subgraph.map_verts` + `Subgraph.verts_top` + `Set.image_univ`, and the
`toSubgraph_adj_iff` LHS gets rewritten under `Subgraph.map_adj` /
`Copy.coe_toHom` before the iff can match. The statements are still
useful as named non-simp rewrites (the `adj_iff` pair carries genuine
injectivity content used in `Automorphism.lean`, and the `verts`
equation supports `mem_range_of_toSubgraph_eq`), so just drop the
attribute.

Author: FordUniver

Mathlib/Combinatorics/SimpleGraph/Copy.lean

@@ -198,13 +198,13 @@ lemma toSubgraph_surjOn :
     Set.SurjOn (toSubgraph (G := G)) .univ {H' : H.Subgraph | Nonempty (G ≃g H'.coe)} :=
   fun H' hH' ↦ by simpa
 
-@[simp] lemma verts_toSubgraph (f : Copy G H) : f.toSubgraph.verts = Set.range f := by
+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} :
+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]
   refine ⟨?_, fun hab ↦ ⟨a, b, hab, rfl, rfl⟩⟩

Mathlib/Combinatorics/SimpleGraph/InducedCopy.lean

@@ -80,13 +80,13 @@ abbrev toSubgraph (f : Embedding G H) : H.Subgraph := f.toCopy.toSubgraph
     (g.comp f).toSubgraph = f.toSubgraph.map g.toHom := by
   simp [toSubgraph]
 
-@[simp] lemma verts_toSubgraph (f : Embedding G H) : f.toSubgraph.verts = Set.range f :=
+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} :
+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