chore(Combinatorics/SimpleGraph/Copy): migrate copyCount/labeledCopyCount to Nat.card

- `copyCount` and `labeledCopyCount` redefined via `Nat.card` instead of `Fintype.card`
- `Fintype` hypotheses weakened to `Finite` throughout (`copyCount_eq_zero`,
  `copyCount_pos`, `labeledCopyCount_eq_zero`, `labeledCopyCount_pos`,
  `copyCount_le_labeledCopyCount`)
- `bot_isContained_iff_card_le`: generalized `[Fintype] → [Finite]`, `Fintype.card → Nat.card`
- `le_card_edgeFinset_killCopies`: proof avoids `Fintype.ofFinite` round-trip via
  `Set.finite_range` + `Set.Finite.toFinset`
- `copyCount_eq_card_image_copyToSubgraph`: deprecated in favour of
  `copyCount_eq_nat_card_range_toSubgraph`; proof via `Nat.subtype_card`
- Various proof tightening and private lemma extraction

Author: FordUniver

Mathlib/Combinatorics/SimpleGraph/Copy.lean

@@ -7,6 +7,8 @@ module
 
 public import Mathlib.Algebra.Order.Group.Nat
 public import Mathlib.Combinatorics.SimpleGraph.Subgraph
+public import Mathlib.Data.Finite.Card
+public import Mathlib.Data.Set.Finite.Range
 
 /-!
 # Containment of graphs
@@ -62,7 +64,6 @@ The following notation is declared in scope `SimpleGraph`:
 public section
 
 open Finset Function
-open Fintype (card)
 
 namespace SimpleGraph
 variable {V W X α β γ : Type*} {G G₁ G₂ G₃ : SimpleGraph V} {H : SimpleGraph W} {I : SimpleGraph X}
@@ -202,6 +203,9 @@ instance [Fintype {f : G →g H // Injective f}] : Fintype (G.Copy H) :=
     invFun f := ⟨f.1, f.2⟩
   }
 
+instance [Finite V] [Finite W] : Finite (G.Copy H) :=
+  Finite.of_injective _ DFunLike.coe_injective
+
 /-- A copy of `⊤` gives rise to an embedding of `⊤`. -/
 @[expose] def topEmbedding (f : Copy (⊤ : SimpleGraph α) G) : (⊤ : SimpleGraph α) ↪g G :=
   { f.toEmbedding with
@@ -297,10 +301,11 @@ lemma IsContained.of_isEmpty [IsEmpty α] : A ⊑ B :=
   ⟨⟨isEmptyElim, fun {a} ↦ isEmptyElim a⟩, isEmptyElim⟩
 
 /-- `⊥` is contained in any simple graph having sufficiently many vertices. -/
-lemma bot_isContained_iff_card_le [Fintype α] [Fintype β] :
-    (⊥ : SimpleGraph α) ⊑ B ↔ Fintype.card α ≤ Fintype.card β :=
-  ⟨fun ⟨f⟩ ↦ Fintype.card_le_of_embedding f.toEmbedding,
-    fun h ↦ ⟨Copy.bot (Function.Embedding.nonempty_of_card_le h).some⟩⟩
+lemma bot_isContained_iff_card_le [Finite α] [Finite β] :
+    (⊥ : SimpleGraph α) ⊑ B ↔ Nat.card α ≤ Nat.card β :=
+  ⟨fun ⟨f⟩ ↦ Finite.card_le_of_embedding f.toEmbedding,
+    fun h ↦ ⟨Copy.bot (Cardinal.lift_mk_le'.mp (by
+      simp only [← Nat.cast_card, Cardinal.lift_natCast]; exact_mod_cast h)).some⟩⟩
 
 protected alias IsContained.bot := bot_isContained_iff_card_le
 
@@ -478,86 +483,113 @@ in `H`.
 -/
 
 section LabeledCopyCount
-variable [Fintype V] [Fintype W]
 
 /-- `G.labeledCopyCount H` is the number of labeled copies of `H` in `G`, i.e. the number of graph
 embeddings from `H` to `G`. See `SimpleGraph.copyCount` for the number of unlabeled copies. -/
-noncomputable def labeledCopyCount (G : SimpleGraph V) (H : SimpleGraph W) : ℕ := by
-  classical exact Fintype.card (Copy H G)
+noncomputable def labeledCopyCount (G : SimpleGraph V) (H : SimpleGraph W) : ℕ :=
+  Nat.card (Copy H G)
 
 @[deprecated (since := "2026-04-30")] alias labelledCopyCount := labeledCopyCount
 
+private instance [IsEmpty W] : Nonempty (H.Copy G) := IsContained.of_isEmpty
+
 @[simp] lemma labeledCopyCount_of_isEmpty [IsEmpty W] (G : SimpleGraph V) (H : SimpleGraph W) :
-    G.labeledCopyCount H = 1 := by
-  convert Fintype.card_unique
-  exact { default := ⟨default, isEmptyElim⟩, uniq := fun _ ↦ Subsingleton.elim _ _ }
+    G.labeledCopyCount H = 1 := Nat.card_unique
 
 @[deprecated (since := "2026-04-30")]
 alias labelledCopyCount_of_isEmpty := labeledCopyCount_of_isEmpty
 
-@[simp] lemma labeledCopyCount_eq_zero : G.labeledCopyCount H = 0 ↔ H.Free G := by
-  simp [labeledCopyCount, Fintype.card_eq_zero_iff]
+@[simp] lemma labeledCopyCount_eq_zero [Finite V] [Finite W] :
+    G.labeledCopyCount H = 0 ↔ H.Free G := by
+  rw [labeledCopyCount, Nat.card_eq_zero, or_iff_left (Finite.not_infinite inferInstance)]
+  simp [Free, IsContained]
 
 @[deprecated (since := "2026-04-30")] alias labelledCopyCount_eq_zero := labeledCopyCount_eq_zero
 
-@[simp] lemma labeledCopyCount_pos : 0 < G.labeledCopyCount H ↔ H ⊑ G := by
-  simp [labeledCopyCount, IsContained, Fintype.card_pos_iff]
+@[simp] lemma labeledCopyCount_pos [Finite V] [Finite W] : 0 < G.labeledCopyCount H ↔ H ⊑ G := by
+  simp [Nat.pos_iff_ne_zero, labeledCopyCount_eq_zero]
 
 @[deprecated (since := "2026-04-30")] alias labelledCopyCount_pos := labeledCopyCount_pos
 
 end LabeledCopyCount
 
 section CopyCount
-variable [Fintype V]
 
 /-- `G.copyCount H` is the number of unlabeled copies of `H` in `G`, i.e. the number of subgraphs
 of `G` isomorphic to `H`. See `SimpleGraph.labeledCopyCount` for the number of labeled copies. -/
-noncomputable def copyCount (G : SimpleGraph V) (H : SimpleGraph W) : ℕ := by
-  classical exact #{G' : G.Subgraph | Nonempty (H ≃g G'.coe)}
+noncomputable def copyCount (G : SimpleGraph V) (H : SimpleGraph W) : ℕ :=
+  Nat.card {G' : G.Subgraph // Nonempty (H ≃g G'.coe)}
+
+lemma copyCount_eq_nat_card_range_toSubgraph :
+    copyCount G H = Nat.card (Set.range (Copy.toSubgraph : H.Copy G → G.Subgraph)) := by
+  rw [copyCount, Copy.range_toSubgraph]; rfl
 
-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
+@[deprecated copyCount_eq_nat_card_range_toSubgraph (since := "2026-05-04")]
+lemma copyCount_eq_card_image_copyToSubgraph [Fintype (H.Copy G)] [DecidableEq G.Subgraph] :
+    copyCount G H = (Finset.univ.image (Copy.toSubgraph (A := H) (B := G))).card := by
   rw [copyCount]
-  congr
-  refine Finset.coe_injective ?_
-  simpa [-Copy.range_toSubgraph] using Copy.range_toSubgraph.symm
+  exact Nat.subtype_card _ fun G' => by
+    simp only [Finset.mem_image, Finset.mem_univ, true_and]
+    constructor
+    · rintro ⟨f, rfl⟩; exact ⟨f.isoToSubgraph⟩
+    · rintro ⟨e⟩
+      exact ⟨⟨G'.hom.comp e.toHom, Subgraph.hom_injective.comp e.injective⟩,
+             by simp [Copy.toSubgraph, Subgraph.map_comp]⟩
 
-@[simp] lemma copyCount_eq_zero : G.copyCount H = 0 ↔ H.Free G := by
-  simp [copyCount, Free, -nonempty_subtype, isContained_iff_exists_iso_subgraph,
-    filter_eq_empty_iff]
+@[simp] lemma copyCount_eq_zero [Finite V] : G.copyCount H = 0 ↔ H.Free G := by
+  rw [copyCount, Nat.card_eq_zero, or_iff_left (Finite.not_infinite inferInstance), 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] lemma copyCount_pos [Finite V] : 0 < G.copyCount H ↔ H ⊑ G := by
+  simp [Nat.pos_iff_ne_zero, copyCount_eq_zero]
 
 /-- There's at least as many labeled copies of `H` in `G` than unlabeled ones. -/
-lemma copyCount_le_labeledCopyCount [Fintype W] : G.copyCount H ≤ G.labeledCopyCount H := by
-  classical rw [copyCount_eq_card_image_copyToSubgraph]; exact card_image_le
+lemma copyCount_le_labeledCopyCount [Finite V] [Finite W] :
+    G.copyCount H ≤ G.labeledCopyCount H :=
+  copyCount_eq_nat_card_range_toSubgraph ▸ Finite.card_range_le _
 
 @[deprecated (since := "2026-04-30")]
 alias copyCount_le_labelledCopyCount := copyCount_le_labeledCopyCount
 
-@[simp] lemma copyCount_bot (G : SimpleGraph V) : copyCount G (⊥ : SimpleGraph V) = 1 := by
+private lemma subgraph_iso_bot [Finite V] (Gx : G.Subgraph) (e : (⊥ : SimpleGraph V) ≃g Gx.coe) :
+    Gx.verts = Set.univ ∧ Gx.Adj = ⊥ := by
+  constructor
+  · apply Set.eq_univ_of_forall
+    intro v
+    obtain ⟨w, hw⟩ := (Finite.injective_iff_surjective.mp
+      (Subtype.val_injective.comp e.toEquiv.injective)) v
+    exact hw ▸ (e.toEquiv w).prop
+  · exact funext₂ fun a b => eq_false fun hadj =>
+        absurd (e.symm.map_rel_iff.mpr hadj.coe) (by simp)
+
+private instance [Finite V] :
+    Nonempty {G' : G.Subgraph // Nonempty ((⊥ : SimpleGraph V) ≃g G'.coe)} :=
+  ⟨{ verts := .univ, Adj := ⊥, adj_sub := False.elim, edge_vert := False.elim },
+    ⟨⟨(Equiv.Set.univ V).symm, by simp⟩⟩⟩
+
+private instance [Finite V] :
+    Subsingleton {G' : G.Subgraph // Nonempty ((⊥ : SimpleGraph V) ≃g G'.coe)} := 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
+  constructor
+  rintro ⟨G', ⟨e⟩⟩ ⟨G'', ⟨e'⟩⟩
+  congr 1
+  exact Subgraph.ext ((subgraph_iso_bot G' e).1.trans (subgraph_iso_bot G'' e').1.symm)
+    ((subgraph_iso_bot G' e).2.trans (subgraph_iso_bot G'' e').2.symm)
+
+@[simp] lemma copyCount_bot [Finite V] (G : SimpleGraph V) :
+    copyCount G (⊥ : SimpleGraph V) = 1 := by
+  rw [copyCount]; exact Nat.card_unique
+
+private instance [IsEmpty W] : Nonempty {G' : G.Subgraph // Nonempty (H ≃g G'.coe)} :=
+  nonempty_subtype.mpr (isContained_iff_exists_iso_subgraph.mp IsContained.of_isEmpty)
+
+private instance [IsEmpty W] : Subsingleton {G' : G.Subgraph // Nonempty (H ≃g G'.coe)} :=
+  ⟨fun ⟨G', ⟨e⟩⟩ ⟨G'', ⟨e'⟩⟩ => Subtype.ext <|
+    (G'.eq_bot_iff_verts_eq_empty.mpr (Set.isEmpty_coe_sort.mp e.toEquiv.symm.isEmpty)).trans
+    (G''.eq_bot_iff_verts_eq_empty.mpr (Set.isEmpty_coe_sort.mp e'.toEquiv.symm.isEmpty)).symm⟩
 
 @[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_labeledCopyCount.trans_eq <| labeledCopyCount_of_isEmpty ..).antisymm <|
-    copyCount_pos.2 <| .of_isEmpty
+    G.copyCount H = 1 := by rw [copyCount]; exact Nat.card_unique
 
 end CopyCount
 
@@ -655,28 +687,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] :
+lemma le_card_edgeFinset_killCopies [Finite V] :
     #G.edgeFinset - G.copyCount 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
-  calc
-    _ = #G.edgeFinset - card {G' : G.Subgraph // Nonempty (H ≃g G'.coe)} := ?_
-    _ ≤ #G.edgeFinset - #(univ.image f) := Nat.sub_le_sub_left card_image_le _
-    _ = #G.edgeFinset - #(Set.range f).toFinset := by rw [Set.toFinset_range]
-    _ ≤ #(G.edgeFinset \ (Set.range f).toFinset) := le_card_sdiff ..
-    _ = #(G.killCopies H).edgeFinset := ?_
-  · simp only [edgeFinset, Set.toFinset_card]
-    rw [← Set.toFinset_card, ← edgeFinset, copyCount, ← card_subtype, subtype_univ, card_univ]
-  congr 1
-  ext e
-  induction e using Sym2.inductionOn with | hf v w
-  simp [mem_edgeSet, killCopies_of_ne_bot hH, f, eq_comm]
+  have hrf : (Set.range f).Finite := Set.finite_range f
+  have hle : hrf.toFinset.card ≤ G.copyCount H := by
+    rw [← Nat.card_eq_card_finite_toFinset hrf, copyCount]
+    exact Finite.card_range_le f
+  calc #G.edgeFinset - G.copyCount H
+      ≤ #G.edgeFinset - hrf.toFinset.card := Nat.sub_le_sub_left hle _
+    _ ≤ #(G.edgeFinset \ hrf.toFinset) := le_card_sdiff ..
+    _ = #(G.killCopies H).edgeFinset := by
+        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] :
+lemma le_card_edgeFinset_killCopies_add_copyCount [Finite V] :
     #G.edgeFinset ≤ #(G.killCopies H).edgeFinset + G.copyCount H :=
   tsub_le_iff_right.1 le_card_edgeFinset_killCopies