diff --git a/CHANGELOG.md b/CHANGELOG.md
index 8cc3f8d193cc117b2373eb378bd5c5834fb46ac6..4fe7fcb46ab6b6a9178f1ef39e04afc40354773b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -19,6 +19,7 @@ lemma.
   invariant opening.
 * Change `iInduction` to always generate a magic wand instead of sometimes
   generating an implication for reverted hypotheses.
+* Add `iUnfold` tactic.
 
 **Changes in `base_logic`:**
 
diff --git a/docs/proof_mode.md b/docs/proof_mode.md
index fe50ddd5c4f84e59391457b281da248e8b117074..4363ddbc4933f82e6f3109245f59944de6068e2f 100644
--- a/docs/proof_mode.md
+++ b/docs/proof_mode.md
@@ -273,6 +273,10 @@ Rewriting / simplification
 - `iSimpl` / `iSimpl in "selpat"` : perform `simpl` on the proof mode
   goal / hypotheses given by the selection pattern `selpat`. This is a
   shorthand for `iEval (simpl)`.
+- `iUnfold xs` / `iUnfold xs in "selpat"` : perform `unfold xs` on the proof
+  mode goal / hypotheses given by the selection pattern `selpat`. This is a
+  shorthand for `iEval (unfold xs)`. Similar to Coq's `unfold`, the argument
+  `xs` should be a comma-separated non-empty list.
 
 Iris
 ----
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 4564a816d8b482f554d4330f3d7253dea6086c5a..2bb82176f0354d4544cc824c434d61d112ddc7ba 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -230,6 +230,14 @@ Tactic Notation "iEval" tactic3(t) "in" constr(Hs) :=
 Tactic Notation "iSimpl" := iEval (simpl).
 Tactic Notation "iSimpl" "in" constr(H) := iEval (simpl) in H.
 
+Ltac _iUnfold r := iEval (unfold r).
+Tactic Notation "iUnfold" ne_reference_list_sep(ids,",") :=
+  ltac1_list_iter _iUnfold ids.
+
+Ltac _iUnfold_in r H := iEval (unfold r) in H.
+Tactic Notation "iUnfold" ne_reference_list_sep(ids,",") "in" constr(H) :=
+  ltac1_list_iter ltac:(fun r => _iUnfold_in r H) ids.
+
 (* It would be nice to also have an `iSsrRewrite`, however, for this we need to
 pass arguments to Ssreflect's `rewrite` like `/= foo /bar` in Ltac, see:
 
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index f13abe06a9a5fefeea4ac920a04101c6c5baf48a..fb7915240669ea1798f5579fca414ab3db4556dd 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -508,6 +508,25 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
      : string
 The command has indeed failed with message:
 Tactic failure: iEval: %: unsupported selection pattern.
+"test_iUnfold"
+     : string
+1 goal
+  
+  PROP : bi
+  Hdef : def2 = 10
+  ============================
+  --------------------------------------∗
+  ⌜10 = 10⌝
+"test_iUnfold_in"
+     : string
+1 goal
+  
+  PROP : bi
+  Hdef : def2 = 10
+  ============================
+  "Hdef" : ⌜10 = 10⌝
+  --------------------------------------∗
+  ⌜def2 = 10⌝
 "test_iRename"
      : string
 1 goal
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 068950e624c2719fb0246b96d246d42fdd0bafaf..c19cac183244182f61f3109a79dbd3fc0c8d4c70 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1311,6 +1311,18 @@ Check "test_iSimpl_in4".
 Lemma test_iSimpl_in4 x y : ⌜ (3 + x)%nat = y ⌝ ⊢@{PROP} ⌜ S (S (S x)) = y ⌝.
 Proof. iIntros "H". Fail iSimpl in "%". by iSimpl in "H". Qed.
 
+Section iUnfold.
+  Definition def1 := 10.
+  Definition def2 := def1.
+  Check "test_iUnfold".
+  Lemma test_iUnfold : def2 = 10 → ⊢@{PROP} ⌜ def2 = 10 ⌝.
+  Proof. intros Hdef. iUnfold def2, def1. Show. done. Qed.
+
+  Check "test_iUnfold_in".
+  Lemma test_iUnfold_in : def2 = 10 → ⌜ def2 = 10 ⌝ ⊢@{PROP} ⌜ def2 = 10 ⌝.
+  Proof. iIntros "%Hdef Hdef". iUnfold def2, def1 in "Hdef". Show. done. Qed.
+End iUnfold.
+
 Check "test_iRename".
 Lemma test_iRename P : □P -∗ P.
 Proof. iIntros "#H". iRename "H" into "X". Show. iExact "X". Qed.