chore(analysis/normed_space/finite_dimension,topology/metric_space): …

…golf (#6285)

* golf two proofs about `finite_dimension`;
* move `proper_image_of_proper` to `antilipschitz`, rename to
  `antilipschitz_with.proper_space`, golf.

src/analysis/normed_space/finite_dimension.lean

@@ -345,12 +345,8 @@ explicitly when needed. -/
 variables (𝕜 E)
 lemma finite_dimensional.complete [finite_dimensional 𝕜 E] : complete_space E :=
 begin
-  rcases exists_is_basis_finite 𝕜 E with ⟨b, b_basis, b_finite⟩,
-  letI : fintype b := finite.fintype b_finite,
-  have : uniform_embedding b_basis.equiv_fun.symm :=
-    linear_equiv.uniform_embedding _ (linear_map.continuous_of_finite_dimensional _)
-    (linear_map.continuous_of_finite_dimensional _),
-  change uniform_embedding b_basis.equiv_fun.symm.to_equiv at this,
+  set e := continuous_linear_equiv.of_findim_eq (@findim_fin_fun 𝕜 _ (findim 𝕜 E)).symm,
+  have : uniform_embedding e.to_linear_equiv.to_equiv.symm := e.symm.uniform_embedding,
   exact (complete_space_congr this).1 (by apply_instance)
 end
 
@@ -403,19 +399,8 @@ properness of `𝕜`, and the search for `𝕜` as an unknown metavariable. Decl
 explicitly when needed. -/
 lemma finite_dimensional.proper [finite_dimensional 𝕜 E] : proper_space E :=
 begin
-  rcases exists_is_basis_finite 𝕜 E with ⟨b, b_basis, b_finite⟩,
-  letI : fintype b := finite.fintype b_finite,
-  let e := b_basis.equiv_fun,
-  let f : E →L[𝕜] (b → 𝕜) :=
-    { cont := linear_map.continuous_of_finite_dimensional _, ..e.to_linear_map },
-  refine metric.proper_image_of_proper e.symm
-    (linear_map.continuous_of_finite_dimensional _) _ (∥f∥)  (λx y, _),
-  { exact equiv.range_eq_univ e.symm.to_equiv },
-  { have A : e (e.symm x) = x := linear_equiv.apply_symm_apply _ _,
-    have B : e (e.symm y) = y := linear_equiv.apply_symm_apply _ _,
-    conv_lhs { rw [← A, ← B] },
-    change dist (f (e.symm x)) (f (e.symm y)) ≤ ∥f∥ * dist (e.symm x) (e.symm y),
-    unfreezingI { exact f.lipschitz.dist_le_mul _ _ } }
+  set e := continuous_linear_equiv.of_findim_eq (@findim_fin_fun 𝕜 _ (findim 𝕜 E)).symm,
+  exact e.symm.antilipschitz.proper_space e.symm.continuous e.symm.surjective
 end
 
 end proper_field

src/topology/metric_space/antilipschitz.lean

@@ -129,6 +129,34 @@ lemma of_subsingleton [subsingleton α] {K : ℝ≥0} : antilipschitz_with K f :
 
 end antilipschitz_with
 
+namespace antilipschitz_with
+
+open metric
+
+variables [metric_space α] [metric_space β] {K : ℝ≥0} {f : α → β}
+
+lemma bounded_preimage (hf : antilipschitz_with K f)
+  {s : set β} (hs : bounded s) :
+  bounded (f ⁻¹' s) :=
+exists.intro (K * diam s) $ λ x y hx hy,
+calc dist x y ≤ K * dist (f x) (f y) : hf.le_mul_dist x y
+... ≤ K * diam s : mul_le_mul_of_nonneg_left (dist_le_diam_of_mem hs hx hy) K.2
+
+/-- The image of a proper space under an expanding onto map is proper. -/
+protected lemma proper_space [proper_space α] (hK : antilipschitz_with K f) (f_cont : continuous f)
+  (hf : function.surjective f) : proper_space β :=
+begin
+  apply proper_space_of_compact_closed_ball_of_le 0 (λx₀ r hr, _),
+  let K := f ⁻¹' (closed_ball x₀ r),
+  have A : is_closed K := is_closed_ball.preimage f_cont,
+  have B : bounded K := hK.bounded_preimage bounded_closed_ball,
+  have : is_compact K := compact_iff_closed_bounded.2 ⟨A, B⟩,
+  convert this.image f_cont,
+  exact (hf.image_preimage _).symm
+end
+
+end antilipschitz_with
+
 lemma lipschitz_with.to_right_inverse [emetric_space α] [emetric_space β] {K : ℝ≥0} {f : α → β}
   (hf : lipschitz_with K f) {g : β → α} (hg : function.right_inverse g f) :
   antilipschitz_with K g :=

src/topology/metric_space/basic.lean

@@ -1574,31 +1574,6 @@ lemma compact_iff_closed_bounded [proper_space α] :
   exact compact_of_is_closed_subset (proper_space.compact_ball x r) hc hr
 end⟩
 
-/-- The image of a proper space under an expanding onto map is proper. -/
-lemma proper_image_of_proper [proper_space α] [metric_space β] (f : α → β)
-  (f_cont : continuous f) (hf : range f = univ) (C : ℝ)
-  (hC : ∀x y, dist x y ≤ C * dist (f x) (f y)) : proper_space β :=
-begin
-  apply proper_space_of_compact_closed_ball_of_le 0 (λx₀ r hr, _),
-  let K := f ⁻¹' (closed_ball x₀ r),
-  have A : is_closed K :=
-    continuous_iff_is_closed.1 f_cont (closed_ball x₀ r) is_closed_ball,
-  have B : bounded K := ⟨max C 0 * (r + r), λx y hx hy, calc
-    dist x y ≤ C * dist (f x) (f y) : hC x y
-    ... ≤ max C 0 * dist (f x) (f y) : mul_le_mul_of_nonneg_right (le_max_left _ _) (dist_nonneg)
-    ... ≤ max C 0 * (dist (f x) x₀ + dist (f y) x₀) :
-      mul_le_mul_of_nonneg_left (dist_triangle_right (f x) (f y) x₀) (le_max_right _ _)
-    ... ≤ max C 0 * (r + r) : begin
-      simp only [mem_closed_ball, mem_preimage] at hx hy,
-      exact mul_le_mul_of_nonneg_left (add_le_add hx hy) (le_max_right _ _)
-    end⟩,
-  have : is_compact K := compact_iff_closed_bounded.2 ⟨A, B⟩,
-  have C : is_compact (f '' K) := this.image f_cont,
-  have : f '' K = closed_ball x₀ r,
-    by { rw image_preimage_eq_of_subset, rw hf, exact subset_univ _ },
-  rwa this at C
-end
-
 end bounded
 
 section diam