feat(Combinatorics/SimpleGraph): Copy.toUnlabeledCopy / UnlabeledCopy.out (and embedding mirror)

Add the standard `Quot.mk` / `Quot.out` style toolage for converting between labeled
and unlabeled copies / embeddings:

* `Copy.toUnlabeledCopy : Copy G H → G.UnlabeledCopy H` — canonical projection
  (computable).
* `UnlabeledCopy.out : G.UnlabeledCopy H → Copy G H` — non-canonical representative
  (noncomputable).
* `Copy.toUnlabeledCopy_val` and `UnlabeledCopy.toSubgraph_out` give the matching simp
  specs.
* `UnlabeledCopy.exists_toSubgraph_eq_val` packages the underlying existence statement.

Mirrored on the Embedding side: `Embedding.toUnlabeledEmbedding`,
`UnlabeledEmbedding.exists_toSubgraph_eq_val`, `UnlabeledEmbedding.out`, and their
respective spec lemmas.

Refactor the existing `unlabeledCopyCount_le_copyCount` and
`unlabeledEmbeddingCount_le_embeddingCount` proofs to use the new names — both shrink
from a 5- and 7-line `apply ... ; rintro ...; obtain ...; exact ...` chain to a
two-line `exact Nat.card_le_card_of_surjective ... fun S ↦ ⟨S.out, ...⟩`.

Author: FordUniver

Mathlib/Combinatorics/SimpleGraph/Copy.lean

@@ -461,6 +461,23 @@ abbrev UnlabeledCopy (G : SimpleGraph V) (H : SimpleGraph W) : Type _ :=
 
 instance [Finite W] : Finite (G.UnlabeledCopy H) := Subtype.finite
 
+/-- The canonical map from a labeled copy to its unlabeled image. -/
+@[expose] def Copy.toUnlabeledCopy (f : Copy G H) : G.UnlabeledCopy H :=
+  ⟨f.toSubgraph, ⟨f.isoToSubgraph⟩⟩
+
+@[simp] lemma Copy.toUnlabeledCopy_val (f : Copy G H) : f.toUnlabeledCopy.val = f.toSubgraph := rfl
+
+lemma UnlabeledCopy.exists_toSubgraph_eq_val (S : G.UnlabeledCopy H) :
+    ∃ f : Copy G H, f.toSubgraph = S.val :=
+  Set.mem_range.mp (Copy.range_toSubgraph ▸ S.property)
+
+/-- A noncomputable representative labeled copy of an unlabeled copy. -/
+noncomputable def UnlabeledCopy.out (S : G.UnlabeledCopy H) : Copy G H :=
+  S.exists_toSubgraph_eq_val.choose
+
+@[simp] lemma UnlabeledCopy.toSubgraph_out (S : G.UnlabeledCopy H) : S.out.toSubgraph = S.val :=
+  S.exists_toSubgraph_eq_val.choose_spec
+
 /-- `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) : ℕ :=
@@ -492,12 +509,8 @@ lemma copyCount_eq_card_image_copyToSubgraph [Fintype {f : G →g H // Injective
 lemma unlabeledCopyCount_le_copyCount [Finite V] [Finite W] :
     H.unlabeledCopyCount G ≤ H.copyCount G := by
   rw [unlabeledCopyCount, copyCount]
-  apply Nat.card_le_card_of_surjective
-    (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⟩
+  exact Nat.card_le_card_of_surjective Copy.toUnlabeledCopy
+    fun S ↦ ⟨S.out, Subtype.ext S.toSubgraph_out⟩
 
 instance uniqueUnlabeledCopyBot [Finite W] (H : SimpleGraph W) :
     Unique ((⊥ : SimpleGraph W).UnlabeledCopy H) where

Mathlib/Combinatorics/SimpleGraph/InducedCopy.lean

@@ -280,6 +280,25 @@ abbrev UnlabeledEmbedding (G : SimpleGraph V) (H : SimpleGraph W) : Type _ :=
 
 instance [Finite W] : Finite (G.UnlabeledEmbedding H) := Subtype.finite
 
+/-- The canonical map from a labeled embedding to its unlabeled induced image. -/
+@[expose] def Embedding.toUnlabeledEmbedding (f : Embedding G H) : G.UnlabeledEmbedding H :=
+  ⟨f.toSubgraph, f.toSubgraph_isInduced, ⟨f.toCopy.isoToSubgraph⟩⟩
+
+@[simp] lemma Embedding.toUnlabeledEmbedding_val (f : Embedding G H) :
+    f.toUnlabeledEmbedding.val = f.toSubgraph := rfl
+
+lemma UnlabeledEmbedding.exists_toSubgraph_eq_val (S : G.UnlabeledEmbedding H) :
+    ∃ f : Embedding G H, f.toSubgraph = S.val :=
+  Set.mem_range.mp (Embedding.range_toSubgraph ▸ S.property)
+
+/-- A noncomputable representative labeled embedding of an unlabeled induced copy. -/
+noncomputable def UnlabeledEmbedding.out (S : G.UnlabeledEmbedding H) : Embedding G H :=
+  S.exists_toSubgraph_eq_val.choose
+
+@[simp] lemma UnlabeledEmbedding.toSubgraph_out (S : G.UnlabeledEmbedding H) :
+    S.out.toSubgraph = S.val :=
+  S.exists_toSubgraph_eq_val.choose_spec
+
 /-- `H.unlabeledEmbeddingCount G` is the number of induced `SimpleGraph.Subgraph`s of `H`
 isomorphic to `G`.
 See `SimpleGraph.embeddingCount` for the number of induced labeled copies. -/
@@ -304,13 +323,8 @@ unlabeled ones. -/
 lemma unlabeledEmbeddingCount_le_embeddingCount [Finite V] [Finite W] :
     H.unlabeledEmbeddingCount G ≤ H.embeddingCount G := by
   rw [unlabeledEmbeddingCount, embeddingCount]
-  apply Nat.card_le_card_of_surjective
-    (fun f : Embedding G H ↦ (⟨Embedding.toSubgraph f, f.toSubgraph_isInduced,
-      ⟨f.toCopy.isoToSubgraph⟩⟩ : G.UnlabeledEmbedding H))
-  rintro ⟨H', hInd, ⟨e⟩⟩
-  obtain ⟨f, hf⟩ : ∃ f : Embedding G H, Embedding.toSubgraph f = H' := by
-    rw [← Set.mem_range, Embedding.range_toSubgraph]; exact ⟨hInd, ⟨e⟩⟩
-  exact ⟨f, Subtype.ext hf⟩
+  exact Nat.card_le_card_of_surjective Embedding.toUnlabeledEmbedding
+    fun S ↦ ⟨S.out, Subtype.ext S.toSubgraph_out⟩
 
 private instance [IsEmpty V] : Nonempty (G.UnlabeledEmbedding H) :=
   let ⟨H', hInd, ⟨e⟩⟩ := (IsIndContained.of_isEmpty (G := G) (H := H)).exists_iso_subgraph