refactor(Combinatorics/SimpleGraph/Copy): rename copy counts, introduce Sub subtype

Aligns the `Copy.lean` naming with the four-axis hom/copy/subgraph taxonomy
discussed in Zulip (#general > "SimpleGraph.Copy is labeled but copyCount
is not"):

  | notion                   | before              | after        |
  | ------------------------ | ------------------- | ------------ |
  | labelled copy (inj hom)  | `Copy A B`          | unchanged    |
  | unlabelled subgraph type | inlined subtype     | `Sub H G`    |
  | labelled count           | `labelledCopyCount` | `copyCount`  |
  | unlabelled count         | `copyCount`         | `subCount`   |

Changes:

* Rename `labelledCopyCount → copyCount` (with British deprecation alias
  `labelledCopyCount`); rename the corresponding `_of_isEmpty`,
  `_eq_zero`, `_pos` lemmas similarly.
* Rename the previous `copyCount → subCount` (no alias — name is
  reassigned to the labelled count). Rename `_eq_zero`, `_pos`, `_bot`,
  `_of_isEmpty`, `_le_*` lemmas accordingly.
* Add `abbrev Sub (H : SimpleGraph W) (G : SimpleGraph V) := {G' : G.Subgraph // Nonempty (H ≃g G'.coe)}`
  alongside `subCount`. The corresponding count name `subCount` matches
  Lovász's blackboard `sub(H, G)`.
* Redefine `subCount` as `Fintype.card (H.Sub G)` (was the filter-set form
  `#{G' : G.Subgraph | Nonempty (H ≃g G'.coe)}`). Proofs of
  `subCount_eq_zero`, `subCount_pos`, `subCount_bot`, and
  `subCount_le_copyCount` updated to use type-form lemmas
  (`Fintype.card_eq_zero_iff`, `Fintype.card_unique`,
  `Fintype.card_le_of_surjective`).
* Drop `copyCount_eq_card_image_copyToSubgraph` (legacy filter-form
  bridge, unused after the type-form refactor).
* Add `instance uniqueSubBot : Unique ((⊥ : SimpleGraph V).Sub G)`,
  factoring the singleton-empty-subgraph fact out of `subCount_bot`.
* Update `le_card_edgeFinset_killCopies` to use `H.Sub G` directly
  (was inline subtype + `card_subtype`/`subtype_univ`/`card_univ`
  rewrite chain).
* Update module docstring: add `Sub`/`subCount` bullets; clarify that
  `Sub` references `SimpleGraph.Subgraph` (the labelled non-induced
  structure); reorder declarations in logical-flow order (`Copy →
  IsContained → Free → Sub → copyCount → subCount → killCopies`); add
  TODOs for `homCount` and the three densities (`copyDensity`,
  `subDensity`, `homDensity`).

Author: FordUniver

Mathlib/Combinatorics/SimpleGraph/Copy.lean

@@ -35,12 +35,12 @@ 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.copyCount G H`: Number of labeled copies of `H` in `G`, i.e. number of injective
+  graph homomorphisms from `H` to `G`.
+* `SimpleGraph.subCount G H`: Number 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`.
 
 Induced containment:
 * Induced copies of `G` inside `H` are already defined as `G ↪g H`.
@@ -56,10 +56,12 @@ 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).
+* Add `homCount G H` for the number of graph homomorphisms `H →g G`.
+* Add `copyDensity G H`, `subDensity G H` (and `homDensity G H` once `homCount` exists).
 -/
 
-public section
+@[expose] public section
 
 open Finset Function
 open Fintype (card)
@@ -125,12 +127,10 @@ def mapNeighborSet (f : Copy A B) (a : α) :
     exact f.injective h
 
 /-- A copy gives rise to an embedding of vertex types. -/
-@[expose] def toEmbedding (f : Copy A B) : α ↪ β := ⟨f, f.injective⟩
-
-@[simp] lemma toEmbedding_apply (f : Copy A B) (a : α) : f.toEmbedding a = f a := rfl
+def toEmbedding (f : Copy A B) : α ↪ β := ⟨f, f.injective⟩
 
 /-- The identity copy from a simple graph to itself. -/
-@[expose, refl] def id (G : SimpleGraph V) : Copy G G := ⟨Hom.id, Function.injective_id⟩
+@[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
 
@@ -145,8 +145,7 @@ theorem comp_apply (g : Copy B C) (f : Copy A B) (a : α) : g.comp f a = g (f a)
   RelHom.comp_apply g.toHom f.toHom a
 
 /-- The copy from a subgraph to the supergraph. -/
-@[expose] def ofLE (G₁ G₂ : SimpleGraph V) (h : G₁ ≤ G₂) : Copy G₁ G₂ :=
-    ⟨Hom.ofLE h, Function.injective_id⟩
+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
@@ -203,12 +202,10 @@ instance [Fintype {f : G →g H // Injective f}] : Fintype (G.Copy H) :=
   }
 
 /-- A copy of `⊤` gives rise to an embedding of `⊤`. -/
-@[expose] def topEmbedding (f : Copy (⊤ : SimpleGraph α) G) : (⊤ : SimpleGraph α) ↪g G :=
+@[simps!]
+def topEmbedding (f : Copy (⊤ : SimpleGraph α) G) : (⊤ : SimpleGraph α) ↪g G :=
   { f.toEmbedding with
-    map_rel_iff' := fun {_ _} ↦ ⟨fun h ↦ f.injective.ne_iff.mp h.ne, f.toHom.map_adj⟩ }
-
-@[simp] lemma topEmbedding_apply (f : Copy (⊤ : SimpleGraph α) G) (v : α) :
-    f.topEmbedding v = f v := rfl
+    map_rel_iff' := fun {v w} ↦ ⟨fun h ↦ by simpa using h.ne, f.toHom.map_adj⟩}
 
 end Copy
 
@@ -390,7 +387,7 @@ We denote "`G` is inducingly contained in `H`" by `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`. -/
-abbrev IsIndContained (G : SimpleGraph V) (H : SimpleGraph W) : Prop := Nonempty (G ↪g H)
+def IsIndContained (G : SimpleGraph V) (H : SimpleGraph W) : Prop := Nonempty (G ↪g H)
 
 @[inherit_doc] scoped infixl:50 " ⊴ " => SimpleGraph.IsIndContained
 
@@ -471,83 +468,98 @@ theorem isIndContained_iff_exists_comap_eq : H ⊴ G ↔ ∃ (f : W ↪ V), G.co
 /-!
 ### Counting the copies
 
-If `G` and `H` are finite graphs, we can count the number of unlabelled and labelled copies of `G`
+If `G` and `H` are finite graphs, we can count the number of unlabeled and labeled copies of `G`
 in `H`.
 
 #### Not necessarily induced copies
 -/
 
-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
+/-- `G.copyCount H` is the number of labeled copies of `H` in `G`, i.e. the number of graph
+embeddings from `H` to `G`. See `SimpleGraph.subCount` for the number of unlabeled copies. -/
+noncomputable def copyCount (G : SimpleGraph V) (H : SimpleGraph W) : ℕ := by
   classical exact Fintype.card (Copy H G)
 
-@[simp] lemma labelledCopyCount_of_isEmpty [IsEmpty W] (G : SimpleGraph V) (H : SimpleGraph W) :
-    G.labelledCopyCount H = 1 := by
+@[deprecated (since := "2026-04-30")] alias labelledCopyCount := copyCount
+
+@[simp] lemma copyCount_of_isEmpty [IsEmpty W] (G : SimpleGraph V) (H : SimpleGraph W) :
+    G.copyCount H = 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 : G.copyCount H = 0 ↔ H.Free G := 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]
+@[simp] lemma copyCount_pos : 0 < G.copyCount H ↔ H ⊑ G := by
+  simp [copyCount, IsContained, Fintype.card_pos_iff]
 
-/-- `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)}
+@[deprecated (since := "2026-04-30")] alias labelledCopyCount_pos := copyCount_pos
 
-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
+end CopyCount
 
-@[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]
+section SubCount
+variable [Fintype V]
 
-@[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]
+/-- `H.Sub G` is the type of `SimpleGraph.Subgraph`s of `G` isomorphic to `H`. The corresponding
+count is `SimpleGraph.subCount`. -/
+abbrev Sub (H : SimpleGraph W) (G : SimpleGraph V) : Type _ :=
+  {G' : G.Subgraph // Nonempty (H ≃g G'.coe)}
+
+/-- `G.subCount H` is the number of `SimpleGraph.Subgraph`s of `G` isomorphic to `H`. See
+`SimpleGraph.copyCount` for the number of labeled copies. -/
+noncomputable def subCount (G : SimpleGraph V) (H : SimpleGraph W) : ℕ := by
+  classical exact Fintype.card (H.Sub G)
+
+@[simp] lemma subCount_eq_zero : G.subCount H = 0 ↔ H.Free G := by
+  simp [subCount, Free, -nonempty_subtype, isContained_iff_exists_iso_subgraph,
+    Fintype.card_eq_zero_iff, isEmpty_subtype, not_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 subCount_pos : 0 < G.subCount H ↔ H ⊑ G := by
+  rw [Nat.pos_iff_ne_zero, ne_eq, subCount_eq_zero, Free, not_not]
 
-@[simp] lemma copyCount_bot (G : SimpleGraph V) : copyCount G (⊥ : SimpleGraph V) = 1 := by
+/-- There's at least as many labeled copies of `H` in `G` than unlabeled ones. -/
+lemma subCount_le_copyCount [Fintype W] : G.subCount H ≤ G.copyCount H := 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
+  rw [subCount, copyCount]
+  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.toSubgraph c = G' := by
+    rwa [← Set.mem_range, Copy.range_toSubgraph]
+  exact ⟨c, Subtype.ext hc⟩
+
+@[deprecated (since := "2026-04-30")]
+alias subCount_le_labelledCopyCount := subCount_le_copyCount
+
+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 ⟨H', ⟨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 subCount_bot (G : SimpleGraph V) : subCount G (⊥ : SimpleGraph V) = 1 := by
+  classical
+  rw [subCount]
+  convert Fintype.card_unique
+  exact uniqueSubBot G
 
-@[simp] lemma copyCount_of_isEmpty [IsEmpty W] (G : SimpleGraph V) (H : SimpleGraph W) :
-    G.copyCount H = 1 := by
+@[simp] lemma subCount_of_isEmpty [IsEmpty W] (G : SimpleGraph V) (H : SimpleGraph W) :
+    G.subCount H = 1 := by
   cases nonempty_fintype W
-  exact (copyCount_le_labelledCopyCount.trans_eq <| labelledCopyCount_of_isEmpty ..).antisymm <|
-    copyCount_pos.2 <| .of_isEmpty
+  exact (subCount_le_copyCount.trans_eq <| copyCount_of_isEmpty ..).antisymm <|
+    subCount_pos.2 <| .of_isEmpty
 
-end CopyCount
+end SubCount
 
 /-!
 #### Induced copies
@@ -644,28 +656,28 @@ noncomputable instance killCopies.edgeSet.instFintype : Fintype (G.killCopies H)
 /-- 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
+    #G.edgeFinset - G.subCount H ≤ #(G.killCopies H).edgeFinset := by
   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 - Fintype.card (H.Sub G) := ?_
     _ ≤ #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]
+    rw [← Set.toFinset_card, ← edgeFinset, subCount]
   congr 1
   ext e
   induction e using Sym2.inductionOn with | hf v w
   simp [mem_edgeSet, killCopies_of_ne_bot hH, 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 [Fintype V] :
+    #G.edgeFinset ≤ #(G.killCopies H).edgeFinset + G.subCount H :=
   tsub_le_iff_right.1 le_card_edgeFinset_killCopies
 
 /-!