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

@@ -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⟩
 

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 _ _

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
 

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 α → β) :=