diff --git a/src/algebra/category/CommRing/basic.lean b/src/algebra/category/CommRing/basic.lean
index afc7e1f4e3a2b..88658cb125735 100644
--- a/src/algebra/category/CommRing/basic.lean
+++ b/src/algebra/category/CommRing/basic.lean
@@ -15,11 +15,6 @@ We introduce the bundled categories:
 * `CommSemiRing`
 * `CommRing`
 along with the relevant forgetful functors between them.
-
-## Implementation notes
-
-See the note [locally reducible category instances].
-
 -/
 
 universes u v
@@ -31,23 +26,18 @@ def SemiRing : Type (u+1) := bundled semiring
 
 namespace SemiRing
 
+instance bundled_hom : bundled_hom @ring_hom :=
+⟨@ring_hom.to_fun, @ring_hom.id, @ring_hom.comp, @ring_hom.coe_inj⟩
+
+attribute [derive [has_coe_to_sort, large_category, concrete_category]] SemiRing
+
 /-- Construct a bundled SemiRing from the underlying type and typeclass. -/
 def of (R : Type u) [semiring R] : SemiRing := bundled.of R
 
 instance : inhabited SemiRing := ⟨of punit⟩
 
-local attribute [reducible] SemiRing
-
-instance : has_coe_to_sort SemiRing := infer_instance -- short-circuit type class inference
-
 instance (R : SemiRing) : semiring R := R.str
 
-instance bundled_hom : bundled_hom @ring_hom :=
-⟨@ring_hom.to_fun, @ring_hom.id, @ring_hom.comp, @ring_hom.coe_inj⟩
-
-instance : category SemiRing := infer_instance -- short-circuit type class inference
-instance : concrete_category SemiRing := infer_instance -- short-circuit type class inference
-
 instance has_forget_to_Mon : has_forget₂ SemiRing Mon :=
 bundled_hom.mk_has_forget₂
   (λ R hR, @monoid_with_zero.to_monoid R (@semiring.to_monoid_with_zero R hR))
@@ -68,20 +58,15 @@ namespace Ring
 
 instance : bundled_hom.parent_projection @ring.to_semiring := ⟨⟩
 
+attribute [derive [has_coe_to_sort, large_category, concrete_category]] Ring
+
 /-- Construct a bundled Ring from the underlying type and typeclass. -/
 def of (R : Type u) [ring R] : Ring := bundled.of R
 
 instance : inhabited Ring := ⟨of punit⟩
 
-local attribute [reducible] Ring
-
-instance : has_coe_to_sort Ring := by apply_instance -- short-circuit type class inference
-
 instance (R : Ring) : ring R := R.str
 
-instance : category Ring := infer_instance -- short-circuit type class inference
-instance : concrete_category Ring := infer_instance -- short-circuit type class inference
-
 instance has_forget_to_SemiRing : has_forget₂ Ring SemiRing := bundled_hom.forget₂ _ _
 instance has_forget_to_AddCommGroup : has_forget₂ Ring AddCommGroup :=
 -- can't use bundled_hom.mk_has_forget₂, since AddCommGroup is an induced category
@@ -98,20 +83,15 @@ namespace CommSemiRing
 
 instance : bundled_hom.parent_projection @comm_semiring.to_semiring := ⟨⟩
 
+attribute [derive [has_coe_to_sort, large_category, concrete_category]] CommSemiRing
+
 /-- Construct a bundled CommSemiRing from the underlying type and typeclass. -/
 def of (R : Type u) [comm_semiring R] : CommSemiRing := bundled.of R
 
 instance : inhabited CommSemiRing := ⟨of punit⟩
 
-local attribute [reducible] CommSemiRing
-
-instance : has_coe_to_sort CommSemiRing := infer_instance -- short-circuit type class inference
-
 instance (R : CommSemiRing) : comm_semiring R := R.str
 
-instance : category CommSemiRing := infer_instance -- short-circuit type class inference
-instance : concrete_category CommSemiRing := infer_instance -- short-circuit type class inference
-
 instance has_forget_to_SemiRing : has_forget₂ CommSemiRing SemiRing := bundled_hom.forget₂ _ _
 
 /-- The forgetful functor from commutative rings to (multiplicative) commutative monoids. -/
@@ -129,20 +109,15 @@ namespace CommRing
 
 instance : bundled_hom.parent_projection @comm_ring.to_ring := ⟨⟩
 
+attribute [derive [has_coe_to_sort, large_category, concrete_category]] CommRing
+
 /-- Construct a bundled CommRing from the underlying type and typeclass. -/
 def of (R : Type u) [comm_ring R] : CommRing := bundled.of R
 
 instance : inhabited CommRing := ⟨of punit⟩
 
-local attribute [reducible] CommRing
-
-instance : has_coe_to_sort CommRing := infer_instance -- short-circuit type class inference
-
 instance (R : CommRing) : comm_ring R := R.str
 
-instance : category CommRing := infer_instance -- short-circuit type class inference
-instance : concrete_category CommRing := infer_instance -- short-circuit type class inference
-
 instance has_forget_to_Ring : has_forget₂ CommRing Ring := bundled_hom.forget₂ _ _
 
 /-- The forgetful functor from commutative rings to (multiplicative) commutative monoids. -/
diff --git a/src/algebra/category/Group/basic.lean b/src/algebra/category/Group/basic.lean
index 6c94b3e99b4e0..a62959c2448e5 100644
--- a/src/algebra/category/Group/basic.lean
+++ b/src/algebra/category/Group/basic.lean
@@ -15,10 +15,6 @@ We introduce the bundled categories:
 * `CommGroup`
 * `AddCommGroup`
 along with the relevant forgetful functors between them, and to the bundled monoid categories.
-
-## Implementation notes
-
-See the note [locally reducible category instances].
 -/
 
 universes u v
@@ -37,17 +33,14 @@ namespace Group
 @[to_additive]
 instance : bundled_hom.parent_projection group.to_monoid := ⟨⟩
 
+attribute [derive [has_coe_to_sort, large_category, concrete_category]] Group AddGroup
+
 /-- Construct a bundled `Group` from the underlying type and typeclass. -/
 @[to_additive] def of (X : Type u) [group X] : Group := bundled.of X
 
 /-- Construct a bundled `AddGroup` from the underlying type and typeclass. -/
 add_decl_doc AddGroup.of
 
-local attribute [reducible] Group
-
-@[to_additive]
-instance : has_coe_to_sort Group := infer_instance -- short-circuit type class inference
-
 @[to_additive add_group]
 instance (G : Group) : group G := G.str
 
@@ -65,13 +58,7 @@ instance : unique (1 : Group) :=
 @[simp, to_additive]
 lemma one_apply (G H : Group) (g : G) : (1 : G ⟶ H) g = 1 := rfl
 
-@[to_additive]
-instance : category Group := infer_instance -- short-circuit type class inference
-
-@[to_additive]
-instance : concrete_category Group := infer_instance -- short-circuit type class inference
-
-@[to_additive,ext]
+@[to_additive, ext]
 lemma ext (G H : Group) (f₁ f₂ : G ⟶ H) (w : ∀ x, f₁ x = f₂ x) : f₁ = f₂ :=
 by { ext1, apply w }
 
@@ -97,17 +84,14 @@ namespace CommGroup
 @[to_additive]
 instance : bundled_hom.parent_projection comm_group.to_group := ⟨⟩
 
+attribute [derive [has_coe_to_sort, large_category, concrete_category]] CommGroup AddCommGroup
+
 /-- Construct a bundled `CommGroup` from the underlying type and typeclass. -/
 @[to_additive] def of (G : Type u) [comm_group G] : CommGroup := bundled.of G
 
 /-- Construct a bundled `AddCommGroup` from the underlying type and typeclass. -/
 add_decl_doc AddCommGroup.of
 
-local attribute [reducible] CommGroup
-
-@[to_additive]
-instance : has_coe_to_sort CommGroup := infer_instance -- short-circuit type class inference
-
 @[to_additive add_comm_group_instance]
 instance comm_group_instance (G : CommGroup) : comm_group G := G.str
 
@@ -123,12 +107,6 @@ instance : unique (1 : CommGroup) :=
 @[simp, to_additive]
 lemma one_apply (G H : CommGroup) (g : G) : (1 : G ⟶ H) g = 1 := rfl
 
-@[to_additive]
-instance : category CommGroup := infer_instance -- short-circuit type class inference
-
-@[to_additive]
-instance : concrete_category CommGroup := infer_instance -- short-circuit type class inference
-
 @[to_additive,ext]
 lemma ext (G H : CommGroup) (f₁ f₂ : G ⟶ H) (w : ∀ x, f₁ x = f₂ x) : f₁ = f₂ :=
 by { ext1, apply w }
diff --git a/src/algebra/category/Mon/basic.lean b/src/algebra/category/Mon/basic.lean
index cd8a3b266e59c..47f6da9d6178c 100644
--- a/src/algebra/category/Mon/basic.lean
+++ b/src/algebra/category/Mon/basic.lean
@@ -15,34 +15,7 @@ We introduce the bundled categories:
 * `CommMon`
 * `AddCommMon`
 along with the relevant forgetful functors between them.
-
-## Implementation notes
-
-See the note [locally reducible category instances].
--/
-
-/--
-We make SemiRing (and the other categories) locally reducible in order
-to define its instances. This is because writing, for example,
-
-```
-instance : concrete_category SemiRing := by { delta SemiRing, apply_instance }
-```
-
-results in an instance of the form `id (bundled_hom.concrete_category _)`
-and this `id`, not being [reducible], prevents a later instance search
-(once SemiRing is no longer reducible) from seeing that the morphisms of
-SemiRing are really semiring morphisms (`→+*`), and therefore have a coercion
-to functions, for example. It's especially important that the `has_coe_to_sort`
-instance not contain an extra `id` as we want the `semiring ↥R` instance to
-also apply to `semiring R.α` (it seems to be impractical to guarantee that
-we always access `R.α` through the coercion rather than directly).
-
-TODO: Probably @[derive] should be able to create instances of the
-required form (without `id`), and then we could use that instead of
-this obscure `local attribute [reducible]` method.
 -/
-library_note "locally reducible category instances"
 
 universes u v
 
@@ -57,11 +30,17 @@ add_decl_doc AddMon
 
 namespace Mon
 
+@[to_additive]
+instance bundled_hom : bundled_hom @monoid_hom :=
+⟨@monoid_hom.to_fun, @monoid_hom.id, @monoid_hom.comp, @monoid_hom.coe_inj⟩
+
+attribute [derive [has_coe_to_sort, large_category, concrete_category]] Mon AddMon
+
 /-- Construct a bundled `Mon` from the underlying type and typeclass. -/
 @[to_additive]
 def of (M : Type u) [monoid M] : Mon := bundled.of M
 
-/-- Construct a bundled Mon from the underlying type and typeclass. -/
+/-- Construct a bundled `Mon` from the underlying type and typeclass. -/
 add_decl_doc AddMon.of
 
 @[to_additive]
@@ -70,24 +49,9 @@ instance : inhabited Mon :=
 -- which breaks to_additive.
 ⟨@of punit $ @group.to_monoid _ $ @comm_group.to_group _ punit.comm_group⟩
 
-local attribute [reducible] Mon
-
-@[to_additive]
-instance : has_coe_to_sort Mon := infer_instance -- short-circuit type class inference
-
 @[to_additive add_monoid]
 instance (M : Mon) : monoid M := M.str
 
-@[to_additive]
-instance bundled_hom : bundled_hom @monoid_hom :=
-⟨@monoid_hom.to_fun, @monoid_hom.id, @monoid_hom.comp, @monoid_hom.coe_inj⟩
-
-@[to_additive]
-instance : category Mon := infer_instance -- short-circuit type class inference
-
-@[to_additive]
-instance : concrete_category Mon := infer_instance -- short-circuit type class inference
-
 end Mon
 
 /-- The category of commutative monoids and monoid morphisms. -/
@@ -102,6 +66,8 @@ namespace CommMon
 @[to_additive]
 instance : bundled_hom.parent_projection comm_monoid.to_monoid := ⟨⟩
 
+attribute [derive [has_coe_to_sort, large_category, concrete_category]] CommMon AddCommMon
+
 /-- Construct a bundled `CommMon` from the underlying type and typeclass. -/
 @[to_additive]
 def of (M : Type u) [comm_monoid M] : CommMon := bundled.of M
@@ -115,20 +81,9 @@ instance : inhabited CommMon :=
 -- which breaks to_additive.
 ⟨@of punit $ @comm_group.to_comm_monoid _ punit.comm_group⟩
 
-local attribute [reducible] CommMon
-
-@[to_additive]
-instance : has_coe_to_sort CommMon := infer_instance -- short-circuit type class inference
-
 @[to_additive add_comm_monoid]
 instance (M : CommMon) : comm_monoid M := M.str
 
-@[to_additive]
-instance : category CommMon := infer_instance -- short-circuit type class inference
-
-@[to_additive]
-instance : concrete_category CommMon := infer_instance -- short-circuit type class inference
-
 @[to_additive has_forget_to_AddMon]
 instance has_forget_to_Mon : has_forget₂ CommMon Mon := bundled_hom.forget₂ _ _
 
diff --git a/src/computability/halting.lean b/src/computability/halting.lean
index a8bb4cc9d35dd..fa561dbcb6001 100644
--- a/src/computability/halting.lean
+++ b/src/computability/halting.lean
@@ -181,7 +181,7 @@ begin
   simp at e,
   by_cases eval c ∈ C,
   { simp [h] at e, rwa ← e },
-  { simp at h, simp [h] at e,
+  { simp [h] at e,
     rw e at h, contradiction }
 end
 
diff --git a/src/linear_algebra/finsupp.lean b/src/linear_algebra/finsupp.lean
index 8b168f3ff7ef0..f3b05084f46ce 100644
--- a/src/linear_algebra/finsupp.lean
+++ b/src/linear_algebra/finsupp.lean
@@ -181,13 +181,9 @@ begin
   rintro l ⟨⟩,
   apply finsupp.induction l, {exact zero_mem _},
   refine λ x a l hl a0, add_mem _ _,
-  haveI := classical.dec_pred (λ x, ∃ i, x ∈ s i),
   by_cases (∃ i, x ∈ s i); simp [h],
   { cases h with i hi,
-    exact le_supr (λ i, supported M R (s i)) i (single_mem_supported R _ hi) },
-  { rw filter_single_of_neg,
-    { simp },
-    { exact h } }
+    exact le_supr (λ i, supported M R (s i)) i (single_mem_supported R _ hi) }
 end
 
 theorem supported_union (s t : set α) :
diff --git a/src/measure_theory/category/Meas.lean b/src/measure_theory/category/Meas.lean
index 168195aea5b83..1b9f1dfec5e9f 100644
--- a/src/measure_theory/category/Meas.lean
+++ b/src/measure_theory/category/Meas.lean
@@ -28,7 +28,8 @@ noncomputable theory
 open category_theory measure_theory
 universes u v
 
-@[reducible] def Meas : Type (u+1) := bundled measurable_space
+@[derive has_coe_to_sort]
+def Meas : Type (u+1) := bundled measurable_space
 
 namespace Meas
 
@@ -39,6 +40,10 @@ def of (α : Type u) [measurable_space α] : Meas := ⟨α⟩
 
 instance unbundled_hom : unbundled_hom @measurable := ⟨@measurable_id, @measurable.comp⟩
 
+attribute [derive [large_category, concrete_category]] Meas
+
+instance : inhabited Meas := ⟨Meas.of empty⟩
+
 /-- `Measure X` is the measurable space of measures over the measurable space `X`. It is the
 weakest measurable space, s.t. λμ, μ s is measurable for all measurable sets `s` in `X`. An
 important purpose is to assign a monadic structure on it, the Giry monad. In the Giry monad,
diff --git a/src/tactic/basic.lean b/src/tactic/basic.lean
index 20721a816ae1a..e9950284366f1 100644
--- a/src/tactic/basic.lean
+++ b/src/tactic/basic.lean
@@ -1,6 +1,7 @@
 import tactic.alias
 import tactic.clear
 import tactic.converter.apply_congr
+import tactic.delta_instance
 import tactic.elide
 import tactic.explode
 import tactic.find
diff --git a/src/tactic/core.lean b/src/tactic/core.lean
index 967dc9aa77d5b..09793441c54e8 100644
--- a/src/tactic/core.lean
+++ b/src/tactic/core.lean
@@ -10,6 +10,7 @@ import meta.rb_map
 import data.bool
 import tactic.lean_core_docs
 import tactic.interactive_expr
+import tactic.fix_by_cases
 
 universe variable u
 
@@ -1985,49 +1986,12 @@ Examples:
 * ```get_pexpr_arg_arity_with_tgt ``(monad) `(true)``` returns 1, since `monad` takes one argument of type `α → α`.
 * ```get_pexpr_arg_arity_with_tgt ``(module R) `(Π (R : Type), comm_ring R → true)``` returns 0
  -/
-private meta def get_pexpr_arg_arity_with_tgt (func : pexpr) (tgt : expr) : tactic ℕ :=
+meta def get_pexpr_arg_arity_with_tgt (func : pexpr) (tgt : expr) : tactic ℕ :=
 lock_tactic_state $ do
   mv ← mk_mvar,
   solve_aux tgt $ intros >> to_expr ``(%%func %%mv),
   expr.pi_arity <$> (infer_type mv >>= instantiate_mvars)
 
-/--
-Tries to derive instances by unfolding the newly introduced type and applying type class resolution.
-
-For example,
-```lean
-@[derive ring] def new_int : Type := ℤ
-```
-adds an instance `ring new_int`, defined to be the instance of `ring ℤ` found by `apply_instance`.
-
-Multiple instances can be added with `@[derive [ring, module ℝ]]`.
-
-This derive handler applies only to declarations made using `def`, and will fail on such a
-declaration if it is unable to derive an instance. It is run with higher priority than the built-in
-handlers, which will fail on `def`s.
--/
-@[derive_handler, priority 2000] meta def delta_instance : derive_handler :=
-λ cls new_decl_name,
-do env ← get_env,
-if env.is_inductive new_decl_name then return ff else
-do new_decl ← get_decl new_decl_name,
-   new_decl_pexpr ← resolve_name new_decl_name,
-   arity ← get_pexpr_arg_arity_with_tgt cls new_decl.type,
-   tgt ← to_expr $ apply_under_n_pis cls new_decl_pexpr new_decl.type (new_decl.type.pi_arity - arity),
-   (_, inst) ← solve_aux tgt
-     (intros >> reset_instance_cache >> delta_target [new_decl_name]  >> apply_instance >> done),
-   inst ← instantiate_mvars inst,
-   inst ← replace_univ_metas_with_univ_params inst,
-   tgt ← instantiate_mvars tgt,
-   nm ← get_unused_decl_name $ new_decl_name <.>
-     match cls with
-     | (expr.const nm _) := nm.last
-     | _ := "inst"
-     end,
-   add_protected_decl $ declaration.defn nm inst.collect_univ_params tgt inst new_decl.reducibility_hints new_decl.is_trusted,
-   set_basic_attribute `instance nm tt,
-   return tt
-
 /-- `find_private_decl n none` finds a private declaration named `n` in any of the imported files.
 
 `find_private_decl n (some m)` finds a private declaration named `n` in the same file where a
diff --git a/src/tactic/delta_instance.lean b/src/tactic/delta_instance.lean
new file mode 100644
index 0000000000000..142a3e4fee6a7
--- /dev/null
+++ b/src/tactic/delta_instance.lean
@@ -0,0 +1,70 @@
+/-
+Copyright (c) 2019 Rob Lewis. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rob Lewis
+-/
+import tactic.simp_result
+
+namespace tactic
+
+/--
+`delta_instance ids` tries to solve the goal by calling `apply_instance`,
+first unfolding the definitions in `ids`.
+-/
+-- We call `dsimp_result` here because otherwise
+-- `delta_target` will insert an `id` in the result.
+-- See the note [locally reducible category instances]
+-- https://github.com/leanprover-community/mathlib/blob/c9fca15420e2ad443707ace831679fd1762580fe/src/algebra/category/Mon/basic.lean#L27
+-- for an example where this used to cause a problem.
+meta def delta_instance (ids : list name) : tactic unit :=
+dsimp_result
+  (intros >> reset_instance_cache >> delta_target ids >> apply_instance >> done)
+
+namespace interactive
+setup_tactic_parser
+
+/--
+`delta_instance id₁ id₂ ...` tries to solve the goal by calling `apply_instance`,
+first unfolding the definitions in `idᵢ`.
+-/
+meta def delta_instance (ids : parse ident*) : itactic :=
+tactic.delta_instance ids
+end interactive
+
+/--
+Tries to derive instances by unfolding the newly introduced type and applying type class resolution.
+
+For example,
+```lean
+@[derive ring] def new_int : Type := ℤ
+```
+adds an instance `ring new_int`, defined to be the instance of `ring ℤ` found by `apply_instance`.
+
+Multiple instances can be added with `@[derive [ring, module ℝ]]`.
+
+This derive handler applies only to declarations made using `def`, and will fail on such a
+declaration if it is unable to derive an instance. It is run with higher priority than the built-in
+handlers, which will fail on `def`s.
+-/
+@[derive_handler, priority 2000] meta def delta_instance_handler : derive_handler :=
+λ cls new_decl_name,
+do env ← get_env,
+if env.is_inductive new_decl_name then return ff else
+do new_decl ← get_decl new_decl_name,
+   new_decl_pexpr ← resolve_name new_decl_name,
+   arity ← get_pexpr_arg_arity_with_tgt cls new_decl.type,
+   tgt ← to_expr $ apply_under_n_pis cls new_decl_pexpr new_decl.type (new_decl.type.pi_arity - arity),
+   (_, inst) ← solve_aux tgt $ tactic.delta_instance [new_decl_name],
+   inst ← instantiate_mvars inst,
+   inst ← replace_univ_metas_with_univ_params inst,
+   tgt ← instantiate_mvars tgt,
+   nm ← get_unused_decl_name $ new_decl_name <.>
+     match cls with
+     | (expr.const nm _) := nm.last
+     | _ := "inst"
+     end,
+   add_protected_decl $ declaration.defn nm inst.collect_univ_params tgt inst new_decl.reducibility_hints new_decl.is_trusted,
+   set_basic_attribute `instance nm tt,
+   return tt
+
+end tactic
diff --git a/src/tactic/fix_by_cases.lean b/src/tactic/fix_by_cases.lean
new file mode 100644
index 0000000000000..f35bd0637c3ff
--- /dev/null
+++ b/src/tactic/fix_by_cases.lean
@@ -0,0 +1,36 @@
+/-
+Copyright (c) 2020 Gabriel Ebner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gabriel Ebner
+-/
+
+/-!
+# Fix the `by_cases` tactic
+
+The core `by_cases` tactic has several bugs:
+ - It only works if the proposition is decidable.
+ - It sometimes unfolds the proposition.
+
+We override the `by_cases` tactic with a correct implementation here.
+-/
+
+namespace tactic
+
+/--
+Do not use this function directly, use `tactic.by_cases`.
+-/
+meta def by_cases' (e : expr) (h : name) : tactic unit := do
+dec_e ← mk_app ``decidable [e] <|> fail "by_cases tactic failed, type is not a proposition",
+inst ← mk_instance dec_e <|> pure `(classical.prop_decidable %%e),
+tgt ← target,
+expr.sort tgt_u ← infer_type tgt >>= whnf,
+g1 ← mk_meta_var (e.imp tgt),
+g2 ← mk_meta_var (`(¬ %%e).imp tgt),
+focus1 $ do
+  exact $ expr.const ``dite [tgt_u] e inst tgt g1 g2,
+  set_goals [g1, g2],
+  all_goals' $ intro h >> skip
+
+attribute [vm_override by_cases'] by_cases
+
+end tactic
diff --git a/src/tactic/omega/coeffs.lean b/src/tactic/omega/coeffs.lean
index d0de42dcc125a..769ca23c08e6b 100644
--- a/src/tactic/omega/coeffs.lean
+++ b/src/tactic/omega/coeffs.lean
@@ -230,14 +230,13 @@ begin
     { rw [add_comm, nat.sub_add_cancel h1] },
     rw h5 at h4, apply eq.trans _ h4,
      simp only [val_between, zero_add], ring },
-  rw not_lt at h1,
   have h2 : (list.length as - (n + 1)) = 0,
   { apply nat.sub_eq_zero_of_le
-    (le_trans h1 (nat.le_add_right _ _)) },
+    (le_trans (not_lt.1 h1) (nat.le_add_right _ _)) },
   have h3 : val_between v as 0 (list.length as) =
             val_between v as 0 (n + 1),
   { simpa only [val] using @val_eq_of_le v as (n+1)
-      (le_trans h1 (nat.le_add_right _ _)) },
+      (le_trans (not_lt.1 h1) (nat.le_add_right _ _)) },
   simp only [add_zero, val_between, zero_add, h2, h3]
 end
 
diff --git a/src/topology/category/Top/basic.lean b/src/topology/category/Top/basic.lean
index 9faaee47056c4..4f9f87ebfa50a 100644
--- a/src/topology/category/Top/basic.lean
+++ b/src/topology/category/Top/basic.lean
@@ -12,15 +12,17 @@ open topological_space
 universe u
 
 /-- The category of topological spaces and continuous maps. -/
-@[reducible] def Top : Type (u+1) := bundled topological_space
+def Top : Type (u+1) := bundled topological_space
 
 namespace Top
 
-instance topological_space_unbundled (x : Top) : topological_space x := x.str
-
-instance concrete_category_continuous : unbundled_hom @continuous :=
+instance : unbundled_hom @continuous :=
 ⟨@continuous_id, @continuous.comp⟩
 
+attribute [derive [has_coe_to_sort, large_category, concrete_category]] Top
+
+instance topological_space_unbundled (x : Top) : topological_space x := x.str
+
 instance hom_has_coe_to_fun (X Y : Top.{u}) : has_coe_to_fun (X ⟶ Y) :=
 { F := _, coe := subtype.val }
 
@@ -30,6 +32,8 @@ instance hom_has_coe_to_fun (X Y : Top.{u}) : has_coe_to_fun (X ⟶ Y) :=
 /-- Construct a bundled `Top` from the underlying type and the typeclass. -/
 def of (X : Type u) [topological_space X] : Top := ⟨X⟩
 
+instance : inhabited Top := ⟨Top.of empty⟩
+
 /-- The discrete topology on any type. -/
 def discrete : Type u ⥤ Top.{u} :=
 { obj := λ X, ⟨X, ⊥⟩,
diff --git a/src/topology/category/UniformSpace.lean b/src/topology/category/UniformSpace.lean
index 9fde02ccdde5a..a07c3d72bbcf8 100644
--- a/src/topology/category/UniformSpace.lean
+++ b/src/topology/category/UniformSpace.lean
@@ -21,18 +21,22 @@ universes u
 open category_theory
 
 /-- A (bundled) uniform space. -/
-@[reducible] def UniformSpace : Type (u+1) := bundled uniform_space
+def UniformSpace : Type (u+1) := bundled uniform_space
 
 namespace UniformSpace
 
+/-- The information required to build morphisms for `UniformSpace`. -/
+instance : unbundled_hom @uniform_continuous :=
+⟨@uniform_continuous_id, @uniform_continuous.comp⟩
+
+attribute [derive [has_coe_to_sort, large_category, concrete_category]] UniformSpace
+
 instance (x : UniformSpace) : uniform_space x := x.str
 
 /-- Construct a bundled `UniformSpace` from the underlying type and the typeclass. -/
 def of (α : Type u) [uniform_space α] : UniformSpace := ⟨α⟩
 
-/-- The information required to build morphisms for `UniformSpace`. -/
-instance concrete_category_uniform_continuous : unbundled_hom @uniform_continuous :=
-⟨@uniform_continuous_id, @uniform_continuous.comp⟩
+instance : inhabited UniformSpace := ⟨UniformSpace.of empty⟩
 
 instance (X Y : UniformSpace) : has_coe_to_fun (X ⟶ Y) :=
 { F := λ _, X → Y, coe := category_theory.functor.map (forget UniformSpace) }
@@ -76,8 +80,14 @@ instance (X : CpltSepUniformSpace) : separated_space ((to_UniformSpace X).α) :=
 /-- Construct a bundled `UniformSpace` from the underlying type and the appropriate typeclasses. -/
 def of (X : Type u) [uniform_space X] [complete_space X] [separated_space X] : CpltSepUniformSpace := ⟨X⟩
 
+instance : inhabited CpltSepUniformSpace :=
+begin
+  haveI : separated_space empty := separated_iff_t2.mpr (by apply_instance),
+  exact ⟨CpltSepUniformSpace.of empty⟩
+end
+
 /-- The category instance on `CpltSepUniformSpace`. -/
-instance category : category CpltSepUniformSpace :=
+instance category : large_category CpltSepUniformSpace :=
 induced_category.category to_UniformSpace
 
 /-- The concrete category instance on `CpltSepUniformSpace`. -/
@@ -101,7 +111,7 @@ noncomputable def completion_functor : UniformSpace ⥤ CpltSepUniformSpace :=
   map_id' := λ X, subtype.eq completion.map_id,
   map_comp' := λ X Y Z f g, subtype.eq (completion.map_comp g.property f.property).symm, }.
 
-/-- The inclusion of any uniform spaces into its completion. -/
+/-- The inclusion of a uniform space into its completion. -/
 def completion_hom (X : UniformSpace) :
   X ⟶ (forget₂ CpltSepUniformSpace UniformSpace).obj (completion_functor.obj X) :=
 { val := (coe : X → completion X),