From f2fd6db67d1d9c991bfcb1725c3a67d815f2d909 Mon Sep 17 00:00:00 2001
From: mcdoll <moritz.doll@googlemail.com>
Date: Wed, 30 Mar 2022 03:51:14 +0000
Subject: [PATCH] chore(*): removing some `by { dunfold .., apply_instance }`
 proofs (#13050)

Replaces the proofs `by { dunfold .., apply_instance }` by the exact term that is outputted by `show_term`.
---
 src/linear_algebra/dual.lean               | 4 ++--
 src/topology/sheaves/limits.lean           | 4 ++--
 src/topology/uniform_space/completion.lean | 8 ++++----
 src/topology/uniform_space/separation.lean | 7 +++----
 4 files changed, 11 insertions(+), 12 deletions(-)

diff --git a/src/linear_algebra/dual.lean b/src/linear_algebra/dual.lean
index 584ce516a8528..67b33607f4dd1 100644
--- a/src/linear_algebra/dual.lean
+++ b/src/linear_algebra/dual.lean
@@ -48,7 +48,7 @@ variables [comm_semiring R] [add_comm_monoid M] [module R M]
 @[derive [add_comm_monoid, module R]] def dual := M →ₗ[R] R
 
 instance {S : Type*} [comm_ring S] {N : Type*} [add_comm_group N] [module S N] :
-  add_comm_group (dual S N) := by {unfold dual, apply_instance}
+  add_comm_group (dual S N) := linear_map.add_comm_group
 
 instance : add_monoid_hom_class (dual R M) M R :=
 linear_map.add_monoid_hom_class
@@ -61,7 +61,7 @@ def dual_pairing (R M) [comm_semiring R] [add_comm_monoid M] [module R M] :
 
 namespace dual
 
-instance : inhabited (dual R M) := by dunfold dual; apply_instance
+instance : inhabited (dual R M) := linear_map.inhabited
 
 instance : has_coe_to_fun (dual R M) (λ _, M → R) := ⟨linear_map.to_fun⟩
 
diff --git a/src/topology/sheaves/limits.lean b/src/topology/sheaves/limits.lean
index 52412f0608a87..b654ec19f869b 100644
--- a/src/topology/sheaves/limits.lean
+++ b/src/topology/sheaves/limits.lean
@@ -24,10 +24,10 @@ variables {C : Type u} [category.{v} C] {J : Type v} [small_category J]
 namespace Top
 
 instance [has_limits C] (X : Top) : has_limits (presheaf C X) :=
-by { dsimp [presheaf], apply_instance, }
+limits.functor_category_has_limits_of_size
 
 instance [has_colimits C] (X : Top) : has_colimits (presheaf C X) :=
-by { dsimp [presheaf], apply_instance, }
+limits.functor_category_has_colimits_of_size
 
 instance [has_limits C] (X : Top) : creates_limits (sheaf.forget C X) :=
 (@@creates_limits_of_nat_iso _ _
diff --git a/src/topology/uniform_space/completion.lean b/src/topology/uniform_space/completion.lean
index fa6e8eb17e10a..4979d8ce94ef2 100644
--- a/src/topology/uniform_space/completion.lean
+++ b/src/topology/uniform_space/completion.lean
@@ -329,14 +329,14 @@ def completion := quotient (separation_setoid $ Cauchy α)
 namespace completion
 
 instance [inhabited α] : inhabited (completion α) :=
-by unfold completion; apply_instance
+quotient.inhabited (separation_setoid (Cauchy α))
 
 @[priority 50]
-instance : uniform_space (completion α) := by dunfold completion ; apply_instance
+instance : uniform_space (completion α) := separation_setoid.uniform_space
 
-instance : complete_space (completion α) := by dunfold completion ; apply_instance
+instance : complete_space (completion α) := uniform_space.complete_space_separation (Cauchy α)
 
-instance : separated_space (completion α) := by dunfold completion ; apply_instance
+instance : separated_space (completion α) := uniform_space.separated_separation
 
 instance : regular_space (completion α) := separated_regular
 
diff --git a/src/topology/uniform_space/separation.lean b/src/topology/uniform_space/separation.lean
index 9568058cb1947..3f217a1320fd8 100644
--- a/src/topology/uniform_space/separation.lean
+++ b/src/topology/uniform_space/separation.lean
@@ -444,11 +444,10 @@ lemma _root_.is_separated.eq_of_uniform_continuous {f : α → β} {x y : α} {s
 def separation_quotient (α : Type*) [uniform_space α] := quotient (separation_setoid α)
 
 namespace separation_quotient
-instance : uniform_space (separation_quotient α) := by dunfold separation_quotient ; apply_instance
-instance : separated_space (separation_quotient α) :=
-  by dunfold separation_quotient ; apply_instance
+instance : uniform_space (separation_quotient α) := separation_setoid.uniform_space
+instance : separated_space (separation_quotient α) := uniform_space.separated_separation
 instance [inhabited α] : inhabited (separation_quotient α) :=
-by unfold separation_quotient; apply_instance
+quotient.inhabited (separation_setoid α)
 
 /-- Factoring functions to a separated space through the separation quotient. -/
 def lift [separated_space β] (f : α → β) : (separation_quotient α → β) :=