diff --git a/library/init/meta/default.lean b/library/init/meta/default.lean
index 758fa252c5..c0c4f6a5ab 100644
--- a/library/init/meta/default.lean
+++ b/library/init/meta/default.lean
@@ -9,7 +9,7 @@ import init.meta.level init.meta.expr init.meta.environment init.meta.attribute
 import init.meta.tactic init.meta.contradiction_tactic init.meta.constructor_tactic
 import init.meta.injection_tactic init.meta.relation_tactics init.meta.fun_info
 import init.meta.congr_lemma init.meta.match_tactic init.meta.rewrite_tactic
-import init.meta.derive init.meta.simp_tactic init.meta.set_get_option_tactics
+import init.meta.simp_tactic init.meta.set_get_option_tactics
 import init.meta.interactive
 import init.meta.comp_value_tactics
 import init.meta.congr_tactic
diff --git a/library/init/meta/derive.lean b/library/init/meta/derive.lean
deleted file mode 100644
index 3a1e2ee5ff..0000000000
--- a/library/init/meta/derive.lean
+++ /dev/null
@@ -1,86 +0,0 @@
-/-
-Copyright (c) 2017 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sebastian Ullrich
-
-Attribute that can automatically derive typeclass instances.
--/
-prelude
-import init.meta.attribute
-import init.meta.interactive_base
-import init.meta.mk_has_reflect_instance
-
-open lean3
-open interactive.types
-open tactic
-
-/-- A handler that may or may not be able to implement the typeclass `cls` for `decl`.
-    It should return `tt` if it was able to derive `cls` and `ff` if it does not know
-    how to derive `cls`, in which case lower-priority handlers will be tried next. -/
-meta def derive_handler := Π (cls : pexpr) (decl : name), tactic bool
-
-@[user_attribute]
-meta def derive_handler_attr : user_attribute :=
-{ name := `derive_handler, descr := "register a definition of type `derive_handler` for use in the [derive] attribute" }
-
-private meta def try_handlers (p : pexpr) (n : name) : list derive_handler → tactic unit
-| []      := fail format!"failed to find a derive handler for '{p}'"
-| (h::hs) :=
-do success ← h p n,
-   when (¬success) $
-     try_handlers hs
-
-@[user_attribute] meta def derive_attr : user_attribute unit (list pexpr) :=
-{ name := `derive, descr := "automatically derive typeclass instances",
-  parser := pexpr_list_or_texpr,
-  after_set := some (λ n _ _,
-  do ps ← derive_attr.get_param n,
-     handlers ← attribute.get_instances `derive_handler,
-     handlers ← handlers.mmap (λ n, eval_expr derive_handler (expr.const n [])),
-     ps.mmap' (λ p, try_handlers p n handlers)) }
-
-/-- Given a tactic `tac` that can solve an application of `cls` in the right context,
-    `instance_derive_handler` uses it to build an instance declaration of `cls n`. -/
-meta def instance_derive_handler (cls : name) (tac : tactic unit) (univ_poly := tt)
-  (modify_target : name → list expr → expr → tactic expr := λ _ _, pure) : derive_handler :=
-λ p n,
-if p.is_constant_of cls then
-do decl ← get_decl n,
-   cls_decl ← get_decl cls,
-   env ← get_env,
-   guard (env.is_inductive n) <|> fail format!"failed to derive '{cls}', '{n}' is not an inductive type",
-   let ls := decl.univ_params.map $ λ n, if univ_poly then level.param n else level.zero,
-   -- incrementally build up target expression `Π (hp : p) [cls hp] ..., cls (n.{ls} hp ...)`
-   -- where `p ...` are the inductive parameter types of `n`
-   let tgt : expr := expr.const n ls,
-   ⟨params, _⟩ ← mk_local_pis (decl.type.instantiate_univ_params (decl.univ_params.zip ls)),
-   let tgt := tgt.mk_app params,
-   tgt ← mk_app cls [tgt],
-   tgt ← modify_target n params tgt,
-   tgt ← params.enum.mfoldr (λ ⟨i, param⟩ tgt,
-   do -- add typeclass hypothesis for each inductive parameter
-      tgt ← do {
-        guard $ i < env.inductive_num_params n,
-        param_cls ← mk_app cls [param],
-        -- TODO(sullrich): omit some typeclass parameters based on usage of `param`?
-        pure $ expr.pi `a binder_info.inst_implicit param_cls tgt
-      } <|> pure tgt,
-      pure $ tgt.bind_pi param
-   ) tgt,
-   (_, val) ← tactic.solve_aux tgt (intros >> tac),
-   val ← instantiate_mvars val,
-   let trusted := decl.is_trusted ∧ cls_decl.is_trusted,
-   add_decl (declaration.defn (n ++ cls)
-             (if univ_poly then decl.univ_params else [])
-             tgt val reducibility_hints.abbrev trusted),
-   set_basic_attribute `instance (n ++ cls) tt,
-   pure true
-else pure false
-
-@[derive_handler] meta def has_reflect_derive_handler :=
-instance_derive_handler ``has_reflect mk_has_reflect_instance ff (λ n params tgt,
-  -- add additional `reflected` assumption for each parameter
-  params.mfoldr (λ param tgt,
-  do param_cls ← mk_app `reflected [param],
-    pure $ expr.pi `a binder_info.inst_implicit param_cls tgt
-  ) tgt)
diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index 4e3e77f02c..eb6bdbfa5f 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import init.meta.tactic init.meta.rewrite_tactic init.meta.simp_tactic
 import init.control.combinators
-import init.meta.interactive_base init.meta.derive init.meta.match_tactic
+import init.meta.interactive_base init.meta.match_tactic
 import init.meta.congr_tactic
 
 open lean3
diff --git a/library/init/meta/mk_has_reflect_instance.lean b/library/init/meta/mk_has_reflect_instance.lean
deleted file mode 100644
index 6046e15d22..0000000000
--- a/library/init/meta/mk_has_reflect_instance.lean
+++ /dev/null
@@ -1,84 +0,0 @@
-/-
-Copyright (c) 2017 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sebastian Ullrich
-
-Helper tactic for constructing a has_reflect instance.
--/
-prelude
-import init.meta.rec_util
-
-namespace tactic
-open expr environment list
-
-/- Retrieve the name of the type we are building a has_reflect instance for. -/
-private meta def get_has_reflect_type_name : tactic name :=
-do {
-  (app (const n ls) t) ← target,
-  when (n ≠ `has_reflect) failed,
-  (const I ls) ← return (get_app_fn t),
-  return I }
-<|>
-fail "mk_has_reflect_instance tactic failed, target type is expected to be of the form (has_reflect ...)"
-
-/- Try to synthesize constructor argument using type class resolution -/
-private meta def mk_has_reflect_instance_for (a : expr) : tactic expr :=
-do t    ← infer_type a,
-   do {
-     m    ← mk_app `reflected [a],
-     inst ← mk_instance m
-     <|> do {
-       f ← pp t,
-       fail (to_fmt "mk_has_reflect_instance failed, failed to generate instance for" ++ format.nest 2 (format.line ++ f))
-     },
-     mk_app `reflect [a, inst] }
-
-/- Synthesize (recursive) instances of `reflected` for all fields -/
-private meta def mk_reflect : name → name → list name → nat → tactic (list expr)
-| I_name F_name []              num_rec := return []
-| I_name F_name (fname::fnames) num_rec := do
-  field ← get_local fname,
-  rec   ← is_type_app_of field I_name,
-  quote    ← if rec then mk_brec_on_rec_value F_name num_rec else mk_has_reflect_instance_for field,
-  quotes   ← mk_reflect I_name F_name fnames (if rec then num_rec + 1 else num_rec),
-  return (quote :: quotes)
-
-/- Solve the subgoal for constructor `F_name` -/
-private meta def has_reflect_case (I_name F_name : name) (field_names : list name) : tactic unit :=
-do field_quotes ← mk_reflect I_name F_name field_names 0,
-   -- fn should be of the form `F_name ps fs`, where ps are the inductive parameter arguments,
-   -- and `fs.length = field_names.length`
-   `(reflected %%fn) ← target,
-   -- `reflected (F_name ps)` should be synthesizable directly, using instances from the context
-   let fn := field_names.foldl (λ fn _, expr.app_fn fn) fn,
-   quote ← mk_app `reflected [fn] >>= mk_instance,
-   -- now extend to an instance of `reflected (F_name ps fs)`
-   quote ← field_quotes.mfoldl (λ quote fquote, to_expr ``(reflected.subst %%quote %%fquote)) quote,
-   exact quote
-
-private meta def for_each_has_reflect_goal : name → name → list (list name) → tactic unit
-| I_name F_name [] := done <|> fail "mk_has_reflect_instance failed, unexpected number of cases"
-| I_name F_name (ns::nss) := do
-  solve1 (has_reflect_case I_name F_name ns),
-  for_each_has_reflect_goal I_name F_name nss
-
-/-- Solves a goal of the form `has_reflect α` where α is an inductive type.
-    Needs to synthesize a `reflected` instance for each inductive parameter type of α
-    and for each constructor parameter of α. -/
-meta def mk_has_reflect_instance : tactic unit :=
-do I_name ← get_has_reflect_type_name,
-   env ← get_env,
-   v_name : name ← return `_v,
-   F_name : name ← return `_F,
-   guard (env.inductive_num_indices I_name = 0) <|>
-     fail "mk_has_reflect_instance failed, indexed families are currently not supported",
-   -- Use brec_on if type is recursive.
-   -- We store the functional in the variable F.
-   if is_recursive env I_name
-   then intro `_v >>= (λ x, induction x [v_name, F_name] (some $ I_name <.> "brec_on") >> return ())
-   else intro v_name >> return (),
-   arg_names : list (list name) ← mk_constructors_arg_names I_name `_p,
-   get_local v_name >>= λ v, cases v (join arg_names),
-   for_each_has_reflect_goal I_name F_name arg_names
-
-end tactic