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/7] 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/7] 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/7] 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/7] 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 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 5/7] 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 6/7] 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 7/7] 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,