diff --git a/library/data/buffer.lean b/library/data/buffer.lean
index 46bab575bf..779935ba69 100644
--- a/library/data/buffer.lean
+++ b/library/data/buffer.lean
@@ -46,11 +46,11 @@ def write' : buffer α → nat → α → buffer α
 
 lemma read_eq_read' [inhabited α] (b : buffer α) (i : nat) (h : i < b.size) :
   read b ⟨i, h⟩ = read' b i :=
-by cases b; unfold read read'; simp [array.read_eq_read']
+by cases b; dunfold read read' size; simp [array.read_eq_read']
 
 lemma write_eq_write' (b : buffer α) (i : nat) (h : i < b.size) (v : α) :
   write b ⟨i, h⟩ v = write' b i v :=
-by cases b; unfold write write'; simp [array.write_eq_write']
+by cases b; dunfold write write' size; simp [array.write_eq_write']
 
 def to_list (b : buffer α) : list α :=
 b.to_array.to_list
diff --git a/library/init/data/fin/basic.lean b/library/init/data/fin/basic.lean
index 673d1b6ca5..afb9c18606 100644
--- a/library/init/data/fin/basic.lean
+++ b/library/init/data/fin/basic.lean
@@ -5,6 +5,7 @@ Author: Leonardo de Moura
 -/
 prelude
 import init.data.nat.basic
+import init.propext
 open nat
 
 /-- `fin n` is the subtype of `ℕ` consisting of natural numbers strictly smaller than `n`. -/
diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index c28ddd6bc2..79433268e1 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -1800,3 +1800,11 @@ by tactic.mk_inj_eq
 
 lemma nat.succ.inj_eq (n₁ n₂ : nat) : (nat.succ n₁ = nat.succ n₂) = (n₁ = n₂) :=
 by tactic.mk_inj_eq
+
+@[simp] lemma fin.subtype_mk_eq_mk {n : ℕ} (a b) (ha hb) :
+  @eq (fin n) ⟨a, ha⟩ ⟨b, hb⟩ ↔ a = b :=
+by dunfold fin; rw subtype.mk.inj_eq
+
+@[simp] lemma fin.mk_eq_mk {n : ℕ} (a b) (ha hb) :
+  (fin.mk a ha : fin n) = fin.mk b hb ↔ a = b :=
+fin.subtype_mk_eq_mk _ _ _ _
diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index 681f2c66df..f61ae0cb08 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -746,6 +746,8 @@ open list nat
 /-- A `tag` is a list of `names`. These are attached to goals to help tactics track them.-/
 def tag : Type := list name
 
+meta instance : decidable_eq tag := list.decidable_eq
+
 /-- Enable/disable goal tagging.  -/
 meta constant enable_tags (b : bool) : tactic unit
 /-- Return tt iff goal tagging is enabled. -/
diff --git a/library/init/meta/widget/interactive_expr.lean b/library/init/meta/widget/interactive_expr.lean
index 223c569b5c..d0be1e3b6e 100644
--- a/library/init/meta/widget/interactive_expr.lean
+++ b/library/init/meta/widget/interactive_expr.lean
@@ -12,6 +12,7 @@ import init.data.punit
 import init.meta.mk_dec_eq_instance
 
 meta def subexpr := (expr × expr.address)
+meta instance : decidable_eq subexpr := prod.decidable_eq
 
 namespace widget
 
diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index eba1f1dd9b..0f7b4c0409 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -2568,7 +2568,7 @@ bool type_context_old::is_def_eq_args(expr const & e1, expr const & e2) {
     /* Second pass: unify implicit arguments.
        In the second pass, we make sure we are unfolding at least semireducible (default setting) definitions. */
     {
-        transparency_scope scope(*this, ensure_semireducible_mode(m_transparency_mode));
+        transparency_scope scope(*this, ensure_instances_mode(m_transparency_mode));
         for (pair<unsigned, bool> const & p : postponed) {
             unsigned i = p.first;
             if (p.second) {
diff --git a/tests/lean/run/mk_byte.lean b/tests/lean/run/mk_byte.lean
index b0c261434f..1b833dde8f 100644
--- a/tests/lean/run/mk_byte.lean
+++ b/tests/lean/run/mk_byte.lean
@@ -35,6 +35,8 @@ begin
   apply vector.eq,
   unfold mk_byte,
   unfold get_data,
-  simp
+  transitivity,
+  exact to_list'_drop _,
+  simp,
 end
 end Ex