diff --git a/CHANGELOG.md b/CHANGELOG.md
index ca42db3673b1fcabd2763148e0e3f4a87576d714..8106f8d2cca21bddc3c21f2cd2f4ef095b3dbd7a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -7,6 +7,8 @@ API-breaking change is listed.
 - Add lemma `lookup_total_fmap`.
 - Add lemmas about `last` and `head`: `last_app_Some`, `last_app_None`,
   `head_app_Some`, `head_app_None` and `head_app`. (by Marijn van Wezel)
+- Add tactic `notypeclasses apply` that works like `notypeclasses refine` but
+  automatically adds `_` until the given lemma takes no more arguments.
 
 ## std++ 1.11.0 (2024-10-30)
 
diff --git a/stdpp/tactics.v b/stdpp/tactics.v
index f838bf02249f22bd8a5e01f2f62d1a89d7071314..dd2c1598960987c19be0eff17859e369102a0bfb 100644
--- a/stdpp/tactics.v
+++ b/stdpp/tactics.v
@@ -736,6 +736,12 @@ Tactic Notation "ospecialize" "*" uconstr(p) :=
       pose proof p as H'; clear H; rename H' into H
   )).
 
+(** Tactic that works like [notypeclasses refine] but automatically determines
+the right number of [_]. This is *not* goal-directed, it will add [_] until the
+given term no longer has a function type (determined via syntactic matching). *)
+Tactic Notation "notypeclasses" "apply" uconstr(p) :=
+  opose_specialize_foralls_core p () ltac:(fun p => notypeclasses refine p).
+
 (** The block definitions are taken from [Coq.Program.Equality] and can be used
 by tactics to separate their goal from hypotheses they generalize over. *)
 Definition block {A : Type} (a : A) := a.
diff --git a/stdpp_bitvector/definitions.v b/stdpp_bitvector/definitions.v
index af70961286cb48cc4ca2f3bd97377ac794941dca..36a1b7381ca5eb2aaa9ae2bce99e002131cf7ec7 100644
--- a/stdpp_bitvector/definitions.v
+++ b/stdpp_bitvector/definitions.v
@@ -755,7 +755,7 @@ Global Hint Resolve bv_wrap_simplify_mul | 10 : bv_wrap_simplify_db.
  tries to simplify them by removing any [bv_wrap] inside z1. *)
 Ltac bv_wrap_simplify_left :=
   lazymatch goal with |- bv_wrap _ _ = _ => idtac end;
-  etrans; [ notypeclasses refine (bv_wrap_simplify_proof _ _ _);
+  etrans; [ notypeclasses apply bv_wrap_simplify_proof;
             typeclasses eauto with bv_wrap_simplify_db | ]
 .
 
diff --git a/tests/tactics.ref b/tests/tactics.ref
index 8004020e70975cdfb901869c2183a3a77a3390ef..439f7902013e75daaa8bdda04934e8a9142b95c5 100644
--- a/tests/tactics.ref
+++ b/tests/tactics.ref
@@ -65,5 +65,27 @@ use opose proof instead.
   H' : even n
   ============================
   even n
+"notypeclasses_apply_test"
+     : string
+1 goal
+  
+  n : nat
+  ============================
+  Decision (n = 0)
+1 goal
+  
+  n : nat
+  ============================
+  Decision (n = 0)
+"notypeclasses_apply_error"
+     : string
+The command has indeed failed with message:
+In environment
+P, Q : Prop
+H : P → Q
+HQ : Q
+opose_internal : P
+The term "H opose_internal" has type "Q" while it is expected to have type
+ "P".
 The command has indeed failed with message:
 No such assumption.
diff --git a/tests/tactics.v b/tests/tactics.v
index 2e755290c691f7bff55d13cc26b7e2bf37b9c9bd..990bccb0da95a279a624d79ccf1395cf3d4cf595 100644
--- a/tests/tactics.v
+++ b/tests/tactics.v
@@ -234,6 +234,22 @@ Proof.
   done.
 Qed.
 
+Check "notypeclasses_apply_test".
+Lemma notypeclasses_apply_test n : {n = 0} + {¬ n = 0}.
+Proof.
+  (* Partially applied lemma with typeclass in one of the trailing [_]. *)
+  notypeclasses apply (@decide (n = 0)). Show.
+Restart. Proof.
+  (* Partially applied lemma with typeclass in one of the explicit [_]. *)
+  notypeclasses apply (@decide (n = 0) _). Show.
+Abort.
+
+Check "notypeclasses_apply_error".
+Lemma notypeclasses_apply_error (P Q : Prop) : (P → Q) → Q → P.
+Proof.
+  intros H HQ. Fail notypeclasses apply H.
+Abort.
+
 (** Some tests for f_equiv. *)
 (* Similar to [f_equal], it should solve goals by [reflexivity]. *)
 Lemma test_f_equiv_refl {A} (R : relation A) `{!Equivalence R} x :