diff --git a/theories/finite.v b/theories/finite.v
index f5d516cc7e12f41ab0c3b19c2a5aa3439740a4b3..d24e9c1ebc628bab92809236d2f943b06b6033c2 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -154,7 +154,7 @@ Lemma finite_bijective A `{Finite A} B `{Finite B} :
 Proof.
   split.
   - intros; destruct (proj1 (finite_inj A B)) as [f ?]; auto with lia.
-    exists f; eauto using finite_inj_surj.
+    exists f; split; [done|]. by apply finite_inj_surj.
   - intros (f&?&?). apply (anti_symm (≤)); apply finite_inj.
     + by exists f.
     + destruct (surj_cancel f) as (g&?). exists g. apply cancel_inj.
@@ -274,7 +274,7 @@ Next Obligation.
 Qed.
 Next Obligation.
   intros ?????? [x|y]; rewrite elem_of_app, !elem_of_list_fmap;
-    eauto using elem_of_enum.
+    [left|right]; (eexists; split; [done|apply elem_of_enum]).
 Qed.
 Lemma sum_card `{Finite A, Finite B} : card (A + B) = card A + card B.
 Proof. unfold card. simpl. by rewrite app_length, !fmap_length. Qed.