chore(data/prod): rename injective_prod to injective.prod (#2058)

This way we can use dot notation

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

Author: urkud

src/data/prod.lean

@@ -87,6 +87,6 @@ end prod
 
 open function
 
-lemma function.injective_prod {f : α → γ} {g : β → δ} (hf : injective f) (hg : injective g) :
+lemma function.injective.prod {f : α → γ} {g : β → δ} (hf : injective f) (hg : injective g) :
   injective (λ p : α × β, (f p.1, g p.2)) :=
 assume ⟨a₁, b₁⟩ ⟨a₂, b₂⟩, by { simp [prod.mk.inj_iff],exact λ ⟨eq₁, eq₂⟩, ⟨hf eq₁, hg eq₂⟩ }

src/topology/uniform_space/uniform_embedding.lean

@@ -157,7 +157,7 @@ lemma uniform_embedding_subtype_emb (p : α → Prop) {e : α → β} (ue : unif
 lemma uniform_embedding.prod {α' : Type*} {β' : Type*} [uniform_space α'] [uniform_space β']
   {e₁ : α → α'} {e₂ : β → β'} (h₁ : uniform_embedding e₁) (h₂ : uniform_embedding e₂) :
   uniform_embedding (λp:α×β, (e₁ p.1, e₂ p.2)) :=
-{ inj := function.injective_prod h₁.inj h₂.inj,
+{ inj := h₁.inj.prod h₂.inj,
   ..h₁.to_uniform_inducing.prod h₂.to_uniform_inducing }
 
 lemma is_complete_of_complete_image {m : α → β} {s : set α} (hm : uniform_inducing m)