diff --git a/src/Iris/BI/Lib/BUpdPlain.lean b/src/Iris/BI/Lib/BUpdPlain.lean
index 00f7080f..4bf1a6bf 100644
--- a/src/Iris/BI/Lib/BUpdPlain.lean
+++ b/src/Iris/BI/Lib/BUpdPlain.lean
@@ -33,14 +33,13 @@ instance BUpdPlain_ne : NonExpansive (BUpdPlain (PROP := PROP)) where
 theorem BUpdPlain_intro {P : PROP} : P ⊢ BUpdPlain P := by
   iintro Hp
   unfold BUpdPlain
-  iintro _ H
+  iintro %_ H
   iapply H $$ Hp
 
 theorem BUpdPlain_mono {P Q : PROP} : (P ⊢ Q) → (BUpdPlain P ⊢ BUpdPlain Q) := by
   intros H
   unfold BUpdPlain
-  iintro R HQR
-  iintro Hp
+  iintro R %HQR Hp
   have H1 : ⊢ iprop(Q -∗ ■ HQR) -∗ iprop(P -∗ ■ HQR) := by
     iintro H Hp
     iapply H
@@ -50,14 +49,14 @@ theorem BUpdPlain_mono {P Q : PROP} : (P ⊢ Q) → (BUpdPlain P ⊢ BUpdPlain Q
 
 theorem BUpdPlain_idemp {P : PROP} : BUpdPlain (BUpdPlain P) ⊢ BUpdPlain P := by
   unfold BUpdPlain
-  iintro Hp R H
+  iintro Hp %R H
   iapply Hp
   iintro Hp
   iapply Hp $$ H
 
 theorem BUpdPlain_frame_r {P Q : PROP} : BUpdPlain P ∗ Q ⊢ (BUpdPlain iprop(P ∗ Q)) := by
   unfold BUpdPlain
-  iintro ⟨Hp, Hq⟩ R H
+  iintro ⟨Hp, Hq⟩ %R H
   iapply Hp
   iintro Hp
   iapply H
@@ -74,7 +73,7 @@ theorem BUpdPlain_plainly {P : PROP} : BUpdPlain iprop(■ P) ⊢ (■ P) := by
 /- BiBUpdPlainly entails the alternative definition -/
 theorem BUpd_BUpdPlain [BIUpdate PROP] [BIBUpdatePlainly PROP] {P : PROP} : (|==> P) ⊢ BUpdPlain P := by
   unfold BUpdPlain
-  iintro _ _ _
+  iintro _ %_ _
   refine BIUpdate.frame_r.trans ?_
   refine (BIUpdate.mono sep_symm).trans ?_
   exact (BIUpdate.mono <| wand_elim .rfl).trans bupd_elim
@@ -89,12 +88,11 @@ theorem own_updateP [UCMRA M] {own : M → PROP} {x : M} {Φ : M → Prop}
     own x ⊢ BUpdPlain iprop(∃ y, ⌜Φ y⌝ ∧ own y) := by
   iintro Hx
   unfold BUpdPlain
-  iintro R H
+  iintro %R H
   iapply own_updateP_plainly x Φ R Hup
   isplitl [Hx]
   · iexact Hx
-  iintro y ⌜HΦ⌝
-  iintro Hy
+  iintro %y %HΦ Hy
   iapply H
   iexists y
   isplit
diff --git a/src/Iris/Examples/IProp.lean b/src/Iris/Examples/IProp.lean
index 8760310c..8027274b 100644
--- a/src/Iris/Examples/IProp.lean
+++ b/src/Iris/Examples/IProp.lean
@@ -42,11 +42,8 @@ example : ⊢ |==> ∃ (γ0 γ1 : GName) (s0 s1 : String),
 
   -- Complete the Iris proof
   istart
-  iintro ⟨⟨γ0, Hγ0⟩, ⟨γ1, Hγ1⟩, -⟩
-  iexists γ0
-  iexists γ1
-  iexists "string0"
-  iexists "string1"
+  iintro ⟨⟨%γ0, Hγ0⟩, ⟨%γ1, Hγ1⟩, -⟩
+  iexists γ0, γ1, "string0", "string1"
   isplitl [Hγ0]
   · iexact Hγ0
   · iexact Hγ1
diff --git a/src/Iris/Examples/Proofs.lean b/src/Iris/Examples/Proofs.lean
index 106fac2e..e742de19 100644
--- a/src/Iris/Examples/Proofs.lean
+++ b/src/Iris/Examples/Proofs.lean
@@ -14,7 +14,7 @@ theorem proof_example_1 [BI PROP] (P Q R : PROP) (Φ : α → PROP) :
 := by
   iintro ⟨HP, HQ, □HR⟩ □HRΦ
   ihave HΦ := HRΦ $$ HR
-  icases HΦ with ⟨x, _HΦ⟩
+  icases HΦ with ⟨%x, _HΦ⟩
   iexists x
   isplitr
   · iassumption
diff --git a/src/Iris/ProofMode/Expr.lean b/src/Iris/ProofMode/Expr.lean
index 08dc2365..80c3bce7 100644
--- a/src/Iris/ProofMode/Expr.lean
+++ b/src/Iris/ProofMode/Expr.lean
@@ -5,10 +5,11 @@ Authors: Lars König, Mario Carneiro
 -/
 import Qq
 import Iris.BI
-import Iris.Std.Expr
+import Iris.ProofMode.Classes
+import Iris.Std
 
 namespace Iris.ProofMode
-open Iris.BI
+open Iris.BI Iris.Std
 open Lean Lean.Expr Lean.Meta Qq
 
 @[match_pattern] def nameAnnotation := `name
@@ -26,6 +27,8 @@ def getFreshName : TSyntax ``binderIdent → CoreM (Name × Syntax)
   | `(binderIdent| $name:ident) => pure (name.getId, name)
   | stx => return (← mkFreshUserName `x, stx)
 
+section hyps
+
 inductive Hyps {prop : Q(Type u)} (bi : Q(BI $prop)) : (e : Q($prop)) → Type where
   | emp (_ : $e =Q emp) : Hyps bi e
   | sep (tm elhs erhs : Q($prop)) (_ : $e =Q iprop($elhs ∗ $erhs))
@@ -89,6 +92,231 @@ partial def Hyps.find? {u prop bi} (name : Name) :
   | _, .hyp _ name' uniq p ty _ => if name == name' then (uniq, p, ty) else none
   | _, .sep _ _ _ _ lhs rhs => rhs.find? name <|> lhs.find? name
 
+variable (oldUniq new : Name) {prop : Q(Type u)} {bi : Q(BI $prop)} in
+def Hyps.rename : ∀ {e}, Hyps bi e → Option (Hyps bi e)
+  | _, .emp _ => none
+  | _, .sep _ _ _ _ lhs rhs =>
+    match rhs.rename with
+    | some rhs' => some (.mkSep lhs rhs' _)
+    | none => match lhs.rename with
+      | some lhs' => some (.mkSep lhs' rhs _)
+      | none => none
+  | _, .hyp _ _ uniq p ty _ =>
+    if oldUniq == uniq then some (Hyps.mkHyp bi new uniq p ty _) else none
+
+def Hyps.select (ty : Expr) : ∀ {s}, @Hyps u prop bi s → MetaM (Name × Q(Bool) × Q($prop))
+  | _, .emp _ => failure
+  | _, .hyp _ _ uniq p ty' _ => do
+    let .true ← isDefEq ty ty' | failure
+    pure (uniq, p, ty')
+  | _, .sep _ _ _ _ lhs rhs => try Hyps.select ty rhs catch _ => Hyps.select ty lhs
+
+
+private theorem intuitionistically_sep_dup [BI PROP] {P : PROP} : □ P ⊣⊢ □ P ∗ □ P :=
+  intuitionistically_sep_idem.symm
+
+private theorem sep_emp_rev [BI PROP] {P : PROP} : P ⊣⊢ P ∗ emp := sep_emp.symm
+
+private theorem emp_sep_rev [BI PROP] {P : PROP} : P ⊣⊢ emp ∗ P := emp_sep.symm
+
+section split
+
+private theorem split_es [BI PROP] {Q Q1 Q2 : PROP} (h : Q ⊣⊢ Q1 ∗ Q2) : emp ∗ Q ⊣⊢ Q1 ∗ Q2 :=
+  emp_sep.trans h
+private theorem split_ls [BI PROP] {P Q Q1 Q2 : PROP} (h : Q ⊣⊢ Q1 ∗ Q2) : P ∗ Q ⊣⊢ (P ∗ Q1) ∗ Q2 :=
+  (sep_congr_r h).trans sep_assoc.symm
+private theorem split_rs [BI PROP] {P Q Q1 Q2 : PROP} (h : Q ⊣⊢ Q1 ∗ Q2) : P ∗ Q ⊣⊢ Q1 ∗ (P ∗ Q2) :=
+  (sep_congr_r h).trans sep_left_comm
+private theorem split_se [BI PROP] {P P1 P2 : PROP} (h : P ⊣⊢ P1 ∗ P2) : P ∗ emp ⊣⊢ P1 ∗ P2 :=
+  sep_emp.trans h
+private theorem split_sl [BI PROP] {P Q P1 P2 : PROP} (h : P ⊣⊢ P1 ∗ P2) : P ∗ Q ⊣⊢ (P1 ∗ Q) ∗ P2 :=
+  (sep_congr_l h).trans sep_right_comm
+private theorem split_sr [BI PROP] {P Q P1 P2 : PROP} (h : P ⊣⊢ P1 ∗ P2) : P ∗ Q ⊣⊢ P1 ∗ (P2 ∗ Q) :=
+  (sep_congr_l h).trans sep_assoc
+private theorem split_ss [BI PROP] {P Q P1 P2 Q1 Q2 : PROP}
+    (h1 : P ⊣⊢ P1 ∗ P2) (h2 : Q ⊣⊢ Q1 ∗ Q2) : P ∗ Q ⊣⊢ (P1 ∗ Q1) ∗ (P2 ∗ Q2) :=
+  (sep_congr h1 h2).trans sep_sep_sep_comm
+
+private inductive SplitResult {prop : Q(Type u)} (bi : Q(BI $prop)) (e : Q($prop)) where
+  | emp (_ : $e =Q BI.emp)
+  | left
+  | right
+  | split {elhs erhs : Q($prop)} (lhs : Hyps bi elhs) (rhs : Hyps bi erhs)
+          (pf : Q($e ⊣⊢ $elhs ∗ $erhs))
+
+variable {prop : Q(Type u)} (bi : Q(BI $prop)) (toRight : Name → Name → Bool) in
+private def Hyps.splitCore : ∀ {e}, Hyps bi e → SplitResult bi e
+  | _, .emp _ => .emp ⟨⟩
+  | ehyp, h@(.hyp _ name uniq b ty _) =>
+    match matchBool b with
+    | .inl _ =>
+      have : $ehyp =Q iprop(□ $ty) := ⟨⟩
+      .split h h q(intuitionistically_sep_dup)
+    | .inr _ => if toRight name uniq then .right else .left
+  | _, .sep _ _ _ _ lhs rhs =>
+    let resl := lhs.splitCore
+    let resr := rhs.splitCore
+    match resl, resr with
+    | .emp _, .emp _ | .left, .emp _ | .emp _, .left | .left, .left => .left
+    | .right, .emp _ | .emp _, .right | .right, .right => .right
+    | .left, .right => .split lhs rhs q(.rfl)
+    | .right, .left => .split rhs lhs q(sep_comm)
+    | .emp _, .split r1 r2 rpf => .split r1 r2 q(split_es $rpf)
+    | .left, .split r1 r2 rpf => .split (lhs.mkSep r1) r2 q(split_ls $rpf)
+    | .right, .split r1 r2 rpf => .split r1 (lhs.mkSep r2) q(split_rs $rpf)
+    | .split l1 l2 lpf, .emp _ => .split l1 l2 q(split_se $lpf)
+    | .split l1 l2 lpf, .left => .split (l1.mkSep rhs) l2 q(split_sl $lpf)
+    | .split l1 l2 lpf, .right => .split l1 (l2.mkSep rhs) q(split_sr $lpf)
+    | .split l1 l2 lpf, .split r1 r2 rpf => .split (l1.mkSep r1) (l2.mkSep r2) q(split_ss $lpf $rpf)
+
+def Hyps.split {prop : Q(Type u)} (bi : Q(BI $prop)) (toRight : Name → Name → Bool)
+    {e} (hyps : Hyps bi e) :
+    (elhs erhs : Q($prop)) × Hyps bi elhs × Hyps bi erhs × Q($e ⊣⊢ $elhs ∗ $erhs) :=
+  match hyps.splitCore bi toRight with
+  | .emp _ => ⟨_, _, hyps, hyps, q(sep_emp_rev)⟩
+  | .left => ⟨_, _, hyps, .mkEmp bi, q(sep_emp_rev)⟩
+  | .right => ⟨_, _, .mkEmp bi, hyps, q(emp_sep_rev)⟩
+  | .split lhs rhs pf => ⟨_, _, lhs, rhs, pf⟩
+
+end split
+
+section remove
+
+structure RemoveHyp {prop : Q(Type u)} (bi : Q(BI $prop)) (e : Q($prop)) where
+  (e' : Q($prop)) (hyps' : Hyps bi e') (out out' : Q($prop)) (p : Q(Bool))
+  (eq : $out =Q iprop(□?$p $out'))
+  (pf : Q($e ⊣⊢ $e' ∗ $out))
+  deriving Inhabited
+
+private inductive RemoveHypCore {prop : Q(Type u)} (bi : Q(BI $prop)) (e : Q($prop)) (α : Type) where
+  | none
+  | one (a : α) (out' : Q($prop)) (p : Q(Bool)) (eq : $e =Q iprop(□?$p $out'))
+  | main (a : α) (_ : RemoveHyp bi e)
+
+private theorem remove_l [BI PROP] {P P' Q R : PROP} (h : P ⊣⊢ P' ∗ R) :
+    P ∗ Q ⊣⊢ (P' ∗ Q) ∗ R :=
+  (sep_congr_l h).trans sep_right_comm
+
+private theorem remove_r [BI PROP] {P Q Q' R : PROP} (h : Q ⊣⊢ Q' ∗ R) :
+    P ∗ Q ⊣⊢ (P ∗ Q') ∗ R :=
+  (sep_congr_r h).trans sep_assoc.symm
+
+variable [Monad m] {prop : Q(Type u)} (bi : Q(BI $prop)) (rp : Bool)
+  (check : Name → Name → Q(Bool) → Q($prop) → m (Option α)) in
+/-- If `rp` is true, the hyp will be removed even if it is in the intuitionistic context. -/
+private def Hyps.removeCore : ∀ {e}, Hyps bi e → m (RemoveHypCore bi e α)
+  | _, .emp _ => pure .none
+  | e, h@(.hyp _ name uniq p ty _) => do
+    if let some a ← check name uniq p ty then
+      match matchBool p, rp with
+      | .inl _, false =>
+        have : $e =Q iprop(□ $ty) := ⟨⟩
+        return .main a ⟨e, h, e, ty, q(true), ⟨⟩, q(intuitionistically_sep_dup)⟩
+      | _, _ => return .one a ty p ⟨⟩
+    else
+      return .none
+  | _, .sep _ elhs erhs _ lhs rhs => do
+    match ← rhs.removeCore with
+    | .one a out' p h =>
+      return .main a ⟨elhs, lhs, erhs, out', p, h, q(.rfl)⟩
+    | .main a ⟨_, rhs', out, out', p, h, pf⟩ =>
+      let hyps' := .mkSep lhs rhs'
+      return .main a ⟨_, hyps', out, out', p, h, q(remove_r $pf)⟩
+    | .none => match ← lhs.removeCore with
+      | .one a out' p h =>
+        return .main a ⟨erhs, rhs, elhs, out', p, h, q(sep_comm)⟩
+      | .main a ⟨_, lhs', out, out', p, h, pf⟩ =>
+        let hyps' := .mkSep lhs' rhs
+        return .main a ⟨_, hyps', out, out', p, h, q(remove_l $pf)⟩
+      | .none => pure .none
+
+def Hyps.removeG [Monad m] {prop : Q(Type u)} {bi : Q(BI $prop)} {e : Q(Prop)}
+    (rp : Bool) (hyps : Hyps bi e)
+    (check : Name → Name → Q(Bool) → Q($prop) → m (Option α)) :
+    m (Option (α × RemoveHyp bi e)) := do
+  match ← hyps.removeCore bi rp check with
+  | .none => return none
+  | .one a out' p h => return some ⟨a, _, .mkEmp bi, e, out', p, h, q(emp_sep_rev)⟩
+  | .main a res => return some (a, res)
+
+def Hyps.remove {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
+    (rp : Bool) (hyps : Hyps bi e) (uniq : Name) : RemoveHyp bi e :=
+  match Id.run (hyps.removeG rp fun _ uniq' _ _ => if uniq == uniq' then some () else none) with
+  | some (_, r) => r
+  | none => panic! "variable not found"
+
+end remove
+
+section replace
+
+-- TODO: What to do with this? Is this necessary? Should this be a general abstraction?
+def Replaces [BI PROP] (K A B : PROP) := (B -∗ K) ⊢ (A -∗ K)
+
+theorem Replaces.apply [BI PROP] {P P' Q : PROP}
+    (h : Replaces Q P P') (h_entails : P' ⊢ Q) : P ⊢ Q :=
+  wand_entails <| (entails_wand h_entails).trans h
+
+theorem replaces_r [BI PROP] {K P Q Q' : PROP} (h : Replaces K Q Q') :
+    Replaces K iprop(P ∗ Q) iprop(P ∗ Q') :=
+  wand_intro <| sep_assoc.2.trans <| wand_elim <|
+  (wand_intro <| sep_assoc.1.trans wand_elim_l).trans h
+
+theorem replaces_l [BI PROP] {K P P' Q : PROP} (h : Replaces K P P') :
+    Replaces K iprop(P ∗ Q) iprop(P' ∗ Q) :=
+  (wand_mono_l sep_comm.1).trans <| (replaces_r h).trans (wand_mono_l sep_comm.1)
+
+theorem to_persistent_spatial [BI PROP] {P P' Q : PROP}
+    [hP : IntoPersistently false P P'] [or : TCOr (Affine P) (Absorbing Q)] :
+    Replaces Q P iprop(□ P') :=
+  match or with
+  | TCOr.l => wand_mono_l <| (affine_affinely P).2.trans (affinely_mono hP.1)
+  | TCOr.r =>
+    wand_intro <| (sep_mono_r <| hP.1.trans absorbingly_intuitionistically.2).trans <|
+    absorbingly_sep_r.1.trans <| (absorbingly_mono wand_elim_l).trans absorbing
+
+theorem to_persistent_intuitionistic [BI PROP] {P P' Q : PROP}
+    [hP : IntoPersistently true P P'] : Replaces Q iprop(□ P) iprop(□ P') :=
+  wand_mono_l <| affinely_mono hP.1
+
+theorem from_affine [BI PROP] {p : Bool} {P P' Q : PROP} [hP : FromAffinely P' P p] :
+    Replaces Q iprop(□?p P) P' :=
+  wand_mono_l <| affinelyIf_of_intuitionisticallyIf.trans hP.1
+
+inductive ReplaceHyp {prop : Q(Type u)} (bi : Q(BI $prop)) (Q : Q($prop)) where
+  | none
+  | unchanged (ehyps') (hyps' : Hyps bi ehyps')
+  | main (e e' : Q($prop)) (hyps' : Hyps bi e') (pf : Q(Replaces $Q $e $e'))
+
+variable [Monad m] [MonadLiftT MetaM m] {prop : Q(Type u)} (bi : Q(BI $prop)) (Q : Q($prop))
+  (uniq : Name) (repl : Name → Q(Bool) → Q($prop) → m (ReplaceHyp bi Q)) in
+def Hyps.replace : ∀ {e}, Hyps bi e → m (ReplaceHyp bi Q)
+  | _, .emp _ => pure .none
+  | _, .hyp _ name uniq' p ty _ => do
+    if uniq == uniq' then
+      let res ← repl name p ty
+      if let .main e e' hyps' _ := res then
+        let e' ← instantiateMVarsQ e'
+        if e == e' then
+          return .unchanged _ hyps'
+      return res
+    else return .none
+  | _, .sep _ elhs erhs _ lhs rhs => do
+    match ← rhs.replace with
+    | .unchanged _ rhs' => return .unchanged _ (.mkSep lhs rhs')
+    | .main erhs₀ _ rhs' pf =>
+      let hyps' := .mkSep lhs rhs'
+      return .main q(iprop($elhs ∗ $erhs₀)) _ hyps' q(replaces_r $pf)
+    | .none => match ← lhs.replace with
+      | .unchanged _ lhs' => return .unchanged _ (.mkSep lhs' rhs)
+      | .main elhs₀ _ lhs' pf =>
+        let hyps' := .mkSep lhs' rhs
+        return .main q(iprop($elhs₀ ∗ $erhs)) _ hyps' q(replaces_l $pf)
+      | .none => pure .none
+
+end replace
+
+end hyps
+
 /-- This is the same as `Entails`, but it takes a `BI` instead.
 This constant is used to detect iris proof goals. -/
 abbrev Entails' [BI PROP] : PROP → PROP → Prop := Entails
@@ -144,7 +372,7 @@ def addHypInfo (stx : Syntax) (name uniq : Name) (prop : Q(Type u)) (ty : Q($pro
 
 /-- Hyps.findWithInfo should be used on names obtained from the syntax of a tactic to highlight them correctly. -/
 def Hyps.findWithInfo {u prop bi} (hyps : @Hyps u prop bi s) (name : Ident) : MetaM Name := do
-  let some (uniq, _, ty) := hyps.find? name.getId | throwError "unknown hypothesis"
+  let some (uniq, _, ty) := hyps.find? name.getId | throwError "unknown hypothesis {name}"
   addHypInfo name name.getId uniq prop ty
   pure uniq
 
diff --git a/src/Iris/ProofMode/Goals.lean b/src/Iris/ProofMode/Goals.lean
deleted file mode 100644
index 2ac3ce6e..00000000
--- a/src/Iris/ProofMode/Goals.lean
+++ /dev/null
@@ -1,45 +0,0 @@
-/-
-Copyright (c) 2025 Michael Sammler. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Michael Sammler
--/
-import Iris.ProofMode.Expr
-
-namespace Iris.ProofMode
-open Lean Elab Tactic Meta Qq BI Std
-
-structure Goals {prop : Q(Type u)} (bi : Q(BI $prop)) where
-  goals : IO.Ref (Array MVarId)
-
-def Goals.new {prop : Q(Type u)} (bi : Q(BI $prop)) : BaseIO (Goals bi) :=
-  do return {goals := ← IO.mkRef #[]}
-
-def Goals.addGoal {prop : Q(Type u)} {bi : Q(BI $prop)} (g : Goals bi)
-    {e} (hyps : Hyps bi e) (goal : Q($prop)) (name : Name := .anonymous) : MetaM Q($e ⊢ $goal) := do
-  let m : Q($e ⊢ $goal) ← mkFreshExprSyntheticOpaqueMVar <|
-    IrisGoal.toExpr { prop, bi, hyps, goal, .. }
-  m.mvarId!.setUserName name
-  g.goals.modify (·.push m.mvarId!)
-  pure m
-
-def Goals.addPureGoal {prop : Q(Type u)} {bi : Q(BI $prop)} (g : Goals bi)
-    (m : MVarId) (name : Name := .anonymous) : MetaM Unit := do
-  if ← m.isAssignedOrDelayedAssigned then
-    return
-  if (← g.goals.get).contains m then
-    return
-  -- don't override an existing name, e.g. for ?_
-  if !name.isAnonymous then
-    m.setUserName name
-  g.goals.modify (·.push m)
-
--- TODO: change this to replace main goal that deduplicates goals
-def Goals.getGoals {prop : Q(Type u)} {bi : Q(BI $prop)} (g : Goals bi) : TermElabM (List MVarId) := do
-  let goals ← g.goals.get
-  -- put the goals that depend on other goals last
-  let mvars ← goals.foldlM (λ m g => do
-    return m ∪ (← g.getMVarDependencies)) ∅
-  let (dep, nonDep) := goals.partition (λ x => mvars.contains x)
-  -- TODO: Is this the right place to do this?
-  Term.synthesizeSyntheticMVarsNoPostponing
-  return (nonDep ++ dep).toList
diff --git a/src/Iris/ProofMode/Instances.lean b/src/Iris/ProofMode/Instances.lean
index c191e3c4..183a79b4 100644
--- a/src/Iris/ProofMode/Instances.lean
+++ b/src/Iris/ProofMode/Instances.lean
@@ -75,6 +75,20 @@ instance intoWand_persistently_false (q : Bool) [BI PROP] ioP ioQ (R P Q : PROP)
 -- FromForall
 instance fromForall_forall [BI PROP] (Φ : α → PROP) : FromForall (BIBase.forall Φ) Φ := ⟨.rfl⟩
 
+instance fromForall_impl_pure [BI PROP] (P Q : PROP) φ
+  [IntoPure P φ] :
+  FromForall iprop(P → Q) (λ _ : φ => Q) where
+  from_forall := imp_intro <| (and_mono_r into_pure).trans <| pure_elim_r forall_elim
+
+instance fromForall_wand_pure [BI PROP] (P Q : PROP) φ
+  [IntoPure P φ] [inst : TCOr (Affine P) (Absorbing Q)] :
+  FromForall iprop(P -∗ Q) (λ _ : φ => Q) where
+  from_forall := wand_intro <|
+    pure_elim _ ((sep_mono_r into_pure).trans sep_elim_r) fun h =>
+      match inst with
+      | .l (t := _) => sep_elim_l |>.trans (forall_elim h)
+      | .r (u := _) => sep_elim_l |>.trans (forall_elim h)
+
 -- IntoForall
 instance intoForall_forall [BI PROP] (Φ : α → PROP) : IntoForall iprop(∀ a, Φ a) Φ := ⟨.rfl⟩
 
@@ -132,6 +146,22 @@ instance intoExists_intuitionistically [BI PROP] (P : PROP) (Φ : α → PROP) [
     IntoExists iprop(□ P) (fun a => iprop(□ (Φ a))) where
   into_exists := (intuitionistically_mono h.1).trans intuitionistically_exists.1
 
+@[ipm_backtrack]
+instance (priority := default - 10) intoExist_and_pure [BI PROP] (PQ P Q : PROP) (Φ : Prop)
+  [IntoAnd false PQ P Q] [IntoPure P Φ] :
+  IntoExists PQ (λ _ : Φ => Q) where
+  into_exists :=
+    (into_and (p:=false) (P:=PQ)).trans
+      <| (and_mono_l into_pure).trans (pure_elim_l (λ h =>
+              exists_intro (Ψ:=λ _ => Q) h))
+
+instance intoExist_sep_pure [BI PROP] (P Q : PROP) (Φ : Prop)
+  [IntoPure P Φ] [TCOr (Affine P) (Absorbing Q)]:
+  IntoExists iprop(P ∗ Q) (λ _ : Φ => Q) where
+  into_exists :=
+    (pure_elim _ ((sep_mono_l into_pure).trans sep_elim_l) (λ h =>
+              sep_elim_r.trans <| exists_intro (Ψ:=λ _ => Q) h))
+
 instance intoExists_absorbingly [BI PROP] (P : PROP) (Φ : α → PROP) [h : IntoExists P Φ] :
     IntoExists iprop(<absorb> P) (fun a => iprop(<absorb> (Φ a))) where
   into_exists := (absorbingly_mono h.1).trans absorbingly_exists.1
@@ -144,6 +174,7 @@ instance intoExists_persistently [BI PROP] {P : PROP} (Φ : α → PROP) [h : In
 instance (priority := default - 10) fromAnd_and [BI PROP] (P1 P2 : PROP) :
     FromAnd iprop(P1 ∧ P2) P1 P2 := ⟨.rfl⟩
 
+@[ipm_backtrack]
 instance (priority := default + 30) fromAnd_sep_persistent_l [BI PROP] (P1 P1' P2 : PROP)
     [Persistent P1] [h : IntoAbsorbingly P1' P1] : FromAnd iprop(P1 ∗ P2) P1' P2 where
   from_and := by
@@ -151,6 +182,7 @@ instance (priority := default + 30) fromAnd_sep_persistent_l [BI PROP] (P1 P1' P
       sep_mono_l <| (affinely_mono ?_).trans intuitionistically_elim
     exact (absorbingly_mono persistent).trans absorbingly_persistently.1
 
+@[ipm_backtrack]
 instance (priority := default + 20) fromAnd_sep_persistent_r [BI PROP] (P1 P2 P2' : PROP)
     [Persistent P2] [h : IntoAbsorbingly P2' P2] : FromAnd iprop(P1 ∗ P2) P1 P2' where
   from_and := by
@@ -174,11 +206,13 @@ instance (priority := default + 10) fromAnd_persistently_sep [BI PROP] (P Q1 Q2
 instance (priority := default - 10) intoAnd_and (p : Bool) [BI PROP] (P Q : PROP) :
     IntoAnd p iprop(P ∧ Q) P Q := ⟨.rfl⟩
 
+@[ipm_backtrack]
 instance intoAnd_and_affine_l [BI PROP] (P Q Q' : PROP) [Affine P]
     [h : FromAffinely Q' Q] : IntoAnd false iprop(P ∧ Q) P Q' where
   into_and := (and_mono_l (affine_affinely _).2).trans <|
     affinely_and_l.1.trans <| affinely_and.1.trans <| and_mono (affine_affinely _).1 h.1
 
+@[ipm_backtrack]
 instance intoAnd_and_affine_r [BI PROP] (P P' Q : PROP) [Affine Q]
     [h : FromAffinely P' P] : IntoAnd false iprop(P ∧ Q) P' Q where
   into_and := (and_mono_r (affine_affinely _).2).trans <|
@@ -242,6 +276,7 @@ instance (priority := default + 10) fromSep_persistently [BI PROP] (P Q1 Q2 : PR
   from_sep := persistently_sep_2.trans (persistently_mono h.1)
 
 -- AndIntoSep
+@[ipm_class]
 class inductive AndIntoSep [BI PROP] : PROP → PROP → PROP → PROP → Prop
   | affine (P Q Q' : PROP) [Affine P] [h : FromAffinely Q' Q] : AndIntoSep P P Q Q'
   | affinely (P Q : PROP) : AndIntoSep P iprop(<affine> P) Q Q
@@ -252,6 +287,7 @@ attribute [instance] AndIntoSep.affine AndIntoSep.affinely
 instance intoSep_sep [BI PROP] (P Q : PROP) : IntoSep iprop(P ∗ Q) P Q := ⟨.rfl⟩
 
 set_option synthInstance.checkSynthOrder false in
+@[ipm_backtrack]
 instance intoSep_and_persistent_l [BI PROP] (P Q P' Q' : PROP) [Persistent P]
     [inst : AndIntoSep P P' Q Q'] : IntoSep iprop(P ∧ Q) P' Q' where
   into_sep :=
@@ -262,6 +298,7 @@ instance intoSep_and_persistent_l [BI PROP] (P Q P' Q' : PROP) [Persistent P]
     | _, AndIntoSep.affinely .. => persistent_and_affinely_sep_l_1
 
 set_option synthInstance.checkSynthOrder false in
+@[ipm_backtrack]
 instance intoSep_and_persistent_r [BI PROP] (P Q P' Q' : PROP) [Persistent Q]
     [inst : AndIntoSep Q Q' P P'] : IntoSep iprop(P ∧ Q) P' Q' where
   into_sep :=
@@ -359,6 +396,7 @@ instance (priority := default - 10) intoPersistently_persistent [BI PROP] (P : P
   into_persistently := h.1
 
 -- FromAffinely
+@[ipm_backtrack]
 instance fromAffinely_affine [BI PROP] (P : PROP) [Affine P] : FromAffinely P P true where
   from_affinely := affinely_elim
 
diff --git a/src/Iris/ProofMode/Patterns.lean b/src/Iris/ProofMode/Patterns.lean
index 64b2e896..3125976c 100644
--- a/src/Iris/ProofMode/Patterns.lean
+++ b/src/Iris/ProofMode/Patterns.lean
@@ -1,3 +1,4 @@
 import Iris.ProofMode.Patterns.CasesPattern
+import Iris.ProofMode.Patterns.IntroPattern
 import Iris.ProofMode.Patterns.ProofModeTerm
 import Iris.ProofMode.Patterns.SpecPattern
diff --git a/src/Iris/ProofMode/Patterns/CasesPattern.lean b/src/Iris/ProofMode/Patterns/CasesPattern.lean
index df1ddfa5..9bd87e03 100644
--- a/src/Iris/ProofMode/Patterns/CasesPattern.lean
+++ b/src/Iris/ProofMode/Patterns/CasesPattern.lean
@@ -14,20 +14,22 @@ syntax binderIdent : icasesPat
 syntax "-" : icasesPat
 syntax "⟨" icasesPatAlts,* "⟩" : icasesPat
 syntax "(" icasesPatAlts ")" : icasesPat
-syntax "⌜" icasesPat "⌝" : icasesPat
+syntax "⌜" binderIdent "⌝" : icasesPat
 syntax "□" icasesPat : icasesPat
 syntax "∗" icasesPat : icasesPat
 
-macro "%" pat:icasesPat : icasesPat => `(icasesPat| ⌜$pat⌝)
+macro "%" pat:binderIdent : icasesPat => `(icasesPat| ⌜$pat⌝)
 macro "#" pat:icasesPat : icasesPat => `(icasesPat| □ $pat)
 macro "*" pat:icasesPat : icasesPat => `(icasesPat| ∗ $pat)
 
+-- TODO: attach syntax to iCasesPat such that one can use withRef to
+-- associate the errors with the right part of the syntax
 inductive iCasesPat
   | one (name : TSyntax ``binderIdent)
   | clear
   | conjunction (args : List iCasesPat)
   | disjunction (args : List iCasesPat)
-  | pure           (pat : iCasesPat)
+  | pure           (pat : TSyntax ``binderIdent)
   | intuitionistic (pat : iCasesPat)
   | spatial        (pat : iCasesPat)
   deriving Repr, Inhabited
@@ -41,7 +43,7 @@ where
   | `(icasesPat| $name:binderIdent) => some <| .one name
   | `(icasesPat| -) => some <| .clear
   | `(icasesPat| ⟨$[$args],*⟩) => args.mapM goAlts |>.map (.conjunction ·.toList)
-  | `(icasesPat| ⌜$pat⌝) => go pat |>.map .pure
+  | `(icasesPat| ⌜$pat⌝) => some <| .pure pat
   | `(icasesPat| □$pat) => go pat |>.map .intuitionistic
   | `(icasesPat| ∗$pat) => go pat |>.map .spatial
   | `(icasesPat| ($pat)) => goAlts pat
diff --git a/src/Iris/ProofMode/Patterns/IntroPattern.lean b/src/Iris/ProofMode/Patterns/IntroPattern.lean
new file mode 100644
index 00000000..fb43da3c
--- /dev/null
+++ b/src/Iris/ProofMode/Patterns/IntroPattern.lean
@@ -0,0 +1,22 @@
+/-
+Copyright (c) 2025 Michael Sammler. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michael Sammler
+-/
+import Iris.ProofMode.Patterns.CasesPattern
+
+namespace Iris.ProofMode
+open Lean
+
+declare_syntax_cat introPat
+
+syntax icasesPat : introPat
+
+inductive IntroPat
+  | intro (case : iCasesPat)
+  deriving Repr, Inhabited
+
+partial def IntroPat.parse (term : Syntax) : MacroM (Syntax × IntroPat) := do
+  match ← expandMacros term with
+  | `(introPat| $case:icasesPat) => return (term, .intro (← iCasesPat.parse case))
+  | _ => Macro.throwUnsupported
diff --git a/src/Iris/ProofMode/ProofModeM.lean b/src/Iris/ProofMode/ProofModeM.lean
new file mode 100644
index 00000000..b0b0b4a6
--- /dev/null
+++ b/src/Iris/ProofMode/ProofModeM.lean
@@ -0,0 +1,95 @@
+/-
+Copyright (c) 2025 Michael Sammler. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michael Sammler
+-/
+import Iris.ProofMode.Expr
+import Iris.ProofMode.Classes
+
+namespace Iris.ProofMode
+open Lean Elab Tactic Meta Qq BI Std
+
+structure ProofModeM.State where
+  goals : Array MVarId := #[]
+
+abbrev ProofModeM := StateRefT ProofModeM.State TacticM
+
+/-
+Make the compiler generate specialized `pure`/`bind` so we do not have to optimize through the
+whole monad stack at every use site. May eventually be covered by `deriving`.
+-/
+@[always_inline]
+instance : Monad ProofModeM :=
+  let i := inferInstanceAs (Monad ProofModeM)
+  { pure := i.pure, bind := i.bind }
+
+instance : Inhabited (ProofModeM α) where
+  default := throw default
+
+def addBIGoal {prop : Q(Type u)} {bi : Q(BI $prop)}
+    {e} (hyps : Hyps bi e) (goal : Q($prop)) (name : Name := .anonymous) : ProofModeM Q($e ⊢ $goal) := do
+  let m : Q($e ⊢ $goal) ← mkFreshExprSyntheticOpaqueMVar <|
+    IrisGoal.toExpr { prop, bi, hyps, goal, .. }
+  m.mvarId!.setUserName name
+  modify ({goals := ·.goals.push m.mvarId!})
+  pure m
+
+def addMVarGoal (m : MVarId) (name : Name := .anonymous) : ProofModeM Unit := do
+  if ← m.isAssignedOrDelayedAssigned then
+    return
+  if (← getThe ProofModeM.State).goals.contains m then
+    return
+  -- don't override an existing name, e.g. for ?_
+  if !name.isAnonymous then
+    m.setUserName name
+  modify ({goals := ·.goals.push m})
+
+def ProofModeM.trySynthInstanceQ (α : Q(Sort v)) : ProofModeM (Option Q($α)) := do
+  let LOption.some (e, mvars) ← ProofMode.trySynthInstance α | return none
+  mvars.forM addMVarGoal
+  return some e
+
+def ProofModeM.synthInstanceQ (α : Q(Sort v)) : ProofModeM Q($α) := do
+  let (e, mvars) ← ProofMode.synthInstance α
+  mvars.forM addMVarGoal
+  return e
+
+def istart (mvar : MVarId) : MetaM (MVarId × IrisGoal) := mvar.withContext do
+  -- parse goal
+  let goal ← instantiateMVars <| ← mvar.getType
+
+  -- check if already in proof mode
+  if let some irisGoal := parseIrisGoal? goal then
+    return (mvar, irisGoal)
+
+  let some goal ← checkTypeQ goal q(Prop)
+    | throwError "type mismatch\n{← mkHasTypeButIsExpectedMsg (← inferType goal) q(Prop)}"
+  let u ← mkFreshLevelMVar
+  let prop ← mkFreshExprMVarQ q(Type u)
+  let P ← mkFreshExprMVarQ q($prop)
+  let bi ← mkFreshExprMVarQ q(BI $prop)
+  let .some (_, mvars) ← ProofMode.trySynthInstanceQ q(AsEmpValid .from $goal $P) | throwError "{goal} is not an emp valid"
+  if !mvars.isEmpty then throwError "istart does not support creating mvars"
+
+  let irisGoal := { u, prop, bi, hyps := .mkEmp bi, goal := P, .. }
+  let subgoal : Quoted q(⊢ $P) ←
+    mkFreshExprSyntheticOpaqueMVar (IrisGoal.toExpr irisGoal) (← mvar.getTag)
+  mvar.assign q(asEmpValid_2 $goal $subgoal)
+  pure (subgoal.mvarId!, irisGoal)
+
+def ProofModeM.runTactic (x : MVarId → IrisGoal → ProofModeM α) (s : ProofModeM.State := {}) : TacticM α := do
+  let (mvar, g) ← istart (← getMainGoal)
+  mvar.withContext do
+
+  let (res, {goals}) ← StateRefT'.run (x mvar g) s
+
+  -- make sure to synthesize everything postponed
+  Term.synthesizeSyntheticMVarsNoPostponing
+
+  -- put the goals that depend on other goals last
+  let mvars ← goals.foldlM (λ m g => do
+    return m ∪ (← g.getMVarDependencies)) ∅
+  let (dep, nonDep) := goals.partition (λ x => mvars.contains x)
+
+  replaceMainGoal (nonDep ++ dep).toList
+  return res
diff --git a/src/Iris/ProofMode/SynthInstance.lean b/src/Iris/ProofMode/SynthInstance.lean
index b9ccac26..7570f0aa 100644
--- a/src/Iris/ProofMode/SynthInstance.lean
+++ b/src/Iris/ProofMode/SynthInstance.lean
@@ -3,7 +3,8 @@ Copyright (c) 2025 Michael Sammler. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michael Sammler
 -/
-import Iris.ProofMode.Goals
+import Qq
+import Iris.BI
 
 /-
 This file implements a custom typeclass synthesis algorithm that is used for the proof mode typeclasses.
@@ -26,7 +27,6 @@ The `InOut` type in Classes.lean is used to dynamically determine, which paramet
 ignores `outParam` and `semiOutParam` annotations, but it is still recommended to add these annotations as documentation.
 
 The `#imp_synth` command allows testing ipm synthesis, similar to the `#synth` command.
-
 -/
 
 namespace Iris.ProofMode
@@ -143,13 +143,22 @@ protected def trySynthInstance (type : Expr) (maxResultSize? : Option Nat := non
     (toLOptionM <| ProofMode.synthInstance? type maxResultSize?)
     (fun _ => pure LOption.undef)
 
+protected def synthInstance (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (Expr × Std.HashSet MVarId) :=
+  catchInternalId isDefEqStuckExceptionId
+    (do
+      let result? ← ProofMode.synthInstance? type maxResultSize?
+      match result? with
+      | some result => pure result
+      | none        => do _ ← throwFailedToSynthesize type; unreachable!)
+    (fun _ => do _ ← throwFailedToSynthesize type; unreachable!)
+
+/- It is recommended to use ProofModeM.trySynthInstanceQ and ProofModeM.synthInstanceQ that automatically handle the newly spawed goals. -/
+
 protected def trySynthInstanceQ (α : Q(Sort u)) : MetaM (LOption (Q($α) × Std.HashSet MVarId)) :=
   ProofMode.trySynthInstance α
 
-protected def trySynthInstanceQAddingGoals {prop : Q(Type u)} {bi : Q(BI $prop)} (gs : Goals bi) (α : Q(Sort v)) : MetaM (Option Q($α)) := do
-  let LOption.some (e, mvars) ← ProofMode.trySynthInstance α | return none
-  mvars.forM gs.addPureGoal
-  return some e
+protected def synthInstanceQ (α : Q(Sort u)) : MetaM (Q($α) × Std.HashSet MVarId) :=
+  ProofMode.synthInstance α
 
 syntax (name := ipm_synth) "#ipm_synth " term : command
 
diff --git a/src/Iris/ProofMode/Tactics.lean b/src/Iris/ProofMode/Tactics.lean
index f02be568..7518ccc1 100644
--- a/src/Iris/ProofMode/Tactics.lean
+++ b/src/Iris/ProofMode/Tactics.lean
@@ -10,9 +10,7 @@ import Iris.ProofMode.Tactics.Exists
 import Iris.ProofMode.Tactics.Have
 import Iris.ProofMode.Tactics.Intro
 import Iris.ProofMode.Tactics.LeftRight
-import Iris.ProofMode.Tactics.Move
 import Iris.ProofMode.Tactics.Pure
-import Iris.ProofMode.Tactics.Remove
 import Iris.ProofMode.Tactics.Rename
 import Iris.ProofMode.Tactics.Specialize
 import Iris.ProofMode.Tactics.Split
diff --git a/src/Iris/ProofMode/Tactics/Apply.lean b/src/Iris/ProofMode/Tactics/Apply.lean
index 105c19ec..e9034b05 100644
--- a/src/Iris/ProofMode/Tactics/Apply.lean
+++ b/src/Iris/ProofMode/Tactics/Apply.lean
@@ -5,43 +5,36 @@ Authors: Oliver Soeser, Michael Sammler
 -/
 import Iris.ProofMode.Patterns.ProofModeTerm
 import Iris.ProofMode.Tactics.Assumption
-import Iris.ProofMode.Tactics.Split
 import Iris.ProofMode.Tactics.Have
 
 namespace Iris.ProofMode
 open Lean Elab Tactic Meta Qq BI Std
 
-theorem apply [BI PROP] {p} {P Q P' Q1 R : PROP}
+private theorem apply [BI PROP] {p} {P Q P' Q1 R : PROP}
     (h1 : P ⊣⊢ P' ∗ □?p Q) (h2 : P' ⊢ Q1)
     [h3 : IntoWand p false Q .out Q1 .in R] : P ⊢ R :=
       h1.1.trans (Entails.trans (sep_mono_l h2) (wand_elim' h3.1))
 
-partial def iApplyCore {prop : Q(Type u)} {bi : Q(BI $prop)} (gs : Goals bi) {e} (hyps : Hyps bi e) (goal : Q($prop)) (uniq : Name) : TacticM Q($e ⊢ $goal) := do
+partial def iApplyCore {prop : Q(Type u)} {bi : Q(BI $prop)} {e} (hyps : Hyps bi e) (goal : Q($prop)) (uniq : Name) : ProofModeM Q($e ⊢ $goal) := do
   let ⟨_, hyps', _, out, p, _, pf⟩ := hyps.remove true uniq
   let A ← mkFreshExprMVarQ q($prop)
-  if let some _ ← ProofMode.trySynthInstanceQAddingGoals gs q(IntoWand $p false $out .out $A .in $goal) then
-     let pf' ← gs.addGoal hyps' A
+  if let some _ ← ProofModeM.trySynthInstanceQ q(IntoWand $p false $out .out $A .in $goal) then
+     let pf' ← addBIGoal hyps' A
      return q(apply $pf $pf')
 
-  let some ⟨_, hyps'', pf''⟩ ← try? <| iSpecializeCore gs hyps uniq [.goal [] .anonymous] | throwError m!"iapply: cannot apply {out} to {goal}"
-  let pf''' ← iApplyCore gs hyps'' goal uniq
+  let some ⟨_, hyps'', pf''⟩ ← try? <| iSpecializeCore hyps uniq [.goal [] .anonymous] | throwError m!"iapply: cannot apply {out} to {goal}"
+  let pf''' ← iApplyCore hyps'' goal uniq
   return q($(pf'').trans $pf''')
 
 elab "iapply" colGt pmt:pmTerm : tactic => do
   let pmt ← liftMacroM <| PMTerm.parse pmt
-  let (mvar, { bi, hyps, goal, .. }) ← istart (← getMainGoal)
-  mvar.withContext do
-  let gs ← Goals.new bi
-  let ⟨uniq, _, hyps, pf⟩ ← iHave gs hyps pmt (← `(binderIdent|_)) true (mayPostpone := true)
+  ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
+  let ⟨uniq, _, hyps, pf⟩ ← iHave hyps pmt (← `(binderIdent|_)) true (mayPostpone := true)
   let ⟨e', _, _, out, p, _, pf'⟩ := hyps.remove true uniq
-  if let some _ ← ProofMode.trySynthInstanceQAddingGoals gs q(FromAssumption $p .in $out $goal) then
+  if let some _ ← ProofModeM.trySynthInstanceQ q(FromAssumption $p .in $out $goal) then
     if let LOption.some _ ← trySynthInstanceQ q(TCOr (Affine $e') (Absorbing $goal)) then
       -- behave like iexact
-      Term.synthesizeSyntheticMVarsNoPostponing
       mvar.assign q($(pf).trans (assumption (Q := $goal) $pf'))
-      replaceMainGoal (← gs.getGoals)
       return
-  let pf' ← iApplyCore gs hyps goal uniq
-  Term.synthesizeSyntheticMVarsNoPostponing
+  let pf' ← iApplyCore hyps goal uniq
   mvar.assign q($(pf).trans $pf')
-  replaceMainGoal (← gs.getGoals)
diff --git a/src/Iris/ProofMode/Tactics/Assumption.lean b/src/Iris/ProofMode/Tactics/Assumption.lean
index b8671c13..f53522e0 100644
--- a/src/Iris/ProofMode/Tactics/Assumption.lean
+++ b/src/Iris/ProofMode/Tactics/Assumption.lean
@@ -4,122 +4,23 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lars König, Mario Carneiro
 -/
 import Iris.ProofMode.Tactics.Basic
-import Iris.ProofMode.Tactics.Remove
 
 namespace Iris.ProofMode
 open Lean Elab Tactic Meta Qq BI Std
 
-theorem pure_assumption [BI PROP] {P A Q : PROP} (h_P : ⊢ A)
-    [inst : FromAssumption true .in A Q] [TCOr (Affine P) (Absorbing Q)] :
-    P ⊢ Q :=
-  have := intuitionistically_emp.2.trans <| (intuitionistically_mono h_P).trans inst.1
-  emp_sep.2.trans <| (sep_mono_l this).trans sep_elim_l
-
-def assumptionLean {prop : Q(Type u)} (_bi : Q(BI $prop)) (ehyps goal : Q($prop))
-    (mvar : MVarId) : MetaM Unit := do
-  mvar.withContext do
-    let _ ← synthInstanceQ q(TCOr (Affine $ehyps) (Absorbing $goal))
-    for h in ← getLCtx do
-      let some #[_, _, (P : Q($prop))] := (← whnfR h.type).appM? ``BIBase.EmpValid | continue
-      have h : Q(⊢ $P) := .fvar h.fvarId
-      -- let (name, type) := (h.userName, ← instantiateMVars h.type)
-
-      -- try to solve the goal
-      try
-        let _ ← synthInstanceQ q(FromAssumption true .in $P $goal)
-        mvar.assign q(pure_assumption (P := $ehyps) (Q := $goal) $h)
-        return
-      catch e => trace[Meta.debug] e.toMessageData; pure ()
-    throwError "no matching hypothesis found"
-
-elab "iassumption_lean" : tactic => do
-  -- retrieve goal mvar declaration
-  let mvar ← getMainGoal
-  mvar.withContext do
-  let g ← instantiateMVars <| ← mvar.getType
-  let some { bi, e, goal, .. } := parseIrisGoal? g | throwError "not in proof mode"
-  assumptionLean bi e goal mvar
-  replaceMainGoal []
-
 theorem assumption [BI PROP] {p : Bool} {P P' A Q : PROP} [inst : FromAssumption p .in A Q]
   [TCOr (Affine P') (Absorbing Q)] (h : P ⊣⊢ P' ∗ □?p A) : P ⊢ Q :=
   h.1.trans <| (sep_mono_r inst.1).trans sep_elim_r
 
-inductive AssumptionFastPath (prop : Q(Type u)) (bi : Q(BI $prop)) (Q : Q($prop)) where
-  | absorbing (_ : Q(Absorbing $Q))
-  | biAffine (_ : Q(BIAffine $prop))
-
-variable {prop : Q(Type u)} (bi : Q(BI $prop)) (Q : Q($prop))
-  (fastPath : AssumptionFastPath prop bi Q) in
-def assumptionFast {e} (hyps : Hyps bi e) : MetaM Q($e ⊢ $Q) := do
-  let some ⟨inst, _, _, out, ty, b, _, pf⟩ ←
-    hyps.removeG true fun _ _ b ty => try? do
-      synthInstance q(FromAssumption $b .in $ty $Q)
-    | failure
-  let _ : Q(FromAssumption $b .in $ty $Q) := inst
-  have : $out =Q iprop(□?$b $ty) := ⟨⟩
-  match fastPath with
-  | .absorbing _ => return q(assumption (Q := $Q) $pf)
-  | .biAffine _ => return q(assumption (Q := $Q) $pf)
-
-inductive AssumptionSlow {prop : Q(Type u)} (bi : Q(BI $prop)) (Q e : Q($prop)) where
-  | none
-  | affine (pf : Q(Affine $e))
-  | main (pf : Q($e ⊢ $Q)) (pf : Option Q(Affine $e))
-
-theorem assumption_l [BI PROP] {P Q R : PROP} [Affine Q] (h : P ⊢ R) : P ∗ Q ⊢ R :=
-  sep_elim_l.trans h
-theorem assumption_r [BI PROP] {P Q R : PROP} [Affine P] (h : Q ⊢ R) : P ∗ Q ⊢ R :=
-  sep_elim_r.trans h
-
-variable {prop : Q(Type u)} (bi : Q(BI $prop)) (Q : Q($prop)) in
-def assumptionSlow (assume : Bool) :
-    ∀ {e}, Hyps bi e → MetaM (AssumptionSlow bi Q e)
-  | _, .emp _ =>
-    Pure.pure (.affine q(emp_affine))
-  | out, .hyp _ _ _ b ty _ => do
-    let fromAssum (_:Unit) := do
-      let _ ← synthInstanceQ q(FromAssumption $b .in $ty $Q)
-      let inst ← try? (synthInstanceQ q(Affine $out))
-      return .main q(FromAssumption.from_assumption .in) inst
-    let affine (_:Unit) := return .affine (← synthInstanceQ q(Affine $out))
-    if assume then
-      try fromAssum () catch _ => try affine () catch _ => return .none
-    else
-      try affine () catch _ => try fromAssum () catch _ => return .none
-  | _, .sep _ elhs erhs _ lhs rhs => do
-    match ← assumptionSlow assume rhs with
-    | .none => return .none
-    | .affine _ =>
-      match ← assumptionSlow assume lhs with
-      | .none => return .none
-      | .affine _ => return .affine q(sep_affine ..)
-      | .main lpf linst =>
-        return .main q(assumption_l $lpf) <| linst.map fun _ => q(sep_affine $elhs $erhs)
-    | .main rpf rinst =>
-      match ← assumptionSlow false lhs, rinst with
-      | .none, _ | .main _ none, none => return .none
-      | .affine _, rinst | .main _ (some _), rinst =>
-        return .main q(assumption_r $rpf) <| rinst.map fun _ => q(sep_affine $elhs $erhs)
-      | .main lpf none, some _ => return .main q(assumption_l $lpf) none
-
 elab "iassumption" : tactic => do
-  let mvar ← getMainGoal
-  mvar.withContext do
-  let g ← instantiateMVars <| ← mvar.getType
-  let some { prop, bi, e, hyps, goal, .. } := parseIrisGoal? g | throwError "not in proof mode"
-
-  let inst : Option (AssumptionFastPath prop bi goal) ← try
-    pure (some (.biAffine (← synthInstanceQ q(BIAffine $prop))))
-  catch _ => try? (AssumptionFastPath.absorbing <$> synthInstanceQ q(Absorbing $goal))
+  ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
 
-  try
-    let pf ← match inst with
-    | some fastPath => assumptionFast bi goal fastPath hyps
-    | none =>
-      let .main pf _ ← assumptionSlow bi goal true hyps | failure
-      pure pf
-    mvar.assign pf
-  catch _ =>
-    assumptionLean bi e goal mvar
-  replaceMainGoal []
+  let some ⟨inst, e', _, out, ty, b, _, pf⟩ ←
+    hyps.removeG true fun _ _ b ty => do
+      ProofModeM.trySynthInstanceQ q(FromAssumption $b .in $ty $goal)
+    | throwError "iassumption: no matching assumption"
+  let _ : Q(FromAssumption $b .in $ty $goal) := inst
+  have : $out =Q iprop(□?$b $ty) := ⟨⟩
+  let .some _ ← trySynthInstanceQ q(TCOr (Affine $e') (Absorbing $goal))
+    | throwError "iassumption: context is not affine or goal is not absorbing"
+  mvar.assign q(assumption (Q := $goal) $pf)
diff --git a/src/Iris/ProofMode/Tactics/Basic.lean b/src/Iris/ProofMode/Tactics/Basic.lean
index e5a63a23..3f4379c7 100644
--- a/src/Iris/ProofMode/Tactics/Basic.lean
+++ b/src/Iris/ProofMode/Tactics/Basic.lean
@@ -5,34 +5,12 @@ Authors: Lars König, Mario Carneiro
 -/
 import Iris.ProofMode.Expr
 import Iris.ProofMode.Classes
-import Iris.ProofMode.Goals
+import Iris.ProofMode.ProofModeM
 import Iris.ProofMode.SynthInstance
 
 namespace Iris.ProofMode
 open Lean Elab.Tactic Meta Qq BI Std
 
-def istart (mvar : MVarId) : MetaM (MVarId × IrisGoal) := mvar.withContext do
-  -- parse goal
-  let goal ← instantiateMVars <| ← mvar.getType
-
-  -- check if already in proof mode
-  if let some irisGoal := parseIrisGoal? goal then
-    return (mvar, irisGoal)
-
-  let some goal ← checkTypeQ goal q(Prop)
-    | throwError "type mismatch\n{← mkHasTypeButIsExpectedMsg (← inferType goal) q(Prop)}"
-  let u ← mkFreshLevelMVar
-  let prop ← mkFreshExprMVarQ q(Type u)
-  let P ← mkFreshExprMVarQ q($prop)
-  let bi ← mkFreshExprMVarQ q(BI $prop)
-  let _ ← synthInstanceQ q(ProofMode.AsEmpValid .from $goal $P)
-
-  let irisGoal := { u, prop, bi, hyps := .mkEmp bi, goal := P, .. }
-  let subgoal : Quoted q(⊢ $P) ←
-    mkFreshExprSyntheticOpaqueMVar (IrisGoal.toExpr irisGoal) (← mvar.getTag)
-  mvar.assign q(ProofMode.asEmpValid_2 $goal $subgoal)
-  pure (subgoal.mvarId!, irisGoal)
-
 elab "istart" : tactic => do
   let (mvar, _) ← istart (← getMainGoal)
   replaceMainGoal [mvar]
@@ -46,10 +24,3 @@ elab "istop" : tactic => do
   -- check if already in proof mode
   let some irisGoal := parseIrisGoal? goal | throwError "not in proof mode"
   mvar.setType irisGoal.strip
-
-def selectHyp (ty : Expr) : ∀ {s}, @Hyps u prop bi s → MetaM (Name × Q(Bool) × Q($prop))
-  | _, .emp _ => failure
-  | _, .hyp _ _ uniq p ty' _ => do
-    let .true ← isDefEq ty ty' | failure
-    pure (uniq, p, ty')
-  | _, .sep _ _ _ _ lhs rhs => try selectHyp ty rhs catch _ => selectHyp ty lhs
diff --git a/src/Iris/ProofMode/Tactics/Cases.lean b/src/Iris/ProofMode/Tactics/Cases.lean
index c146cfa7..7a1037ca 100644
--- a/src/Iris/ProofMode/Tactics/Cases.lean
+++ b/src/Iris/ProofMode/Tactics/Cases.lean
@@ -1,210 +1,173 @@
 /-
 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, Mario Carneiro
+Authors: Lars König, Mario Carneiro, Michael Sammler
 -/
-import Iris.ProofMode.Instances
+import Iris.ProofMode.Patterns.ProofModeTerm
 import Iris.ProofMode.Patterns.CasesPattern
+import Iris.ProofMode.Tactics.Basic
 import Iris.ProofMode.Tactics.Clear
-import Iris.ProofMode.Tactics.Move
 import Iris.ProofMode.Tactics.Pure
+import Iris.ProofMode.Tactics.Have
 
 namespace Iris.ProofMode
 open Lean Elab Tactic Meta Qq BI Std
 
-theorem false_elim_spatial [BI PROP] {P Q : PROP} : P ∗ False ⊢ Q := wand_elim' false_elim
+private theorem false_elim' [BI PROP] {P Q : PROP} : P ∗ □?p False ⊢ Q :=
+  wand_elim' <| intuitionisticallyIf_elim.trans false_elim
 
-theorem false_elim_intuitionistic [BI PROP] {P Q : PROP} : P ∗ □ False ⊢ Q :=
-  wand_elim' <| intuitionistically_elim.trans false_elim
-
-theorem sep_emp_intro_spatial [BI PROP] {P Q : PROP} (h : P ⊢ Q) : P ∗ emp ⊢ Q := sep_emp.1.trans h
-
-theorem sep_emp_intro_intuitionistic [BI PROP] {P Q : PROP}
-    (h : P ⊢ Q) : P ∗ □ emp ⊢ Q := (sep_mono_r intuitionistically_emp.1).trans <| sep_emp.1.trans h
+-- private theorem sep_emp_intro [BI PROP] {P Q : PROP} (h : P ⊢ Q) : P ∗ □?p emp ⊢ Q := (sep_mono_r intuitionisticallyIf_elim).trans <| (sep_emp.1).trans h
 
 def iCasesEmptyConj {prop : Q(Type u)} (bi : Q(BI $prop))
-    {P} (hyps : Hyps bi P) (Q A' : Q($prop)) (p : Q(Bool))
-    (k : ∀ {P}, Hyps bi P → MetaM Q($P ⊢ $Q)) :
-    MetaM (Q($P ∗ □?$p $A' ⊢ $Q)) := do
-  try
-    let ⟨_⟩ ← assertDefEqQ A' q(iprop(False))
-    if p.constName! == ``true then
-      have : $p =Q true := ⟨⟩; return q(false_elim_intuitionistic)
-    else
-      have : $p =Q false := ⟨⟩; return q(false_elim_spatial)
-  catch _ =>
-    let ⟨_⟩ ← assertDefEqQ A' q(iprop(emp))
-    if p.constName! == ``true then
-      have : $p =Q true := ⟨⟩; return q(sep_emp_intro_intuitionistic $(← k hyps))
-    else
-      have : $p =Q false := ⟨⟩; return q(sep_emp_intro_spatial $(← k hyps))
-
-
-theorem exists_elim_spatial [BI PROP] {P A Q : PROP} {Φ : α → PROP} [inst : IntoExists A Φ]
-    (h : ∀ a, P ∗ Φ a ⊢ Q) : P ∗ A ⊢ Q :=
-  (sep_mono_r inst.1).trans <| sep_exists_l.1.trans (exists_elim h)
-
-theorem exists_elim_intuitionistic [BI PROP] {P A Q : PROP} {Φ : α → PROP} [IntoExists A Φ]
-    (h : ∀ a, P ∗ □ Φ a ⊢ Q) : P ∗ □ A ⊢ Q := exists_elim_spatial h
-
-def iCasesExists {prop : Q(Type u)} (_bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q(Bool))
-    (name : TSyntax ``binderIdent) (α : Q(Sort v)) (Φ : Q(«$α» → «$prop»))
-    (_inst : Q(IntoExists «$A'» «$Φ»))
-    (k : (B B' : Q($prop)) → (_ : $B =Q iprop(□?$p $B')) → MetaM Q($P ∗ $B ⊢ $Q)) :
-    MetaM (Q($P ∗ □?$p $A' ⊢ $Q)) := do
+    {P} (_hyps : Hyps bi P) (Q A' : Q($prop)) (p : Q(Bool))
+    (_k : ∀ {P}, Hyps bi P → ProofModeM Q($P ⊢ $Q)) :
+    ProofModeM (Q($P ∗ □?$p $A' ⊢ $Q)) := do
+  if let .defEq _ ← isDefEqQ A' q(iprop(False)) then
+    return q(false_elim')
+  -- TODO: Is this something we want to support? Rocq does not support this. One can use the clearing pattern instead
+  -- else if let .defEq _ ← isDefEqQ A' q(iprop(emp)) then
+    -- return q(sep_emp_intro $(← k hyps))
+  else
+    throwError "icases: cannot destruct {A'} as an empty conjunct"
+
+
+private theorem exists_elim' [BI PROP] {p} {P A Q : PROP} {Φ : α → PROP} [inst : IntoExists A Φ]
+    (h : ∀ a, P ∗ □?p Φ a ⊢ Q) : P ∗ □?p A ⊢ Q :=
+  (sep_mono_r <| (intuitionisticallyIf_mono inst.1).trans intuitionisticallyIf_exists.1).trans <| sep_exists_l.1.trans (exists_elim h)
+
+def iCasesExists {prop : Q(Type u)} (bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q(Bool))
+    (name : TSyntax ``binderIdent)
+    (k : (B B' : Q($prop)) → (_ : $B =Q iprop(□?$p $B')) → ProofModeM Q($P ∗ $B ⊢ $Q)) :
+    ProofModeM (Q($P ∗ □?$p $A' ⊢ $Q)) := do
+  let v ← mkFreshLevelMVar
+  let α : Quoted q(Sort v) ← mkFreshExprMVarQ q(Sort v)
+  let Φ : Quoted q($α → $prop) ← mkFreshExprMVarQ q($α → $prop)
+  let .some _ ← ProofModeM.trySynthInstanceQ q(IntoExists $A' $Φ)
+    | throwError "icases: {A'} is not an existential quantifier"
   let (name, ref) ← getFreshName name
   withLocalDeclDQ name α fun x => do
     addLocalVarInfo ref (← getLCtx) x α
     have B' : Q($prop) := Expr.headBeta q($Φ $x)
     have : $B' =Q $Φ $x := ⟨⟩
-    if p.constName! == ``true then
-      have : $p =Q true := ⟨⟩
-      let pf : Q(∀ x, $P ∗ □ $Φ x ⊢ $Q) ← mkLambdaFVars #[x] <|← k q(iprop(□ $B')) B' ⟨⟩
-      return q(exists_elim_intuitionistic (A := $A') $pf)
-    else
-      have : $p =Q false := ⟨⟩
-      let pf : Q(∀ x, $P ∗ $Φ x ⊢ $Q) ← mkLambdaFVars #[x] <|← k B' B' ⟨⟩
-      return q(exists_elim_spatial (A := $A') $pf)
+    have ⟨B, _⟩ := mkIntuitionisticIf bi p B'
+    let pf : Q(∀ x, $P ∗ □?$p $Φ x ⊢ $Q) ← mkLambdaFVars #[x] <|← k B B' ⟨⟩
+    return q(exists_elim' (A := $A') $pf)
 
-theorem sep_and_elim_l [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoAnd p A A1 A2]
+
+private theorem sep_and_elim_l [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoAnd p A A1 A2]
     (h : P ∗ □?p A1 ⊢ Q) : P ∗ □?p A ⊢ Q :=
   (sep_mono_r <| inst.1.trans <| intuitionisticallyIf_mono and_elim_l).trans h
 
-theorem and_elim_l_spatial [BI PROP] {P A Q A1 A2 : PROP} [IntoAnd false A A1 A2]
-    (h : P ∗ A1 ⊢ Q) : P ∗ A ⊢ Q := sep_and_elim_l (p := false) h
-
-theorem and_elim_l_intuitionistic [BI PROP] {P A Q A1 A2 : PROP} [IntoAnd true A A1 A2]
-    (h : P ∗ □ A1 ⊢ Q) : P ∗ □ A ⊢ Q := sep_and_elim_l (p := true) h
-
-theorem sep_and_elim_r [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoAnd p A A1 A2]
+private theorem sep_and_elim_r [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoAnd p A A1 A2]
     (h : P ∗ □?p A2 ⊢ Q) : P ∗ □?p A ⊢ Q :=
   (sep_mono_r <| inst.1.trans <| intuitionisticallyIf_mono and_elim_r).trans h
 
-theorem and_elim_r_spatial [BI PROP] {P A Q A1 A2 : PROP} [IntoAnd false A A1 A2]
-    (h : P ∗ A2 ⊢ Q) : P ∗ A ⊢ Q := sep_and_elim_r (p := false) h
-
-theorem and_elim_r_intuitionistic [BI PROP] {P A Q A1 A2 : PROP} [IntoAnd true A A1 A2]
-    (h : P ∗ □ A2 ⊢ Q) : P ∗ □ A ⊢ Q := sep_and_elim_r (p := true) h
-
-def iCasesAndLR {prop : Q(Type u)} (_bi : Q(BI $prop)) (P Q A' A1 A2 : Q($prop)) (p : Q(Bool))
-    (_inst : Q(IntoAnd $p $A' $A1 $A2)) (right : Bool)
-    (k : (B B' : Q($prop)) → (_ : $B =Q iprop(□?$p $B')) → MetaM Q($P ∗ $B ⊢ $Q)) :
-    MetaM (Q($P ∗ □?$p $A' ⊢ $Q)) := do
-  if p.constName! == ``true then
-    have : $p =Q true := ⟨⟩
-    if right then
-      return q(and_elim_r_intuitionistic (A := $A') $(← k q(iprop(□ $A2)) A2 ⟨⟩))
-    else
-      return q(and_elim_l_intuitionistic (A := $A') $(← k q(iprop(□ $A1)) A1 ⟨⟩))
+def iCasesAndLR {prop : Q(Type u)} (bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q(Bool)) (right : Bool)
+  (k : (B B' : Q($prop)) → (_ : $B =Q iprop(□?$p $B')) → ProofModeM Q($P ∗ $B ⊢ $Q)) :
+    ProofModeM (Option Q($P ∗ □?$p $A' ⊢ $Q)) := do
+  let A1 ← mkFreshExprMVarQ q($prop)
+  let A2 ← mkFreshExprMVarQ q($prop)
+  let .some _ ← ProofModeM.trySynthInstanceQ q(IntoAnd $p $A' $A1 $A2)
+    | return none
+  if right then
+    have ⟨A2', _⟩ := mkIntuitionisticIf bi p A2
+    return some q(sep_and_elim_r $(← k A2' A2 ⟨⟩))
   else
-    have : $p =Q false := ⟨⟩
-    if right then
-      return q(and_elim_r_spatial (A := $A') $(← k A2 A2 ⟨⟩))
-    else
-      return q(and_elim_l_spatial (A := $A') $(← k A1 A1 ⟨⟩))
+    have ⟨A1', _⟩ := mkIntuitionisticIf bi p A1
+    return some q(sep_and_elim_l $(← k A1' A1 ⟨⟩))
 
-theorem sep_elim_spatial [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoSep A A1 A2]
+private theorem sep_elim_spatial [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoSep A A1 A2]
     (h : P ∗ A1 ⊢ A2 -∗ Q) : P ∗ A ⊢ Q :=
   (sep_mono_r inst.1).trans <| sep_assoc.2.trans <| wand_elim h
 
-theorem and_elim_intuitionistic [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoAnd true A A1 A2]
+private theorem and_elim_intuitionistic [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoAnd true A A1 A2]
     (h : P ∗ □ A1 ⊢ □ A2 -∗ Q) : P ∗ □ A ⊢ Q :=
   (sep_mono_r <| inst.1.trans intuitionistically_and_sep.1).trans <|
   sep_assoc.2.trans <| wand_elim h
 
 def iCasesSep {prop : Q(Type u)} (bi : Q(BI $prop))
-    {P} (hyps : Hyps bi P) (Q A' A1 A2 : Q($prop)) (p : Q(Bool))
-    (inst : Option Q(IntoAnd $p $A' $A1 $A2))
-    (k : ∀ {P}, Hyps bi P → MetaM Q($P ⊢ $Q))
+    {P} (hyps : Hyps bi P) (Q A' : Q($prop)) (p : Q(Bool))
+    (k : ∀ {P}, Hyps bi P → ProofModeM Q($P ⊢ $Q))
     (k1 k2 : ∀ {P}, Hyps bi P → (Q B B' : Q($prop)) → (_ : $B =Q iprop(□?$p $B')) →
-      (∀ {P}, Hyps bi P → MetaM Q($P ⊢ $Q)) → MetaM Q($P ∗ $B ⊢ $Q)) :
-    MetaM (Q($P ∗ □?$p $A' ⊢ $Q)) := do
-  if p.constName! == ``true then
-    let some _ := inst | _ ← synthInstanceQ q(IntoAnd $p $A' $A1 $A2); unreachable!
-    have : $p =Q true := ⟨⟩
+      (∀ {P}, Hyps bi P → ProofModeM Q($P ⊢ $Q)) → ProofModeM Q($P ∗ $B ⊢ $Q)) :
+    ProofModeM (Q($P ∗ □?$p $A' ⊢ $Q)) := do
+  let A1 ← mkFreshExprMVarQ q($prop)
+  let A2 ← mkFreshExprMVarQ q($prop)
+  match matchBool p with
+  | .inl _ =>
+    let .some _ ← ProofModeM.trySynthInstanceQ q(IntoAnd $p $A' $A1 $A2)
+      | throwError "icases: cannot destruct {A'}"
     let Q' := q(iprop(□ $A2 -∗ $Q))
     let pf ← k1 hyps Q' q(iprop(□ $A1)) A1 ⟨⟩ fun hyps => do
       let pf ← k2 hyps Q q(iprop(□ $A2)) A2 ⟨⟩ k
       return q(wand_intro $pf)
     return q(and_elim_intuitionistic (A := $A') $pf)
-  else
-    let _ ← synthInstanceQ q(IntoSep $A' $A1 $A2)
-    have : $p =Q false := ⟨⟩
+  | .inr _ =>
+    let .some _ ← ProofModeM.trySynthInstanceQ q(IntoSep $A' $A1 $A2)
+      | throwError "icases: cannot destruct {A'}"
     let Q' := q(iprop($A2 -∗ $Q))
     let pf ← k1 hyps Q' A1 A1 ⟨⟩ fun hyps => do
       let pf ← k2 hyps Q A2 A2 ⟨⟩ k
       return q(wand_intro $pf)
     return q(sep_elim_spatial (A := $A') $pf)
 
-theorem or_elim_spatial [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoOr A A1 A2]
-    (h1 : P ∗ A1 ⊢ Q) (h2 : P ∗ A2 ⊢ Q) : P ∗ A ⊢ Q :=
-  (sep_mono_r inst.1).trans <| BI.sep_or_l.1.trans <| or_elim h1 h2
-
-theorem or_elim_intuitionistic [BI PROP] {P A Q A1 A2 : PROP} [IntoOr A A1 A2]
-    (h1 : P ∗ □ A1 ⊢ Q) (h2 : P ∗ □ A2 ⊢ Q) : P ∗ □ A ⊢ Q := or_elim_spatial h1 h2
+private theorem or_elim' [BI PROP] {p} {P A Q A1 A2 : PROP} [inst : IntoOr A A1 A2]
+    (h1 : P ∗ □?p A1 ⊢ Q) (h2 : P ∗ □?p A2 ⊢ Q) : P ∗ □?p A ⊢ Q :=
+  (sep_mono_r <| (intuitionisticallyIf_mono inst.1).trans (intuitionisticallyIf_or _).1).trans <| BI.sep_or_l.1.trans <| or_elim h1 h2
 
-def iCasesOr {prop : Q(Type u)} (_bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q(Bool))
-    (k1 k2 : (B B' : Q($prop)) → (_ : $B =Q iprop(□?$p $B')) → MetaM Q($P ∗ $B ⊢ $Q)) :
-    MetaM (Q($P ∗ □?$p $A' ⊢ $Q)) := do
+def iCasesOr {prop : Q(Type u)} (bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q(Bool))
+    (k1 k2 : (B B' : Q($prop)) → (_ : $B =Q iprop(□?$p $B')) → ProofModeM Q($P ∗ $B ⊢ $Q)) :
+    ProofModeM (Q($P ∗ □?$p $A' ⊢ $Q)) := do
   let A1 ← mkFreshExprMVarQ q($prop)
   let A2 ← mkFreshExprMVarQ q($prop)
-  let _ ← synthInstanceQ q(IntoOr $A' $A1 $A2)
-  if p.constName! == ``true then
-    have : $p =Q true := ⟨⟩
-    let pf1 ← k1 q(iprop(□ $A1)) A1 ⟨⟩
-    let pf2 ← k2 q(iprop(□ $A2)) A2 ⟨⟩
-    return q(or_elim_intuitionistic (A := $A') $pf1 $pf2)
-  else
-    have : $p =Q false := ⟨⟩
-    let pf1 ← k1 A1 A1 ⟨⟩
-    let pf2 ← k2 A2 A2 ⟨⟩
-    return q(or_elim_spatial (A := $A') $pf1 $pf2)
-
-theorem intuitionistic_elim_spatial [BI PROP] {A A' Q : PROP}
+  let .some _ ← ProofModeM.trySynthInstanceQ q(IntoOr $A' $A1 $A2)
+    | throwError "icases: {A'} is not a disjunction"
+  have ⟨A1', _⟩ := mkIntuitionisticIf bi p A1
+  have ⟨A2', _⟩ := mkIntuitionisticIf bi p A2
+  let pf1 ← k1 A1' A1 ⟨⟩
+  let pf2 ← k2 A2' A2 ⟨⟩
+  return q(or_elim' (A := $A') $pf1 $pf2)
+
+private theorem intuitionistic_elim_spatial [BI PROP] {A A' Q : PROP}
     [IntoPersistently false A A'] [TCOr (Affine A) (Absorbing Q)]
     (h : P ∗ □ A' ⊢ Q) : P ∗ A ⊢ Q := (replaces_r to_persistent_spatial).apply h
 
-theorem intuitionistic_elim_intuitionistic [BI PROP] {A A' Q : PROP} [IntoPersistently true A A']
+private theorem intuitionistic_elim_intuitionistic [BI PROP] {A A' Q : PROP} [IntoPersistently true A A']
     (h : P ∗ □ A' ⊢ Q) : P ∗ □ A ⊢ Q := intuitionistic_elim_spatial h
 
 def iCasesIntuitionistic {prop : Q(Type u)} (_bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q(Bool))
-    (k : (B' : Q($prop)) → MetaM Q($P ∗ □ $B' ⊢ $Q)) :
-    MetaM (Q($P ∗ □?$p $A' ⊢ $Q)) := do
+    (k : (B' : Q($prop)) → ProofModeM Q($P ∗ □ $B' ⊢ $Q)) :
+    ProofModeM (Q($P ∗ □?$p $A' ⊢ $Q)) := do
   let B' ← mkFreshExprMVarQ q($prop)
-  let _ ← synthInstanceQ q(IntoPersistently $p $A' $B')
-  if p.constName! == ``true then
-    have : $p =Q true := ⟨⟩
+  let .some _ ← ProofModeM.trySynthInstanceQ q(IntoPersistently $p $A' $B')
+    | throwError "icases: {A'} not persistent"
+  match matchBool p with
+  | .inl _ =>
     return q(intuitionistic_elim_intuitionistic $(← k B'))
-  else
-    have : $p =Q false := ⟨⟩
-    let _ ← synthInstanceQ q(TCOr (Affine $A') (Absorbing $Q))
+  | .inr _ =>
+    let .some _ ← trySynthInstanceQ q(TCOr (Affine $A') (Absorbing $Q))
+      | throwError "icases: {A'} not affine and the goal not absorbing"
     return q(intuitionistic_elim_spatial (A := $A') $(← k B'))
 
-theorem spatial_elim_spatial [BI PROP] {A A' Q : PROP} [FromAffinely A' A false]
-    (h : P ∗ A' ⊢ Q) : P ∗ A ⊢ Q := (replaces_r (from_affine (p := false))).apply h
-
-theorem spatial_elim_intuitionistic [BI PROP] {A A' Q : PROP} [FromAffinely A' A true]
-    (h : P ∗ A' ⊢ Q) : P ∗ □ A ⊢ Q := (replaces_r (from_affine (p := true))).apply h
+private theorem spatial_elim [BI PROP] {p} {A A' Q : PROP} [FromAffinely A' A p]
+    (h : P ∗ A' ⊢ Q) : P ∗ □?p A ⊢ Q :=
+      (sep_mono_r <| (affinelyIf_of_intuitionisticallyIf).trans from_affinely).trans h
 
 def iCasesSpatial {prop : Q(Type u)} (_bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q(Bool))
-    (k : (B' : Q($prop)) → MetaM Q($P ∗ $B' ⊢ $Q)) :
-    MetaM (Q($P ∗ □?$p $A' ⊢ $Q)) := do
+    (k : (B' : Q($prop)) → ProofModeM Q($P ∗ $B' ⊢ $Q)) :
+    ProofModeM (Q($P ∗ □?$p $A' ⊢ $Q)) := do
   let B' ← mkFreshExprMVarQ q($prop)
-  let _ ← synthInstanceQ q(FromAffinely $B' $A' $p)
-  if p.constName! == ``true then
-    have : $p =Q true := ⟨⟩
-    return q(spatial_elim_intuitionistic $(← k B'))
-  else
-    have : $p =Q false := ⟨⟩
-    return q(spatial_elim_spatial (A := $A') $(← k B'))
+  -- this should always succeed
+  let _ ← ProofModeM.synthInstanceQ q(FromAffinely $B' $A' $p)
+  return q(spatial_elim (A := $A') $(← k B'))
 
-theorem of_emp_sep [BI PROP] {A Q : PROP} (h : A ⊢ Q) : emp ∗ A ⊢ Q := emp_sep.1.trans h
+private theorem of_emp_sep [BI PROP] {A Q : PROP} (h : A ⊢ Q) : emp ∗ A ⊢ Q := emp_sep.1.trans h
 
 variable {u : Level} {prop : Q(Type u)} (bi : Q(BI $prop)) in
 partial def iCasesCore
     {P} (hyps : Hyps bi P) (Q : Q($prop)) (p : Q(Bool))
     (A A' : Q($prop)) (_ : $A =Q iprop(□?$p $A'))
-    (pat : iCasesPat) (k : ∀ {P}, Hyps bi P → MetaM Q($P ⊢ $Q)) : MetaM (Q($P ∗ $A ⊢ $Q)) :=
+    (pat : iCasesPat) (k : ∀ {P}, Hyps bi P → ProofModeM Q($P ⊢ $Q)) : ProofModeM (Q($P ∗ $A ⊢ $Q)) :=
   match pat with
   | .one name => do
     -- TODO: use Hyps.addWithInfo here?
@@ -219,7 +182,7 @@ partial def iCasesCore
       k (.mkSep hyps hyp)
 
   | .clear => do
-    let pf ← clearCore bi q(iprop($P ∗ $A)) P A Q q(.rfl)
+    let pf ← iClearCore bi q(iprop($P ∗ $A)) P p A' Q q(.rfl)
     pure q($pf $(← k hyps))
 
   | .conjunction [arg] | .disjunction [arg] => iCasesCore hyps Q p A A' ⟨⟩ arg @k
@@ -228,33 +191,24 @@ partial def iCasesCore
 
   | .conjunction [] => iCasesEmptyConj bi hyps Q A' p @k
 
+  -- pure conjunctions are always handled as existentials. There is
+  -- intoExist_and_pure and intoExist_sep_pure to make this work as
+  -- expected for pure assertions that are not explicit existentials.
+  | .conjunction (.pure arg :: args) => do
+    iCasesExists bi P Q A' p arg
+      (iCasesCore hyps Q p · · · (.conjunction args) k)
   | .conjunction (arg :: args) => do
-    let exres ← try? (α := _ × (v : Level) × (α : Q(Sort v)) × (Φ : Q($α → $prop)) ×
-        Q(IntoExists $A' $Φ)) do
-      let .one n := arg | failure
-      let v ← mkFreshLevelMVar
-      let α ← mkFreshExprMVarQ q(Sort v)
-      let Φ ← mkFreshExprMVarQ q($α → $prop)
-      Pure.pure ⟨n, v, α, Φ, ← synthInstanceQ q(IntoExists $A' $Φ)⟩
-    if let some ⟨n, _, α, Φ, inst⟩ := exres then
-      iCasesExists bi P Q A' p n α Φ inst
-        (iCasesCore hyps Q p · · · (.conjunction args) k)
-    else
-      let A1 ← mkFreshExprMVarQ q($prop)
-      let A2 ← mkFreshExprMVarQ q($prop)
-      let inst ← try? (α := Q(IntoAnd $p $A' $A1 $A2)) do
-        unless arg matches .clear || args matches [.clear] || p.constName! == ``true do failure
-        synthInstanceQ q(IntoAnd $p $A' $A1 $A2)
-      if let (.clear, some inst) := (arg, inst) then
-        iCasesAndLR bi P Q A' A1 A2 p inst (right := true) fun B B' h =>
-          iCasesCore hyps Q p B B' h (.conjunction args) @k
-      else if let ([.clear], some inst) := (args, inst) then
-        iCasesAndLR bi P Q A' A1 A2 p inst (right := false) fun B B' h =>
-          iCasesCore hyps Q p B B' h arg @k
-      else
-        iCasesSep bi hyps Q A' A1 A2 p inst @k
-          (iCasesCore · · p · · · arg)
-          (iCasesCore · · p · · · (.conjunction args))
+    if arg matches .clear then
+      let pf ← iCasesAndLR bi P Q A' p (right := true) fun B B' h =>
+        iCasesCore hyps Q p B B' h (.conjunction args) @k
+      if let some pf := pf then return pf
+    if args matches [.clear] then
+      let pf ← iCasesAndLR bi P Q A' p (right := false) fun B B' h =>
+        iCasesCore hyps Q p B B' h arg @k
+      if let some pf := pf then return pf
+    iCasesSep bi hyps Q A' p @k
+      (iCasesCore · · p · · · arg)
+      (iCasesCore · · p · · · (.conjunction args))
 
   | .disjunction (arg :: args) =>
     iCasesOr bi P Q A' p
@@ -262,10 +216,7 @@ partial def iCasesCore
       (iCasesCore hyps Q p · · · (.disjunction args) @k)
 
   | .pure arg => do
-    let .one n := arg
-      | throwError "cannot further destruct a hypothesis after moving it to the Lean context"
-    (·.2) <$> ipureCore bi q(iprop($P ∗ $A)) P A Q n q(.rfl) fun _ _ =>
-      ((), ·) <$> k hyps
+    iPureCore bi q(iprop($P ∗ $A)) P p A' Q arg q(.rfl) fun _ _ => k hyps
 
   | .intuitionistic arg =>
     iCasesIntuitionistic bi P Q A' p fun B' =>
@@ -275,19 +226,20 @@ partial def iCasesCore
     iCasesSpatial bi P Q A' p fun B' =>
       iCasesCore hyps Q q(false) B' B' ⟨⟩ arg @k
 
-elab "icases" colGt hyp:ident "with" colGt pat:icasesPat : tactic => do
+elab "icases" colGt pmt:pmTerm "with" colGt pat:icasesPat : tactic => do
   -- parse syntax
+  let pmt ← liftMacroM <| PMTerm.parse pmt
   let pat ← liftMacroM <| iCasesPat.parse pat
+  ProofModeM.runTactic λ mvar { bi, goal, hyps, .. } => do
 
-  let (mvar, { u, prop := _, bi, e := _, hyps, goal }) ← istart (← getMainGoal)
-  mvar.withContext do
-
-  let uniq ← hyps.findWithInfo hyp
-  let ⟨_, hyps', A, A', b, h, pf⟩ := hyps.remove true uniq
+  let ⟨uniq, _, hyps, pf⟩ ← iHave hyps pmt (← `(binderIdent|_)) false
+  let ⟨_, hyps', A, A', b, h, pf'⟩ := hyps.remove true uniq
 
   -- process pattern
-  let gs ← Goals.new bi
-  let pf2 ← iCasesCore bi hyps' goal b A A' h pat (λ hyps => gs.addGoal hyps goal)
+  let pf2 ← iCasesCore bi hyps' goal b A A' h pat (λ hyps => addBIGoal hyps goal)
+
+  mvar.assign q(($pf).trans (($pf').1.trans $pf2))
 
-  mvar.assign q(($pf).1.trans $pf2)
-  replaceMainGoal (← gs.getGoals)
+-- TODO: are these shortcuts necessary?
+macro "iintuitionistic" hyp:ident : tactic => `(tactic | icases $hyp:ident with □$hyp:ident)
+macro "ispatial" hyp:ident : tactic => `(tactic | icases $hyp:ident with ∗$hyp:ident)
diff --git a/src/Iris/ProofMode/Tactics/Clear.lean b/src/Iris/ProofMode/Tactics/Clear.lean
index cd6455a2..849684a4 100644
--- a/src/Iris/ProofMode/Tactics/Clear.lean
+++ b/src/Iris/ProofMode/Tactics/Clear.lean
@@ -3,39 +3,32 @@ 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, Mario Carneiro
 -/
-import Iris.ProofMode.Tactics.Remove
+import Iris.ProofMode.Tactics.Basic
 
 namespace Iris.ProofMode
 open Lean Elab Tactic Meta Qq BI Std
 
-theorem clear_spatial [BI PROP] {P P' A Q : PROP} [TCOr (Affine A) (Absorbing Q)]
+private theorem clear_spatial [BI PROP] {P P' A Q : PROP} [TCOr (Affine A) (Absorbing Q)]
     (h_rem : P ⊣⊢ P' ∗ A) (h : P' ⊢ Q) : P ⊢ Q :=
   h_rem.1.trans <| (sep_mono_l h).trans sep_elim_l
 
-theorem clear_intuitionistic [BI PROP] {P P' A Q : PROP}
+private theorem clear_intuitionistic [BI PROP] {P P' A Q : PROP}
     (h_rem : P ⊣⊢ P' ∗ □ A) (h : P' ⊢ Q) : P ⊢ Q := clear_spatial h_rem h
 
-def clearCore {prop : Q(Type u)} (_bi : Q(BI $prop)) (e e' out goal : Q($prop))
-    (pf : Q($e ⊣⊢ $e' ∗ $out)) : MetaM Q(($e' ⊢ $goal) → $e ⊢ $goal) := do
-  if out.isAppOfArity ``intuitionistically 3 then
-    have out' : Q($prop) := out.appArg!
-    have : $out =Q iprop(□ $out') := ⟨⟩
-    pure q(clear_intuitionistic (Q := $goal) $pf)
-  else
-    let _ ← synthInstanceQ q(TCOr (Affine $out) (Absorbing $goal))
-    pure q(clear_spatial $pf)
+def iClearCore {prop : Q(Type u)} (_bi : Q(BI $prop)) (e e' : Q($prop))
+    (p : Q(Bool)) (out goal : Q($prop))
+    (pf : Q($e ⊣⊢ $e' ∗ □?$p $out)) : ProofModeM Q(($e' ⊢ $goal) → $e ⊢ $goal) := do
+    match matchBool p with
+    | .inl _ => return q(clear_intuitionistic (Q := $goal) $pf)
+    | .inr _ =>
+      let .some _ ← trySynthInstanceQ q(TCOr (Affine $out) (Absorbing $goal))
+        | throwError "iclear: {out} is not affine and the goal not absorbing"
+      return q(clear_spatial (A:=$out) $pf)
 
 elab "iclear" colGt hyp:ident : tactic => do
-  let mvar ← getMainGoal
-  mvar.withContext do
-  let g ← instantiateMVars <| ← mvar.getType
-  let some { u, prop, bi, e, hyps, goal } := parseIrisGoal? g | throwError "not in proof mode"
+  ProofModeM.runTactic λ mvar { bi, e, hyps, goal, .. } => do
 
   let uniq ← hyps.findWithInfo hyp
-  let ⟨e', hyps', out, _, _, _, pf⟩ := hyps.remove true uniq
-
-  let m : Q($e' ⊢ $goal) ← mkFreshExprSyntheticOpaqueMVar <|
-    IrisGoal.toExpr { u, prop, bi, hyps := hyps', goal, .. }
-
-  mvar.assign ((← clearCore bi e e' out goal pf).app m)
-  replaceMainGoal [m.mvarId!]
+  let ⟨e', hyps', _, out', p, _, pf⟩ := hyps.remove true uniq
+  let m ← addBIGoal hyps' goal
+  mvar.assign ((← iClearCore bi e e' p out' goal pf).app m)
diff --git a/src/Iris/ProofMode/Tactics/ExFalso.lean b/src/Iris/ProofMode/Tactics/ExFalso.lean
index a68dab05..31b1f5bd 100644
--- a/src/Iris/ProofMode/Tactics/ExFalso.lean
+++ b/src/Iris/ProofMode/Tactics/ExFalso.lean
@@ -3,20 +3,14 @@ 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, Mario Carneiro
 -/
-import Iris.ProofMode.Expr
+import Iris.ProofMode.Tactics.Basic
 
 namespace Iris.ProofMode
 open Lean Elab.Tactic Meta Qq BI
 
-theorem exfalso [BI PROP] {P Q : PROP} (h : P ⊢ False) : P ⊢ Q := h.trans false_elim
+private theorem exfalso [BI PROP] {P Q : PROP} (h : P ⊢ False) : P ⊢ Q := h.trans false_elim
 
 elab "iexfalso" : tactic => do
-  let mvar ← getMainGoal
-  mvar.withContext do
-  let g ← instantiateMVars <| ← mvar.getType
-  let some { u, prop, bi, e, hyps, goal } := parseIrisGoal? g | throwError "not in proof mode"
-
-  let m : Q($e ⊢ False) ← mkFreshExprSyntheticOpaqueMVar <|
-    IrisGoal.toExpr { u, prop, bi, e, hyps, goal := q(iprop(False)) }
+  ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
+  let m ← addBIGoal hyps q(iprop(False))
   mvar.assign q(exfalso (Q := $goal) $m)
-  replaceMainGoal [m.mvarId!]
diff --git a/src/Iris/ProofMode/Tactics/Exact.lean b/src/Iris/ProofMode/Tactics/Exact.lean
index 0a8e5d34..7cdc3d74 100644
--- a/src/Iris/ProofMode/Tactics/Exact.lean
+++ b/src/Iris/ProofMode/Tactics/Exact.lean
@@ -5,21 +5,18 @@ Authors: Lars König, Mario Carneiro, Michael Sammler
 -/
 import Iris.ProofMode.Tactics.Basic
 import Iris.ProofMode.Tactics.Assumption
-import Iris.ProofMode.Tactics.Remove
 
 namespace Iris.ProofMode
 open Lean Elab Tactic Meta Qq BI Std
 
 elab "iexact" colGt hyp:ident : tactic => do
-  let (mvar, { bi, hyps, goal, .. }) ← istart (← getMainGoal)
-  mvar.withContext do
-  let gs ← Goals.new bi
+  ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
   let uniq ← hyps.findWithInfo hyp
   let ⟨e', _, _, out, p, _, pf⟩ := hyps.remove true uniq
 
-  let some _ ← ProofMode.trySynthInstanceQAddingGoals gs q(FromAssumption $p .in $out $goal)
+  let some _ ← ProofModeM.trySynthInstanceQ q(FromAssumption $p .in $out $goal)
     | throwError "iexact: cannot unify {out} and {goal}"
-  let _ ← synthInstanceQ q(TCOr (Affine $e') (Absorbing $goal))
+  let .some _ ← trySynthInstanceQ q(TCOr (Affine $e') (Absorbing $goal))
+    | throwError "iexact: context is not affine or goal is not absorbing"
 
   mvar.assign q(assumption (Q := $goal) $pf)
-  replaceMainGoal (← gs.getGoals)
diff --git a/src/Iris/ProofMode/Tactics/Exists.lean b/src/Iris/ProofMode/Tactics/Exists.lean
index d1ca14c0..9c8a5594 100644
--- a/src/Iris/ProofMode/Tactics/Exists.lean
+++ b/src/Iris/ProofMode/Tactics/Exists.lean
@@ -8,17 +8,15 @@ import Iris.ProofMode.Tactics.Basic
 namespace Iris.ProofMode
 open Lean Elab Tactic Meta Qq BI
 
-theorem exists_intro' [BI PROP] {Φ : α → PROP} {P Q : PROP} [inst : FromExists P Φ]
+private theorem exists_intro' [BI PROP] {Φ : α → PROP} {P Q : PROP} [inst : FromExists P Φ]
     (a : α) (h : P ⊢ Q) : Φ a ⊢ Q :=
   ((exists_intro a).trans inst.1).trans h
 
 elab "iexists" xs:term,+ : tactic => do
   -- resolve existential quantifier with the given argument
+  ProofModeM.runTactic λ mvar { prop, e, hyps, goal, .. } => do
 
-  let (mvar, { prop, bi, e, hyps, goal, .. }) ← istart (← getMainGoal)
-  mvar.withContext do
   let mut new_goal_and_pf : ((g : Q($prop)) × Q($g ⊢ $goal)) := ⟨goal, q(.rfl)⟩
-  let gs ← Goals.new bi
 
   for x in xs.getElems do
     have new_goal : Q($prop) := new_goal_and_pf.1
@@ -26,15 +24,14 @@ elab "iexists" xs:term,+ : tactic => do
     let v ← mkFreshLevelMVar
     let α ← mkFreshExprMVarQ q(Sort v)
     let Φ ← mkFreshExprMVarQ q($α → $prop)
-    let some _ ← ProofMode.trySynthInstanceQAddingGoals gs q(FromExists $(new_goal) $Φ)
+    let some _ ← ProofModeM.trySynthInstanceQ q(FromExists $(new_goal) $Φ)
       | throwError "iexists: cannot turn {new_goal} into an existential quantifier"
     let x ← elabTermEnsuringTypeQ (u := .succ .zero) x α
     let newMVarIds ← getMVarsNoDelayed x
-    for mvar in newMVarIds do gs.addPureGoal mvar
+    for mvar in newMVarIds do addMVarGoal mvar
     let new_goal' : Q($prop) := Expr.headBeta q($Φ $x)
     let new_goal_pf' : Q($Φ $x ⊢ $goal) := q(exists_intro' _ $(new_goal_pf))
     new_goal_and_pf := ⟨new_goal', new_goal_pf'⟩
 
-  let m : Q($e ⊢ $(new_goal_and_pf.1)) ← gs.addGoal hyps new_goal_and_pf.1
+  let m : Q($e ⊢ $(new_goal_and_pf.1)) ← addBIGoal hyps new_goal_and_pf.1
   mvar.assign q($(m).trans $(new_goal_and_pf.2))
-  replaceMainGoal (← gs.getGoals)
diff --git a/src/Iris/ProofMode/Tactics/Have.lean b/src/Iris/ProofMode/Tactics/Have.lean
index 1c4e97a5..9dafcd71 100644
--- a/src/Iris/ProofMode/Tactics/Have.lean
+++ b/src/Iris/ProofMode/Tactics/Have.lean
@@ -10,12 +10,12 @@ import Iris.ProofMode.Tactics.Specialize
 namespace Iris.ProofMode
 open Lean Elab Tactic Meta Qq BI Std
 
-theorem have_asEmpValid [BI PROP] {φ} {P Q : PROP}
+private theorem have_asEmpValid [BI PROP] {φ} {P Q : PROP}
     [h1 : AsEmpValid .into φ P] (h : φ) : Q ⊢ Q ∗ P :=
   sep_emp.2.trans (sep_mono_r (asEmpValid_1 _ h))
 
-private def iHaveCore (gs : @Goals u prop bi) {e} (hyps : Hyps bi e)
-  (tm : Term) (name : TSyntax ``binderIdent) (keep : Bool) (mayPostpone : Bool) : TacticM (Name × (e' : _) × Hyps bi e' × Q($e ⊢ $e')) := do
+private def iHaveCore {e} (hyps : @Hyps u prop bi e)
+  (tm : Term) (name : TSyntax ``binderIdent) (keep : Bool) (mayPostpone : Bool) : ProofModeM (Name × (e' : _) × Hyps bi e' × Q($e ⊢ $e')) := do
   if let some uniq ← try? <| hyps.findWithInfo ⟨tm⟩ then
     -- assertion from the Iris context
     let ⟨_, hyps, _, out', p, _, pf⟩ := hyps.remove (!keep) uniq
@@ -33,29 +33,26 @@ private def iHaveCore (gs : @Goals u prop bi) {e} (hyps : Hyps bi e)
     let otherMVarIds ← getMVarsNoDelayed val
     let otherMVarIds := otherMVarIds.filter (!newMVarIds.contains ·)
     for mvar in newMVarIds ++ otherMVarIds do
-      gs.addPureGoal mvar
+      addMVarGoal mvar
 
     -- TODO: can we do this without re typechecking?
     let ⟨0, ty, val⟩ ← inferTypeQ val | throwError m!"{val} is not a Prop"
 
     let hyp ← mkFreshExprMVarQ q($prop)
-    let some _ ← ProofMode.trySynthInstanceQAddingGoals gs q(AsEmpValid .into $ty $hyp) | throwError m!"{ty} is not an entailment"
+    let some _ ← ProofModeM.trySynthInstanceQ q(AsEmpValid .into $ty $hyp) | throwError m!"{ty} is not an entailment"
 
     let ⟨uniq', hyps⟩ ← Hyps.addWithInfo bi name q(false) hyp hyps
     return ⟨uniq', _, hyps, q(have_asEmpValid $val)⟩
 
-def iHave (gs : @Goals u prop bi) {e} (hyps : Hyps bi e)
-  (pmt : PMTerm) (name : TSyntax ``binderIdent) (keep : Bool) (mayPostpone := false) : TacticM (Name × (e' : _) × Hyps bi e' × Q($e ⊢ $e')) := do
-  let ⟨uniq, _, hyps', pf⟩ ← iHaveCore gs hyps pmt.term name keep mayPostpone
-  let ⟨_, hyps'', pf'⟩ ← iSpecializeCore gs hyps' uniq pmt.spats
+def iHave{e} (hyps : @Hyps u prop bi e)
+  (pmt : PMTerm) (name : TSyntax ``binderIdent) (keep : Bool) (mayPostpone := false) : ProofModeM (Name × (e' : _) × Hyps bi e' × Q($e ⊢ $e')) := do
+  let ⟨uniq, _, hyps', pf⟩ ← iHaveCore hyps pmt.term name keep mayPostpone
+  let ⟨_, hyps'', pf'⟩ ← iSpecializeCore hyps' uniq pmt.spats
   return ⟨uniq, _, hyps'', q($(pf).trans $pf')⟩
 
 elab "ihave" colGt name:binderIdent " := " pmt:pmTerm  : tactic => do
   let pmt ← liftMacroM <| PMTerm.parse pmt
-  let (mvar, { bi, hyps, goal, .. }) ← istart (← getMainGoal)
-  mvar.withContext do
-  let gs ← Goals.new bi
-  let ⟨_, _, hyps, pf⟩ ← iHave gs hyps pmt name true
-  let pf' ← gs.addGoal hyps goal
+  ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
+  let ⟨_, _, hyps, pf⟩ ← iHave hyps pmt name true
+  let pf' ← addBIGoal hyps goal
   mvar.assign q(($pf).trans $pf')
-  replaceMainGoal (← gs.getGoals)
diff --git a/src/Iris/ProofMode/Tactics/Intro.lean b/src/Iris/ProofMode/Tactics/Intro.lean
index 5d901a91..a59bc771 100644
--- a/src/Iris/ProofMode/Tactics/Intro.lean
+++ b/src/Iris/ProofMode/Tactics/Intro.lean
@@ -1,26 +1,27 @@
 /-
 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, Mario Carneiro
+Authors: Lars König, Mario Carneiro, Michael Sammler
 -/
+import Iris.ProofMode.Patterns.IntroPattern
 import Iris.ProofMode.Tactics.Cases
 
 namespace Iris.ProofMode
 open Lean Elab Tactic Meta Qq BI Std
 
-theorem imp_intro_drop [BI PROP] {P Q A1 A2 : PROP} [inst : FromImp Q A1 A2] (h : P ⊢ A2) : P ⊢ Q :=
+private theorem imp_intro_drop [BI PROP] {P Q A1 A2 : PROP} [inst : FromImp Q A1 A2] (h : P ⊢ A2) : P ⊢ Q :=
   BI.imp_intro (and_elim_l' h) |>.trans inst.1
 
-theorem from_forall_intro [BI PROP] {P Q : PROP} {Φ : α → PROP} [inst : FromForall Q Φ]
+private theorem from_forall_intro [BI PROP] {P Q : PROP} {Φ : α → PROP} [inst : FromForall Q Φ]
     (h : ∀ a, P ⊢ Φ a) : P ⊢ Q :=
   (forall_intro h).trans inst.1
 
-theorem imp_intro_intuitionistic [BI PROP] {P Q A1 A2 B : PROP}
+private theorem imp_intro_intuitionistic [BI PROP] {P Q A1 A2 B : PROP}
     [FromImp Q A1 A2] [inst : IntoPersistently false A1 B] (h : P ∗ □ B ⊢ A2) : P ⊢ Q := by
   refine BI.imp_intro ?_ |>.trans from_imp
   exact (and_mono_r inst.1).trans <| persistently_and_intuitionistically_sep_r.1.trans h
 
-theorem wand_intro_intuitionistic [BI PROP] {P Q A1 A2 B : PROP}
+private theorem wand_intro_intuitionistic [BI PROP] {P Q A1 A2 B : PROP}
     [FromWand Q A1 A2] [inst : IntoPersistently false A1 B] [or : TCOr (Affine A1) (Absorbing A2)]
     (h : P ∗ □ B ⊢ A2) : P ⊢ Q := by
   refine (wand_intro ?_).trans from_wand
@@ -29,7 +30,7 @@ theorem wand_intro_intuitionistic [BI PROP] {P Q A1 A2 B : PROP}
   | TCOr.r => (sep_mono_r <| inst.1.trans absorbingly_intuitionistically.2).trans <|
       absorbingly_sep_r.1.trans <| (absorbingly_mono h).trans absorbing
 
-theorem imp_intro_spatial [BI PROP] {P Q A1 A2 B : PROP}
+private theorem imp_intro_spatial [BI PROP] {P Q A1 A2 B : PROP}
     [FromImp Q A1 A2] [inst : FromAffinely B A1] [or : TCOr (Persistent A1) (Intuitionistic P)]
     (h : P ∗ B ⊢ A2) : P ⊢ Q := by
   refine (BI.imp_intro ?_).trans from_imp
@@ -40,73 +41,73 @@ theorem imp_intro_spatial [BI PROP] {P Q A1 A2 B : PROP}
     (and_mono_l u.1).trans <| affinely_and_lr.1.trans <|
     persistently_and_intuitionistically_sep_l.1.trans <| sep_mono_l intuitionistically_elim
 
-theorem wand_intro_spatial [BI PROP] {P Q A1 A2 : PROP}
+private theorem wand_intro_spatial [BI PROP] {P Q A1 A2 : PROP}
     [FromWand Q A1 A2] (h : P ∗ A1 ⊢ A2) : P ⊢ Q := (wand_intro h).trans from_wand
 
 variable {prop : Q(Type u)} (bi : Q(BI $prop)) in
 partial def iIntroCore
-    {P} (gs : Goals bi) (hyps : Hyps bi P) (Q : Q($prop)) (pats : List iCasesPat) :
-    MetaM (Q($P ⊢ $Q)) := do
+    {P} (hyps : Hyps bi P) (Q : Q($prop)) (pats : List (Syntax × IntroPat)) :
+    ProofModeM (Q($P ⊢ $Q)) := do
   match pats with
-  | [] => gs.addGoal hyps Q
-  | pat :: pats =>
+  | [] => addBIGoal hyps Q
+  | (ref, .intro (.pure n)) :: pats =>
+    withRef ref do
+    let v ← mkFreshLevelMVar
+    let α : Quoted q(Sort v) ← mkFreshExprMVarQ q(Sort v)
+    let Φ : Quoted q($α → $prop) ← mkFreshExprMVarQ q($α → $prop)
+    let .some _ ← ProofModeM.trySynthInstanceQ q(FromForall $Q $Φ)
+      | throwError "iintro: {Q} cannot be turned into a universal quantifier or pure hypothesis"
+    let (n, ref) ← getFreshName n
+    withLocalDeclDQ n α fun x => do
+      addLocalVarInfo ref (← getLCtx) x α
+      have B : Q($prop) := Expr.headBeta q($Φ $x)
+      have : $B =Q $Φ $x := ⟨⟩
+      let pf : Q(∀ x, $P ⊢ $Φ x) ← mkLambdaFVars #[x] <|← iIntroCore hyps B pats
+      return q(from_forall_intro (Q := $Q) $pf)
+  | (ref, .intro pat) :: pats =>
+    withRef ref do
     let A1 ← mkFreshExprMVarQ q($prop)
     let A2 ← mkFreshExprMVarQ q($prop)
-    let fromImp ← try? (α := Q(FromImp $Q $A1 $A2)) do
-      synthInstanceQ q(FromImp $Q $A1 $A2)
+    let fromImp ← ProofModeM.trySynthInstanceQ q(FromImp $Q $A1 $A2)
     if let (.clear, some _) := (pat, fromImp) then
-      let pf ← iIntroCore gs hyps A2 pats
+      let pf ← iIntroCore hyps A2 pats
       return q(imp_intro_drop (Q := $Q) $pf)
     else
-    let alres ← try? (α := _ × (v : Level) × (α : Q(Sort v)) × (Φ : Q($α → $prop)) ×
-        Q(FromForall $Q $Φ)) do
-      let .one n := pat | failure
-      let v ← mkFreshLevelMVar
-      let α ← mkFreshExprMVarQ q(Sort v)
-      let Φ ← mkFreshExprMVarQ q($α → $prop)
-      Pure.pure ⟨n, v, α, Φ, ← synthInstanceQ q(FromForall $Q $Φ)⟩
-    if let some ⟨n, _, α, Φ, _⟩ := alres then
-      let (n, ref) ← getFreshName n
-      withLocalDeclDQ n α fun x => do
-        addLocalVarInfo ref (← getLCtx) x α
-        have B : Q($prop) := Expr.headBeta q($Φ $x)
-        have : $B =Q $Φ $x := ⟨⟩
-        let pf : Q(∀ x, $P ⊢ $Φ x) ← mkLambdaFVars #[x] <|← iIntroCore gs hyps B pats
-        return q(from_forall_intro (Q := $Q) $pf)
-    else
     let B ← mkFreshExprMVarQ q($prop)
     match pat, fromImp with
     | .intuitionistic pat, some _ =>
-      let _ ← synthInstanceQ q(IntoPersistently false $A1 $B)
-      let pf ← iCasesCore bi hyps A2 q(true) q(iprop(□ $B)) B ⟨⟩ pat (iIntroCore gs · A2 pats)
+      let .some _ ← ProofModeM.trySynthInstanceQ q(IntoPersistently false $A1 $B)
+        | throwError "iintro: {A1} not persistent"
+      let pf ← iCasesCore bi hyps A2 q(true) q(iprop(□ $B)) B ⟨⟩ pat (iIntroCore · A2 pats)
       return q(imp_intro_intuitionistic (Q := $Q) $pf)
     | .intuitionistic pat, none =>
-      let _ ← synthInstanceQ q(FromWand $Q $A1 $A2)
-      let _ ← synthInstanceQ q(IntoPersistently false $A1 $B)
-      let _ ← synthInstanceQ q(TCOr (Affine $A1) (Absorbing $A2))
-      let pf ← iCasesCore bi hyps A2 q(true) q(iprop(□ $B)) B ⟨⟩ pat (iIntroCore gs · A2 pats)
+      let .some _ ← ProofModeM.trySynthInstanceQ q(FromWand $Q $A1 $A2)
+        | throwError "iintro: {Q} not a wand"
+      let .some _ ← ProofModeM.trySynthInstanceQ q(IntoPersistently false $A1 $B)
+        | throwError "iintro: {A1} not persistent"
+      let .some _ ← trySynthInstanceQ q(TCOr (Affine $A1) (Absorbing $A2))
+        | throwError "iintro: {A1} not affine and the goal not absorbing"
+      let pf ← iCasesCore bi hyps A2 q(true) q(iprop(□ $B)) B ⟨⟩ pat (iIntroCore · A2 pats)
       return q(wand_intro_intuitionistic (Q := $Q) $pf)
     | _, some _ =>
-      let _ ← synthInstanceQ q(FromAffinely $B $A1)
-      let _ ← synthInstanceQ q(TCOr (Persistent $A1) (Intuitionistic $P))
-      let pf ← iCasesCore bi hyps A2 q(false) B B ⟨⟩ pat (iIntroCore gs · A2 pats)
+      -- should always succeed
+      let _ ← ProofModeM.synthInstanceQ q(FromAffinely $B $A1)
+      let .some _ ← trySynthInstanceQ q(TCOr (Persistent $A1) (Intuitionistic $P))
+        | throwError "iintro: {A1} is not persistent and spatial context is non-empty"
+      let pf ← iCasesCore bi hyps A2 q(false) B B ⟨⟩ pat (iIntroCore · A2 pats)
       return q(imp_intro_spatial (Q := $Q) $pf)
     | _, none =>
-      let _ ← synthInstanceQ q(FromWand $Q $A1 $A2)
-      let pf ← iCasesCore bi hyps A2 q(false) A1 A1 ⟨⟩ pat (iIntroCore gs · A2 pats)
+      let .some _ ← ProofModeM.trySynthInstanceQ q(FromWand $Q $A1 $A2)
+        | throwError "iintro: {Q} not a wand"
+      let pf ← iCasesCore bi hyps A2 q(false) A1 A1 ⟨⟩ pat (iIntroCore · A2 pats)
       return q(wand_intro_spatial (Q := $Q) $pf)
 
 
-elab "iintro" pats:(colGt icasesPat)* : tactic => do
+elab "iintro" pats:(colGt introPat)* : tactic => do
   -- parse syntax
-  let pats ← liftMacroM <| pats.mapM <| iCasesPat.parse
-
-  let (mvar, { bi, hyps, goal, .. }) ← istart (← getMainGoal)
-  mvar.withContext do
+  let pats ← liftMacroM <| pats.mapM <| IntroPat.parse
 
-  -- process patterns
-  let gs ← Goals.new bi
-  let pf ← iIntroCore bi gs hyps goal pats.toList
+  ProofModeM.runTactic λ mvar { bi, hyps, goal, .. } => do
+  let pf ← iIntroCore bi hyps goal pats.toList
 
   mvar.assign pf
-  replaceMainGoal (← gs.getGoals)
diff --git a/src/Iris/ProofMode/Tactics/LeftRight.lean b/src/Iris/ProofMode/Tactics/LeftRight.lean
index 3e801937..e864ad5f 100644
--- a/src/Iris/ProofMode/Tactics/LeftRight.lean
+++ b/src/Iris/ProofMode/Tactics/LeftRight.lean
@@ -8,39 +8,31 @@ import Iris.ProofMode.Tactics.Basic
 namespace Iris.ProofMode
 open Lean Elab.Tactic Meta Qq BI Std
 
-theorem from_or_l [BI PROP] {P Q A1 A2 : PROP} [inst : FromOr Q A1 A2]
+private theorem from_or_l [BI PROP] {P Q A1 A2 : PROP} [inst : FromOr Q A1 A2]
     (h1 : P ⊢ A1) : P ⊢ Q :=
   (or_intro_l' h1).trans inst.1
 
 elab "ileft" : tactic => do
-  let (mvar, { u, prop, bi, e, hyps, goal }) ← istart (← getMainGoal)
-  mvar.withContext do
-  let gs ← Goals.new bi
-
+  ProofModeM.runTactic λ mvar { prop, e, hyps, goal, .. } => do
   -- choose left side of disjunction
   let A1 ← mkFreshExprMVarQ prop
   let A2 ← mkFreshExprMVarQ prop
-  let some _ ← ProofMode.trySynthInstanceQAddingGoals gs q(FromOr $goal $A1 $A2)
+  let some _ ← ProofModeM.trySynthInstanceQ q(FromOr $goal $A1 $A2)
     | throwError "ileft: {goal} is not a disjunction"
 
-  let m : Q($e ⊢ $A1) ← gs.addGoal hyps A1
+  let m : Q($e ⊢ $A1) ← addBIGoal hyps A1
   mvar.assign q(from_or_l (Q := $goal) $m)
-  replaceMainGoal (← gs.getGoals)
 
-theorem from_or_r [BI PROP] {P Q A1 A2 : PROP} [inst : FromOr Q A1 A2]
+private theorem from_or_r [BI PROP] {P Q A1 A2 : PROP} [inst : FromOr Q A1 A2]
     (h1 : P ⊢ A2) : P ⊢ Q :=
   (or_intro_r' h1).trans inst.1
 
 elab "iright" : tactic => do
-  let (mvar, { u, prop, bi, e, hyps, goal }) ← istart (← getMainGoal)
-  mvar.withContext do
-  let gs ← Goals.new bi
-
+  ProofModeM.runTactic λ mvar { prop, e, hyps, goal, .. } => do
   -- choose right side of disjunction
   let A1 ← mkFreshExprMVarQ prop
   let A2 ← mkFreshExprMVarQ prop
-  let some _ ← ProofMode.trySynthInstanceQAddingGoals gs q(FromOr $goal $A1 $A2)
-    | throwError "ileft: {goal} is not a disjunction"
-  let m : Q($e ⊢ $A2) ← gs.addGoal hyps A2
+  let some _ ← ProofModeM.trySynthInstanceQ q(FromOr $goal $A1 $A2)
+    | throwError "iright: {goal} is not a disjunction"
+  let m : Q($e ⊢ $A2) ← addBIGoal hyps A2
   mvar.assign q(from_or_r (Q := $goal) $m)
-  replaceMainGoal (← gs.getGoals)
diff --git a/src/Iris/ProofMode/Tactics/Move.lean b/src/Iris/ProofMode/Tactics/Move.lean
deleted file mode 100644
index ad57d4fb..00000000
--- a/src/Iris/ProofMode/Tactics/Move.lean
+++ /dev/null
@@ -1,129 +0,0 @@
-/-
-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, Mario Carneiro
--/
-import Iris.ProofMode.Expr
-import Iris.ProofMode.Classes
-
-namespace Iris.ProofMode
-open Lean Elab Tactic Meta Qq BI Std
-
-def Replaces [BI PROP] (K A B : PROP) := (B -∗ K) ⊢ (A -∗ K)
-
-theorem replaces_r [BI PROP] {K P Q Q' : PROP} (h : Replaces K Q Q') :
-    Replaces K iprop(P ∗ Q) iprop(P ∗ Q') :=
-  wand_intro <| sep_assoc.2.trans <| wand_elim <|
-  (wand_intro <| sep_assoc.1.trans wand_elim_l).trans h
-
-theorem replaces_l [BI PROP] {K P P' Q : PROP} (h : Replaces K P P') :
-    Replaces K iprop(P ∗ Q) iprop(P' ∗ Q) :=
-  (wand_mono_l sep_comm.1).trans <| (replaces_r h).trans (wand_mono_l sep_comm.1)
-
-theorem Replaces.apply [BI PROP] {P P' Q : PROP}
-    (h : Replaces Q P P') (h_entails : P' ⊢ Q) : P ⊢ Q :=
-  wand_entails <| (entails_wand h_entails).trans h
-
-inductive ReplaceHyp {prop : Q(Type u)} (bi : Q(BI $prop)) (Q : Q($prop)) where
-  | none
-  | unchanged (ehyps') (hyps' : Hyps bi ehyps')
-  | main (e e' : Q($prop)) (hyps' : Hyps bi e') (pf : Q(Replaces $Q $e $e'))
-
-variable [Monad m] {prop : Q(Type u)} (bi : Q(BI $prop)) (Q : Q($prop))
-  (uniq : Name) (repl : Name → Q(Bool) → Q($prop) → MetaM (ReplaceHyp bi Q)) in
-def Hyps.replace : ∀ {e}, Hyps bi e → MetaM (ReplaceHyp bi Q)
-  | _, .emp _ => pure .none
-  | _, .hyp _ name uniq' p ty _ => do
-    if uniq == uniq' then
-      let res ← repl name p ty
-      if let .main e e' hyps' _ := res then
-        let e' ← instantiateMVarsQ e'
-        if e == e' then
-          return .unchanged _ hyps'
-      return res
-    else return .none
-  | _, .sep _ elhs erhs _ lhs rhs => do
-    match ← rhs.replace with
-    | .unchanged _ rhs' => return .unchanged _ (.mkSep lhs rhs')
-    | .main erhs₀ _ rhs' pf =>
-      let hyps' := .mkSep lhs rhs'
-      return .main q(iprop($elhs ∗ $erhs₀)) _ hyps' q(replaces_r $pf)
-    | .none => match ← lhs.replace with
-      | .unchanged _ lhs' => return .unchanged _ (.mkSep lhs' rhs)
-      | .main elhs₀ _ lhs' pf =>
-        let hyps' := .mkSep lhs' rhs
-        return .main q(iprop($elhs₀ ∗ $erhs)) _ hyps' q(replaces_l $pf)
-      | .none => pure .none
-
-theorem to_persistent_spatial [BI PROP] {P P' Q : PROP}
-    [hP : IntoPersistently false P P'] [or : TCOr (Affine P) (Absorbing Q)] :
-    Replaces Q P iprop(□ P') :=
-  match or with
-  | TCOr.l => wand_mono_l <| (affine_affinely P).2.trans (affinely_mono hP.1)
-  | TCOr.r =>
-    wand_intro <| (sep_mono_r <| hP.1.trans absorbingly_intuitionistically.2).trans <|
-    absorbingly_sep_r.1.trans <| (absorbingly_mono wand_elim_l).trans absorbing
-
-theorem to_persistent_intuitionistic [BI PROP] {P P' Q : PROP}
-    [hP : IntoPersistently true P P'] : Replaces Q iprop(□ P) iprop(□ P') :=
-  wand_mono_l <| affinely_mono hP.1
-
-elab "iintuitionistic" colGt hyp:ident : tactic => do
-  let mvar ← getMainGoal
-  mvar.withContext do
-  let g ← instantiateMVars <| ← mvar.getType
-  let some { prop, bi, hyps, goal, .. } := parseIrisGoal? g | throwError "not in proof mode"
-
-  let uniq ← hyps.findWithInfo hyp
-  match ← hyps.replace bi goal uniq fun name p ty => do
-    let P' ← mkFreshExprMVarQ prop
-    let _ ← synthInstanceQ q(IntoPersistently $p $ty $P')
-    addHypInfo hyp name uniq prop P' (isBinder := true)
-    match matchBool p with
-    | .inl _ =>
-      return .main q(iprop(□ $ty)) q(iprop(□ $P')) (.mkHyp bi name uniq p P' _)
-        q(to_persistent_intuitionistic)
-    | .inr _ =>
-      let _ ← synthInstanceQ q(TCOr (Affine $ty) (Absorbing $goal))
-      return .main ty q(iprop(□ $P')) (.mkHyp bi name uniq q(true) P' _) q(to_persistent_spatial)
-  with
-  | .none => panic! "missing variable"
-  | .unchanged _ hyps' =>
-    mvar.setType <| IrisGoal.toExpr { prop, bi, hyps := hyps', goal, .. }
-  | .main _e e' hyps' pf =>
-    let m : Q($e' ⊢ $goal) ← mkFreshExprSyntheticOpaqueMVar <|
-      IrisGoal.toExpr { prop, bi, hyps := hyps', goal, .. }
-    mvar.assign q(Replaces.apply $pf $m)
-    replaceMainGoal [m.mvarId!]
-
-theorem from_affine [BI PROP] {p : Bool} {P P' Q : PROP} [hP : FromAffinely P' P p] :
-    Replaces Q iprop(□?p P) P' :=
-  wand_mono_l <| affinelyIf_of_intuitionisticallyIf.trans hP.1
-
-elab "ispatial" colGt hyp:ident : tactic => do
-  let mvar ← getMainGoal
-  mvar.withContext do
-  let g ← instantiateMVars <| ← mvar.getType
-  let some { prop, bi, hyps, goal, .. } := parseIrisGoal? g | throwError "not in proof mode"
-
-  let uniq ← hyps.findWithInfo hyp
-  match ← hyps.replace bi goal uniq fun name p ty => do
-    let P' ← mkFreshExprMVarQ prop
-    match matchBool p with
-    | .inl _ =>
-      let _ ← synthInstanceQ q(FromAffinely $P' $ty true)
-      addHypInfo hyp name uniq prop P' (isBinder := true)
-      return .main q(iprop(□ $ty)) P' (.mkHyp bi name uniq q(false) P' _) q(from_affine (p := true))
-    | .inr _ =>
-      let _ ← synthInstanceQ q(FromAffinely $P' $ty false)
-      addHypInfo hyp name uniq prop P' (isBinder := true)
-      return .main ty P' (.mkHyp bi name uniq p P' _) q(from_affine (p := false))
-  with
-  | .none => panic! "missing variable"
-  | .unchanged _ hyps' =>
-    mvar.setType <| IrisGoal.toExpr { prop, bi, hyps := hyps', goal, .. }
-  | .main _e e' hyps' pf =>
-    let m : Q($e' ⊢ $goal) ← mkFreshExprSyntheticOpaqueMVar <|
-      IrisGoal.toExpr { prop, bi, hyps := hyps', goal, .. }
-    mvar.assign q(Replaces.apply $pf $m)
-    replaceMainGoal [m.mvarId!]
diff --git a/src/Iris/ProofMode/Tactics/Pure.lean b/src/Iris/ProofMode/Tactics/Pure.lean
index abfb99cf..220a5c95 100644
--- a/src/Iris/ProofMode/Tactics/Pure.lean
+++ b/src/Iris/ProofMode/Tactics/Pure.lean
@@ -5,12 +5,11 @@ Authors: Lars König, Mario Carneiro
 -/
 import Iris.ProofMode.Instances
 import Iris.ProofMode.Tactics.Basic
-import Iris.ProofMode.Tactics.Remove
 
 namespace Iris.ProofMode
 open Lean Elab Tactic Meta Qq BI Std
 
-theorem pure_elim_spatial [BI PROP] {P P' A Q : PROP} {φ : Prop}
+private theorem pure_elim_spatial [BI PROP] {P P' A Q : PROP} {φ : Prop}
     [hA : IntoPure A φ] [or : TCOr (Affine A) (Absorbing Q)]
     (h : P ⊣⊢ P' ∗ A) (h_entails : φ → P' ⊢ Q) : P ⊢ Q :=
   h.1.trans <| match or with
@@ -22,86 +21,74 @@ theorem pure_elim_spatial [BI PROP] {P P' A Q : PROP} {φ : Prop}
     absorbingly_sep_lr.2.trans <| persistent_and_affinely_sep_r.2.trans <|
     pure_elim_r fun hφ => (absorbingly_mono <| h_entails hφ).trans absorbing
 
-theorem pure_elim_intuitionistic [BI PROP] {P P' A Q : PROP} {φ : Prop}
+private theorem pure_elim_intuitionistic [BI PROP] {P P' A Q : PROP} {φ : Prop}
     [IntoPure A φ] (h : P ⊣⊢ P' ∗ □ A) (h' : φ → P' ⊢ Q) : P ⊢ Q :=
   pure_elim_spatial h h'
 
-def ipureCore {prop : Q(Type u)} (_bi : Q(BI $prop))
-    (P P' A Q : Q($prop)) (name : TSyntax ``binderIdent) (pf : Q($P ⊣⊢ $P' ∗ $A))
-    (k : (φ : Q(Prop)) → Q($φ) → MetaM (α × Q($P' ⊢ $Q))) : MetaM (α × Q($P ⊢ $Q)) := do
+def iPureCore {prop : Q(Type u)} (_bi : Q(BI $prop))
+    (P P' : Q($prop)) (p : Q(Bool)) (A Q : Q($prop)) (name : TSyntax ``binderIdent) (pf : Q($P ⊣⊢ $P' ∗ □?$p $A))
+    (k : (φ : Q(Prop)) → Q($φ) → ProofModeM (Q($P' ⊢ $Q))) : ProofModeM (Q($P ⊢ $Q)) := do
   let φ : Q(Prop) ← mkFreshExprMVarQ q(Prop)
-  let inst ← if A.isAppOfArity ``intuitionistically 3 then
-    have A' : Q($prop) := A.appArg!
-    synthInstance q(IntoPure $A' $φ)
-  else
-    synthInstance q(IntoPure $A $φ)
+  let .some _ ← ProofModeM.trySynthInstanceQ q(IntoPure $A $φ)
+    | throwError "ipure: {A} is not pure"
 
   let (name, ref) ← getFreshName name
-  withLocalDeclDQ name φ fun p => do
-    addLocalVarInfo ref (← getLCtx) p φ
-    let (a, m) ← k φ p
-    let f : Q($φ → $P' ⊢ $Q) ← mkLambdaFVars #[p] m
-
-    if A.isAppOfArity ``intuitionistically 3 then
-      have A' : Q($prop) := A.appArg!
-      have : $A =Q iprop(□ $A') := ⟨⟩
-      have : Q(IntoPure $A' $φ) := inst
-      pure (a, q(pure_elim_intuitionistic $pf $f))
-    else
-      let _ ← synthInstanceQ q(TCOr (Affine $A) (Absorbing $Q))
-      have : Q(IntoPure $A $φ) := inst
-      pure (a, q(pure_elim_spatial $pf $f))
+  withLocalDeclDQ name φ fun h => do
+    addLocalVarInfo ref (← getLCtx) h φ
+    let m ← k φ h
+    let f : Q($φ → $P' ⊢ $Q) ← mkLambdaFVars #[h] m
+
+    match matchBool p with
+    | .inl _ =>
+      return (q(pure_elim_intuitionistic $pf $f))
+    | .inr _ =>
+      let .some _ ← trySynthInstanceQ q(TCOr (Affine $A) (Absorbing $Q))
+        | throwError "ipure: {A} is not affine and the goal not absorbing"
+      return q(pure_elim_spatial (A:=$A) $pf $f)
 
 elab "ipure" colGt hyp:ident : tactic => do
-  let mvar ← getMainGoal
-  mvar.withContext do
-  let g ← instantiateMVars <| ← mvar.getType
-  let some { prop, bi, e, hyps, goal, .. } := parseIrisGoal? g | throwError "not in proof mode"
+  ProofModeM.runTactic λ mvar { bi, e, hyps, goal, .. } => do
 
   let uniq ← hyps.findWithInfo hyp
-  let ⟨e', hyps', out, _, _, _, pf⟩ := hyps.remove true uniq
+  let ⟨e', hyps', _, out', p, _, pf⟩ := hyps.remove true uniq
 
-  let (m, pf) ← ipureCore bi e e' out goal (← `(binderIdent| $hyp:ident)) pf fun _ _ => do
-    let m ← mkFreshExprSyntheticOpaqueMVar <| IrisGoal.toExpr { prop, bi, hyps := hyps', goal, .. }
-    pure (m, m)
+  let pf ← iPureCore bi e e' p out' goal (← `(binderIdent| $hyp:ident)) pf fun _ _ => addBIGoal hyps' goal
 
   mvar.assign pf
-  replaceMainGoal [m.mvarId!]
 
--- TODO: Is this necessary or can it be replaced by ipure_intro; trivial?
 elab "iemp_intro" : tactic => do
-  let (mvar, { prop, e, goal, .. }) ← istart (← getMainGoal)
-  mvar.withContext do
+  ProofModeM.runTactic λ mvar { prop, e, goal, .. } => do
 
   let .true ← isDefEq goal q(emp : $prop) | throwError "goal is not `emp`"
-  let _ ← synthInstanceQ q(Affine $e)
+  let .some _ ← trySynthInstanceQ q(Affine $e)
+    | throwError "iemp_intro: context is not affine"
   mvar.assign q(affine (P := $e))
-  replaceMainGoal []
 
-theorem pure_intro_affine [BI PROP] {Q : PROP} {φ : Prop}
+private theorem pure_intro_affine [BI PROP] {Q : PROP} {φ : Prop}
     [h : FromPure true Q φ] [Affine P] (hφ : φ) : P ⊢ Q :=
   (affine.trans (eq_true hφ ▸ affinely_true.2)).trans h.1
 
-theorem pure_intro_spatial [BI PROP] {Q : PROP} {φ : Prop}
+private theorem pure_intro_spatial [BI PROP] {Q : PROP} {φ : Prop}
     [h : FromPure false Q φ] (hφ : φ) : P ⊢ Q :=
   (pure_intro hφ).trans h.1
 
 elab "ipure_intro" : tactic => do
-  let (mvar, { e, goal, .. }) ← istart (← getMainGoal)
-  mvar.withContext do
+  ProofModeM.runTactic λ mvar { e, goal, .. } => do
 
   let b : Q(Bool) ← mkFreshExprMVarQ q(Bool)
   let φ : Q(Prop) ← mkFreshExprMVarQ q(Prop)
-  let _ ← synthInstanceQ q(FromPure $b $goal $φ)
+  let .some _ ← ProofModeM.trySynthInstanceQ q(FromPure $b $goal $φ)
+    | throwError "ipure_intro: {goal} is not pure"
   let m : Q($φ) ← mkFreshExprMVar (← instantiateMVars φ)
+  addMVarGoal m.mvarId!
 
   match ← whnf b with
   | .const ``true _ =>
     have : $b =Q true := ⟨⟩
-    let _ ← synthInstanceQ q(Affine $e)
+    let .some _ ← trySynthInstanceQ q(Affine $e)
+      | throwError "ipure_intro: context is not affine"
     mvar.assign q(pure_intro_affine (P := $e) (Q := $goal) $m)
   | .const ``false _ =>
     have : $b =Q false := ⟨⟩
     mvar.assign q(pure_intro_spatial (P := $e) (Q := $goal) $m)
-  | _ => throwError "failed to prove `FromPure _ {goal} _`"
-  replaceMainGoal [m.mvarId!]
+  | _ => throwError "ipure_intro: {b} must be either true or false"
diff --git a/src/Iris/ProofMode/Tactics/Remove.lean b/src/Iris/ProofMode/Tactics/Remove.lean
deleted file mode 100644
index bef16bf9..00000000
--- a/src/Iris/ProofMode/Tactics/Remove.lean
+++ /dev/null
@@ -1,83 +0,0 @@
-/-
-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, Mario Carneiro
--/
-import Iris.BI
-import Iris.ProofMode.Expr
-import Iris.ProofMode.Classes
-import Iris.Std
-import Lean.Elab
-
-namespace Iris.ProofMode
-open Lean Elab.Tactic Meta Qq BI
-
-structure RemoveHyp {prop : Q(Type u)} (bi : Q(BI $prop)) (e : Q($prop)) where
-  (e' : Q($prop)) (hyps' : Hyps bi e') (out out' : Q($prop)) (p : Q(Bool))
-  (eq : $out =Q iprop(□?$p $out'))
-  (pf : Q($e ⊣⊢ $e' ∗ $out))
-  deriving Inhabited
-
-inductive RemoveHypCore {prop : Q(Type u)} (bi : Q(BI $prop)) (e : Q($prop)) (α : Type) where
-  | none
-  | one (a : α) (out' : Q($prop)) (p : Q(Bool)) (eq : $e =Q iprop(□?$p $out'))
-  | main (a : α) (_ : RemoveHyp bi e)
-
-theorem remove_l [BI PROP] {P P' Q R : PROP} (h : P ⊣⊢ P' ∗ R) :
-    P ∗ Q ⊣⊢ (P' ∗ Q) ∗ R :=
-  (sep_congr_l h).trans sep_right_comm
-
-theorem remove_r [BI PROP] {P Q Q' R : PROP} (h : Q ⊣⊢ Q' ∗ R) :
-    P ∗ Q ⊣⊢ (P ∗ Q') ∗ R :=
-  (sep_congr_r h).trans sep_assoc.symm
-
-theorem intuitionistically_sep_dup [BI PROP] {P : PROP} : □ P ⊣⊢ □ P ∗ □ P :=
-  intuitionistically_sep_idem.symm
-
-variable [Monad m] {prop : Q(Type u)} (bi : Q(BI $prop)) (rp : Bool)
-  (check : Name → Name → Q(Bool) → Q($prop) → m (Option α)) in
-/-- If `rp` is true, the hyp will be removed even if it is in the intuitionistic context. -/
-def Hyps.removeCore : ∀ {e}, Hyps bi e → m (RemoveHypCore bi e α)
-  | _, .emp _ => pure .none
-  | e, h@(.hyp _ name uniq p ty _) => do
-    if let some a ← check name uniq p ty then
-      match matchBool p, rp with
-      | .inl _, false =>
-        have : $e =Q iprop(□ $ty) := ⟨⟩
-        return .main a ⟨e, h, e, ty, q(true), ⟨⟩, q(intuitionistically_sep_dup)⟩
-      | _, _ => return .one a ty p ⟨⟩
-    else
-      return .none
-  | _, .sep _ elhs erhs _ lhs rhs => do
-    match ← rhs.removeCore with
-    | .one a out' p h =>
-      return .main a ⟨elhs, lhs, erhs, out', p, h, q(.rfl)⟩
-    | .main a ⟨_, rhs', out, out', p, h, pf⟩ =>
-      let hyps' := .mkSep lhs rhs'
-      return .main a ⟨_, hyps', out, out', p, h, q(remove_r $pf)⟩
-    | .none => match ← lhs.removeCore with
-      | .one a out' p h =>
-        return .main a ⟨erhs, rhs, elhs, out', p, h, q(sep_comm)⟩
-      | .main a ⟨_, lhs', out, out', p, h, pf⟩ =>
-        let hyps' := .mkSep lhs' rhs
-        return .main a ⟨_, hyps', out, out', p, h, q(remove_l $pf)⟩
-      | .none => pure .none
-
-theorem sep_emp_rev [BI PROP] {P : PROP} : P ⊣⊢ P ∗ emp := sep_emp.symm
-
-theorem emp_sep_rev [BI PROP] {P : PROP} : P ⊣⊢ emp ∗ P := emp_sep.symm
-
-def Hyps.removeG [Monad m] {prop : Q(Type u)} {bi : Q(BI $prop)} {e : Q(Prop)}
-    (rp : Bool) (hyps : Hyps bi e)
-    (check : Name → Name → Q(Bool) → Q($prop) → m (Option α)) :
-    m (Option (α × RemoveHyp bi e)) := do
-  match ← hyps.removeCore bi rp check with
-  | .none => return none
-  | .one a out' p h => return some ⟨a, _, .mkEmp bi, e, out', p, h, q(emp_sep_rev)⟩
-  | .main a res => return some (a, res)
-
-def Hyps.remove {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
-    (rp : Bool) (hyps : Hyps bi e) (uniq : Name) : RemoveHyp bi e :=
-  match Id.run (hyps.removeG rp fun _ uniq' _ _ => if uniq == uniq' then some () else none) with
-  | some (_, r) => r
-  | none => panic! "variable not found"
diff --git a/src/Iris/ProofMode/Tactics/Rename.lean b/src/Iris/ProofMode/Tactics/Rename.lean
index 19d364fb..70c87579 100644
--- a/src/Iris/ProofMode/Tactics/Rename.lean
+++ b/src/Iris/ProofMode/Tactics/Rename.lean
@@ -3,41 +3,22 @@ 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, Mario Carneiro
 -/
-import Iris.BI
-import Iris.ProofMode.Expr
-import Iris.ProofMode.Classes
 import Iris.ProofMode.Tactics.Basic
-import Iris.Std
-import Lean.Elab
 
 namespace Iris.ProofMode
 open Lean Elab Tactic Qq
 
-variable (oldUniq new : Name) {prop : Q(Type u)} {bi : Q(BI $prop)} in
-def Hyps.rename : ∀ {e}, Hyps bi e → Option (Hyps bi e)
-  | _, .emp _ => none
-  | _, .sep _ _ _ _ lhs rhs =>
-    match rhs.rename with
-    | some rhs' => some (.mkSep lhs rhs' _)
-    | none => match lhs.rename with
-      | some lhs' => some (.mkSep lhs' rhs _)
-      | none => none
-  | _, .hyp _ _ uniq p ty _ =>
-    if oldUniq == uniq then some (Hyps.mkHyp bi new uniq p ty _) else none
-
 elab "irename" colGt nameFrom:ident " => " colGt nameTo:ident : tactic => do
-  -- find hypothesis index
-  let mvar ← getMainGoal
-  mvar.withContext do
-  let g ← instantiateMVars <| ← mvar.getType
-  let some { prop, bi, hyps, goal, .. } := parseIrisGoal? g | throwError "not in proof mode"
+  ProofModeM.runTactic λ mvar { prop, bi, hyps, goal, .. } => do
 
-  let some (uniq, _, ty) := hyps.find? nameFrom.getId | throwError "unknown hypothesis"
+  -- find hypothesis index
+  let some (uniq, _, ty) := hyps.find? nameFrom.getId | throwError "irename: unknown hypothesis"
   addHypInfo nameFrom nameFrom.getId uniq prop ty
   let some hyps' := hyps.rename uniq nameTo.getId | unreachable!
   addHypInfo nameTo nameTo.getId uniq prop ty (isBinder := true)
 
   mvar.setType (IrisGoal.toExpr { prop, bi, hyps := hyps', goal, .. })
+  addMVarGoal mvar
 
 elab "irename" ":" colGt ty:term " => " colGt nameTo:ident : tactic => do
   -- parse syntax
@@ -45,14 +26,12 @@ elab "irename" ":" colGt ty:term " => " colGt nameTo:ident : tactic => do
     throwUnsupportedSyntax
 
   -- find hypothesis index
-  let mvar ← getMainGoal
-  mvar.withContext do
-  let g ← instantiateMVars <| ← mvar.getType
-  let some { prop, bi, hyps, goal, .. } := parseIrisGoal? g | throwError "not in proof mode"
+  ProofModeM.runTactic λ mvar { prop, bi, hyps, goal, .. } => do
 
   let ty ← elabTerm ty prop
-  let (uniq, _, ty) ← try selectHyp ty hyps catch _ => throwError "unknown hypothesis"
+  let (uniq, _, ty) ← try Hyps.select ty hyps catch _ => throwError "irename: unknown hypothesis"
   let some hyps' := hyps.rename uniq nameTo.getId | unreachable!
   addHypInfo nameTo nameTo.getId uniq prop ty (isBinder := true)
 
   mvar.setType (IrisGoal.toExpr { prop, bi, hyps := hyps', goal, .. })
+  addMVarGoal mvar
diff --git a/src/Iris/ProofMode/Tactics/Specialize.lean b/src/Iris/ProofMode/Tactics/Specialize.lean
index 082192a7..deee83a6 100644
--- a/src/Iris/ProofMode/Tactics/Specialize.lean
+++ b/src/Iris/ProofMode/Tactics/Specialize.lean
@@ -5,17 +5,15 @@ Authors: Lars König, Mario Carneiro, Michael Sammler
 -/
 import Iris.ProofMode.Patterns.ProofModeTerm
 import Iris.ProofMode.Tactics.Basic
-import Iris.ProofMode.Tactics.Remove
-import Iris.ProofMode.Tactics.Split
 
 namespace Iris.ProofMode
 open Lean Elab Tactic Meta Qq BI Std
 
-structure SpecializeState {prop : Q(Type u)} (bi : Q(BI $prop)) (orig : Q($prop)) where
+private structure SpecializeState {prop : Q(Type u)} (bi : Q(BI $prop)) (orig : Q($prop)) where
   (e : Q($prop)) (hyps : Hyps bi e) (p : Q(Bool)) (out : Q($prop))
   pf : Q($orig ⊢ $e ∗ □?$p $out)
 
-theorem specialize_wand [BI PROP] {q p : Bool} {A1 A2 A3 Q P1 P2 : PROP}
+private theorem specialize_wand [BI PROP] {q p : Bool} {A1 A2 A3 Q P1 P2 : PROP}
     (h1 : A1 ⊢ A2 ∗ □?q Q) (h2 : A2 ⊣⊢ A3 ∗ □?p P1)
     [h3 : IntoWand q p Q .in P1 .out P2] :
     A1 ⊢ A3 ∗ □?(p && q) P2 := by
@@ -28,18 +26,18 @@ theorem specialize_wand [BI PROP] {q p : Bool} {A1 A2 A3 Q P1 P2 : PROP}
 
 -- TODO: if q is true and A1 is persistent, this proof can guarantee □ P2 instead of P2
 -- see https://gitlab.mpi-sws.org/iris/iris/-/blob/846ed45bed6951035c6204fef365d9a344022ae6/iris/proofmode/coq_tactics.v#L336
-theorem specialize_wand_subgoal [BI PROP] {q : Bool} {A1 A2 A3 A4 Q P1 : PROP} P2
+private theorem specialize_wand_subgoal [BI PROP] {q : Bool} {A1 A2 A3 A4 Q P1 : PROP} P2
     (h1 : A1 ⊢ A2 ∗ □?q Q) (h2 : A2 ⊣⊢ A3 ∗ A4) (h3 : A4 ⊢ P1)
     [inst : IntoWand q false Q .out P1 .out P2] : A1 ⊢ A3 ∗ P2 := by
   refine h1.trans <| (sep_mono_l h2.1).trans <| sep_assoc.1.trans (sep_mono_r ((sep_mono_l h3).trans ?_))
   exact (sep_mono_r inst.1).trans wand_elim_r
 
-theorem specialize_forall [BI PROP] {p : Bool} {A1 A2 P : PROP} {α : Sort _} {Φ : α → PROP}
+private theorem specialize_forall [BI PROP] {p : Bool} {A1 A2 P : PROP} {α : Sort _} {Φ : α → PROP}
     [inst : IntoForall P Φ] (h : A1 ⊢ A2 ∗ □?p P) (a : α) : A1 ⊢ A2 ∗ □?p (Φ a) := by
   refine h.trans <| sep_mono_r <| intuitionisticallyIf_mono <| inst.1.trans (forall_elim a)
 
-def SpecializeState.process_wand (gs : @Goals u prop bi) :
-    @SpecializeState u prop bi orig → SpecPat → TermElabM (SpecializeState bi orig)
+private def SpecializeState.process_wand :
+    @SpecializeState u prop bi orig → SpecPat → ProofModeM (SpecializeState bi orig)
   | { hyps, p, out, pf, .. }, .ident i => do
     let uniq ← hyps.findWithInfo i
     let ⟨e', hyps', out₁, out₁', p1, _, pf'⟩ := hyps.remove false uniq
@@ -48,7 +46,7 @@ def SpecializeState.process_wand (gs : @Goals u prop bi) :
     have : $p2 =Q ($p1 && $p) := ⟨⟩
 
     let out₂ ← mkFreshExprMVarQ prop
-    let some _ ← ProofMode.trySynthInstanceQAddingGoals gs q(IntoWand $p $p1 $out .in $out₁' .out $out₂) |
+    let some _ ← ProofModeM.trySynthInstanceQ q(IntoWand $p $p1 $out .in $out₁' .out $out₂) |
       throwError m!"ispecialize: cannot instantiate {out} with {out₁'}"
     let pf := q(specialize_wand $pf $pf')
     return { e := e', hyps := hyps', p := p2, out := out₂, pf }
@@ -56,12 +54,13 @@ def SpecializeState.process_wand (gs : @Goals u prop bi) :
     let v ← mkFreshLevelMVar
     let α : Q(Sort v) ← mkFreshExprMVarQ q(Sort v)
     let Φ : Q($α → $prop) ← mkFreshExprMVarQ q($α → $prop)
-    let some _ ← ProofMode.trySynthInstanceQAddingGoals gs q(IntoForall $out $Φ) | throwError "ispecialize: {out} is not a lean premise"
+    let some _ ← ProofModeM.trySynthInstanceQ q(IntoForall $out $Φ)
+      | throwError "ispecialize: {out} is not a lean premise"
     let x ← elabTermEnsuringTypeQ (u := .succ .zero) t α
     have out' : Q($prop) := Expr.headBeta q($Φ $x)
     have : $out' =Q $Φ $x := ⟨⟩
     let newMVarIds ← getMVarsNoDelayed x
-    for mvar in newMVarIds do gs.addPureGoal mvar
+    for mvar in newMVarIds do addMVarGoal mvar
     return { e, hyps, p, out := out', pf := q(specialize_forall $pf $x) }
   | { hyps, p, out, pf, .. }, .goal ns g => do
     let mut uniqs : NameSet := {}
@@ -70,31 +69,30 @@ def SpecializeState.process_wand (gs : @Goals u prop bi) :
     let ⟨el', _, hypsl', hypsr', h'⟩ := Hyps.split bi (λ _ uniq => uniqs.contains uniq) hyps
     let out₁ ← mkFreshExprMVarQ prop
     let out₂ ← mkFreshExprMVarQ prop
-    let some _ ← ProofMode.trySynthInstanceQAddingGoals gs q(IntoWand $p false $out .out $out₁ .out $out₂) | throwError m!"ispecialize: {out} is not a wand"
-    let pf' ← gs.addGoal hypsr' out₁ g
+    let some _ ← ProofModeM.trySynthInstanceQ q(IntoWand $p false $out .out $out₁ .out $out₂)
+      | throwError m!"ispecialize: {out} is not a wand"
+    let pf' ← addBIGoal hypsr' out₁ g
     let pf := q(specialize_wand_subgoal $out₂ $pf $h' $pf')
     return { e := el', hyps := hypsl', p := q(false), out := out₂, pf }
 
-def iSpecializeCore (gs : @Goals u prop bi) {e} (hyps : Hyps bi e)
-  (uniq : Name) (spats : List SpecPat) : TacticM ((e' : _) × Hyps bi e' × Q($e ⊢ $e')) := do
+def iSpecializeCore {e} (hyps : @Hyps u prop bi e)
+  (uniq : Name) (spats : List SpecPat) : ProofModeM ((e' : _) × Hyps bi e' × Q($e ⊢ $e')) := do
   let some ⟨name, _, hyps, _, out, p, _, pf⟩ := Id.run <|
     hyps.removeG true λ name uniq' _ _ => if uniq == uniq' then some name else none
     | throwError "ispecialize: cannot find argument"
   let state := { hyps, out, p, pf := q(($pf).1), .. }
-  let state ← liftM <| spats.foldlM (SpecializeState.process_wand gs) state
+  let state ← spats.foldlM SpecializeState.process_wand state
 
   let hyps' := Hyps.add bi name uniq state.p state.out state.hyps
   return ⟨_, hyps', state.pf⟩
 
 elab "ispecialize" colGt pmt:pmTerm : tactic => do
   let pmt ← liftMacroM <| PMTerm.parse pmt
-  let (mvar, { bi, hyps, goal, .. }) ← istart (← getMainGoal)
-  mvar.withContext do
-  let gs ← Goals.new bi
-  -- hypothesis must be in the context, otherwise use pose proof
+  ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
+  -- hypothesis must be in the context, otherwise use ihave
   let name := ⟨pmt.term⟩
-  let some uniq ← try? <| hyps.findWithInfo name | throwError s!"{name} should be a hypothesis, use ihave instead"
-  let ⟨_, hyps', pf⟩ ← iSpecializeCore gs hyps uniq pmt.spats
-  let pf' ← gs.addGoal hyps' goal
+  let some uniq ← try? <| hyps.findWithInfo name
+    | throwError "{name} should be a hypothesis, use ihave instead"
+  let ⟨_, hyps', pf⟩ ← iSpecializeCore hyps uniq pmt.spats
+  let pf' ← addBIGoal hyps' goal
   mvar.assign q(($pf).trans $pf')
-  replaceMainGoal (← gs.getGoals)
diff --git a/src/Iris/ProofMode/Tactics/Split.lean b/src/Iris/ProofMode/Tactics/Split.lean
index 4468601a..817a3874 100644
--- a/src/Iris/ProofMode/Tactics/Split.lean
+++ b/src/Iris/ProofMode/Tactics/Split.lean
@@ -4,88 +4,25 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lars König, Mario Carneiro
 -/
 import Iris.ProofMode.Tactics.Basic
-import Iris.ProofMode.Tactics.Remove
 
 namespace Iris.ProofMode
 open Lean Elab Tactic Meta Qq BI
 
-theorem from_and_intro [BI PROP] {P Q A1 A2 : PROP} [inst : FromAnd Q A1 A2]
+private theorem from_and_intro [BI PROP] {P Q A1 A2 : PROP} [inst : FromAnd Q A1 A2]
     (h1 : P ⊢ A1) (h2 : P ⊢ A2) : P ⊢ Q :=
   (and_intro h1 h2).trans inst.1
 
 elab "isplit" : tactic => do
-  let (mvar, { prop, bi, e, hyps, goal, .. }) ← istart (← getMainGoal)
-  mvar.withContext do
+  ProofModeM.runTactic λ mvar { prop, hyps, goal, .. } => do
 
   let A1 ← mkFreshExprMVarQ prop
   let A2 ← mkFreshExprMVarQ prop
-  let _ ← synthInstanceQ q(FromAnd $goal $A1 $A2)
-  let m1 : Q($e ⊢ $A1) ← mkFreshExprSyntheticOpaqueMVar <|
-    IrisGoal.toExpr { prop, bi, hyps, goal := A1, .. }
-  let m2 : Q($e ⊢ $A2) ← mkFreshExprSyntheticOpaqueMVar <|
-    IrisGoal.toExpr { prop, bi, hyps, goal := A2, .. }
+  let some _ ← ProofModeM.trySynthInstanceQ q(FromAnd $goal $A1 $A2) | throwError "isplit: {goal} is not a conjunction"
+  let m1 ← addBIGoal hyps A1
+  let m2 ← addBIGoal hyps A2
   mvar.assign q(from_and_intro (Q := $goal) $m1 $m2)
-  replaceMainGoal [m1.mvarId!, m2.mvarId!]
 
-
-theorem split_es [BI PROP] {Q Q1 Q2 : PROP} (h : Q ⊣⊢ Q1 ∗ Q2) : emp ∗ Q ⊣⊢ Q1 ∗ Q2 :=
-  emp_sep.trans h
-theorem split_ls [BI PROP] {P Q Q1 Q2 : PROP} (h : Q ⊣⊢ Q1 ∗ Q2) : P ∗ Q ⊣⊢ (P ∗ Q1) ∗ Q2 :=
-  (sep_congr_r h).trans sep_assoc.symm
-theorem split_rs [BI PROP] {P Q Q1 Q2 : PROP} (h : Q ⊣⊢ Q1 ∗ Q2) : P ∗ Q ⊣⊢ Q1 ∗ (P ∗ Q2) :=
-  (sep_congr_r h).trans sep_left_comm
-theorem split_se [BI PROP] {P P1 P2 : PROP} (h : P ⊣⊢ P1 ∗ P2) : P ∗ emp ⊣⊢ P1 ∗ P2 :=
-  sep_emp.trans h
-theorem split_sl [BI PROP] {P Q P1 P2 : PROP} (h : P ⊣⊢ P1 ∗ P2) : P ∗ Q ⊣⊢ (P1 ∗ Q) ∗ P2 :=
-  (sep_congr_l h).trans sep_right_comm
-theorem split_sr [BI PROP] {P Q P1 P2 : PROP} (h : P ⊣⊢ P1 ∗ P2) : P ∗ Q ⊣⊢ P1 ∗ (P2 ∗ Q) :=
-  (sep_congr_l h).trans sep_assoc
-theorem split_ss [BI PROP] {P Q P1 P2 Q1 Q2 : PROP}
-    (h1 : P ⊣⊢ P1 ∗ P2) (h2 : Q ⊣⊢ Q1 ∗ Q2) : P ∗ Q ⊣⊢ (P1 ∗ Q1) ∗ (P2 ∗ Q2) :=
-  (sep_congr h1 h2).trans sep_sep_sep_comm
-
-inductive SplitResult {prop : Q(Type u)} (bi : Q(BI $prop)) (e : Q($prop)) where
-  | emp (_ : $e =Q BI.emp)
-  | left
-  | right
-  | split {elhs erhs : Q($prop)} (lhs : Hyps bi elhs) (rhs : Hyps bi erhs)
-          (pf : Q($e ⊣⊢ $elhs ∗ $erhs))
-
-variable {prop : Q(Type u)} (bi : Q(BI $prop)) (toRight : Name → Name → Bool) in
-def Hyps.splitCore : ∀ {e}, Hyps bi e → SplitResult bi e
-  | _, .emp _ => .emp ⟨⟩
-  | ehyp, h@(.hyp _ name uniq b ty _) =>
-    match matchBool b with
-    | .inl _ =>
-      have : $ehyp =Q iprop(□ $ty) := ⟨⟩
-      .split h h q(intuitionistically_sep_dup)
-    | .inr _ => if toRight name uniq then .right else .left
-  | _, .sep _ _ _ _ lhs rhs =>
-    let resl := lhs.splitCore
-    let resr := rhs.splitCore
-    match resl, resr with
-    | .emp _, .emp _ | .left, .emp _ | .emp _, .left | .left, .left => .left
-    | .right, .emp _ | .emp _, .right | .right, .right => .right
-    | .left, .right => .split lhs rhs q(.rfl)
-    | .right, .left => .split rhs lhs q(sep_comm)
-    | .emp _, .split r1 r2 rpf => .split r1 r2 q(split_es $rpf)
-    | .left, .split r1 r2 rpf => .split (lhs.mkSep r1) r2 q(split_ls $rpf)
-    | .right, .split r1 r2 rpf => .split r1 (lhs.mkSep r2) q(split_rs $rpf)
-    | .split l1 l2 lpf, .emp _ => .split l1 l2 q(split_se $lpf)
-    | .split l1 l2 lpf, .left => .split (l1.mkSep rhs) l2 q(split_sl $lpf)
-    | .split l1 l2 lpf, .right => .split l1 (l2.mkSep rhs) q(split_sr $lpf)
-    | .split l1 l2 lpf, .split r1 r2 rpf => .split (l1.mkSep r1) (l2.mkSep r2) q(split_ss $lpf $rpf)
-
-def Hyps.split {prop : Q(Type u)} (bi : Q(BI $prop)) (toRight : Name → Name → Bool)
-    {e} (hyps : Hyps bi e) :
-    (elhs erhs : Q($prop)) × Hyps bi elhs × Hyps bi erhs × Q($e ⊣⊢ $elhs ∗ $erhs) :=
-  match hyps.splitCore bi toRight with
-  | .emp _ => ⟨_, _, hyps, hyps, q(sep_emp_rev)⟩
-  | .left => ⟨_, _, hyps, .mkEmp bi, q(sep_emp_rev)⟩
-  | .right => ⟨_, _, .mkEmp bi, hyps, q(emp_sep_rev)⟩
-  | .split lhs rhs pf => ⟨_, _, lhs, rhs, pf⟩
-
-theorem sep_split [BI PROP] {P P1 P2 Q Q1 Q2 : PROP} [inst : FromSep Q Q1 Q2]
+private theorem sep_split [BI PROP] {P P1 P2 Q Q1 Q2 : PROP} [inst : FromSep Q Q1 Q2]
     (h : P ⊣⊢ P1 ∗ P2) (h1 : P1 ⊢ Q1) (h2 : P2 ⊢ Q2) : P ⊢ Q :=
   h.1.trans <| (sep_mono h1 h2).trans inst.1
 
@@ -98,8 +35,7 @@ def isplitCore (side : splitSide) (names : Array (TSyntax `ident)) : TacticM Uni
     | .splitRight => true
 
   -- extract environment
-  let (mvar, { u, prop, bi, hyps, goal, .. }) ← istart (← getMainGoal)
-  mvar.withContext do
+  ProofModeM.runTactic λ mvar { prop, bi, hyps, goal, .. } => do
 
   let mut uniqs : NameSet := {}
   for name in names do
@@ -107,17 +43,15 @@ def isplitCore (side : splitSide) (names : Array (TSyntax `ident)) : TacticM Uni
 
   let Q1 ← mkFreshExprMVarQ prop
   let Q2 ← mkFreshExprMVarQ prop
-  let _ ← synthInstanceQ q(FromSep $goal $Q1 $Q2)
+  let some _ ← ProofModeM.trySynthInstanceQ q(FromSep $goal $Q1 $Q2) |
+    throwError "isplit: {goal} is not a separating conjunction"
 
   -- split conjunction
-  let ⟨el, er, lhs, rhs, pf⟩ := hyps.split bi (fun _ uniq => uniqs.contains uniq == splitRight)
+  let ⟨_, _, lhs, rhs, pf⟩ := hyps.split bi (fun _ uniq => uniqs.contains uniq == splitRight)
 
-  let m1 : Q($el ⊢ $Q1) ← mkFreshExprSyntheticOpaqueMVar <|
-    IrisGoal.toExpr { u, prop, bi, hyps := lhs, goal := Q1, .. }
-  let m2 : Q($er ⊢ $Q2) ← mkFreshExprSyntheticOpaqueMVar <|
-    IrisGoal.toExpr { u, prop, bi, hyps := rhs, goal := Q2, .. }
+  let m1 ← addBIGoal lhs Q1
+  let m2 ← addBIGoal rhs Q2
   mvar.assign q(sep_split (Q := $goal) $pf $m1 $m2)
-  replaceMainGoal [m1.mvarId!, m2.mvarId!]
 
 elab "isplitl" "[" names:(colGt ident)* "]": tactic => do
   isplitCore .splitLeft names
diff --git a/src/Iris/Tests/Tactics.lean b/src/Iris/Tests/Tactics.lean
index e63cb91d..7aaed786 100644
--- a/src/Iris/Tests/Tactics.lean
+++ b/src/Iris/Tests/Tactics.lean
@@ -54,19 +54,26 @@ end rename
 namespace clear
 
 /-- Tests clearing an intuitionistic hypothesis with `iclear` -/
-example [BI PROP] (Q : PROP) : □ P ⊢ Q -∗ Q := by
+example [BI PROP] (P Q : PROP) : □ P ⊢ Q -∗ Q := by
   iintro □HP
   iintro HQ
   iclear HP
   iexact HQ
 
 /-- Tests clearing a spatial affine hypothesis with `iclear` -/
-example [BI PROP] (Q : PROP) : <affine> P ⊢ Q -∗ Q := by
+example [BI PROP] (P Q : PROP) : <affine> P ⊢ Q -∗ Q := by
   iintro HP
   iintro HQ
   iclear HP
   iexact HQ
 
+/- Tests `iclear` failing -/
+/-- error: iclear: P is not affine and the goal not absorbing -/
+#guard_msgs in
+example [BI PROP] (P Q : PROP) : P ⊢ Q -∗ Q := by
+  iintro HP HQ
+  iclear HP
+
 end clear
 
 -- intro
@@ -92,6 +99,11 @@ example [BI PROP] (Q : PROP) : ⊢ <pers> Q → Q := by
   iintro HQ
   iexact HQ
 
+/- Tests introducing an implication in an intuitionistic context -/
+example [BI PROP] (P : PROP) : ⊢ □ P -∗ P → P := by
+  iintro □HP1 HP2
+  iexact HP2
+
 /-- Tests dropping a hypothesis in an implication with the `-` pattern -/
 example [BI PROP] (Q : PROP) : ⊢ P → Q -∗ Q := by
   iintro - HQ
@@ -104,7 +116,7 @@ example [BI PROP] (Q : PROP) : ⊢ Q -∗ P → Q := by
 
 /-- Tests introducing an universally quantified variable -/
 example [BI PROP] : ⊢@{PROP} ∀ x, ⌜x = 0⌝ → ⌜x = 0⌝ := by
-  iintro x
+  iintro %x
   iintro H
   iexact H
 
@@ -133,6 +145,43 @@ example [BI PROP] (Q : PROP) : ⊢ □ (P1 ∧ P2) -∗ Q ∨ Q -∗ Q := by
   iintro □⟨_HP1, ∗_HP2⟩ (HQ | HQ)
   <;> iexact HQ
 
+/- Tests `iintro` failing to introduce pure hypothesis -/
+/-- error: iintro: iprop(P -∗ Q) cannot be turned into a universal quantifier or pure hypothesis -/
+#guard_msgs in
+example [BI PROP] (P Q : PROP) : ⊢ P -∗ Q := by
+  iintro %H
+
+/- Tests `iintro` failing to introduce -/
+/-- error: iintro: Q not a wand -/
+#guard_msgs in
+example [BI PROP] (Q : PROP) : ⊢ Q := by
+  iintro H
+
+/- Tests `iintro` failing to introduce intuitionistically -/
+/-- error: iintro: Q not a wand -/
+#guard_msgs in
+example [BI PROP] (Q : PROP) : ⊢ Q := by
+  iintro □H
+
+/- Tests `iintro` failing to introduce non-intuitionistic wand as intuitionistic -/
+/-- error: iintro: P not persistent -/
+#guard_msgs in
+example [BI PROP] (P Q : PROP) : ⊢ P -∗ Q := by
+  iintro □H
+
+/- Tests `iintro` failing to introduce non-intuitionistic implication as intuitionistic -/
+/-- error: iintro: P not persistent -/
+#guard_msgs in
+example [BI PROP] (P Q : PROP) : ⊢ P → Q := by
+  iintro □H
+
+/- Tests `iintro` failing to introduce implication with non-empty spatial context -/
+/-- error: iintro: P is not persistent and spatial context is non-empty -/
+#guard_msgs in
+example [BI PROP] (P : PROP) : ⊢ P -∗ P → P := by
+  iintro HP1 HP2
+
+
 end intro
 
 -- exists
@@ -176,6 +225,11 @@ example [BI PROP] : ⊢@{PROP} ∃ x y : Nat, ⌜x = y⌝ := by
   ipure_intro
   rfl
 
+/- Tests `iexists` failing with non-quantifier -/
+/-- error: iexists: cannot turn iprop(True) into an existential quantifier -/
+#guard_msgs in
+example [BI PROP] : ⊢@{PROP} True := by
+  iexists _
 
 end «exists»
 
@@ -197,6 +251,20 @@ example [BI PROP] (Q : PROP) : □ Q ⊢ Q := by
   iintro HQ
   iexact HQ
 
+/- Tests `iexact` failing with not-affine assumption -/
+/-- error: iexact: context is not affine or goal is not absorbing -/
+#guard_msgs in
+example [BI PROP] (Q : PROP) : ⊢ Q -∗ True -∗ Q := by
+  iintro HQ _
+  iexact HQ
+
+/- Tests `iexact` failing with non-matching goal -/
+/-- error: iexact: cannot unify Q 1 and Q 2 -/
+#guard_msgs in
+example [BI PROP] (Q : Nat → PROP) : ⊢ Q 1 -∗ Q 2 := by
+  iintro HQ
+  iexact HQ
+
 end exact
 
 -- assumption
@@ -217,14 +285,11 @@ example [BI PROP] (Q : PROP) : □ Q ⊢ Q := by
   iintro □_HQ
   iassumption
 
-/-- Tests `iassumption` using a Lean hypothesis -/
-example [BI PROP] (Q : PROP) (H : ⊢ Q) : <affine> P ⊢ Q := by
-  iintro _HP
-  iassumption
-
-/-- Tests `iassumption` with Lean hypothesis first introduced -/
-example [BI PROP] (Q : PROP) : <affine> ⌜⊢ Q⌝ ⊢ Q := by
-  iintro ⌜H⌝
+/- Tests `iassumption` failure -/
+/-- error: iassumption: no matching assumption -/
+#guard_msgs in
+example [BI PROP] (P Q : PROP) : □ P ⊢ Q := by
+  iintro □_HQ
   iassumption
 
 end assumption
@@ -558,20 +623,34 @@ example [BI PROP] (Q : PROP) : (⌜φ1⌝ ∧ <affine> ⌜φ2⌝) ⊢ Q -∗ Q :
   ipure Hφ
   iexact HQ
 
+/- Tests `ipure` failure -/
+/-- error: ipure: P is not pure -/
+#guard_msgs in
+example [BI PROP] (P Q : PROP) : P ⊢ Q := by
+  iintro HP
+  ipure HP
+
+/- Tests `ipure` failure for non-affine -/
+/-- error: ipure: iprop(⌜φ⌝) is not affine and the goal not absorbing -/
+#guard_msgs in
+example [BI PROP] φ (Q : PROP) : ⌜φ⌝ ⊢ Q := by
+  iintro HP
+  ipure HP
+
 end pure
 
 -- intuitionistic
 namespace intuitionistic
 
 /-- Tests `iintuitionistic` to move hypothesis to intuitionistic context -/
-example [BI PROP] (P : PROP) : □ P ⊢ Q -∗ Q := by
+example [BI PROP] (P Q : PROP) : □ P ⊢ Q -∗ Q := by
   iintro HP
   iintro HQ
   iintuitionistic HP
   iexact HQ
 
 /-- Tests `iintuitionistic` with multiple hypotheses -/
-example [BI PROP] (P : PROP) : □ P ⊢ □ Q -∗ Q := by
+example [BI PROP] (P Q : PROP) : □ P ⊢ □ Q -∗ Q := by
   iintro HP
   iintro HQ
   iintuitionistic HP
@@ -579,13 +658,27 @@ example [BI PROP] (P : PROP) : □ P ⊢ □ Q -∗ Q := by
   iexact HQ
 
 /-- Tests `iintuitionistic` applied twice to same hypothesis -/
-example [BI PROP] (P : PROP) : □ P ⊢ Q -∗ Q := by
+example [BI PROP] (P Q : PROP) : □ P ⊢ Q -∗ Q := by
   iintro HP
   iintro HQ
   iintuitionistic HP
   iintuitionistic HP
   iexact HQ
 
+/- Tests `iintuitionistic` failure for non-persistent assumption -/
+/-- error: icases: P not persistent -/
+#guard_msgs in
+example [BI PROP] (P Q : PROP) : P ⊢ Q := by
+  iintro HP
+  iintuitionistic HP
+
+/- Tests `iintuitionistic` failure for non-affine assumption -/
+/-- error: icases: iprop(<pers> P) not affine and the goal not absorbing -/
+#guard_msgs in
+example [BI PROP] (P Q : PROP) : <pers> P ⊢ Q := by
+  iintro HP
+  iintuitionistic HP
+
 end intuitionistic
 
 -- spatial
@@ -649,6 +742,12 @@ example [BI PROP] (H : A → B) (P Q : PROP) : <affine> P ⊢ <pers> Q → ⌜A
   ipure_intro
   exact H
 
+/- Tests `ipure_intro` failure -/
+/-- error: ipure_intro: P is not pure -/
+#guard_msgs in
+example [BI PROP] (P : PROP) : ⊢ P := by
+  ipure_intro
+
 end pureintro
 
 -- specialize
@@ -866,13 +965,13 @@ end split
 namespace leftright
 
 /-- Tests `ileft` -/
-example [BI PROP] (P : PROP) : P ⊢ P ∨ Q := by
+example [BI PROP] (P Q : PROP) : P ⊢ P ∨ Q := by
   iintro HP
   ileft
   iexact HP
 
 /-- Tests `iright` -/
-example [BI PROP] (Q : PROP) : Q ⊢ P ∨ Q := by
+example [BI PROP] (P Q : PROP) : Q ⊢ P ∨ Q := by
   iintro HQ
   iright
   iexact HQ
@@ -886,6 +985,20 @@ example [BI PROP] (P Q : PROP) : ⊢ P -∗ Q -∗ P ∗ (R ∨ Q ∨ R) := by
   ileft
   iexact HQ
 
+/- Tests `ileft` failure -/
+/-- error: ileft: Q is not a disjunction -/
+#guard_msgs in
+example [BI PROP] (P Q : PROP) : P ⊢ Q := by
+  iintro HP
+  ileft
+
+/- Tests `iright` failure -/
+/-- error: iright: Q is not a disjunction -/
+#guard_msgs in
+example [BI PROP] (P Q : PROP) : P ⊢ Q := by
+  iintro HP
+  iright
+
 end leftright
 
 -- cases
@@ -941,6 +1054,14 @@ example [BI PROP] (Q : PROP) : Q ⊢ <affine> (P1 ∨ P2 ∨ P3) -∗ Q := by
   icases HP with (_HP1 | _HP2 | _HP3)
   <;> iexact HQ
 
+/- Tests `icases` failure too many nested disjunction -/
+/-- error: icases: P2 is not a disjunction -/
+#guard_msgs in
+example [BI PROP] (Q : PROP) : Q ⊢ (P1 ∨ P2) -∗ Q := by
+  iintro HQ
+  iintro HP
+  icases HP with (_HP1 | _HP2 | _HP3)
+
 /-- Tests `icases` with complex mixed conjunction and disjunction -/
 example [BI PROP] [BIAffine PROP] (Q : PROP) :
     (P11 ∨ P12 ∨ P13) ∗ P2 ∗ (P31 ∨ P32 ∨ P33) ∗ Q ⊢ Q := by
@@ -1087,16 +1208,49 @@ example [BI PROP] (Q : PROP) : □ (P1 ∧ P2 ∧ Q ∧ P3) ⊢ Q := by
 
 /-- Tests `icases` with existential -/
 example [BI PROP] (Q : Nat → PROP) : (∃ x, Q x) ⊢ ∃ x, Q x ∨ False := by
-  iintro ⟨x, H⟩
+  iintro ⟨%x, H⟩
   iexists x
   ileft
   iexact H
 
 /-- Tests `icases` with intuitionistic existential -/
 example [BI PROP] (Q : Nat → PROP) : □ (∃ x, Q x) ⊢ ∃ x, □ Q x ∨ False := by
-  iintro ⟨x, □H⟩
+  iintro ⟨%x, □H⟩
   iexists x
   ileft
   iexact H
 
+/-- Tests `icases` with proof mode term -/
+example [BI PROP] P (Q : Nat → PROP) :
+  (P -∗ ∃ x, □ Q x ∗ Q 1) ⊢ P -∗ Q 1 := by
+  iintro Hwand HP
+  icases Hwand $$ HP with ⟨%_, -, HQ⟩
+  iexact HQ
+
+/-- Tests `icases` with False -/
+example [BI PROP] (Q : PROP) : False ⊢ Q := by
+  iintro H
+  icases H with ⟨⟩
+
+/- Tests `icases` failing with empty conjunction -/
+/-- error: icases: cannot destruct Q as an empty conjunct -/
+#guard_msgs in
+example [BI PROP] (Q : PROP) : Q ⊢ Q := by
+  iintro H
+  icases H with ⟨⟩
+
+/- Tests `icases` failing to destruct -/
+/-- error: icases: cannot destruct Q -/
+#guard_msgs in
+example [BI PROP] (Q : PROP) : Q ⊢ Q := by
+  iintro H
+  icases H with ⟨HA, HB⟩
+
+/- Tests `icases` failing to destruct intuitionistic -/
+/-- error: icases: cannot destruct iprop(□ Q) -/
+#guard_msgs in
+example [BI PROP] (Q : PROP) : □ Q ⊢ Q := by
+  iintro H
+  icases H with ⟨HA, HB⟩
+
 end cases