Address review comments from YaelDillies

- Rename `Embedding.comp_toHom` → `Embedding.toHom_comp` (Maps.lean)
- Add `protected` to `IsInduced.map` (Subgraph.lean)
- Rename `IsInduced.toEmbedding` → `Embedding.ofIsInduced`, move outside
  `Subgraph` namespace so it lives in `SimpleGraph.Embedding` (Subgraph.lean)
- Drop redundant `simp only [indLabelledCopyCount, labelledCopyCount]` (Copy.lean)
- Style: `¬(H ⊴ G)` → `¬ H ⊴ G` (Copy.lean)
- Golf `indCopyCount_le_copyCount` with `grind` (Copy.lean)

Author: FordUniver

Mathlib/Combinatorics/SimpleGraph/Copy.lean

@@ -201,7 +201,8 @@ lemma range_embeddingToSubgraph :
   · rintro ⟨f, rfl⟩
     exact ⟨Subgraph.IsInduced.top.map f, ⟨f.toCopy.isoToSubgraph⟩⟩
   · rintro ⟨hInd, ⟨e⟩⟩
-    exact ⟨hInd.toEmbedding.comp e.toEmbedding, by simp [toSubgraph, Subgraph.map_comp]⟩
+    exact ⟨(Embedding.ofIsInduced _ hInd).comp e.toEmbedding,
+      by simp [toSubgraph, Subgraph.map_comp]⟩
 
 lemma toSubgraph_surjOn :
     Set.SurjOn (toSubgraph (A := A)) .univ {B' : B.Subgraph | Nonempty (A ≃g B'.coe)} :=
@@ -427,7 +428,7 @@ protected lemma Iso.isIndContained' (e : G ≃g H) : H ⊴ G := e.symm.isIndCont
 
 protected lemma Subgraph.IsInduced.isIndContained {G' : G.Subgraph} (hG' : G'.IsInduced) :
     G'.coe ⊴ G :=
-  ⟨hG'.toEmbedding⟩
+  ⟨Embedding.ofIsInduced _ hG'⟩
 
 @[refl] lemma IsIndContained.refl (G : SimpleGraph V) : G ⊴ G := ⟨Embedding.refl⟩
 lemma IsIndContained.rfl : G ⊴ G := .refl _
@@ -575,7 +576,7 @@ noncomputable def indLabelledCopyCount (G : SimpleGraph V) (H : SimpleGraph W) :
   exact { default := RelEmbedding.ofIsEmpty H.Adj G.Adj
           uniq := fun f => RelEmbedding.ext fun a => isEmptyElim a }
 
-@[simp] lemma indLabelledCopyCount_eq_zero : G.indLabelledCopyCount H = 0 ↔ ¬(H ⊴ G) := by
+@[simp] lemma indLabelledCopyCount_eq_zero : G.indLabelledCopyCount H = 0 ↔ ¬ H ⊴ G := by
   simp [indLabelledCopyCount, Fintype.card_eq_zero_iff, IsIndContained]
 
 @[simp] lemma indLabelledCopyCount_pos : 0 < G.indLabelledCopyCount H ↔ H ⊴ G := by
@@ -585,7 +586,6 @@ noncomputable def indLabelledCopyCount (G : SimpleGraph V) (H : SimpleGraph W) :
 lemma indLabelledCopyCount_le_labelledCopyCount :
     G.indLabelledCopyCount H ≤ G.labelledCopyCount H := by
   classical
-  simp only [indLabelledCopyCount, labelledCopyCount]
   exact Fintype.card_le_of_injective Embedding.toCopy fun f g h =>
     RelEmbedding.ext fun w => DFunLike.congr_fun h w
 
@@ -616,7 +616,7 @@ lemma indCopyCount_eq_card_image_embeddingToSubgraph
   exact ⟨fun ⟨G', hInd, hn⟩ => ⟨G', hn.some, hInd⟩,
          fun ⟨G', e, hInd⟩ => ⟨G', hInd, ⟨e⟩⟩⟩
 
-@[simp] lemma indCopyCount_eq_zero : G.indCopyCount H = 0 ↔ ¬(H ⊴ G) := by
+@[simp] lemma indCopyCount_eq_zero : G.indCopyCount H = 0 ↔ ¬ H ⊴ G := by
   rw [← indCopyCount_pos]; omega
 
 /-- Every induced unlabelled copy corresponds to at least one induced labelled copy. -/
@@ -638,7 +638,7 @@ lemma indCopyCount_le_copyCount : G.indCopyCount H ≤ G.copyCount H := by
   classical
   simp only [indCopyCount, copyCount]
   exact Finset.card_le_card fun G' hG' => by
-    simp only [mem_filter, mem_univ, true_and] at hG' ⊢; exact hG'.2
+    simp only [mem_filter, mem_univ, true_and] at hG'; grind
 
 end IndCopyCount
 

Mathlib/Combinatorics/SimpleGraph/Maps.lean

@@ -529,7 +529,7 @@ abbrev comp (f' : G' ↪g G'') (f : G ↪g G') : G ↪g G'' :=
 theorem coe_comp (f' : G' ↪g G'') (f : G ↪g G') : ⇑(f'.comp f) = f' ∘ f :=
   rfl
 
-@[simp] lemma comp_toHom (f' : G' ↪g G'') (f : G ↪g G') :
+@[simp] lemma toHom_comp (f' : G' ↪g G'') (f : G ↪g G') :
     (f'.comp f).toHom = f'.toHom.comp f.toHom := rfl
 
 /-- Graph embeddings from `G` to `H` are the same thing as graph embeddings from `Gᶜ` to `Hᶜ`. -/

Mathlib/Combinatorics/SimpleGraph/Subgraph.lean

@@ -669,7 +669,7 @@ theorem map_sup (f : G →g G') (H₁ H₂ : G.Subgraph) : (H₁ ⊔ H₂).map f
 @[simp] lemma edgeSet_map (f : G →g G') (H : G.Subgraph) :
     (H.map f).edgeSet = Sym2.map f '' H.edgeSet := Sym2.fromRel_relationMap ..
 
-lemma IsInduced.map {H : G.Subgraph} (hH : H.IsInduced) (e : G ↪g G') :
+protected lemma IsInduced.map {H : G.Subgraph} (hH : H.IsInduced) (e : G ↪g G') :
     (H.map e.toHom).IsInduced := by
   intro v hv w hw hAdj
   rw [map_verts] at hv hw
@@ -756,15 +756,6 @@ theorem hom_injective {x : Subgraph G} : Function.Injective x.hom :=
 @[simp] lemma map_hom_top (G' : G.Subgraph) : Subgraph.map G'.hom ⊤ = G' := by
   aesop (add unfold safe Relation.Map, unsafe G'.edge_vert, unsafe Adj.symm)
 
-/-- The canonical embedding of an induced subgraph into the ambient graph.
-Unlike `Subgraph.hom`, this is an embedding rather than a homomorphism, since induced subgraphs
-reflect adjacency. -/
-def IsInduced.toEmbedding {G' : G.Subgraph} (hG' : G'.IsInduced) : G'.coe ↪g G :=
-  { toFun := (↑), inj' := Subtype.coe_injective, map_rel_iff' := hG'.adj.symm }
-
-@[simp] lemma IsInduced.toHom_toEmbedding {G' : G.Subgraph} (hG' : G'.IsInduced) :
-    hG'.toEmbedding.toHom = G'.hom := rfl
-
 /-- There is an induced injective homomorphism of a subgraph of `G` as
 a spanning subgraph into `G`. -/
 @[simps]
@@ -886,6 +877,16 @@ lemma adj_iff_of_neighborSet_equiv {v : V} {H : Subgraph G}
 
 end Subgraph
 
+/-- The canonical embedding of an induced subgraph into the ambient graph.
+Unlike `Subgraph.hom`, this is an embedding rather than a homomorphism, since induced subgraphs
+reflect adjacency. -/
+def Embedding.ofIsInduced {G : SimpleGraph V} (G' : G.Subgraph) (hG' : G'.IsInduced) :
+    G'.coe ↪g G :=
+  { toFun := (↑), inj' := Subtype.coe_injective, map_rel_iff' := hG'.adj.symm }
+
+@[simp] lemma Embedding.toHom_ofIsInduced {G : SimpleGraph V} (G' : G.Subgraph)
+    (hG' : G'.IsInduced) : (Embedding.ofIsInduced G' hG').toHom = G'.hom := rfl
+
 @[simp]
 theorem card_neighborSet_toSubgraph (G H : SimpleGraph V) (h : H ≤ G)
     (v : V) [Fintype ↑((toSubgraph H h).neighborSet v)] [Fintype ↑(H.neighborSet v)] :