feat(Combinatorics/SimpleGraph): add toUnlabeledCopy / out Quot-style pair

Standard "labeled ↔ unlabeled" toolage for `Copy` / `Embedding` ↔ `UnlabeledCopy` /
`UnlabeledEmbedding`, mirroring the `Quot.mk` / `Quot.out` pattern:

* `Copy.toUnlabeledCopy : Copy G H → G.UnlabeledCopy H` — canonical projection (computable).
* `UnlabeledCopy.out : G.UnlabeledCopy H → Copy G H` — non-canonical representative
  (noncomputable, via `exists_toSubgraph_eq_val.choose`).
* `Copy.toUnlabeledCopy_val` and `UnlabeledCopy.toSubgraph_out` are the matching simp specs.

Mirrored on the Embedding side: `Embedding.toUnlabeledEmbedding` /
`UnlabeledEmbedding.out` with their respective spec lemmas.

Refactor existing inlined anonymous-constructor / `.choose`+`.choose_spec` call sites to
use the new functions:
* `unlabeledCopyCount_le_copyCount` / `unlabeledEmbeddingCount_le_embeddingCount`
* `Copy.equivSigma` / `Embedding.equivSigma` in `Automorphism.lean`
* `Copy.fiberEquivAutOf` / `Embedding.fiberEquivAutOf` in `Automorphism.lean`

Both `Copy.toUnlabeledCopy` and `Embedding.toUnlabeledEmbedding` are marked `@[expose]`
so their `_val` spec lemmas (which are `rfl`) work across modules.

Author: FordUniver

Mathlib/Combinatorics/SimpleGraph/Automorphism.lean

@@ -94,14 +94,13 @@ noncomputable def fiberEquivAut (f₀ : Copy G H) :
 equivalent to `Aut G`. -/
 noncomputable def fiberEquivAutOf (S : G.UnlabeledCopy H) :
     {f : Copy G H // f.toSubgraph = S.val} ≃ G.Aut :=
-  have h := S.exists_toSubgraph_eq_val
-  h.choose_spec ▸ fiberEquivAut h.choose
+  S.toSubgraph_out ▸ fiberEquivAut S.out
 
 /-- `Copy G H` decomposes as the dependent sum over unlabelled copies of `G` in `H`, with each
 fiber the set of labelled copies sharing that image subgraph. -/
 noncomputable def equivSigma :
     Copy G H ≃ Σ S : G.UnlabeledCopy H, {f : Copy G H // f.toSubgraph = S.val} where
-  toFun f := ⟨⟨f.toSubgraph, ⟨f.isoToSubgraph⟩⟩, ⟨f, rfl⟩⟩
+  toFun f := ⟨f.toUnlabeledCopy, ⟨f, rfl⟩⟩
   invFun := fun ⟨_, f⟩ ↦ f.1
   left_inv _ := rfl
   right_inv := fun ⟨⟨S, hS⟩, ⟨f, hf⟩⟩ => by
@@ -151,14 +150,13 @@ noncomputable def fiberEquivAut (f₀ : Embedding G H) :
 `S.val` is equivalent to `Aut G`. -/
 noncomputable def fiberEquivAutOf (S : G.UnlabeledEmbedding H) :
     {f : Embedding G H // f.toSubgraph = S.val} ≃ G.Aut :=
-  have h := S.exists_toSubgraph_eq_val
-  h.choose_spec ▸ fiberEquivAut h.choose
+  S.toSubgraph_out ▸ fiberEquivAut S.out
 
 /-- `Embedding G H` decomposes as the dependent sum over unlabelled induced copies of `G` in `H`,
 with each fiber the set of labelled induced copies sharing that image subgraph. -/
 noncomputable def equivSigma :
     Embedding G H ≃ Σ S : G.UnlabeledEmbedding H, {f : Embedding G H // f.toSubgraph = S.val} where
-  toFun f := ⟨⟨f.toSubgraph, f.toSubgraph_isInduced, ⟨f.toCopy.isoToSubgraph⟩⟩, ⟨f, rfl⟩⟩
+  toFun f := ⟨f.toUnlabeledEmbedding, ⟨f, rfl⟩⟩
   invFun := fun ⟨_, f⟩ ↦ f.1
   left_inv _ := rfl
   right_inv := fun ⟨⟨S, hS⟩, ⟨f, hf⟩⟩ => by

Mathlib/Combinatorics/SimpleGraph/Copy.lean

@@ -493,10 +493,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) : ℕ :=
@@ -517,12 +530,8 @@ lemma unlabeledCopyCount_eq_nat_card (H : SimpleGraph W) (G : SimpleGraph V) :
 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

@@ -324,10 +324,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. -/
@@ -352,13 +367,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