diff --git a/hott/algebra/precategory/iso.hlean b/hott/algebra/precategory/iso.hlean
index cf2a7aee4..164aaba98 100644
--- a/hott/algebra/precategory/iso.hlean
+++ b/hott/algebra/precategory/iso.hlean
@@ -22,6 +22,8 @@ namespace iso
     (left_inverse  : inverse ∘ f = id)
     (right_inverse : f ∘ inverse = id)
 
+  attribute is_iso.inverse [quasireducible]
+
   attribute is_iso [multiple-instances]
   open split_mono split_epi is_iso
   definition retraction_of [reducible] := @split_mono.retraction_of
diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean
index df0f4b52b..cdba8f499 100644
--- a/hott/init/equiv.hlean
+++ b/hott/init/equiv.hlean
@@ -22,6 +22,7 @@ structure is_equiv [class] {A B : Type} (f : A → B) :=
   (sect : (inv ∘ f) ∼ id)
   (adj : Πx, retr (f x) = ap f (sect x))
 
+attribute is_equiv.inv [quasireducible]
 
 -- A more bundled version of equivalence
 structure equiv (A B : Type) :=
diff --git a/src/library/tactic/class_instance_synth.cpp b/src/library/tactic/class_instance_synth.cpp
index 3c17c1b90..5ba8d7fc4 100644
--- a/src/library/tactic/class_instance_synth.cpp
+++ b/src/library/tactic/class_instance_synth.cpp
@@ -316,7 +316,7 @@ constraint mk_class_instance_cnstr(std::shared_ptr<class_instance_context> const
     };
     bool owner      = false;
     bool relax      = C->m_relax;
-    return mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::ClassInstance),
+    return mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::Basic),
                            owner, j, relax);
 }