From 6bf406ff015e178106d059251504f9ef363d9320 Mon Sep 17 00:00:00 2001
From: Christoph Spiegel <christophspiegel.berlin@gmail.com>
Date: Wed, 13 May 2026 16:41:14 +0200
Subject: [PATCH 1/8] feat(Combinatorics/SimpleGraph/Copy): introduce `Sub`
 carrier subtype
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Adds `abbrev Sub A B := {B' : B.Subgraph // Nonempty (A ≃g B'.coe)}`, the
subtype of `SimpleGraph.Subgraph`s of `B` isomorphic to `A`. Redefines
`copyCount G H` via `Fintype.card (H.Sub G)`, replacing the previous inline
filter-set body, and rewrites the affected proofs (`copyCount_eq_zero`,
`copyCount_pos`, `copyCount_le_labelledCopyCount`, `copyCount_bot`,
`le_card_edgeFinset_killCopies`) to use `Sub` directly.

The singleton-empty-subgraph reasoning previously inlined in `copyCount_bot`'s
proof is factored out as `instance uniqueSubBot (G : SimpleGraph V) :
Unique ((⊥ : SimpleGraph V).Sub G)`, making `copyCount_bot` a one-liner via
`Fintype.card_unique`. The cardinality proof inside the instance stays inline
to keep the introduction minimal — extraction to a separate private helper
and the rename to `_emptyGraph` per the convention from #23838 (and adopted
in `AdjMatrix.lean`) happen in the next PR.

Drops `copyCount_eq_card_image_copyToSubgraph` (the legacy bridge between the
filter-set and Finset.image-of-Copy.toSubgraph forms) — unused after the
type-form refactor.
---
 Mathlib/Combinatorics/SimpleGraph/Copy.lean | 61 +++++++++++----------
 1 file changed, 31 insertions(+), 30 deletions(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Copy.lean b/Mathlib/Combinatorics/SimpleGraph/Copy.lean
index 7ec6f8e34559ab..22fa15e80e9aaa 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Copy.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Copy.lean
@@ -35,6 +35,7 @@ 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.Sub H G`: Type of `SimpleGraph.Subgraph`s of `G` isomorphic to `H`.
 * `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`
@@ -506,46 +507,48 @@ end LabelledCopyCount
 section CopyCount
 variable [Fintype V]
 
+/-- `Sub A B` is the type of `SimpleGraph.Subgraph`s of `B` isomorphic to `A`. The corresponding
+count is `SimpleGraph.copyCount`. -/
+abbrev Sub (A : SimpleGraph α) (B : SimpleGraph β) : Type _ :=
+  {B' : B.Subgraph // Nonempty (A ≃g B'.coe)}
+
 /-- `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
+  classical exact Fintype.card (H.Sub G)
 
 @[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]
+  classical
+  rw [copyCount, Fintype.card_eq_zero_iff, isEmpty_subtype]
+  simp [Free, isContained_iff_exists_iso_subgraph]
 
 @[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]
+  simp [Nat.pos_iff_ne_zero, copyCount_eq_zero]
 
 /-- 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
+  classical
+  rw [copyCount, labelledCopyCount]
+  apply Fintype.card_le_of_surjective
+    (fun c : Copy H G ↦ (⟨c.toSubgraph, ⟨c.isoToSubgraph⟩⟩ : H.Sub G))
+  rintro ⟨G', hG'⟩
+  obtain ⟨c, hc⟩ : ∃ c : Copy H G, c.toSubgraph = G' := by
+    rwa [← Set.mem_range, Copy.range_toSubgraph]
+  exact ⟨c, Subtype.ext hc⟩
+
+instance uniqueSubBot (G : SimpleGraph V) : Unique ((⊥ : SimpleGraph V).Sub G) where
+  default := ⟨{ verts := .univ, Adj := ⊥, adj_sub := False.elim, edge_vert := False.elim },
+              ⟨(Equiv.Set.univ _).symm, by simp⟩⟩
+  uniq := fun ⟨G', ⟨e⟩⟩ ↦ Subtype.ext <| Subgraph.ext
+    (by classical exact (set_fintype_card_eq_univ_iff _).1 <| Fintype.card_congr e.toEquiv.symm)
+    (by 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_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
+  exact Fintype.card_unique
 
 @[simp] lemma copyCount_of_isEmpty [IsEmpty W] (G : SimpleGraph V) (H : SimpleGraph W) :
     G.copyCount H = 1 := by
@@ -654,15 +657,13 @@ lemma le_card_edgeFinset_killCopies [Fintype V] :
   classical
   obtain rfl | hH := eq_or_ne H ⊥
   · simp [← card_edgeSet]
-  let f (G' : {G' : G.Subgraph // Nonempty (H ≃g G'.coe)}) := (aux hH G'.2).some
+  let f (G' : H.Sub G) := (aux hH G'.2).some
   calc
-    _ = #G.edgeFinset - card {G' : G.Subgraph // Nonempty (H ≃g G'.coe)} := ?_
+    _ = #G.edgeFinset - card (H.Sub G) := by rw [copyCount]
     _ ≤ #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

From 65fb74a7b267658ed16e049b1106a07b2578b93a Mon Sep 17 00:00:00 2001
From: Christoph Spiegel <christophspiegel.berlin@gmail.com>
Date: Sun, 17 May 2026 18:13:42 +0200
Subject: [PATCH 2/8] Renamed Sub to UnlabeledCopy per suggestion by
 mitchell-horner

---
 Mathlib/Combinatorics/SimpleGraph/Copy.lean | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Copy.lean b/Mathlib/Combinatorics/SimpleGraph/Copy.lean
index 22fa15e80e9aaa..d39026c14c4dea 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Copy.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Copy.lean
@@ -35,7 +35,7 @@ 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.Sub H G`: Type of `SimpleGraph.Subgraph`s of `G` isomorphic to `H`.
+* `SimpleGraph.UnlabeledCopy H G`: Type of `SimpleGraph.Subgraph`s of `G` isomorphic to `H`.
 * `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`
@@ -509,13 +509,13 @@ variable [Fintype V]
 
 /-- `Sub A B` is the type of `SimpleGraph.Subgraph`s of `B` isomorphic to `A`. The corresponding
 count is `SimpleGraph.copyCount`. -/
-abbrev Sub (A : SimpleGraph α) (B : SimpleGraph β) : Type _ :=
+abbrev UnlabeledCopy (A : SimpleGraph α) (B : SimpleGraph β) : Type _ :=
   {B' : B.Subgraph // Nonempty (A ≃g B'.coe)}
 
 /-- `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 Fintype.card (H.Sub G)
+  classical exact Fintype.card (H.UnlabeledCopy G)
 
 @[simp] lemma copyCount_eq_zero : G.copyCount H = 0 ↔ H.Free G := by
   classical
@@ -530,13 +530,14 @@ lemma copyCount_le_labelledCopyCount [Fintype W] : G.copyCount H ≤ G.labelledC
   classical
   rw [copyCount, labelledCopyCount]
   apply Fintype.card_le_of_surjective
-    (fun c : Copy H G ↦ (⟨c.toSubgraph, ⟨c.isoToSubgraph⟩⟩ : H.Sub G))
+    (fun c : Copy H G ↦ (⟨c.toSubgraph, ⟨c.isoToSubgraph⟩⟩ : H.UnlabeledCopy G))
   rintro ⟨G', hG'⟩
   obtain ⟨c, hc⟩ : ∃ c : Copy H G, c.toSubgraph = G' := by
     rwa [← Set.mem_range, Copy.range_toSubgraph]
   exact ⟨c, Subtype.ext hc⟩
 
-instance uniqueSubBot (G : SimpleGraph V) : Unique ((⊥ : SimpleGraph V).Sub G) where
+instance uniqueUnlabeledCopyBot (G : SimpleGraph V) :
+    Unique ((⊥ : SimpleGraph V).UnlabeledCopy G) where
   default := ⟨{ verts := .univ, Adj := ⊥, adj_sub := False.elim, edge_vert := False.elim },
               ⟨(Equiv.Set.univ _).symm, by simp⟩⟩
   uniq := fun ⟨G', ⟨e⟩⟩ ↦ Subtype.ext <| Subgraph.ext
@@ -657,9 +658,9 @@ lemma le_card_edgeFinset_killCopies [Fintype V] :
   classical
   obtain rfl | hH := eq_or_ne H ⊥
   · simp [← card_edgeSet]
-  let f (G' : H.Sub G) := (aux hH G'.2).some
+  let f (G' : H.UnlabeledCopy G) := (aux hH G'.2).some
   calc
-    _ = #G.edgeFinset - card (H.Sub G) := by rw [copyCount]
+    _ = #G.edgeFinset - card (H.UnlabeledCopy G) := by rw [copyCount]
     _ ≤ #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 ..

From 2b608efc00544a9d158cca6a5e66cfa6d4dccb59 Mon Sep 17 00:00:00 2001
From: Christoph Spiegel <christophspiegel.berlin@gmail.com>
Date: Wed, 8 Jul 2026 17:24:49 +0200
Subject: [PATCH 3/8] chore: fix stale Sub reference in UnlabeledCopy docstring

---
 Mathlib/Combinatorics/SimpleGraph/Copy.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Copy.lean b/Mathlib/Combinatorics/SimpleGraph/Copy.lean
index d39026c14c4dea..fa680514808524 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Copy.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Copy.lean
@@ -507,8 +507,8 @@ end LabelledCopyCount
 section CopyCount
 variable [Fintype V]
 
-/-- `Sub A B` is the type of `SimpleGraph.Subgraph`s of `B` isomorphic to `A`. The corresponding
-count is `SimpleGraph.copyCount`. -/
+/-- `UnlabeledCopy A B` is the type of `SimpleGraph.Subgraph`s of `B` isomorphic to `A`.
+The corresponding count is `SimpleGraph.copyCount`. -/
 abbrev UnlabeledCopy (A : SimpleGraph α) (B : SimpleGraph β) : Type _ :=
   {B' : B.Subgraph // Nonempty (A ≃g B'.coe)}
 

From 53a94cca2275dfc1d01de70fa86d48690c479069 Mon Sep 17 00:00:00 2001
From: Christoph Spiegel <christophspiegel.berlin@gmail.com>
Date: Sun, 12 Jul 2026 03:26:18 +0200
Subject: [PATCH 4/8] feat(Combinatorics/SimpleGraph/Copy): re-add
 copyCount_eq_card_image_copyToSubgraph as deprecated

Restores the exact statement of the legacy bridge lemma dropped when copyCount
was redefined via UnlabeledCopy, now carrying @[deprecated] (since 2026-07-12)
per review, with a proof against the new Fintype.card (H.UnlabeledCopy G) body.
---
 Mathlib/Combinatorics/SimpleGraph/Copy.lean | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Copy.lean b/Mathlib/Combinatorics/SimpleGraph/Copy.lean
index 485e575f5af617..6e593ebee6868e 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Copy.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Copy.lean
@@ -536,6 +536,18 @@ of `G` isomorphic to `H`. See `SimpleGraph.labelledCopyCount` for the number of
 noncomputable def copyCount (G : SimpleGraph V) (H : SimpleGraph W) : ℕ := by
   classical exact Fintype.card (H.UnlabeledCopy G)
 
+@[deprecated "`copyCount` is now defined directly as `Fintype.card (H.UnlabeledCopy G)`; there is \
+no longer a need to bridge through the image of `Copy.toSubgraph`" (since := "2026-07-12")]
+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
+  classical
+  rw [copyCount, Fintype.card_subtype]
+  congr 1
+  ext G'
+  simp only [Finset.mem_filter, Finset.mem_univ, true_and, Finset.mem_image]
+  rw [← Set.mem_range, Copy.range_toSubgraph, Set.mem_setOf_eq]
+
 @[simp] lemma copyCount_eq_zero : G.copyCount H = 0 ↔ H.Free G := by
   classical
   rw [copyCount, Fintype.card_eq_zero_iff, isEmpty_subtype]

From 3669ba684e3430294a5df7527476b880fb011fb4 Mon Sep 17 00:00:00 2001
From: Christoph Spiegel <christophspiegel.berlin@gmail.com>
Date: Wed, 13 May 2026 17:07:34 +0200
Subject: [PATCH 5/8] refactor(Combinatorics/SimpleGraph/Copy): rename copy
 counts and unify graph variables
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Aligns the labelled/unlabelled naming in `Copy.lean` so that the type `Copy G H`
(labelled, injective hom from `G` into `H`) is paired with the count
`H.copyCount G` (labelled count, host-first per mathlib op convention) and the
`UnlabeledCopy G H` carrier (introduced in the previous PR) is paired with the
count `H.unlabeledCopyCount G`. Also unifies the graph-variable letters: the
`A B C` set that was local to `Copy.lean` is dropped in favour of mathlib's
wider `G H I` convention, with `α β γ` → `V W X` correspondingly. Within the
new convention `G` is the guest (pattern, contained side) and `H` is the host
(container), matching `G ⊑ H` and the hom direction `G →g H`.

Types are guest-first (`Copy G H`, `UnlabeledCopy G H`); operations are
host-first via dot notation (`H.copyCount G`, `H.unlabeledCopyCount G`,
`H.killCopies G`). This matches the existing mathlib convention split (hom
types use source-first, host-side operations use the host as the dot-notation
receiver).

Changes:

* Rename `labelledCopyCount → copyCount` (with British `@[deprecated]` alias
  `labelledCopyCount`). The previous `copyCount → unlabeledCopyCount` rename
  has no alias — `copyCount` is reassigned to mean the labelled count. Same
  for the `_of_isEmpty` / `_eq_zero` / `_pos` lemma families.
* Rename `copyCount_bot → unlabeledCopyCount_bot` (count name rename only;
  `_bot` spelling preserved per @SnirBroshi).
* Unify `A B C / α β γ` to `G H I / V W X` throughout. Variable block follows
  the mathlib convention (cf. `SimpleGraph/Maps.lean`): subscripted names
  (`G₁ G₂ G₃`) for same-vertex-type variants used in `≤` chains and `ofLE`;
  primed names (`G'`, `H'`) on independent universes (`V'`, `W'`) for the
  cross-universe variants used in `isContained_congr` / `free_congr` (and
  their `_left` / `_right` partial-iso forms). This preserves the universe
  polymorphism the old `A B C / α β γ` block provided implicitly and that
  `Extremal/Basic.lean` (line 96, `← free_congr .refl (.map e G)`) relies on.
* Fix the docstring direction on `IsContained.trans` and `.trans'`: the
  previous wording ("`G` contains `H`") read the relation backwards relative
  to the lemma signature (`G ⊑ H` means `G` is contained in `H`).
* Update module docstring (`UnlabeledCopy` / `unlabeledCopyCount` bullets,
  logical-flow ordering, `SimpleGraph.Subgraph` cross-references); add TODOs
  for `homCount` and the three densities.
---
 Mathlib/Combinatorics/SimpleGraph/Copy.lean | 467 ++++++++++----------
 1 file changed, 229 insertions(+), 238 deletions(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Copy.lean b/Mathlib/Combinatorics/SimpleGraph/Copy.lean
index 6e593ebee6868e..e66526124fcd40 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Copy.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Copy.lean
@@ -9,25 +9,29 @@ public import Mathlib.Algebra.Order.Group.Nat
 public import Mathlib.Combinatorics.SimpleGraph.Subgraph
 
 /-!
-# 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`, `UnlabeledCopy G H`,
+`IsContained G H`, …) and operations are host-first via dot notation (`H.copyCount G`,
+`H.unlabeledCopyCount 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.UnlabeledCopy 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,17 +39,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.UnlabeledCopy H G`: Type of `SimpleGraph.Subgraph`s of `G` isomorphic to `H`.
-* `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.unlabeledCopyCount 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
 
@@ -57,7 +61,9 @@ 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`/`unlabeledCopyCount` computable (not necessarily efficiently).
+* Count the number of graph homomorphisms `G →g H` with `homCount G H`.
+* Add densities `copyDensity G H`, `unlabeledCopyDensity G H`, and `homDensity G H`.
 -/
 
 @[expose] public section
@@ -66,67 +72,64 @@ 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⟩
+def toEmbedding (f : Copy G H) : V ↪ W := ⟨f, f.injective⟩
 
 /-- The identity copy from a simple graph to itself. -/
 @[refl] def id (G : SimpleGraph V) : Copy G G := ⟨Hom.id, Function.injective_id⟩
@@ -134,20 +137,20 @@ def toEmbedding (f : Copy A B) : α ↪ β := ⟨f, f.injective⟩
 @[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⟩
 
 @[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
 
@@ -161,26 +164,26 @@ 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.defeqAttrib.useBackward true in
 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⟩
@@ -190,7 +193,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
@@ -203,13 +206,13 @@ instance [Fintype {f : G →g H // Injective f}] : Fintype (G.Copy H) :=
 
 /-- A copy of `⊤` gives rise to an embedding of `⊤`. -/
 @[simps!]
-def topEmbedding (f : Copy (⊤ : SimpleGraph α) G) : (⊤ : SimpleGraph α) ↪g G :=
+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⟩}
 
 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
@@ -217,27 +220,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
 
@@ -249,66 +248,66 @@ 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 β :=
+lemma bot_isContained_iff_card_le [Fintype V] [Fintype W] :
+    (⊥ : SimpleGraph V) ⊑ H ↔ Fintype.card V ≤ Fintype.card W :=
   ⟨fun ⟨f⟩ ↦ Fintype.card_le_of_embedding f.toEmbedding,
     fun h ↦ ⟨Copy.bot (Function.Embedding.nonempty_of_card_le 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
@@ -369,24 +368,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
@@ -398,10 +397,7 @@ 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
@@ -440,12 +436,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
 
@@ -487,88 +483,94 @@ theorem eq_top_of_isIndContained_top (h : G ⊴ completeGraph W) : 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
+### Counting copies
 
-If `G` and `H` are finite graphs, we can count the number of unlabelled and labelled copies of `G`
-in `H`.
-
-#### Not necessarily induced copies
+For finite `G` and `H`, we count labeled and unlabeled copies of `G` in `H`.
 -/
 
-section LabelledCopyCount
+section CopyCount
 variable [Fintype V] [Fintype W]
 
-/-- `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.unlabeledCopyCount` for the number of
+unlabeled copies. -/
+noncomputable def copyCount (H : SimpleGraph W) (G : SimpleGraph V) : ℕ := by
+  classical exact Fintype.card (Copy G H)
+
+@[deprecated (since := "2026-04-30")] alias labelledCopyCount := copyCount
 
-@[simp] lemma labelledCopyCount_of_isEmpty [IsEmpty W] (G : SimpleGraph V) (H : SimpleGraph W) :
-    G.labelledCopyCount H = 1 := by
+@[simp] lemma copyCount_of_isEmpty [IsEmpty V] (H : SimpleGraph W) (G : SimpleGraph V) :
+    H.copyCount G = 1 := by
   convert! Fintype.card_unique
   exact { default := ⟨default, isEmptyElim⟩, uniq := fun _ ↦ Subsingleton.elim _ _ }
 
-@[simp] lemma labelledCopyCount_eq_zero : G.labelledCopyCount H = 0 ↔ H.Free G := by
-  simp [labelledCopyCount, Fintype.card_eq_zero_iff]
+@[deprecated (since := "2026-04-30")]
+alias labelledCopyCount_of_isEmpty := copyCount_of_isEmpty
 
-@[simp] lemma labelledCopyCount_pos : 0 < G.labelledCopyCount H ↔ H ⊑ G := by
-  simp [labelledCopyCount, IsContained, Fintype.card_pos_iff]
+@[simp] lemma copyCount_eq_zero : H.copyCount G = 0 ↔ G.Free H := by
+  simp [copyCount, Fintype.card_eq_zero_iff]
 
-end LabelledCopyCount
+@[deprecated (since := "2026-04-30")] alias labelledCopyCount_eq_zero := copyCount_eq_zero
 
-section CopyCount
-variable [Fintype V]
-
-/-- `UnlabeledCopy A B` is the type of `SimpleGraph.Subgraph`s of `B` isomorphic to `A`.
-The corresponding count is `SimpleGraph.copyCount`. -/
-abbrev UnlabeledCopy (A : SimpleGraph α) (B : SimpleGraph β) : Type _ :=
-  {B' : B.Subgraph // Nonempty (A ≃g B'.coe)}
-
-/-- `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 Fintype.card (H.UnlabeledCopy G)
-
-@[deprecated "`copyCount` is now defined directly as `Fintype.card (H.UnlabeledCopy G)`; there is \
-no longer a need to bridge through the image of `Copy.toSubgraph`" (since := "2026-07-12")]
-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
+@[simp] lemma copyCount_pos : 0 < H.copyCount G ↔ G ⊑ H := by
+  simp [copyCount, IsContained, Fintype.card_pos_iff]
+
+@[deprecated (since := "2026-04-30")] alias labelledCopyCount_pos := copyCount_pos
+
+end CopyCount
+
+section UnlabeledCopyCount
+variable [Fintype W]
+
+/-- `G.UnlabeledCopy H` is the type of `SimpleGraph.Subgraph`s of `H` isomorphic to `G`. The
+corresponding count is `SimpleGraph.unlabeledCopyCount`. -/
+abbrev UnlabeledCopy (G : SimpleGraph V) (H : SimpleGraph W) : Type _ :=
+  {H' : H.Subgraph // Nonempty (G ≃g H'.coe)}
+
+/-- `H.unlabeledCopyCount G` is the number of `SimpleGraph.Subgraph`s of `H` isomorphic to `G`. See
+`SimpleGraph.copyCount` for the number of labeled copies. -/
+noncomputable def unlabeledCopyCount (H : SimpleGraph W) (G : SimpleGraph V) : ℕ := by
+  classical exact Fintype.card (G.UnlabeledCopy H)
+
+@[deprecated "the bridge through the image of `Copy.toSubgraph` is no longer needed now that the \
+count is defined directly on the subtype of isomorphic subgraphs" (since := "2026-07-12")]
+lemma copyCount_eq_card_image_copyToSubgraph [Fintype {f : G →g H // Injective f}]
+    [DecidableEq H.Subgraph] :
+    H.unlabeledCopyCount G = #((Finset.univ : Finset (G.Copy H)).image Copy.toSubgraph) := by
   classical
-  rw [copyCount, Fintype.card_subtype]
+  rw [unlabeledCopyCount, Fintype.card_subtype]
   congr 1
-  ext G'
+  ext H'
   simp only [Finset.mem_filter, Finset.mem_univ, true_and, Finset.mem_image]
   rw [← Set.mem_range, Copy.range_toSubgraph, Set.mem_setOf_eq]
 
-@[simp] lemma copyCount_eq_zero : G.copyCount H = 0 ↔ H.Free G := by
-  classical
-  rw [copyCount, Fintype.card_eq_zero_iff, isEmpty_subtype]
-  simp [Free, isContained_iff_exists_iso_subgraph]
+@[simp] lemma unlabeledCopyCount_eq_zero : H.unlabeledCopyCount G = 0 ↔ G.Free H := by
+  simp [unlabeledCopyCount, Free, -nonempty_subtype, isContained_iff_exists_iso_subgraph,
+    Fintype.card_eq_zero_iff, isEmpty_subtype, not_nonempty_iff]
 
-@[simp] lemma copyCount_pos : 0 < G.copyCount H ↔ H ⊑ G := by
-  simp [Nat.pos_iff_ne_zero, copyCount_eq_zero]
+@[simp] lemma unlabeledCopyCount_pos : 0 < H.unlabeledCopyCount G ↔ G ⊑ H := by
+  rw [Nat.pos_iff_ne_zero, ne_eq, unlabeledCopyCount_eq_zero, Free, not_not]
 
-/-- 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
+/-- There are at least as many labeled copies of `G` in `H` as there are unlabeled ones. -/
+lemma unlabeledCopyCount_le_copyCount [Fintype V] : H.unlabeledCopyCount G ≤ H.copyCount G := by
   classical
-  rw [copyCount, labelledCopyCount]
+  rw [unlabeledCopyCount, copyCount]
   apply Fintype.card_le_of_surjective
-    (fun c : Copy H G ↦ (⟨c.toSubgraph, ⟨c.isoToSubgraph⟩⟩ : H.UnlabeledCopy G))
-  rintro ⟨G', hG'⟩
-  obtain ⟨c, hc⟩ : ∃ c : Copy H G, c.toSubgraph = G' := by
+    (fun c : Copy G H ↦ (⟨c.toSubgraph, ⟨c.isoToSubgraph⟩⟩ : G.UnlabeledCopy H))
+  rintro ⟨H', hG'⟩
+  obtain ⟨c, hc⟩ : ∃ c, Copy.toSubgraph c = H' := by
     rwa [← Set.mem_range, Copy.range_toSubgraph]
   exact ⟨c, Subtype.ext hc⟩
 
-instance uniqueUnlabeledCopyBot (G : SimpleGraph V) :
-    Unique ((⊥ : SimpleGraph V).UnlabeledCopy G) where
+instance uniqueUnlabeledCopyBot (H : SimpleGraph W) :
+    Unique ((⊥ : SimpleGraph W).UnlabeledCopy H) where
   default := ⟨{ verts := .univ, Adj := ⊥, adj_sub := False.elim, edge_vert := False.elim },
               ⟨(Equiv.Set.univ _).symm, by simp⟩⟩
   uniq := fun ⟨G', ⟨e⟩⟩ ↦ Subtype.ext <| Subgraph.ext
@@ -577,140 +579,129 @@ instance uniqueUnlabeledCopyBot (G : SimpleGraph V) :
         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_bot (G : SimpleGraph V) : copyCount G (⊥ : SimpleGraph V) = 1 := by
+@[simp] lemma unlabeledCopyCount_bot (H : SimpleGraph W) :
+    H.unlabeledCopyCount (⊥ : SimpleGraph W) = 1 := by
   classical
-  rw [copyCount]
-  exact Fintype.card_unique
+  rw [unlabeledCopyCount]
+  convert Fintype.card_unique
+  exact uniqueUnlabeledCopyBot H
 
-@[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 unlabeledCopyCount_of_isEmpty [IsEmpty V] (H : SimpleGraph W) (G : SimpleGraph V) :
+    H.unlabeledCopyCount G = 1 := by
+  cases nonempty_fintype V
+  exact (unlabeledCopyCount_le_copyCount.trans_eq <| copyCount_of_isEmpty ..).antisymm <|
+    unlabeledCopyCount_pos.2 <| .of_isEmpty
 
-end CopyCount
+end UnlabeledCopyCount
 
 /-!
-#### Induced copies
-
-TODO
+### Killing all copies of a graph
 
-### Killing a subgraph
-
-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`.
-
-#### Killing not necessarily induced copies
-
-`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`.
+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_sdiff,
     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 [Fintype W] :
+    #H.edgeFinset - H.unlabeledCopyCount 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' : H.UnlabeledCopy G) := (aux hH G'.2).some
+  let f (H' : G.UnlabeledCopy H) := (aux hG H'.2).some
   calc
-    _ = #G.edgeFinset - card (H.UnlabeledCopy G) := by rw [copyCount]
-    _ ≤ #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 := ?_
+    _ = #H.edgeFinset - Fintype.card (G.UnlabeledCopy H) := ?_
+    _ ≤ #H.edgeFinset - #(univ.image f) := Nat.sub_le_sub_left card_image_le _
+    _ = #H.edgeFinset - #(Set.range f).toFinset := by rw [Set.toFinset_range]
+    _ ≤ #(H.edgeFinset \ (Set.range f).toFinset) := le_card_sdiff ..
+    _ = #(H.killCopies G).edgeFinset := ?_
+  · simp only [edgeFinset, Set.toFinset_card]
+    rw [← Set.toFinset_card, ← edgeFinset, unlabeledCopyCount]
   congr 1
   ext e
   induction e using Sym2.inductionOn with | hf v w
-  simp [mem_edgeSet, killCopies_of_ne_bot hH, f, eq_comm]
+  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_unlabeledCopyCount [Fintype W] :
+    #H.edgeFinset ≤ #(H.killCopies G).edgeFinset + H.unlabeledCopyCount G :=
   tsub_le_iff_right.1 le_card_edgeFinset_killCopies
 
-/-!
-#### Killing induced copies
-
-TODO
--/
-
 end SimpleGraph

From dec7da1ccdac49210b6af6e9c86c31325738813f Mon Sep 17 00:00:00 2001
From: Christoph Spiegel <christophspiegel.berlin@gmail.com>
Date: Fri, 17 Jul 2026 14:27:09 +0200
Subject: [PATCH 6/8] restored simpler proof of copyCount_eq_zero

---
 Mathlib/Combinatorics/SimpleGraph/Copy.lean | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Copy.lean b/Mathlib/Combinatorics/SimpleGraph/Copy.lean
index 6e593ebee6868e..2ba4d606ff6ccf 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Copy.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Copy.lean
@@ -549,9 +549,8 @@ lemma copyCount_eq_card_image_copyToSubgraph [Fintype {f : H →g G // Injective
   rw [← Set.mem_range, Copy.range_toSubgraph, Set.mem_setOf_eq]
 
 @[simp] lemma copyCount_eq_zero : G.copyCount H = 0 ↔ H.Free G := by
-  classical
-  rw [copyCount, Fintype.card_eq_zero_iff, isEmpty_subtype]
-  simp [Free, isContained_iff_exists_iso_subgraph]
+  simp [copyCount, Free, -nonempty_subtype, isContained_iff_exists_iso_subgraph,
+    Fintype.card_eq_zero_iff, isEmpty_subtype, not_nonempty_iff]
 
 @[simp] lemma copyCount_pos : 0 < G.copyCount H ↔ H ⊑ G := by
   simp [Nat.pos_iff_ne_zero, copyCount_eq_zero]

From 9a02a88518e65a110f3840c28cd0ec36d739bda4 Mon Sep 17 00:00:00 2001
From: Christoph Spiegel <christophspiegel.berlin@gmail.com>
Date: Fri, 17 Jul 2026 14:39:20 +0200
Subject: [PATCH 7/8] un-deprecated copyCount_eq_card_image_copyToSubgraph and
 restored proof of copyCount_le_labelledCopyCount

---
 Mathlib/Combinatorics/SimpleGraph/Copy.lean | 11 +----------
 1 file changed, 1 insertion(+), 10 deletions(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Copy.lean b/Mathlib/Combinatorics/SimpleGraph/Copy.lean
index 2ba4d606ff6ccf..ce3125c376f157 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Copy.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Copy.lean
@@ -536,8 +536,6 @@ of `G` isomorphic to `H`. See `SimpleGraph.labelledCopyCount` for the number of
 noncomputable def copyCount (G : SimpleGraph V) (H : SimpleGraph W) : ℕ := by
   classical exact Fintype.card (H.UnlabeledCopy G)
 
-@[deprecated "`copyCount` is now defined directly as `Fintype.card (H.UnlabeledCopy G)`; there is \
-no longer a need to bridge through the image of `Copy.toSubgraph`" (since := "2026-07-12")]
 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
@@ -557,14 +555,7 @@ lemma copyCount_eq_card_image_copyToSubgraph [Fintype {f : H →g G // Injective
 
 /-- 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, labelledCopyCount]
-  apply Fintype.card_le_of_surjective
-    (fun c : Copy H G ↦ (⟨c.toSubgraph, ⟨c.isoToSubgraph⟩⟩ : H.UnlabeledCopy G))
-  rintro ⟨G', hG'⟩
-  obtain ⟨c, hc⟩ : ∃ c : Copy H G, c.toSubgraph = G' := by
-    rwa [← Set.mem_range, Copy.range_toSubgraph]
-  exact ⟨c, Subtype.ext hc⟩
+  classical rw [copyCount_eq_card_image_copyToSubgraph]; exact card_image_le
 
 instance uniqueUnlabeledCopyBot (G : SimpleGraph V) :
     Unique ((⊥ : SimpleGraph V).UnlabeledCopy G) where

From 40e1050f366d76febfa163a4d52cc01af3e28668 Mon Sep 17 00:00:00 2001
From: Christoph Spiegel <christophspiegel.berlin@gmail.com>
Date: Fri, 17 Jul 2026 17:49:26 +0200
Subject: [PATCH 8/8] replace deprecated mem_setOf_eq with mem_ofPred_eq

---
 Mathlib/Combinatorics/SimpleGraph/Copy.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Copy.lean b/Mathlib/Combinatorics/SimpleGraph/Copy.lean
index 7b01ba1c8b45ec..de2edbb5f21adc 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Copy.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Copy.lean
@@ -544,7 +544,7 @@ lemma copyCount_eq_card_image_copyToSubgraph [Fintype {f : H →g G // Injective
   congr 1
   ext G'
   simp only [Finset.mem_filter, Finset.mem_univ, true_and, Finset.mem_image]
-  rw [← Set.mem_range, Copy.range_toSubgraph, Set.mem_setOf_eq]
+  rw [← Set.mem_range, Copy.range_toSubgraph, Set.mem_ofPred_eq]
 
 @[simp] lemma copyCount_eq_zero : G.copyCount H = 0 ↔ H.Free G := by
   simp [copyCount, Free, -nonempty_subtype, isContained_iff_exists_iso_subgraph,