chore(logic/function): drop function.uncurry' (#2678)

See [lean#161](https://github.com/leanprover-community/lean/pull/161/files#diff-42c23da308a4d5900f9f3244953701daR132)
Also add `uniform_continuous.prod_map` and `uniform_continuous₂.bicompl`

src/logic/function/basic.lean

@@ -264,18 +264,7 @@ end
 end update
 
 lemma uncurry_def {α β γ} (f : α → β → γ) : uncurry f = (λp, f p.1 p.2) :=
-funext $ assume ⟨a, b⟩, rfl
-
--- `uncurry'` is the version of `uncurry` with correct definitional reductions
-def uncurry' {α β γ} (f : α → β → γ) := λ p : α × β, f p.1 p.2
-
-@[simp]
-lemma curry_uncurry' {α : Type*} {β : Type*} {γ : Type*} (f : α → β → γ) : curry (uncurry' f) = f :=
-by funext ; refl
-
-@[simp]
-lemma uncurry'_curry {α : Type*} {β : Type*} {γ : Type*} (f : α × β → γ) : uncurry' (curry f) = f :=
-by { funext, simp [curry, uncurry', prod.mk.eta] }
+rfl
 
 section bicomp
 variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*} {ε : Type*}
@@ -293,11 +282,12 @@ f (g a b)
 local notation f `∘₂` g := bicompr f g
 
 lemma uncurry_bicompr (f : α → β → γ) (g : γ → δ) :
-  uncurry (g ∘₂ f) = (g ∘ uncurry f) :=
-funext $ λ ⟨p, q⟩, rfl
+  uncurry (g ∘₂ f) = (g ∘ uncurry f) := rfl
+
+lemma uncurry_bicompl (f : γ → δ → ε) (g : α → γ) (h : β → δ) :
+  uncurry (bicompl f g h) = (uncurry f) ∘ (prod.map g h) :=
+rfl
 
-lemma uncurry'_bicompr (f : α → β → γ) (g : γ → δ) :
-  uncurry' (g ∘₂ f) = (g ∘ uncurry' f) := rfl
 end bicomp
 
 /-- A function is involutive, if `f ∘ f = id`. -/

src/order/filter/extr.lean

@@ -62,7 +62,7 @@ Similar predicates with `_on` suffix are particular cases for `l = principal s`.
 
 * Multiplication and division;
 * `is_*_*.bicompl` : if `x` is a minimum for `f`, `y` is a minimum for `g`, and `op` is a monotone
-  binary operation, then `(x, y)` is a minimum for `uncurry' (bicompl op f g)`. From this point of view,
+  binary operation, then `(x, y)` is a minimum for `uncurry (bicompl op f g)`. From this point of view,
   `is_*_*.bicomp` is a composition
 * It would be nice to have a tactic that specializes `comp_(anti)mono` or `bicomp_mono`
   based on a proof of monotonicity of a given (binary) function. The tactic should maintain a `meta`

src/topology/algebra/group_completion.lean

@@ -56,8 +56,7 @@ instance : add_group (completion α) :=
   .. completion.has_zero, .. completion.has_neg, ..completion.has_add }
 
 instance : uniform_add_group (completion α) :=
-⟨((uniform_continuous_map₂ (+)).comp
-  (uniform_continuous_fst.prod_mk (uniform_continuous_map.comp uniform_continuous_snd)) : _)⟩
+⟨(uniform_continuous_map₂ (+)).bicompl uniform_continuous_id uniform_continuous_map⟩
 
 instance is_add_group_hom_coe : is_add_group_hom (coe : α → completion α) :=
 { map_add := coe_add }

src/topology/algebra/uniform_ring.lean

@@ -19,7 +19,7 @@ variables (α : Type*) [ring α] [uniform_space α]
 instance : has_one (completion α) := ⟨(1:α)⟩
 
 instance : has_mul (completion α) :=
-  ⟨curry $ (dense_inducing_coe.prod dense_inducing_coe).extend (coe ∘ uncurry' (*))⟩
+  ⟨curry $ (dense_inducing_coe.prod dense_inducing_coe).extend (coe ∘ uncurry (*))⟩
 
 @[norm_cast] lemma coe_one : ((1 : α) : completion α) = 1 := rfl
 
@@ -34,7 +34,7 @@ variables [uniform_add_group α]
 
 lemma continuous_mul : continuous (λ p : completion α × completion α, p.1 * p.2) :=
 begin
-  haveI : is_Z_bilin ((coe ∘ uncurry' (*)) : α × α → completion α) :=
+  haveI : is_Z_bilin ((coe ∘ uncurry (*)) : α × α → completion α) :=
   { add_left := begin
       introv,
       change coe ((a + a')*b) = coe (a*b) + coe (a'*b),
@@ -45,7 +45,7 @@ begin
       change coe (a*(b + b')) = coe (a*b) + coe (a*b'),
       rw_mod_cast mul_add
     end },
-  have : continuous ((coe ∘ uncurry' (*)) : α × α → completion α),
+  have : continuous ((coe ∘ uncurry (*)) : α × α → completion α),
     from (continuous_coe α).comp continuous_mul,
   convert dense_inducing_coe.extend_Z_bilin dense_inducing_coe this,
   simp only [(*), curry, prod.mk.eta]

src/topology/metric_space/closeds.lean

@@ -405,7 +405,7 @@ by { rw dist_comm,
 
 lemma lipschitz_inf_dist :
   lipschitz_with 2 (λ p : α × (nonempty_compacts α), inf_dist p.1 p.2.val) :=
-@lipschitz_with.uncurry' _ _ _ _ _ _ (λ (x : α) (s : nonempty_compacts α), inf_dist x s.val) 1 1
+@lipschitz_with.uncurry _ _ _ _ _ _ (λ (x : α) (s : nonempty_compacts α), inf_dist x s.val) 1 1
   (λ s, lipschitz_inf_dist_pt s.val) lipschitz_inf_dist_set
 
 lemma uniform_continuous_inf_dist_Hausdorff_dist :

src/topology/metric_space/lipschitz.lean

@@ -137,22 +137,17 @@ begin
   exact max_le_max (hf x y) (hg x y)
 end
 
-protected lemma uncurry' {f : α → β → γ} {Kα Kβ : ℝ≥0} (hα : ∀ b, lipschitz_with Kα (λ a, f a b))
+protected lemma uncurry {f : α → β → γ} {Kα Kβ : ℝ≥0} (hα : ∀ b, lipschitz_with Kα (λ a, f a b))
   (hβ : ∀ a, lipschitz_with Kβ (f a)) :
-  lipschitz_with (Kα + Kβ) (function.uncurry' f) :=
+  lipschitz_with (Kα + Kβ) (function.uncurry f) :=
 begin
   rintros ⟨a₁, b₁⟩ ⟨a₂, b₂⟩,
-  simp only [function.uncurry', ennreal.coe_add, add_mul],
+  simp only [function.uncurry, ennreal.coe_add, add_mul],
   apply le_trans (edist_triangle _ (f a₂ b₁) _),
   exact add_le_add' (le_trans (hα _ _ _) $ ennreal.mul_left_mono $ le_max_left _ _)
     (le_trans (hβ _ _ _) $ ennreal.mul_left_mono $ le_max_right _ _)
 end
 
-protected lemma uncurry {f : α → β → γ} {Kα Kβ : ℝ≥0} (hα : ∀ b, lipschitz_with Kα (λ a, f a b))
-  (hβ : ∀ a, lipschitz_with Kβ (f a)) :
-  lipschitz_with (Kα + Kβ) (function.uncurry f) :=
-by { rw function.uncurry_def, apply lipschitz_with.uncurry'; assumption }
-
 protected lemma iterate {f : α → α} (hf : lipschitz_with K f) :
   ∀n, lipschitz_with (K ^ n) (f^[n])
 | 0       := lipschitz_with.id
@@ -246,8 +241,8 @@ lipschitz_with.of_le_add $ assume x z, by { rw [add_comm], apply dist_triangle }
 protected lemma dist_right (x : α) : lipschitz_with 1 (dist x) :=
 lipschitz_with.of_le_add $ assume y z, dist_triangle_right _ _ _
 
-protected lemma dist : lipschitz_with 2 (function.uncurry' $ @dist α _) :=
-lipschitz_with.uncurry' lipschitz_with.dist_left lipschitz_with.dist_right
+protected lemma dist : lipschitz_with 2 (function.uncurry $ @dist α _) :=
+lipschitz_with.uncurry lipschitz_with.dist_left lipschitz_with.dist_right
 
 lemma dist_iterate_succ_le_geometric {f : α → α} (hf : lipschitz_with K f) (x n) :
   dist (f^[n] x) (f^[n + 1] x) ≤ dist x (f x) * K ^ n :=

src/topology/uniform_space/abstract_completion.lean

@@ -261,20 +261,20 @@ open function
 
 /-- Extend two variable map to completions. -/
 protected def extend₂ (f : α → β → γ) : hatα → hatβ → γ :=
-curry $ (pkg.prod pkg').extend (uncurry' f)
+curry $ (pkg.prod pkg').extend (uncurry f)
 
 variables [separated γ] {f : α → β → γ}
 
-lemma extension₂_coe_coe (hf : uniform_continuous $ uncurry' f) (a : α) (b : β) :
+lemma extension₂_coe_coe (hf : uniform_continuous $ uncurry f) (a : α) (b : β) :
   pkg.extend₂ pkg' f (ι a) (ι' b) = f a b :=
-show (pkg.prod pkg').extend (uncurry' f) ((pkg.prod pkg').coe (a, b)) = uncurry' f (a, b),
+show (pkg.prod pkg').extend (uncurry f) ((pkg.prod pkg').coe (a, b)) = uncurry f (a, b),
   from (pkg.prod pkg').extend_coe hf _
 
 variables [complete_space γ] (f)
 
 lemma uniform_continuous_extension₂ : uniform_continuous₂ (pkg.extend₂ pkg' f) :=
 begin
-  rw [uniform_continuous₂_def, abstract_completion.extend₂, uncurry'_curry],
+  rw [uniform_continuous₂_def, abstract_completion.extend₂, uncurry_curry],
   apply uniform_continuous_extend
 end
 
@@ -295,7 +295,7 @@ local notation f `∘₂` g := bicompr f g
 protected def map₂ (f : α → β → γ) : hatα → hatβ → hatγ :=
 pkg.extend₂ pkg' (pkg''.coe ∘₂ f)
 
-lemma uniform_continuous_map₂ (f : α → β → γ) : uniform_continuous (uncurry' $ pkg.map₂ pkg' pkg'' f) :=
+lemma uniform_continuous_map₂ (f : α → β → γ) : uniform_continuous₂ (pkg.map₂ pkg' pkg'' f) :=
 pkg.uniform_continuous_extension₂ pkg' _
 
 lemma continuous_map₂ {δ} [topological_space δ] {f : α → β → γ}

src/topology/uniform_space/basic.lean

@@ -770,6 +770,11 @@ lemma uniform_continuous.prod_mk_right {f : α × β → γ} (h : uniform_contin
   uniform_continuous (λ b, f (a,b)) :=
 h.comp (uniform_continuous_const.prod_mk  uniform_continuous_id)
 
+lemma uniform_continuous.prod_map [uniform_space δ] {f : α → γ} {g : β → δ}
+  (hf : uniform_continuous f) (hg : uniform_continuous g) :
+  uniform_continuous (prod.map f g) :=
+(hf.comp uniform_continuous_fst).prod_mk (hg.comp uniform_continuous_snd)
+
 lemma to_topological_space_prod {α} {β} [u : uniform_space α] [v : uniform_space β] :
   @uniform_space.to_topological_space (α × β) prod.uniform_space =
     @prod.topological_space α β u.to_topological_space v.to_topological_space := rfl
@@ -778,22 +783,33 @@ end prod
 
 section
 open uniform_space function
-variables [uniform_space α] [uniform_space β] [uniform_space γ] [uniform_space δ]
+variables {δ' : Type*} [uniform_space α] [uniform_space β] [uniform_space γ] [uniform_space δ]
+  [uniform_space δ']
 
 local notation f `∘₂` g := function.bicompr f g
 
-def uniform_continuous₂ (f : α → β → γ) := uniform_continuous (uncurry' f)
+def uniform_continuous₂ (f : α → β → γ) := uniform_continuous (uncurry f)
+
+lemma uniform_continuous₂_def (f : α → β → γ) :
+  uniform_continuous₂ f ↔ uniform_continuous (uncurry f) := iff.rfl
 
-lemma uniform_continuous₂_def (f : α → β → γ) : uniform_continuous₂ f ↔ uniform_continuous (uncurry' f) := iff.rfl
+lemma uniform_continuous₂.uniform_continuous {f : α → β → γ} (h : uniform_continuous₂ f) :
+  uniform_continuous (uncurry f) := h
 
-lemma uniform_continuous₂_curry (f : α × β → γ) : uniform_continuous₂ (function.curry f) ↔ uniform_continuous f :=
-by rw  [←uncurry'_curry f] {occs := occurrences.pos [2]} ; refl
+lemma uniform_continuous₂_curry (f : α × β → γ) :
+  uniform_continuous₂ (function.curry f) ↔ uniform_continuous f :=
+by rw [uniform_continuous₂, uncurry_curry]
 
 lemma uniform_continuous₂.comp {f : α → β → γ} {g : γ → δ}
   (hg : uniform_continuous g) (hf : uniform_continuous₂ f) :
   uniform_continuous₂ (g ∘₂ f) :=
 hg.comp hf
 
+lemma uniform_continuous₂.bicompl {f : α → β → γ} {ga : δ → α} {gb : δ' → β}
+  (hf : uniform_continuous₂ f) (hga : uniform_continuous ga) (hgb : uniform_continuous gb) :
+  uniform_continuous₂ (bicompl f ga gb) :=
+hf.uniform_continuous.comp (hga.prod_map hgb)
+
 end
 
 lemma to_topological_space_subtype [u : uniform_space α] {p : α → Prop} :

src/topology/uniform_space/completion.lean

@@ -545,7 +545,7 @@ cpkg.extend₂ cpkg f
 
 variables [separated γ] {f}
 
-@[simp] lemma extension₂_coe_coe (hf : uniform_continuous $ uncurry' f) (a : α) (b : β) :
+@[simp] lemma extension₂_coe_coe (hf : uniform_continuous₂ f) (a : α) (b : β) :
   completion.extension₂ f a b = f a b :=
 cpkg.extension₂_coe_coe cpkg hf a b
 
@@ -562,15 +562,15 @@ open function
 protected def map₂ (f : α → β → γ) : completion α → completion β → completion γ :=
 cpkg.map₂ cpkg cpkg f
 
-lemma uniform_continuous_map₂ (f : α → β → γ) : uniform_continuous (uncurry' $ completion.map₂ f) :=
+lemma uniform_continuous_map₂ (f : α → β → γ) : uniform_continuous₂ (completion.map₂ f) :=
 cpkg.uniform_continuous_map₂ cpkg cpkg f
 
 lemma continuous_map₂ {δ} [topological_space δ] {f : α → β → γ}
   {a : δ → completion α} {b : δ → completion β} (ha : continuous a) (hb : continuous b) :
   continuous (λd:δ, completion.map₂ f (a d) (b d)) :=
 cpkg.continuous_map₂ cpkg cpkg ha hb
 
-lemma map₂_coe_coe (a : α) (b : β) (f : α → β → γ) (hf : uniform_continuous $ uncurry' f) :
+lemma map₂_coe_coe (a : α) (b : β) (f : α → β → γ) (hf : uniform_continuous₂ f) :
   completion.map₂ f (a : completion α) (b : completion β) = f a b :=
 cpkg.map₂_coe_coe cpkg cpkg a b f hf