diff --git a/src/Iris/ProofMode/Tactics.lean b/src/Iris/ProofMode/Tactics.lean
index 7758fa714..62b7cd1e0 100644
--- a/src/Iris/ProofMode/Tactics.lean
+++ b/src/Iris/ProofMode/Tactics.lean
@@ -11,6 +11,7 @@ import Iris.ProofMode.Tactics.LeftRight
 import Iris.ProofMode.Tactics.Move
 import Iris.ProofMode.Tactics.Pure
 import Iris.ProofMode.Tactics.Remove
+import Iris.ProofMode.Tactics.Revert
 import Iris.ProofMode.Tactics.Rename
 import Iris.ProofMode.Tactics.Specialize
 import Iris.ProofMode.Tactics.Split
diff --git a/src/Iris/ProofMode/Tactics/Revert.lean b/src/Iris/ProofMode/Tactics/Revert.lean
new file mode 100644
index 000000000..8c5c9442e
--- /dev/null
+++ b/src/Iris/ProofMode/Tactics/Revert.lean
@@ -0,0 +1,68 @@
+/-
+Copyright (c) 2025 Oliver Soeser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Oliver Soeser
+-/
+import Iris.ProofMode.Tactics.Cases
+
+namespace Iris.ProofMode
+open Lean Elab Tactic Meta Qq BI Std
+
+theorem wand_revert [BI PROP] {P Q A1 A2 : PROP}
+    (h1 : P ⊣⊢ A1 ∗ A2) (h2 : A1 ⊢ A2 -∗ Q) : P ⊢ Q :=
+  h1.mp.trans (wand_elim h2)
+
+theorem forall_revert [BI PROP] {P : PROP} {Ψ : α → PROP}
+    (h : P ⊢ ∀ x, Ψ x) : ∀ x, P ⊢ Ψ x :=
+  λ x => h.trans (forall_elim x)
+
+theorem pure_revert [BI PROP] {P Q : PROP} {φ : Prop}
+    (h : P ⊢ ⌜φ⌝ -∗ Q) : φ → P ⊢ Q :=
+  λ hp => (sep_emp.mpr.trans (sep_mono .rfl (pure_intro hp))).trans (wand_elim h)
+
+elab "irevert" colGt hyp:ident : tactic => do
+  let (mvar, { u, prop, bi, e, hyps, goal, .. }) ← istart (← getMainGoal)
+
+  mvar.withContext do
+    let uniq? ← try? do pure (← hyps.findWithInfo hyp)
+    if let some uniq := uniq? then
+      let ⟨e', hyps', out, _, _, _, h⟩ := hyps.remove true uniq
+      let m : Q($e' ⊢ $out -∗ $goal) ← mkFreshExprSyntheticOpaqueMVar <|
+        IrisGoal.toExpr { hyps := hyps', goal := q(wand $out $goal), .. }
+
+      mvar.assign q(wand_revert $h $m)
+      replaceMainGoal [m.mvarId!]
+    else
+      let f ← getFVarId hyp
+      let some ldecl := (← getLCtx).find? f | throwError "irevert: {hyp.getId} not in scope"
+
+      let bibase : Q(BIBase $prop) := q(@BI.toBIBase $prop $bi)
+
+      let v : Level ← Meta.getLevel ldecl.type
+      have α : Q(Sort v) := ldecl.type
+
+      let (_, mvarId) ← mvar.revert #[f]
+      mvarId.withContext do
+        if ← Meta.isProp α then
+          have φ : Q(Prop) := α
+          let p : Q($prop) := q(@BI.pure $prop $bibase $φ)
+
+          let m : Q($e ⊢ $p -∗ $goal) ← mkFreshExprSyntheticOpaqueMVar <|
+            IrisGoal.toExpr { u, prop, bi, hyps, goal := q(wand $p $goal), .. }
+
+          let pf : Q($φ → ($e ⊢ $goal)) := q(pure_revert $m)
+
+          mvarId.assign pf
+          replaceMainGoal [m.mvarId!]
+        else
+          let Φ : Q($α → $prop) ← mapForallTelescope' (λ t _ => do
+            let (some ig) := parseIrisGoal? t | throwError "irevert: not in proof mode"
+            return ig.goal
+          ) (Expr.mvar mvarId)
+          let m : Q($e ⊢ ∀ x, $Φ x) ← mkFreshExprSyntheticOpaqueMVar <|
+            IrisGoal.toExpr { u, prop, bi, hyps, goal := q(BI.forall $Φ), ..}
+
+          let pf : Q(∀ (x : $α), $e ⊢ $Φ x) := q(forall_revert $m)
+
+          mvarId.assign pf
+          replaceMainGoal [m.mvarId!]
diff --git a/src/Iris/Tests/Tactics.lean b/src/Iris/Tests/Tactics.lean
index 48c610a47..30b9ff3a8 100644
--- a/src/Iris/Tests/Tactics.lean
+++ b/src/Iris/Tests/Tactics.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Lars König
+Authors: Lars König, Oliver Soeser
 -/
 import Iris.BI
 import Iris.ProofMode
@@ -115,6 +115,43 @@ theorem multiple_patterns [BI PROP] (Q : PROP) : ⊢ □ (P1 ∧ P2) -∗ Q ∨
 
 end intro
 
+-- revert
+namespace revert
+
+theorem spatial [BI PROP] (P Q : PROP) (H : ⊢ P -∗ Q) : P ⊢ Q := by
+  iintro HP
+  irevert HP
+  exact H
+
+theorem intuitionistic [BI PROP] (P : PROP) (H : ⊢ □ P -∗ P) : □ P ⊢ P := by
+  iintro □HP
+  irevert HP
+  exact H
+
+theorem pure [BI PROP] (P : PROP) (Hφ : φ) : ⊢ (⌜φ⌝ -∗ P) -∗ P := by
+  iintro H
+  irevert Hφ
+  iexact H
+
+theorem «forall» [BI PROP] (x : α) (Φ : α → PROP) : ⊢ (∀ x, Φ x) → Φ x := by
+  iintro H
+  irevert x
+  iexact H
+
+theorem multiple_spatial [BI PROP] (P Q : PROP) :
+    ⊢ (P -∗ P) -∗ P -∗ <affine> Q -∗ P := by
+  iintro H HP HQ
+  irevert HP
+  iexact H
+
+theorem multiple_intuitionistic [BI PROP] (P Q : PROP) :
+    ⊢ (□ P -∗ P) -∗ □ P -∗ <affine> Q -∗ P := by
+  iintro H □HP HQ
+  irevert HP
+  iexact H
+
+end revert
+
 -- exists
 namespace «exists»
 
diff --git a/tactics.md b/tactics.md
index 4b0d7b566..b769ec7d9 100644
--- a/tactics.md
+++ b/tactics.md
@@ -23,6 +23,7 @@
 | `ileft`<br>`iright`                    | Choose to prove the left (`ileft`) or right (`iright`) side of a disjunction in the goal.                                                                                                                                            |
 | `icases` *hyp* `with` *cases-pat*      | Destruct the hypothesis *hyp* using the cases pattern *cases-pat*.                                                                                                                                                                   |
 | `iintro` *cases-pats*                  | Introduce up to multiple hypotheses and destruct them using the cases patterns *cases-pats*.                                                                                                                                         |
+| `irevert` *hyp*                        | Revert the hypothesis *hyp*.                                                                                                                                                                                                         |
 
 ## Cases Patterns