diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 137683a284b121d95d702bcb6c54251ba91d18e7..86be845c607dfbc1685394a784858cbe8da45673 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -66,6 +66,8 @@ Tactic Notation "iSelect" open_constr(pat) tactic1(tac) :=
 (** * Start a proof *)
 Tactic Notation "iStartProof" :=
   lazymatch goal with
+  | |- (let _ := _ in _) => fail "iStartProof: goal is a `let`, use `simpl`,"
+                                 "`intros x`, `iIntros (x)`, or `iIntros ""%x"""
   | |- envs_entails _ _ => idtac
   | |- ?φ => notypeclasses refine (as_emp_valid_2 φ _ _);
                [tc_solve || fail "iStartProof: not a BI assertion"