docs(Combinatorics/SimpleGraph/Automorphism): drop over-documented small lemmas

Remove docstrings on `Copy.toSubgraph_comp_iso`, `Copy.comp_toCopy_injective`, and
their Embedding mirrors. The names (`toSubgraph_comp_iso`,
`comp_toCopy_injective` / `comp_toEmbedding_injective`) and signatures are
self-evident; the docstrings just restated them in prose.

Other docstrings (`Aut`, `autCount`, the `fiber*` defs, the `equiv*` packagings,
and the two `**Orbit-stabiliser**`-tagged main theorems) all add content over
their names and stay.

Author: FordUniver

Mathlib/Combinatorics/SimpleGraph/Automorphism.lean

@@ -63,11 +63,9 @@ lemma one_le_autCount [Finite V] : 1 ≤ G.autCount := autCount_pos
 
 namespace Copy
 
-/-- Precomposing a copy by an automorphism of the guest does not change the image subgraph. -/
 lemma toSubgraph_comp_iso (f : Copy G H) (σ : G.Aut) :
     (f.comp σ.toCopy).toSubgraph = f.toSubgraph := by simp
 
-/-- Precomposition with automorphisms of the guest is injective on copies. -/
 lemma comp_toCopy_injective (f : Copy G H) :
     Injective fun σ : G.Aut ↦ f.comp σ.toCopy := fun σ₁ σ₂ h ↦ by
   ext v; simpa using DFunLike.congr_fun h v
@@ -118,11 +116,9 @@ end Copy
 
 namespace Embedding
 
-/-- Precomposing an embedding by an automorphism of the guest does not change the image subgraph. -/
 lemma toSubgraph_comp_iso (f : Embedding G H) (σ : G.Aut) :
     (f.comp σ.toEmbedding).toSubgraph = f.toSubgraph := by simp
 
-/-- Precomposition with automorphisms of the guest is injective on embeddings. -/
 lemma comp_toEmbedding_injective (f : Embedding G H) :
     Injective fun σ : G.Aut ↦ f.comp σ.toEmbedding := fun σ₁ σ₂ h ↦ by
   ext v; simpa using DFunLike.congr_fun h v