diff --git a/CHANGELOG.md b/CHANGELOG.md
index ef8a23a4c57779e3de4aae128324656a5637662a..3c06e152d1a04c0001da6f4b82726ad5fa1fc671 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -95,6 +95,9 @@ Coq 8.11 is no longer supported in this version of Iris.
 * Rename the main entry point module for the proofmode from
   `iris.proofmode.tactics` to `iris.proofmode.proofmode`. Under normal
   circumstances, this should be the only proofmode file you need to import.
+* Improve performance of the `iIntoEmpValid` tactic used by `iPoseProof`,
+  especially in the case of large goals and lemmas with many forall quantifiers
+  (by Armaël Guéneau)
 
 **Changes in `bi`:**
 
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index d9ab16e89b60ad8eaf85a22679e003574e15645e..944a0bc67e617d51a37d215233f77d5e53446506 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -816,17 +816,41 @@ generates a goal [A_i] for each non-dependent argument [x_i : A_i].
 
 For example, if goal is [IntoEmpValid (∀ x, P x → R1 x ⊢ R2 x) ?Q], then the
 [iIntoEmpValid] tactic generates an evar [?x], a subgoal [P ?x], and unifies
-[?Q] with [R1 ?x -∗ R2 ?x]. *)
-Ltac iIntoEmpValid_go := first
-  [(* Case [φ → ψ] *)
-   notypeclasses refine (into_emp_valid_impl _ _ _ _ _);
-     [(*goal for [φ] *)|iIntoEmpValid_go]
-  |(* Case [∀ x : A, φ] *)
-   notypeclasses refine (into_emp_valid_forall _ _ _ _); iIntoEmpValid_go
-  |(* Case [∀.. x : TT, φ] *)
-   notypeclasses refine (into_emp_valid_tforall _ _ _ _); iIntoEmpValid_go
-  |(* Case [P ⊢ Q], [P ⊣⊢ Q], [⊢ P] *)
-   notypeclasses refine (into_emp_valid_here _ _ _)].
+[?Q] with [R1 ?x -∗ R2 ?x].
+
+The tactic is implemented so as to provide a "fast path" for the arrow, forall
+and tforall cases, gated by syntactic ltac pattern matching on the shape of the
+goal. This is an optimization: the behavior of the tactic is equivalent to the
+code in the last "wildcard" case, but faster on larger goals, where running
+(possibly failing) [notypeclasses refine]s can take a significant amount of
+time.
+*)
+Ltac iIntoEmpValid_go :=
+  lazymatch goal with
+  | |- IntoEmpValid (?φ → ?ψ) _ =>
+    (* Case [φ → ψ] *)
+    (* note: the ltac pattern [_ → _] would not work as it would also match
+       [∀ _, _] *)
+    notypeclasses refine (into_emp_valid_impl _ _ _ _ _);
+      [(*goal for [φ] *)|iIntoEmpValid_go]
+  | |- IntoEmpValid (∀ _, _) _ =>
+    (* Case [∀ x : A, φ] *)
+    notypeclasses refine (into_emp_valid_forall _ _ _ _); iIntoEmpValid_go
+  | |- IntoEmpValid (∀.. _, _) _ =>
+    (* Case [∀.. x : TT, φ] *)
+    notypeclasses refine (into_emp_valid_tforall _ _ _ _); iIntoEmpValid_go
+  | |- _ =>
+    first
+      [(* Case [φ → ψ] *)
+       notypeclasses refine (into_emp_valid_impl _ _ _ _ _);
+         [(*goal for [φ] *)|iIntoEmpValid_go]
+      |(* Case [∀ x : A, φ] *)
+       notypeclasses refine (into_emp_valid_forall _ _ _ _); iIntoEmpValid_go
+      |(* Case [∀.. x : TT, φ] *)
+       notypeclasses refine (into_emp_valid_tforall _ _ _ _); iIntoEmpValid_go
+      |(* Case [P ⊢ Q], [P ⊣⊢ Q], [⊢ P] *)
+       notypeclasses refine (into_emp_valid_here _ _ _) ]
+  end.
 
 Ltac iIntoEmpValid :=
   (* Factor out the base case of the loop to avoid needless backtracking *)