diff --git a/Mathlib/Combinatorics/SimpleGraph/Copy.lean b/Mathlib/Combinatorics/SimpleGraph/Copy.lean
index f3662614ba254e..0d1835191942d5 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Copy.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Copy.lean
@@ -7,27 +7,32 @@ module
 
 public import Mathlib.Algebra.Order.Group.Nat
 public import Mathlib.Combinatorics.SimpleGraph.Subgraph
+public import Mathlib.Data.Finite.Card
+public import Mathlib.Data.Set.Finite.Range
 
 /-!
-# Containment of graphs
+# Copies, containment, and counting of subgraphs
 
-This file introduces the concept of one simple graph containing a copy of another.
+For two simple graphs `G` and `H`, a *(labeled) copy* of `G` in `H` is an injective map from the
+vertices of `G` into those of `H` that preserves adjacency, picking out a (not necessarily
+induced) subgraph of `H` isomorphic to `G`. An *unlabeled copy* drops the labeling and retains
+only the resulting subgraph.
 
-For two simple graphs `G` and `H`, a *copy* of `G` in `H` is a (not necessarily induced) subgraph of
-`H` isomorphic to `G`.
+If `H` contains a copy of `G`, we say that `H` *contains* `G`. If the copy is induced (i.e., the
+vertex map also *reflects* adjacency), we say that `H` *inducingly contains* `G`.
 
-If there exists a copy of `G` in `H`, we say that `H` *contains* `G`. This is equivalent to saying
-that there is an injective graph homomorphism `G → H` between them (this is **not** the same as a
-graph embedding, as we do not require the subgraph to be induced).
-
-If there exists an induced copy of `G` in `H`, we say that `H` *inducingly contains* `G`. This is
-equivalent to saying that there is a graph embedding `G ↪ H`.
+Throughout, `G` denotes the smaller guest, `H` the larger host, and `I` a third graph for
+transitivity, with letters in size order (`G < H < I`) matching the hom direction `G →g H` and
+the containment relation `G ⊑ H`. Types are guest-first (`Copy G H`, `Sub G H`, `IsContained G H`,
+…) and operations are host-first via dot notation (`H.copyCount G`, `H.subCount G`, …).
 
 ## Main declarations
 
 Containment:
-* `SimpleGraph.Copy G H` is the type of copies of `G` in `H`, implemented as the subtype of
-  *injective* homomorphisms.
+* `SimpleGraph.Copy G H` is the type of labeled copies of `G` in `H`, implemented as the subtype
+  of *injective* homomorphisms.
+* `SimpleGraph.Sub G H` is the type of unlabeled copies of `G` in `H`, implemented as the subtype
+  of `SimpleGraph.Subgraph`s of `H` isomorphic to `G`.
 * `SimpleGraph.IsContained G H`, `G ⊑ H` is the relation that `H` contains a copy of `G`, that
   is, the type of copies of `G` in `H` is nonempty. This is equivalent to the existence of an
   isomorphism from `G` to a subgraph of `H`.
@@ -35,16 +40,17 @@ Containment:
   same underlying vertex type.
 * `SimpleGraph.Free` is the predicate that `H` is `G`-free, that is, `H` does not contain a copy of
   `G`. This is the negation of `SimpleGraph.IsContained` implemented for convenience.
-* `SimpleGraph.killCopies G H`: Subgraph of `G` that does not contain `H`. Obtained by arbitrarily
-  removing an edge from each copy of `H` in `G`.
-* `SimpleGraph.copyCount G H`: Number of copies of `H` in `G`, i.e. number of subgraphs of `G`
-  isomorphic to `H`.
-* `SimpleGraph.labelledCopyCount G H`: Number of labelled copies of `H` in `G`, i.e. number of
-  graph embeddings from `H` to `G`.
+* `SimpleGraph.copyCount H G` is the number of labeled copies of `G` in `H`, i.e. the number of
+  injective graph homomorphisms from `G` to `H`.
+* `SimpleGraph.subCount H G` is the number of unlabeled copies of `G` in `H`, i.e. the number of
+  `SimpleGraph.Subgraph`s of `H` isomorphic to `G`.
+* `SimpleGraph.killCopies H G` is a subgraph of `H` that does not contain `G`, obtained by
+  arbitrarily removing an edge from each copy of `G` in `H`.
 
 Induced containment:
 * Induced copies of `G` inside `H` are already defined as `G ↪g H`.
-* `SimpleGraph.IsIndContained G H` : `G` is contained as an induced subgraph in `H`.
+* `SimpleGraph.IsIndContained G H` is the relation that `G` is contained as an induced subgraph
+  in `H`.
 
 ## Notation
 
@@ -56,97 +62,103 @@ The following notation is declared in scope `SimpleGraph`:
 
 * Relate `⊥ ⊴ H` to there being an independent set in `H`.
 * Count induced copies of a graph inside another.
-* Make `copyCount`/`labelledCopyCount` computable (not necessarily efficiently).
+* Make `copyCount`/`subCount` computable (not necessarily efficiently).
+* Count the number of graph homomorphisms `G →g H` with `homCount G H`.
+* Add densities `copyDensity G H`, `subDensity G H`, and `homDensity G H`.
+* Generalize `subCount_emptyGraph` to cross-universe `V`:
+  `H.subCount (⊥ : SimpleGraph V) = (Nat.card W).choose (Nat.card V)`, subsuming
+  `subCount_of_isEmpty` and the current diagonal `V = W` case.
+* Add `subCount_completeGraph` (clique count, naturally lives in `Clique.lean` since it
+  imports this file).
 -/
 
-@[expose] public section
+public section
 
 open Finset Function
-open Fintype (card)
 
 namespace SimpleGraph
-variable {V W X α β γ : Type*} {G G₁ G₂ G₃ : SimpleGraph V} {H : SimpleGraph W} {I : SimpleGraph X}
-  {A : SimpleGraph α} {B : SimpleGraph β} {C : SimpleGraph γ}
+variable {V V' W W' X : Type*}
+  {G G₁ G₂ G₃ : SimpleGraph V} {G' : SimpleGraph V'}
+  {H : SimpleGraph W} {H' : SimpleGraph W'}
+  {I : SimpleGraph X}
 
 /-!
 ### Copies
 
 #### Not necessarily induced copies
-
-A copy of a subgraph `G` inside a subgraph `H` is an embedding of the vertices of `G` into the
-vertices of `H`, such that adjacency in `G` implies adjacency in `H`.
-
-We capture this concept by injective graph homomorphisms.
 -/
 
 section Copy
 
 /-- The type of copies as a subtype of *injective* homomorphisms. -/
-structure Copy (A : SimpleGraph α) (B : SimpleGraph β) where
+structure Copy (G : SimpleGraph V) (H : SimpleGraph W) where
   /-- A copy gives rise to a homomorphism. -/
-  toHom : A →g B
+  toHom : G →g H
   injective' : Injective toHom
 
 /-- An injective homomorphism gives rise to a copy. -/
-abbrev Hom.toCopy (f : A →g B) (h : Injective f) : Copy A B := .mk f h
+abbrev Hom.toCopy (f : G →g H) (h : Injective f) : Copy G H := .mk f h
 
 /-- An embedding gives rise to a copy. -/
-abbrev Embedding.toCopy (f : A ↪g B) : Copy A B := f.toHom.toCopy f.injective
+abbrev Embedding.toCopy (f : G ↪g H) : Copy G H := f.toHom.toCopy f.injective
 
 /-- An isomorphism gives rise to a copy. -/
-abbrev Iso.toCopy (f : A ≃g B) : Copy A B := f.toEmbedding.toCopy
+abbrev Iso.toCopy (f : G ≃g H) : Copy G H := f.toEmbedding.toCopy
 
 namespace Copy
 
-instance : FunLike (Copy A B) α β where
+instance : FunLike (Copy G H) V W where
   coe f := DFunLike.coe f.toHom
   coe_injective' f g h := by obtain ⟨⟨_, _⟩, _⟩ := f; congr!
 
-lemma injective (f : Copy A B) : Injective f.toHom := f.injective'
+lemma injective (f : Copy G H) : Injective f.toHom := f.injective'
 
-@[ext] lemma ext {f g : Copy A B} : (∀ a, f a = g a) → f = g := DFunLike.ext _ _
+@[ext] lemma ext {f g : Copy G H} : (∀ a, f a = g a) → f = g := DFunLike.ext _ _
 
-@[simp] lemma coe_toHom (f : Copy A B) : ⇑f.toHom = f := rfl
-@[simp] lemma toHom_apply (f : Copy A B) (a : α) : ⇑f.toHom a = f a := rfl
+@[simp] lemma coe_toHom (f : Copy G H) : ⇑f.toHom = f := rfl
+@[simp] lemma toHom_apply (f : Copy G H) (a : V) : ⇑f.toHom a = f a := rfl
 
-@[simp] lemma coe_mk (f : A →g B) (hf) : ⇑(.mk f hf : Copy A B) = f := rfl
+@[simp] lemma coe_mk (f : G →g H) (hf) : ⇑(.mk f hf : Copy G H) = f := rfl
 
 /-- A copy induces an embedding of edge sets. -/
-def mapEdgeSet (f : Copy A B) : A.edgeSet ↪ B.edgeSet where
+def mapEdgeSet (f : Copy G H) : G.edgeSet ↪ H.edgeSet where
   toFun := f.toHom.mapEdgeSet
   inj' := Hom.mapEdgeSet.injective f.toHom f.injective
 
 /-- A copy induces an embedding of neighbor sets. -/
-def mapNeighborSet (f : Copy A B) (a : α) :
-    A.neighborSet a ↪ B.neighborSet (f a) where
+def mapNeighborSet (f : Copy G H) (a : V) :
+    G.neighborSet a ↪ H.neighborSet (f a) where
   toFun v := ⟨f v, f.toHom.apply_mem_neighborSet v.prop⟩
   inj' _ _ h := by
     rw [Subtype.mk_eq_mk] at h ⊢
     exact f.injective h
 
 /-- A copy gives rise to an embedding of vertex types. -/
-def toEmbedding (f : Copy A B) : α ↪ β := ⟨f, f.injective⟩
+@[expose] def toEmbedding (f : Copy G H) : V ↪ W := ⟨f, f.injective⟩
+
+@[simp] lemma toEmbedding_apply (f : Copy G H) (a : V) : f.toEmbedding a = f a := rfl
 
 /-- The identity copy from a simple graph to itself. -/
-@[refl] def id (G : SimpleGraph V) : Copy G G := ⟨Hom.id, Function.injective_id⟩
+@[expose, refl] def id (G : SimpleGraph V) : Copy G G := ⟨Hom.id, Function.injective_id⟩
 
 @[simp, norm_cast] lemma coe_id : ⇑(id G) = _root_.id := rfl
 
 /-- The composition of copies is a copy. -/
-def comp (g : Copy B C) (f : Copy A B) : Copy A C := by
+def comp (g : Copy H I) (f : Copy G H) : Copy G I := by
   use g.toHom.comp f.toHom
   rw [Hom.coe_comp]
   exact g.injective.comp f.injective
 
 @[simp]
-theorem comp_apply (g : Copy B C) (f : Copy A B) (a : α) : g.comp f a = g (f a) :=
+theorem comp_apply (g : Copy H I) (f : Copy G H) (a : V) : g.comp f a = g (f a) :=
   RelHom.comp_apply g.toHom f.toHom a
 
 /-- The copy from a subgraph to the supergraph. -/
-def ofLE (G₁ G₂ : SimpleGraph V) (h : G₁ ≤ G₂) : Copy G₁ G₂ := ⟨Hom.ofLE h, Function.injective_id⟩
+@[expose] def ofLE (G₁ G₂ : SimpleGraph V) (h : G₁ ≤ G₂) : Copy G₁ G₂ :=
+    ⟨Hom.ofLE h, Function.injective_id⟩
 
 @[simp, norm_cast]
-theorem coe_comp (g : Copy B C) (f : Copy A B) : ⇑(g.comp f) = g ∘ f := by ext; simp
+theorem coe_comp (g : Copy H I) (f : Copy G H) : ⇑(g.comp f) = g ∘ f := by ext; simp
 
 @[simp, norm_cast] lemma coe_ofLE (h : G₁ ≤ G₂) : ⇑(ofLE G₁ G₂ h) = _root_.id := rfl
 
@@ -160,25 +172,25 @@ theorem ofLE_comp (h₁₂ : G₁ ≤ G₂) (h₂₃ : G₂ ≤ G₃) :
 def induce (G : SimpleGraph V) (s : Set V) : Copy (G.induce s) G := (Embedding.induce s).toCopy
 
 /-- The copy of `⊥` in any simple graph that can embed its vertices. -/
-protected def bot (f : α ↪ β) : Copy (⊥ : SimpleGraph α) B := ⟨⟨f, False.elim⟩, f.injective⟩
+protected def bot (f : V ↪ W) : Copy (⊥ : SimpleGraph V) H := ⟨⟨f, False.elim⟩, f.injective⟩
 
 set_option backward.isDefEq.respectTransparency false in
-/-- The isomorphism from a subgraph of `A` to its map under a copy `f : Copy A B`. -/
-noncomputable def isoSubgraphMap (f : Copy A B) (A' : A.Subgraph) :
-    A'.coe ≃g (A'.map f.toHom).coe := by
+/-- The isomorphism from a subgraph of `G` to its map under a copy `f : Copy G H`. -/
+noncomputable def isoSubgraphMap (f : Copy G H) (G' : G.Subgraph) :
+    G'.coe ≃g (G'.map f.toHom).coe := by
   use Equiv.Set.image f.toHom _ f.injective
   simp_rw [Subgraph.map_verts, Equiv.Set.image_apply, Subgraph.coe_adj, Subgraph.map_adj,
     Relation.map_apply, f.injective.eq_iff, exists_eq_right_right, exists_eq_right, forall_true_iff]
 
-/-- The subgraph of `B` corresponding to a copy of `A` inside `B`. -/
-abbrev toSubgraph (f : Copy A B) : B.Subgraph := .map f.toHom ⊤
+/-- The subgraph of `H` corresponding to a copy of `G` inside `H`. -/
+abbrev toSubgraph (f : Copy G H) : H.Subgraph := .map f.toHom ⊤
 
-/-- The isomorphism from `A` to its copy under `f : Copy A B`. -/
-noncomputable def isoToSubgraph (f : Copy A B) : A ≃g f.toSubgraph.coe :=
+/-- The isomorphism from `G` to its copy under `f : Copy G H`. -/
+noncomputable def isoToSubgraph (f : Copy G H) : G ≃g f.toSubgraph.coe :=
   (f.isoSubgraphMap ⊤).comp Subgraph.topIso.symm
 
 @[simp] lemma range_toSubgraph :
-    .range (toSubgraph (A := A)) = {B' : B.Subgraph | Nonempty (A ≃g B'.coe)} := by
+    .range (toSubgraph (G := G)) = {H' : H.Subgraph | Nonempty (G ≃g H'.coe)} := by
   ext H'
   constructor
   · rintro ⟨f, hf, rfl⟩
@@ -188,7 +200,7 @@ noncomputable def isoToSubgraph (f : Copy A B) : A ≃g f.toSubgraph.coe :=
     simp [toSubgraph, Subgraph.map_comp]
 
 lemma toSubgraph_surjOn :
-    Set.SurjOn (toSubgraph (A := A)) .univ {B' : B.Subgraph | Nonempty (A ≃g B'.coe)} :=
+    Set.SurjOn (toSubgraph (G := G)) .univ {H' : H.Subgraph | Nonempty (G ≃g H'.coe)} :=
   fun H' hH' ↦ by simpa
 
 instance [Subsingleton (V → W)] : Subsingleton (G.Copy H) := DFunLike.coe_injective.subsingleton
@@ -199,15 +211,20 @@ instance [Fintype {f : G →g H // Injective f}] : Fintype (G.Copy H) :=
     invFun f := ⟨f.1, f.2⟩
   }
 
+instance [Finite V] [Finite W] : Finite (G.Copy H) :=
+  Finite.of_injective _ DFunLike.coe_injective
+
 /-- A copy of `⊤` gives rise to an embedding of `⊤`. -/
-@[simps!]
-def topEmbedding (f : Copy (⊤ : SimpleGraph α) G) : (⊤ : SimpleGraph α) ↪g G :=
+@[expose] def topEmbedding (f : Copy (⊤ : SimpleGraph V) H) : (⊤ : SimpleGraph V) ↪g H :=
   { f.toEmbedding with
-    map_rel_iff' := fun {v w} ↦ ⟨fun h ↦ by simpa using h.ne, f.toHom.map_adj⟩}
+    map_rel_iff' := fun {_ _} ↦ ⟨fun h ↦ f.injective.ne_iff.mp h.ne, f.toHom.map_adj⟩ }
+
+@[simp] lemma topEmbedding_apply (f : Copy (⊤ : SimpleGraph V) H) (v : V) :
+    f.topEmbedding v = f v := rfl
 
 end Copy
 
-/-- A `Subgraph G` gives rise to a copy from the coercion to `G`. -/
+/-- A `G.Subgraph` gives rise to a copy from its coercion to `G`. -/
 def Subgraph.coeCopy (G' : G.Subgraph) : Copy G'.coe G := G'.hom.toCopy hom_injective
 
 end Copy
@@ -215,27 +232,23 @@ end Copy
 /-!
 #### Induced copies
 
-An induced copy of a graph `G` inside a graph `H` is an embedding from the vertices of
-`G` into the vertices of `H` which preserves the adjacency relation.
-
-This is already captured by the notion of graph embeddings, defined as `G ↪g H`.
+An induced copy of `G` in `H` is an injective map from the vertices of `G` into those of `H`
+that *preserves and reflects* adjacency (an edge between two images must come from an edge in
+`G`). This is already captured by `G ↪g H`.
 
 ### Containment
 
 #### Not necessarily induced containment
 
-A graph `H` *contains* a graph `G` if there is some copy `f : Copy G H` of `G` inside `H`. This
-amounts to `H` having a subgraph isomorphic to `G`.
-
-We denote "`G` is contained in `H`" by `G ⊑ H` (`\squb`).
+`G ⊑ H` (`\squb`).
 -/
 
 section IsContained
 
-/-- The relation `IsContained A B`, `A ⊑ B` says that `B` contains a copy of `A`.
+/-- The relation `IsContained G H`, `G ⊑ H` says that `H` contains a copy of `G`.
 
-This is equivalent to the existence of an isomorphism from `A` to a subgraph of `B`. -/
-abbrev IsContained (A : SimpleGraph α) (B : SimpleGraph β) := Nonempty (Copy A B)
+This is equivalent to the existence of an isomorphism from `G` to a subgraph of `H`. -/
+abbrev IsContained (G : SimpleGraph V) (H : SimpleGraph W) := Nonempty (Copy G H)
 
 @[inherit_doc] scoped infixl:50 " ⊑ " => SimpleGraph.IsContained
 
@@ -247,66 +260,67 @@ protected theorem IsContained.rfl : G ⊑ G := IsContained.refl G
 /-- A simple graph contains its subgraphs. -/
 theorem IsContained.of_le (h : G₁ ≤ G₂) : G₁ ⊑ G₂ := ⟨.ofLE G₁ G₂ h⟩
 
-/-- If `A` contains `B` and `B` contains `C`, then `A` contains `C`. -/
-theorem IsContained.trans : A ⊑ B → B ⊑ C → A ⊑ C := fun ⟨f⟩ ⟨g⟩ ↦ ⟨g.comp f⟩
+/-- If `G` is contained in `H` and `H` is contained in `I`, then `G` is contained in `I`. -/
+theorem IsContained.trans : G ⊑ H → H ⊑ I → G ⊑ I := fun ⟨f⟩ ⟨g⟩ ↦ ⟨g.comp f⟩
 
-/-- If `B` contains `C` and `A` contains `B`, then `A` contains `C`. -/
-theorem IsContained.trans' : B ⊑ C → A ⊑ B → A ⊑ C := flip IsContained.trans
+/-- If `H` is contained in `I` and `G` is contained in `H`, then `G` is contained in `I`. -/
+theorem IsContained.trans' : H ⊑ I → G ⊑ H → G ⊑ I := flip IsContained.trans
 
 @[gcongr]
-lemma IsContained.mono_right {B' : SimpleGraph β} (h_isub : A ⊑ B) (h_sub : B ≤ B') : A ⊑ B' :=
+lemma IsContained.mono_right {H' : SimpleGraph W} (h_isub : G ⊑ H) (h_sub : H ≤ H') : G ⊑ H' :=
   h_isub.trans <| IsContained.of_le h_sub
 
 alias IsContained.trans_le := IsContained.mono_right
 
 @[gcongr]
-lemma IsContained.mono_left {A' : SimpleGraph α} (h_sub : A ≤ A') (h_isub : A' ⊑ B) : A ⊑ B :=
+lemma IsContained.mono_left {G' : SimpleGraph V} (h_sub : G ≤ G') (h_isub : G' ⊑ H) : G ⊑ H :=
   (IsContained.of_le h_sub).trans h_isub
 
 alias IsContained.trans_le' := IsContained.mono_left
 
-/-- If `A ≃g H` and `B ≃g G` then `A` is contained in `B` if and only if `H` is contained
-in `G`. -/
-theorem isContained_congr (e₁ : A ≃g H) (e₂ : B ≃g G) : A ⊑ B ↔ H ⊑ G :=
+/-- If `G ≃g G'` and `H ≃g H'` then `G` is contained in `H` if and only if `G'` is
+contained in `H'`. -/
+theorem isContained_congr (e₁ : G ≃g G') (e₂ : H ≃g H') : G ⊑ H ↔ G' ⊑ H' :=
   ⟨.trans' ⟨e₂.toCopy⟩ ∘ .trans ⟨e₁.symm.toCopy⟩, .trans' ⟨e₂.symm.toCopy⟩ ∘ .trans ⟨e₁.toCopy⟩⟩
 
-lemma isContained_congr_left (e₁ : A ≃g B) : A ⊑ C ↔ B ⊑ C := isContained_congr e₁ .refl
+lemma isContained_congr_left (e₁ : G ≃g G') : G ⊑ H ↔ G' ⊑ H := isContained_congr e₁ .refl
 
 alias ⟨_, IsContained.congr_left⟩ := isContained_congr_left
 
-lemma isContained_congr_right (e₂ : B ≃g C) : A ⊑ B ↔ A ⊑ C := isContained_congr .refl e₂
+lemma isContained_congr_right (e₂ : H ≃g H') : G ⊑ H ↔ G ⊑ H' := isContained_congr .refl e₂
 
 alias ⟨_, IsContained.congr_right⟩ := isContained_congr_right
 
-instance : IsPreorder (SimpleGraph α) IsContained where
+instance : IsPreorder (SimpleGraph V) IsContained where
   refl := .refl
   trans _ _ _ := .trans
 
 instance :
-    Trans (α := SimpleGraph α) (β := SimpleGraph β) (γ := SimpleGraph γ)
+    Trans (α := SimpleGraph V) (β := SimpleGraph W) (γ := SimpleGraph X)
       IsContained IsContained IsContained where
   trans := .trans
 
 /-- A simple graph having no vertices is contained in any simple graph. -/
-lemma IsContained.of_isEmpty [IsEmpty α] : A ⊑ B :=
+lemma IsContained.of_isEmpty [IsEmpty V] : G ⊑ H :=
   ⟨⟨isEmptyElim, fun {a} ↦ isEmptyElim a⟩, isEmptyElim⟩
 
 /-- `⊥` is contained in any simple graph having sufficiently many vertices. -/
-lemma bot_isContained_iff_card_le [Fintype α] [Fintype β] :
-    (⊥ : SimpleGraph α) ⊑ B ↔ Fintype.card α ≤ Fintype.card β :=
-  ⟨fun ⟨f⟩ ↦ Fintype.card_le_of_embedding f.toEmbedding,
-    fun h ↦ ⟨Copy.bot (Function.Embedding.nonempty_of_card_le h).some⟩⟩
+lemma bot_isContained_iff_card_le [Finite V] [Finite W] :
+    (⊥ : SimpleGraph V) ⊑ H ↔ Nat.card V ≤ Nat.card W :=
+  ⟨fun ⟨f⟩ ↦ Finite.card_le_of_embedding f.toEmbedding,
+    fun h ↦ ⟨Copy.bot (Cardinal.lift_mk_le'.mp (by
+      simp only [← Nat.cast_card, Cardinal.lift_natCast]; exact_mod_cast h)).some⟩⟩
 
 protected alias IsContained.bot := bot_isContained_iff_card_le
 
-/-- A simple graph `G` contains all `Subgraph G` coercions. -/
+/-- A simple graph `G` contains the coercion of any of its `G.Subgraph`s. -/
 lemma Subgraph.coe_isContained (G' : G.Subgraph) : G'.coe ⊑ G := ⟨G'.coeCopy⟩
 
-/-- `B` contains `A` if and only if `B` has a subgraph `B'` and `B'` is isomorphic to `A`. -/
+/-- `H` contains `G` if and only if `H` has a subgraph `H'` and `H'` is isomorphic to `G`. -/
 theorem isContained_iff_exists_iso_subgraph :
-    A ⊑ B ↔ ∃ B' : B.Subgraph, Nonempty (A ≃g B'.coe) where
+    G ⊑ H ↔ ∃ H' : H.Subgraph, Nonempty (G ≃g H'.coe) where
   mp := fun ⟨f⟩ ↦ ⟨.map f.toHom ⊤, ⟨f.isoToSubgraph⟩⟩
-  mpr := fun ⟨B', ⟨e⟩⟩ ↦ B'.coe_isContained.trans' ⟨e.toCopy⟩
+  mpr := fun ⟨H', ⟨e⟩⟩ ↦ H'.coe_isContained.trans' ⟨e.toCopy⟩
 
 alias ⟨IsContained.exists_iso_subgraph, IsContained.of_exists_iso_subgraph⟩ :=
   isContained_iff_exists_iso_subgraph
@@ -348,24 +362,24 @@ end IsContained
 
 section Free
 
-/-- `A.Free B` means that `B` does not contain a copy of `A`. -/
-abbrev Free (A : SimpleGraph α) (B : SimpleGraph β) := ¬A ⊑ B
+/-- `G.Free H` means that `H` does not contain a copy of `G`. -/
+abbrev Free (G : SimpleGraph V) (H : SimpleGraph W) := ¬G ⊑ H
 
-lemma not_free : ¬A.Free B ↔ A ⊑ B := not_not
+lemma not_free : ¬G.Free H ↔ G ⊑ H := not_not
 
-/-- If `A ≃g H` and `B ≃g G` then `B` is `A`-free if and only if `G` is `H`-free. -/
-theorem free_congr (e₁ : A ≃g H) (e₂ : B ≃g G) : A.Free B ↔ H.Free G :=
+/-- If `G ≃g G'` and `H ≃g H'` then `H` is `G`-free if and only if `H'` is `G'`-free. -/
+theorem free_congr (e₁ : G ≃g G') (e₂ : H ≃g H') : G.Free H ↔ G'.Free H' :=
   (isContained_congr e₁ e₂).not
 
-lemma free_congr_left (e₁ : A ≃g B) : A.Free C ↔ B.Free C := free_congr e₁ .refl
+lemma free_congr_left (e₁ : G ≃g G') : G.Free H ↔ G'.Free H := free_congr e₁ .refl
 
 alias ⟨_, Free.congr_left⟩ := free_congr_left
 
-lemma free_congr_right (e₂ : B ≃g C) : A.Free B ↔ A.Free C := free_congr .refl e₂
+lemma free_congr_right (e₂ : H ≃g H') : G.Free H ↔ G.Free H' := free_congr .refl e₂
 
 alias ⟨_, Free.congr_right⟩ := free_congr_right
 
-lemma free_bot (h : A ≠ ⊥) : A.Free (⊥ : SimpleGraph β) := by
+lemma free_bot (h : G ≠ ⊥) : G.Free (⊥ : SimpleGraph W) := by
   rw [← edgeSet_nonempty] at h
   intro ⟨f, hf⟩
   absurd f.map_mem_edgeSet h.choose_spec
@@ -377,15 +391,12 @@ end Free
 /-!
 #### Induced containment
 
-A graph `H` *inducingly contains* a graph `G` if there is some graph embedding `G ↪ H`. This amounts
-to `H` having an induced subgraph isomorphic to `G`.
-
-We denote "`G` is inducingly contained in `H`" by `G ⊴ H` (`\trianglelefteq`).
+`G ⊴ H` (`\trianglelefteq`).
 -/
 
 /-- A simple graph `G` is inducingly contained in a simple graph `H` if there exists an induced
 subgraph of `H` isomorphic to `G`. This is denoted by `G ⊴ H`. -/
-def IsIndContained (G : SimpleGraph V) (H : SimpleGraph W) : Prop := Nonempty (G ↪g H)
+abbrev IsIndContained (G : SimpleGraph V) (H : SimpleGraph W) : Prop := Nonempty (G ↪g H)
 
 @[inherit_doc] scoped infixl:50 " ⊴ " => SimpleGraph.IsIndContained
 
@@ -419,12 +430,12 @@ protected lemma Subgraph.IsInduced.isIndContained {G' : G.Subgraph} (hG' : G'.Is
 lemma IsIndContained.rfl : G ⊴ G := .refl _
 @[trans] lemma IsIndContained.trans : G ⊴ H → H ⊴ I → G ⊴ I := fun ⟨f⟩ ⟨g⟩ ↦ ⟨g.comp f⟩
 
-instance : IsPreorder (SimpleGraph α) IsIndContained where
+instance : IsPreorder (SimpleGraph V) IsIndContained where
   refl := .refl
   trans _ _ _ := .trans
 
 instance :
-    Trans (α := SimpleGraph α) (β := SimpleGraph β) (γ := SimpleGraph γ)
+    Trans (α := SimpleGraph V) (β := SimpleGraph W) (γ := SimpleGraph X)
       IsIndContained IsIndContained IsIndContained where
   trans := .trans
 
@@ -457,216 +468,218 @@ theorem isIndContained_iff_exists_iso_induce : G ⊴ H ↔ ∃ s, Nonempty (G 
 
 protected alias ⟨IsIndContained.of_compl, IsIndContained.compl⟩ := compl_isIndContained_compl
 
-theorem isContained_iff_exists_le_comap : H ⊑ G ↔ ∃ (f : W ↪ V), H ≤ G.comap f :=
+theorem isContained_iff_exists_le_comap : G ⊑ H ↔ ∃ (f : V ↪ W), G ≤ H.comap f :=
   ⟨fun ⟨f⟩ ↦ ⟨f.toEmbedding, f.toHom.le_comap⟩, fun ⟨f, h⟩ ↦ ⟨⟨f, (h ·)⟩, f.injective⟩⟩
 
-theorem isIndContained_iff_exists_comap_eq : H ⊴ G ↔ ∃ (f : W ↪ V), G.comap f = H :=
+theorem isIndContained_iff_exists_comap_eq : G ⊴ H ↔ ∃ (f : V ↪ W), H.comap f = G :=
   ⟨fun ⟨f⟩ ↦ ⟨f.toEmbedding, f.comap_eq⟩, fun ⟨f, h⟩ ↦ ⟨f, h ▸ .rfl⟩⟩
 
 /-!
-### Counting the copies
-
-If `G` and `H` are finite graphs, we can count the number of unlabelled and labelled copies of `G`
-in `H`.
+### Counting copies
 
-#### Not necessarily induced copies
+For finite `G` and `H`, we count labeled and unlabeled copies of `G` in `H`.
 -/
 
-section LabelledCopyCount
-variable [Fintype V] [Fintype W]
+section CopyCount
 
-/-- `G.labelledCopyCount H` is the number of labelled copies of `H` in `G`, i.e. the number of graph
-embeddings from `H` to `G`. See `SimpleGraph.copyCount` for the number of unlabelled copies. -/
-noncomputable def labelledCopyCount (G : SimpleGraph V) (H : SimpleGraph W) : ℕ := by
-  classical exact Fintype.card (Copy H G)
+/-- `H.copyCount G` is the number of labeled copies of `G` in `H`, i.e. the number of injective
+graph homomorphisms from `G` to `H`. See `SimpleGraph.subCount` for the number of unlabeled
+copies. -/
+@[expose] noncomputable def copyCount (H : SimpleGraph W) (G : SimpleGraph V) : ℕ :=
+  Nat.card (Copy G H)
 
-@[simp] lemma labelledCopyCount_of_isEmpty [IsEmpty W] (G : SimpleGraph V) (H : SimpleGraph W) :
-    G.labelledCopyCount H = 1 := by
-  convert Fintype.card_unique
-  exact { default := ⟨default, isEmptyElim⟩, uniq := fun _ ↦ Subsingleton.elim _ _ }
+@[deprecated (since := "2026-04-30")] alias labelledCopyCount := copyCount
 
-@[simp] lemma labelledCopyCount_eq_zero : G.labelledCopyCount H = 0 ↔ H.Free G := by
-  simp [labelledCopyCount, Fintype.card_eq_zero_iff]
+private instance [IsEmpty V] : Nonempty (Copy G H) := IsContained.of_isEmpty
 
-@[simp] lemma labelledCopyCount_pos : 0 < G.labelledCopyCount H ↔ H ⊑ G := by
-  simp [labelledCopyCount, IsContained, Fintype.card_pos_iff]
+@[simp] lemma copyCount_of_isEmpty [IsEmpty V] (H : SimpleGraph W) (G : SimpleGraph V) :
+    H.copyCount G = 1 := Nat.card_unique
 
-end LabelledCopyCount
+@[deprecated (since := "2026-04-30")]
+alias labelledCopyCount_of_isEmpty := copyCount_of_isEmpty
 
-section CopyCount
-variable [Fintype V]
-
-/-- `G.copyCount H` is the number of unlabelled copies of `H` in `G`, i.e. the number of subgraphs
-of `G` isomorphic to `H`. See `SimpleGraph.labelledCopyCount` for the number of labelled copies. -/
-noncomputable def copyCount (G : SimpleGraph V) (H : SimpleGraph W) : ℕ := by
-  classical exact #{G' : G.Subgraph | Nonempty (H ≃g G'.coe)}
-
-lemma copyCount_eq_card_image_copyToSubgraph [Fintype {f : H →g G // Injective f}]
-    [DecidableEq G.Subgraph] :
-    copyCount G H = #((Finset.univ : Finset (H.Copy G)).image Copy.toSubgraph) := by
-  rw [copyCount]
-  congr
-  refine Finset.coe_injective ?_
-  simpa [-Copy.range_toSubgraph] using Copy.range_toSubgraph.symm
-
-@[simp] lemma copyCount_eq_zero : G.copyCount H = 0 ↔ H.Free G := by
-  simp [copyCount, Free, -nonempty_subtype, isContained_iff_exists_iso_subgraph,
-    filter_eq_empty_iff]
-
-@[simp] lemma copyCount_pos : 0 < G.copyCount H ↔ H ⊑ G := by
-  simp [copyCount, -nonempty_subtype, isContained_iff_exists_iso_subgraph, card_pos,
-    filter_nonempty_iff]
-
-/-- There's at least as many labelled copies of `H` in `G` than unlabelled ones. -/
-lemma copyCount_le_labelledCopyCount [Fintype W] : G.copyCount H ≤ G.labelledCopyCount H := by
-  classical rw [copyCount_eq_card_image_copyToSubgraph]; exact card_image_le
-
-@[simp] lemma copyCount_bot (G : SimpleGraph V) : copyCount G (⊥ : SimpleGraph V) = 1 := by
-  classical
-  rw [copyCount]
-  convert card_singleton (α := G.Subgraph)
-    { verts := .univ
-      Adj := ⊥
-      adj_sub := False.elim
-      edge_vert := False.elim }
-  simp only [eq_singleton_iff_unique_mem, mem_filter_univ, Nonempty.forall]
-  refine ⟨⟨⟨(Equiv.Set.univ _).symm, by simp⟩⟩, fun H' e ↦
-    Subgraph.ext ((set_fintype_card_eq_univ_iff _).1 <| Fintype.card_congr e.toEquiv.symm) ?_⟩
-  ext a b
-  simp only [Prop.bot_eq_false, Pi.bot_apply, iff_false]
-  exact fun hab ↦ e.symm.map_rel_iff.2 hab.coe
-
-@[simp] lemma copyCount_of_isEmpty [IsEmpty W] (G : SimpleGraph V) (H : SimpleGraph W) :
-    G.copyCount H = 1 := by
-  cases nonempty_fintype W
-  exact (copyCount_le_labelledCopyCount.trans_eq <| labelledCopyCount_of_isEmpty ..).antisymm <|
-    copyCount_pos.2 <| .of_isEmpty
+@[simp] lemma copyCount_eq_zero [Finite V] [Finite W] : H.copyCount G = 0 ↔ G.Free H := by
+  rw [copyCount, Nat.card_eq_zero, or_iff_left (Finite.not_infinite inferInstance)]
+  simp [Free, IsContained]
+
+@[deprecated (since := "2026-04-30")] alias labelledCopyCount_eq_zero := copyCount_eq_zero
+
+@[simp] lemma copyCount_pos [Finite V] [Finite W] : 0 < H.copyCount G ↔ G ⊑ H := by
+  simp [Nat.pos_iff_ne_zero, copyCount_eq_zero]
+
+@[deprecated (since := "2026-04-30")] alias labelledCopyCount_pos := copyCount_pos
 
 end CopyCount
 
-/-!
-#### Induced copies
+section SubCount
 
-TODO
+/-- `G.Sub H` is the type of `SimpleGraph.Subgraph`s of `H` isomorphic to `G`. The corresponding
+count is `SimpleGraph.subCount`. -/
+abbrev Sub (G : SimpleGraph V) (H : SimpleGraph W) : Type _ :=
+  {H' : H.Subgraph // Nonempty (G ≃g H'.coe)}
 
-### Killing a subgraph
+/-- `H.subCount G` is the number of `SimpleGraph.Subgraph`s of `H` isomorphic to `G`. See
+`SimpleGraph.copyCount` for the number of labeled copies. -/
+@[expose] noncomputable def subCount (H : SimpleGraph W) (G : SimpleGraph V) : ℕ :=
+  Nat.card (G.Sub H)
 
-An important aspect of graph containment is that we can remove not too many edges from a graph `H`
-to get a graph `H'` that doesn't contain `G`.
+lemma subCount_eq_nat_card_range_toSubgraph :
+    H.subCount G = Nat.card (Set.range (Copy.toSubgraph : G.Copy H → H.Subgraph)) := by
+  rw [subCount, Copy.range_toSubgraph]; rfl
 
-#### Killing not necessarily induced copies
+@[simp] lemma subCount_eq_zero [Finite W] : H.subCount G = 0 ↔ G.Free H := by
+  rw [subCount, Nat.card_eq_zero, or_iff_left (Finite.not_infinite inferInstance), isEmpty_subtype]
+  simp [Free, isContained_iff_exists_iso_subgraph]
 
-`SimpleGraph.killCopies G H` is a subgraph of `G` where an edge was removed from each copy of `H` in
-`G`. By construction, it doesn't contain `H` and has at most the number of copies of `H` edges less
-than `G`.
+@[simp] lemma subCount_pos [Finite W] : 0 < H.subCount G ↔ G ⊑ H := by
+  simp [Nat.pos_iff_ne_zero, subCount_eq_zero]
+
+/-- There are at least as many labeled copies of `G` in `H` as there are unlabeled ones. -/
+lemma subCount_le_copyCount [Finite V] [Finite W] : H.subCount G ≤ H.copyCount G :=
+  subCount_eq_nat_card_range_toSubgraph ▸ Finite.card_range_le _
+
+set_option backward.privateInPublic true in
+set_option backward.privateInPublic.warn false in
+private lemma subgraph_iso_emptyGraph [Finite W] (H' : H.Subgraph)
+    (e : (⊥ : SimpleGraph W) ≃g H'.coe) : H'.verts = Set.univ ∧ H'.Adj = ⊥ := by
+  refine ⟨Set.eq_univ_of_forall fun v ↦ ?_,
+    funext₂ fun a b ↦ eq_false fun hadj ↦ absurd (e.symm.map_rel_iff.mpr hadj.coe) (by simp)⟩
+  obtain ⟨w, hw⟩ := (Finite.injective_iff_surjective.mp
+    (Subtype.val_injective.comp e.toEquiv.injective)) v
+  exact hw ▸ (e.toEquiv w).prop
+
+set_option backward.privateInPublic true in
+set_option backward.privateInPublic.warn false in
+instance uniqueSubEmptyGraph [Finite W] (H : SimpleGraph W) :
+    Unique ((⊥ : SimpleGraph W).Sub H) where
+  default := ⟨{ verts := .univ, Adj := ⊥, adj_sub := False.elim, edge_vert := False.elim },
+              ⟨(Equiv.Set.univ _).symm, by simp⟩⟩
+  uniq := fun ⟨H', ⟨e⟩⟩ ↦ Subtype.ext <|
+    Subgraph.ext (subgraph_iso_emptyGraph H' e).1 (subgraph_iso_emptyGraph H' e).2
+
+@[deprecated (since := "2026-05-13")] alias uniqueSubBot := uniqueSubEmptyGraph
+
+@[simp] lemma subCount_emptyGraph [Finite W] (H : SimpleGraph W) :
+    H.subCount (⊥ : SimpleGraph W) = 1 :=
+  Nat.card_unique
+
+@[deprecated (since := "2026-05-13")] alias subCount_bot := subCount_emptyGraph
+
+@[simp] lemma subCount_of_isEmpty [Finite V] [Finite W] [IsEmpty V]
+    (H : SimpleGraph W) (G : SimpleGraph V) : H.subCount G = 1 :=
+  (subCount_le_copyCount.trans_eq <| copyCount_of_isEmpty ..).antisymm <|
+    subCount_pos.2 <| .of_isEmpty
+
+end SubCount
+
+/-!
+### Killing all copies of a graph
+
+We can remove not too many edges from a graph `H` to get a graph `H'` that doesn't contain `G`.
+By construction, `H.killCopies G` doesn't contain `G` and differs from `H` by at most one edge
+per copy.
 -/
 
 set_option backward.privateInPublic true in
-private lemma aux (hH : H ≠ ⊥) {G' : G.Subgraph} :
-    Nonempty (H ≃g G'.coe) → G'.edgeSet.Nonempty := by
-  obtain ⟨e, he⟩ := edgeSet_nonempty.2 hH
+private lemma aux (hG : G ≠ ⊥) {H' : H.Subgraph} :
+    Nonempty (G ≃g H'.coe) → H'.edgeSet.Nonempty := by
+  obtain ⟨e, he⟩ := edgeSet_nonempty.2 hG
   rw [← Subgraph.image_coe_edgeSet_coe]
   exact fun ⟨f⟩ ↦ Set.Nonempty.image _ ⟨_, f.map_mem_edgeSet_iff.2 he⟩
 
 set_option backward.privateInPublic true in
 set_option backward.privateInPublic.warn false in
-/-- `G.killCopies H` is a subgraph of `G` where an *arbitrary* edge was removed from each copy of
-`H` in `G`. By construction, it doesn't contain `H` (unless `H` had no edges) and has at most the
-number of copies of `H` edges less than `G`. See `free_killCopies` and
+/-- `H.killCopies G` is a subgraph of `H` where an *arbitrary* edge was removed from each copy of
+`G` in `H`. By construction, it doesn't contain `G` (unless `G` had no edges) and has at most the
+number of copies of `G` edges less than `H`. See `free_killCopies` and
 `le_card_edgeFinset_killCopies` for these two properties. -/
-noncomputable irreducible_def killCopies (G : SimpleGraph V) (H : SimpleGraph W) :
-    SimpleGraph V := by
+noncomputable irreducible_def killCopies (H : SimpleGraph W) (G : SimpleGraph V) :
+    SimpleGraph W := by
   classical exact
-  if hH : H = ⊥ then G
-  else G.deleteEdges <| ⋃ (G' : G.Subgraph) (hG' : Nonempty (H ≃g G'.coe)), {(aux hH hG').some}
+  if hG : G = ⊥ then H
+  else H.deleteEdges <| ⋃ (H' : H.Subgraph) (hG' : Nonempty (G ≃g H'.coe)), {(aux hG hG').some}
 
-/-- Removing an edge from `G` for each subgraph isomorphic to `H` results in a subgraph of `G`. -/
-lemma killCopies_le_left : G.killCopies H ≤ G := by
+/-- Removing an edge from `H` for each subgraph isomorphic to `G` results in a subgraph of `H`. -/
+lemma killCopies_le_left : H.killCopies G ≤ H := by
   rw [killCopies]; split_ifs; exacts [le_rfl, deleteEdges_le _]
 
-@[simp] lemma killCopies_bot (G : SimpleGraph V) : G.killCopies (⊥ : SimpleGraph W) = G := by
+@[simp] lemma killCopies_bot (H : SimpleGraph W) : H.killCopies (⊥ : SimpleGraph V) = H := by
   rw [killCopies]; exact dif_pos rfl
 
-private lemma killCopies_of_ne_bot (hH : H ≠ ⊥) (G : SimpleGraph V) :
-    G.killCopies H =
-      G.deleteEdges (⋃ (G' : G.Subgraph) (hG' : Nonempty (H ≃g G'.coe)), {(aux hH hG').some}) := by
-  rw [killCopies]; exact dif_neg hH
+private lemma killCopies_of_ne_bot (hG : G ≠ ⊥) (H : SimpleGraph W) :
+    H.killCopies G =
+      H.deleteEdges (⋃ (H' : H.Subgraph) (hG' : Nonempty (G ≃g H'.coe)), {(aux hG hG').some}) := by
+  rw [killCopies]; exact dif_neg hG
 
-/-- `G.killCopies H` has no effect on `G` if and only if `G` already contained no copies of `H`. See
-`Free.killCopies_eq_left` for the reverse implication with no assumption on `H`. -/
-lemma killCopies_eq_left (hH : H ≠ ⊥) : G.killCopies H = G ↔ H.Free G := by
-  simp only [killCopies_of_ne_bot hH, Set.disjoint_left, isContained_iff_exists_iso_subgraph,
-    @forall_comm _ G.Subgraph, deleteEdges_eq_self, Set.mem_iUnion,
+/-- `H.killCopies G` has no effect on `H` if and only if `H` already contained no copies of `G`. See
+`Free.killCopies_eq_left` for the reverse implication with no assumption on `G`. -/
+lemma killCopies_eq_left (hG : G ≠ ⊥) : H.killCopies G = H ↔ G.Free H := by
+  simp only [killCopies_of_ne_bot hG, Set.disjoint_left, isContained_iff_exists_iso_subgraph,
+    @forall_comm _ H.Subgraph, deleteEdges_eq_self, Set.mem_iUnion,
     not_exists, not_nonempty_iff, Nonempty.forall, Free]
-  exact forall_congr' fun G' ↦ ⟨fun h ↦ ⟨fun f ↦ h _
-    (Subgraph.edgeSet_subset _ <| (aux hH ⟨f⟩).choose_spec) f rfl⟩, fun h _ _ ↦ h.elim⟩
+  exact forall_congr' fun H' ↦ ⟨fun h ↦ ⟨fun f ↦ h _
+    (Subgraph.edgeSet_subset _ <| (aux hG ⟨f⟩).choose_spec) f rfl⟩, fun h _ _ ↦ h.elim⟩
 
-protected lemma Free.killCopies_eq_left (hHG : H.Free G) : G.killCopies H = G := by
-  obtain rfl | hH := eq_or_ne H ⊥
+protected lemma Free.killCopies_eq_left (hGH : G.Free H) : H.killCopies G = H := by
+  obtain rfl | hG := eq_or_ne G ⊥
   · exact killCopies_bot _
-  · exact (killCopies_eq_left hH).2 hHG
-
-/-- Removing an edge from `G` for each subgraph isomorphic to `H` results in a graph that doesn't
-contain `H`. -/
-lemma free_killCopies (hH : H ≠ ⊥) : H.Free (G.killCopies H) := by
-  rw [killCopies_of_ne_bot hH, deleteEdges, Free, isContained_iff_exists_iso_subgraph]
-  rintro ⟨G', hHG'⟩
-  have hG' : (G'.map <| .ofLE (sdiff_le : G \ _ ≤ G)).edgeSet.Nonempty := by
+  · exact (killCopies_eq_left hG).2 hGH
+
+/-- Removing an edge from `H` for each subgraph isomorphic to `G` results in a graph that doesn't
+contain `G`. -/
+lemma free_killCopies (hG : G ≠ ⊥) : G.Free (H.killCopies G) := by
+  rw [killCopies_of_ne_bot hG, deleteEdges, Free, isContained_iff_exists_iso_subgraph]
+  rintro ⟨H', hGH'⟩
+  have hH' : (H'.map <| .ofLE (sdiff_le : H \ _ ≤ H)).edgeSet.Nonempty := by
     rw [Subgraph.edgeSet_map]
-    exact (aux hH hHG').image _
-  set e := hG'.some with he
-  have : e ∈ _ := hG'.some_mem
+    exact (aux hG hGH').image _
+  set e := hH'.some with he
+  have : e ∈ _ := hH'.some_mem
   clear_value e
   rw [← Subgraph.image_coe_edgeSet_coe] at this
   subst he
   obtain ⟨e, he₀, he₁⟩ := this
-  let e' : Sym2 G'.verts := Sym2.map (Copy.isoSubgraphMap (.ofLE _ _ _) _).symm e
-  have he' : e' ∈ G'.coe.edgeSet := (Iso.map_mem_edgeSet_iff _).2 he₀
+  let e' : Sym2 H'.verts := Sym2.map (Copy.isoSubgraphMap (.ofLE _ _ _) _).symm e
+  have he' : e' ∈ H'.coe.edgeSet := (Iso.map_mem_edgeSet_iff _).2 he₀
   rw [Subgraph.edgeSet_coe] at he'
   have := Subgraph.edgeSet_subset _ he'
   simp only [edgeSet_sdiff, edgeSet_fromEdgeSet, edgeSet_sdiff_sdiff_isDiag, Set.mem_diff,
     Set.mem_iUnion, not_exists] at this
-  refine this.2 (G'.map <| .ofLE sdiff_le) ⟨((Copy.ofLE _ _ _).isoSubgraphMap _).comp hHG'.some⟩ ?_
+  refine this.2 (H'.map <| .ofLE sdiff_le) ⟨((Copy.ofLE _ _ _).isoSubgraphMap _).comp hGH'.some⟩ ?_
   rw [Sym2.map_map, Set.mem_singleton_iff, ← he₁]
   congr 1 with x
   exact congr_arg _ (Equiv.Set.image_symm_apply _ _ injective_id _ _)
 
-variable [Fintype G.edgeSet]
+variable [Fintype H.edgeSet]
 
-noncomputable instance killCopies.edgeSet.instFintype : Fintype (G.killCopies H).edgeSet :=
+noncomputable instance killCopies.edgeSet.instFintype : Fintype (H.killCopies G).edgeSet :=
   .ofInjective (Set.inclusion <| edgeSet_mono killCopies_le_left) <| Set.inclusion_injective _
 
 /-- Removing an edge from `H` for each subgraph isomorphic to `G` means that the number of edges
 we've removed is at most the number of copies of `G` in `H`. -/
-lemma le_card_edgeFinset_killCopies [Fintype V] :
-    #G.edgeFinset - G.copyCount H ≤ #(G.killCopies H).edgeFinset := by
+lemma le_card_edgeFinset_killCopies [Finite W] :
+    #H.edgeFinset - H.subCount G ≤ #(H.killCopies G).edgeFinset := by
   classical
-  obtain rfl | hH := eq_or_ne H ⊥
+  obtain rfl | hG := eq_or_ne G ⊥
   · simp [← card_edgeSet]
-  let f (G' : {G' : G.Subgraph // Nonempty (H ≃g G'.coe)}) := (aux hH G'.2).some
-  calc
-    _ = #G.edgeFinset - card {G' : G.Subgraph // Nonempty (H ≃g G'.coe)} := ?_
-    _ ≤ #G.edgeFinset - #(univ.image f) := Nat.sub_le_sub_left card_image_le _
-    _ = #G.edgeFinset - #(Set.range f).toFinset := by rw [Set.toFinset_range]
-    _ ≤ #(G.edgeFinset \ (Set.range f).toFinset) := le_card_sdiff ..
-    _ = #(G.killCopies H).edgeFinset := ?_
-  · simp only [edgeFinset, Set.toFinset_card]
-    rw [← Set.toFinset_card, ← edgeFinset, copyCount, ← card_subtype, subtype_univ, card_univ]
-  congr 1
-  ext e
-  induction e using Sym2.inductionOn with | hf v w
-  simp [mem_edgeSet, killCopies_of_ne_bot hH, f, eq_comm]
+  let f (H' : G.Sub H) := (aux hG H'.2).some
+  have hrf : (Set.range f).Finite := Set.finite_range f
+  have hle : hrf.toFinset.card ≤ H.subCount G := by
+    rw [← Nat.card_eq_card_finite_toFinset hrf, subCount]
+    exact Finite.card_range_le f
+  calc #H.edgeFinset - H.subCount G
+      ≤ #H.edgeFinset - hrf.toFinset.card := Nat.sub_le_sub_left hle _
+    _ ≤ #(H.edgeFinset \ hrf.toFinset) := le_card_sdiff ..
+    _ = #(H.killCopies G).edgeFinset := by
+        congr 1
+        ext e
+        induction e using Sym2.inductionOn with | hf v w
+        simp [mem_edgeSet, killCopies_of_ne_bot hG, f, eq_comm]
 
 /-- Removing an edge from `H` for each subgraph isomorphic to `G` means that the number of edges
 we've removed is at most the number of copies of `G` in `H`. -/
-lemma le_card_edgeFinset_killCopies_add_copyCount [Fintype V] :
-    #G.edgeFinset ≤ #(G.killCopies H).edgeFinset + G.copyCount H :=
+lemma le_card_edgeFinset_killCopies_add_subCount [Finite W] :
+    #H.edgeFinset ≤ #(H.killCopies G).edgeFinset + H.subCount G :=
   tsub_le_iff_right.1 le_card_edgeFinset_killCopies
 
-/-!
-#### Killing induced copies
-
-TODO
--/
-
 end SimpleGraph