refactor(combinatorics/simple_graph/basic): rename induced embedding …

…on complete graphs (#14404)

src/combinatorics/simple_graph/basic.lean

@@ -1040,7 +1040,8 @@ map_adj_iff f
   end }
 
 /-- Embeddings of types induce embeddings of complete graphs on those types. -/
-def complete_graph.of_embedding {α β : Type*} (f : α ↪ β) : complete_graph α ↪g complete_graph β :=
+protected def complete_graph {α β : Type*} (f : α ↪ β) :
+  (⊤ : simple_graph α) ↪g (⊤ : simple_graph β) :=
 { to_fun := f,
   inj' := f.inj',
   map_rel_iff' := by simp }

src/combinatorics/simple_graph/coloring.lean

@@ -157,13 +157,13 @@ Inf { n : ℕ | G.colorable n }
 
 /-- Given an embedding, there is an induced embedding of colorings. -/
 def recolor_of_embedding {α β : Type*} (f : α ↪ β) : G.coloring α ↪ G.coloring β :=
-{ to_fun := λ C, (embedding.complete_graph.of_embedding f).to_hom.comp C,
+{ to_fun := λ C, (embedding.complete_graph f).to_hom.comp C,
   inj' := begin -- this was strangely painful; seems like missing lemmas about embeddings
     intros C C' h,
     dsimp only at h,
     ext v,
-    apply (embedding.complete_graph.of_embedding f).inj',
-    change ((embedding.complete_graph.of_embedding f).to_hom.comp C) v = _,
+    apply (embedding.complete_graph f).inj',
+    change ((embedding.complete_graph f).to_hom.comp C) v = _,
     rw h,
     refl,
   end }
@@ -214,7 +214,7 @@ begin
   split,
   { rintro hc,
     have C : G.coloring (fin n) := hc.to_coloring (by simp),
-    let f := embedding.complete_graph.of_embedding (fin.coe_embedding n).to_embedding,
+    let f := embedding.complete_graph (fin.coe_embedding n).to_embedding,
     use f.to_hom.comp C,
     intro v,
     cases C with color valid,
@@ -383,7 +383,7 @@ begin
   convert_to (⊤ : simple_graph {m | m < n + 1}).chromatic_number ≤ _,
   { simp, },
   refine (colorable_of_chromatic_number_pos hc).chromatic_number_mono_of_embedding _,
-  apply embedding.complete_graph.of_embedding,
+  apply embedding.complete_graph,
   exact (function.embedding.subtype _).trans (infinite.nat_embedding V),
 end