diff --git a/src/Iris/ProofMode/Classes.lean b/src/Iris/ProofMode/Classes.lean
index 4150397b..3ed3cd6a 100644
--- a/src/Iris/ProofMode/Classes.lean
+++ b/src/Iris/ProofMode/Classes.lean
@@ -4,34 +4,32 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lars König
 -/
 import Iris.BI
+import Iris.ProofMode.SynthInstance
 
 namespace Iris.ProofMode
 open Iris.BI
 
-/-
-The two type classes `AsEmpValid1` and `AsEmpValid2` are necessary since type class instance
-search is used in both directions in `as_emp_valid_1` and `as_emp_valid_2`. When type class
-instance search is supposed to generate `φ` based on `P`, `AsEmpValid1` is used, since `φ` is
-declared as an `outParam`. Consequently, if type class instance search is supposed to generate `P`,
-`AsEmpValid2` is used.
--/
-
-class AsEmpValid1 (φ : semiOutParam Prop) {PROP : Type _} (P : PROP) [BI PROP] where
-  as_emp_valid : φ ↔ ⊢ P
+/-- [InOut] is used to dynamically determine whether a type class
+parameter is an input or an output. This is important for classes that
+are used with multiple modings, e.g., IntoWand. Instances can match on
+the InOut parameter to avoid accidentially instantiating outputs if
+matching on an input was intended. -/
+inductive InOut where
+  | in
+  | out
 
-class AsEmpValid2 (φ : Prop) {PROP : outParam (Type _)} (P : outParam PROP) [BI PROP] where
-  as_emp_valid : φ ↔ ⊢ P
+inductive AsEmpValid.Direction where
+  | into
+  | from
 
-def AsEmpValid1.to2 {φ : Prop} {PROP : Type _} {P : PROP} [BI PROP]
-    [AsEmpValid1 φ P] : AsEmpValid2 φ P := ⟨AsEmpValid1.as_emp_valid⟩
+@[ipm_class]
+class AsEmpValid (d : AsEmpValid.Direction) (φ : Prop) {PROP : outParam (Type _)} (P : outParam PROP) [BI PROP] where
+  as_emp_valid : (d = .into → φ → ⊢ P) ∧ (d = .from → (⊢ P) → φ)
 
-def AsEmpValid2.to1 {φ : Prop} {PROP : Type _} {P : PROP} [BI PROP]
-    [AsEmpValid2 φ P] : AsEmpValid1 φ P := ⟨AsEmpValid2.as_emp_valid⟩
-
-theorem as_emp_valid_1 [BI PROP] (P : PROP) [AsEmpValid1 φ P] : φ → ⊢ P :=
-  AsEmpValid1.as_emp_valid.mp
-theorem as_emp_valid_2 [BI PROP] (φ : Prop) [AsEmpValid2 φ (P : PROP)] : (⊢ P) → φ :=
-  AsEmpValid2.as_emp_valid.mpr
+theorem asEmpValid_1 [BI PROP] (P : PROP) [AsEmpValid .into φ P] : φ → ⊢ P :=
+  AsEmpValid.as_emp_valid.1 rfl
+theorem asEmpValid_2 [BI PROP] (φ : Prop) [AsEmpValid .from φ (P : PROP)] : (⊢ P) → φ :=
+  AsEmpValid.as_emp_valid.2 rfl
 
 
 /- Depending on the use case, type classes with the prefix `From` or `Into` are used. Type classes
@@ -40,84 +38,101 @@ proposition can be derived. Type classes with the prefix `Into` are used to gene
 *into* which the original proposition can be turned by derivation. Additional boolean flags are
 used to indicate that certain propositions should be intuitionistic. -/
 
-class IntoEmpValid (φ : Prop) {PROP : outParam (Type _)} (P : outParam PROP) [BI PROP] where
-  into_emp_valid : φ → ⊢ P
-export IntoEmpValid (into_emp_valid)
-
+@[ipm_class]
 class FromImp [BI PROP] (P : PROP) (Q1 Q2 : outParam PROP) where
   from_imp : (Q1 → Q2) ⊢ P
 export FromImp (from_imp)
 
+@[ipm_class]
 class FromWand [BI PROP] (P : PROP) (Q1 Q2 : outParam PROP) where
   from_wand : (Q1 -∗ Q2) ⊢ P
 export FromWand (from_wand)
 
-class IntoWand [BI PROP] (p q : Bool) (R : PROP) (P Q : outParam PROP) where
+@[ipm_class]
+class IntoWand [BI PROP] (p q : Bool) (R : PROP)
+  (ioP : InOut) (P : semiOutParam PROP)
+  (ioQ : InOut) (Q : semiOutParam PROP) where
   into_wand : □?p R ⊢ □?q P -∗ Q
 export IntoWand (into_wand)
 
+@[ipm_class]
 class FromForall [BI PROP] (P : PROP) {α : outParam (Sort _)} (Ψ : outParam <| α → PROP) where
   from_forall : (∀ x, Ψ x) ⊢ P
 export FromForall (from_forall)
 
+@[ipm_class]
 class IntoForall [BI PROP] (P : PROP) {α : outParam (Sort _)} (Φ : outParam <| α → PROP) where
   into_forall : P ⊢ ∀ x, Φ x
 export IntoForall (into_forall)
 
+@[ipm_class]
 class FromExists [BI PROP] (P : PROP) {α : outParam (Sort _)} (Φ : outParam <| α → PROP) where
   from_exists : (∃ x, Φ x) ⊢ P
 export FromExists (from_exists)
 
+@[ipm_class]
 class IntoExists [BI PROP] (P : PROP) {α : outParam (Sort _)} (Φ : outParam <| α → PROP) where
   into_exists : P ⊢ ∃ x, Φ x
 export IntoExists (into_exists)
 
+@[ipm_class]
 class FromAnd [BI PROP] (P : PROP) (Q1 Q2 : outParam PROP) where
   from_and : Q1 ∧ Q2 ⊢ P
 export FromAnd (from_and)
 
+@[ipm_class]
 class IntoAnd (p : Bool) [BI PROP] (P : PROP) (Q1 Q2 : outParam PROP) where
   into_and : □?p P ⊢ □?p (Q1 ∧ Q2)
 export IntoAnd (into_and)
 
+@[ipm_class]
 class FromSep [BI PROP] (P : PROP) (Q1 Q2 : outParam PROP) where
   from_sep : Q1 ∗ Q2 ⊢ P
 export FromSep (from_sep)
 
+@[ipm_class]
 class IntoSep [BI PROP] (P : PROP) (Q1 Q2 : outParam PROP) where
   into_sep : P ⊢ Q1 ∗ Q2
 export IntoSep (into_sep)
 
+@[ipm_class]
 class FromOr [BI PROP] (P : PROP) (Q1 Q2 : outParam PROP) where
   from_or : Q1 ∨ Q2 ⊢ P
 export FromOr (from_or)
 
+@[ipm_class]
 class IntoOr [BI PROP] (P : PROP) (Q1 Q2 : outParam PROP) where
   into_or : P ⊢ Q1 ∨ Q2
 export IntoOr (into_or)
 
 
+@[ipm_class]
 class IntoPersistently (p : Bool) [BI PROP] (P : PROP) (Q : outParam PROP) where
   into_persistently : <pers>?p P ⊢ <pers> Q
 export IntoPersistently (into_persistently)
 
+@[ipm_class]
 class FromAffinely [BI PROP] (P : outParam PROP) (Q : PROP) (p : Bool := true) where
   from_affinely : <affine>?p Q ⊢ P
 export FromAffinely (from_affinely)
 
+@[ipm_class]
 class IntoAbsorbingly [BI PROP] (P : outParam PROP) (Q : PROP) where
   into_absorbingly : P ⊢ <absorb> Q
 export IntoAbsorbingly (into_absorbingly)
 
 
-class FromAssumption (p : Bool) [BI PROP] (P : semiOutParam PROP) (Q : PROP) where
+@[ipm_class]
+class FromAssumption (p : Bool) [BI PROP] (ioP : InOut) (P : semiOutParam PROP) (Q : PROP) where
   from_assumption : □?p P ⊢ Q
 export FromAssumption (from_assumption)
 
+@[ipm_class]
 class IntoPure [BI PROP] (P : PROP) (φ : outParam Prop) where
   into_pure : P ⊢ ⌜φ⌝
 export IntoPure (into_pure)
 
+@[ipm_class]
 class FromPure [BI PROP] (a : outParam Bool) (P : PROP) (φ : outParam Prop) where
   from_pure : <affine>?a ⌜φ⌝ ⊢ P
 export FromPure (from_pure)
diff --git a/src/Iris/ProofMode/Goals.lean b/src/Iris/ProofMode/Goals.lean
new file mode 100644
index 00000000..80a9ba77
--- /dev/null
+++ b/src/Iris/ProofMode/Goals.lean
@@ -0,0 +1,43 @@
+/-
+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) : MetaM (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)
+  return (nonDep ++ dep).toList
diff --git a/src/Iris/ProofMode/Instances.lean b/src/Iris/ProofMode/Instances.lean
index 5141513c..f7ea079e 100644
--- a/src/Iris/ProofMode/Instances.lean
+++ b/src/Iris/ProofMode/Instances.lean
@@ -11,82 +11,65 @@ namespace Iris.ProofMode
 open Iris.BI Iris.Std
 
 -- AsEmpValid
-instance (priority := default - 10) asEmpValidEmpValid1
-    [BI PROP] (P : PROP) : AsEmpValid1 (⊢ P) P := ⟨by simp⟩
-instance (priority := default + 10) asEmpValidEmpValid2
-    [BI PROP] (P : PROP) : AsEmpValid2 (⊢ P) P := AsEmpValid1.to2
+instance (priority := default + 10) asEmpValidEmpValid
+    [BI PROP] d (P : PROP) : AsEmpValid d (⊢ P) P := ⟨by simp⟩
 
-instance asEmpValid1_entails [BI PROP] (P Q : PROP) : AsEmpValid1 (P ⊢ Q) iprop(P -∗ Q) where
-  as_emp_valid := ⟨entails_wand, wand_entails⟩
-instance asEmpValid2_entails [BI PROP] (P Q : PROP) : AsEmpValid2 (P ⊢ Q) iprop(P -∗ Q) :=
-  AsEmpValid1.to2
+instance asEmpValid_entails [BI PROP] d (P Q : PROP) : AsEmpValid d (P ⊢ Q) iprop(P -∗ Q) where
+  as_emp_valid := ⟨λ _ => entails_wand, λ _ => wand_entails⟩
 
-instance asEmpValid1_equiv [BI PROP] (P Q : PROP) : AsEmpValid1 (P ⊣⊢ Q) iprop(P ∗-∗ Q) where
-  as_emp_valid := ⟨equiv_wandIff, wandIff_equiv⟩
-instance asEmpValid2_equiv [BI PROP] (P Q : PROP) : AsEmpValid2 (P ⊣⊢ Q) iprop(P ∗-∗ Q) :=
-  AsEmpValid1.to2
-
--- IntoEmpValid
-instance intoEmpValid_emp_entails [BI PROP] (P : PROP) : IntoEmpValid (⊢ P) iprop(P) where
-  into_emp_valid := id
-
-instance intoEmpValid_entails [BI PROP] (P Q : PROP) : IntoEmpValid (P ⊢ Q) iprop(P -∗ Q) where
-  into_emp_valid := entails_wand
-
-instance intoEmpValid_equiv [BI PROP] (P Q : PROP) : IntoEmpValid (P ⊣⊢ Q) iprop(P ∗-∗ Q) where
-  into_emp_valid := equiv_wandIff
+instance asEmpValid_equiv [BI PROP] (P Q : PROP) : AsEmpValid d (P ⊣⊢ Q) iprop(P ∗-∗ Q) where
+  as_emp_valid := ⟨λ _ => equiv_wandIff, λ _ => wandIff_equiv⟩
 
 -- FromImp
 instance fromImp_imp [BI PROP] (P1 P2 : PROP) : FromImp iprop(P1 → P2) P1 P2 := ⟨.rfl⟩
 -- FromWand
 instance fromWand_wand [BI PROP] (P1 P2 : PROP) : FromWand iprop(P1 -∗ P2) P1 P2 := ⟨.rfl⟩
 -- IntoWand
-instance intoWand_wand (p q : Bool) [BI PROP] (P Q P' : PROP) [h : FromAssumption q P P'] :
-    IntoWand p q iprop(P' -∗ Q) P Q where
+instance intoWand_wand (p q : Bool) [BI PROP] ioP ioQ (P Q P' : PROP) [h : FromAssumption q ioP P P'] :
+    IntoWand p q iprop(P' -∗ Q) ioP P ioQ Q where
   into_wand := (intuitionisticallyIf_mono <| wand_mono_l h.1).trans intuitionisticallyIf_elim
 
-instance intoWand_imp_false [BI PROP] (P Q P' : PROP) [Absorbing P'] [Absorbing iprop(P' → Q)]
-    [h : FromAssumption b P P'] : IntoWand false b iprop(P' → Q) P Q where
+instance intoWand_imp_false [BI PROP] ioP ioQ (P Q P' : PROP) [Absorbing P'] [Absorbing iprop(P' → Q)]
+    [h : FromAssumption b ioP P P'] : IntoWand false b iprop(P' → Q) ioP P ioQ Q where
   into_wand := wand_intro <| (sep_mono_r h.1).trans <| by dsimp; exact sep_and.trans imp_elim_l
 
-instance intoWand_imp_true [BI PROP] (P Q P' : PROP) [Affine P']
-    [h : FromAssumption b P P'] : IntoWand true b iprop(P' → Q) P Q where
+instance intoWand_imp_true [BI PROP] ioP ioQ (P Q P' : PROP) [Affine P']
+    [h : FromAssumption b ioP P P'] : IntoWand true b iprop(P' → Q) ioP P ioQ Q where
   into_wand := wand_intro <| (sep_mono_r h.1).trans <| by
     dsimp; exact sep_and.trans <| imp_elim intuitionistically_elim
 
-instance intoWand_and_l (p q : Bool) [BI PROP] (R1 R2 P' Q' : PROP)
-    [h : IntoWand p q R1 P' Q'] : IntoWand p q iprop(R1 ∧ R2) P' Q' where
+@[ipm_backtrack]
+instance intoWand_and_l (p q : Bool) [BI PROP] ioP ioQ (R1 R2 P' Q' : PROP)
+    [h : IntoWand p q R1 ioP P' ioQ Q'] : IntoWand p q iprop(R1 ∧ R2) ioP P' ioQ Q' where
   into_wand := (intuitionisticallyIf_mono and_elim_l).trans h.1
 
-instance intoWand_and_r (p q : Bool) [BI PROP] (R1 R2 P' Q' : PROP)
-    [h : IntoWand p q R2 Q' P'] : IntoWand p q iprop(R1 ∧ R2) Q' P' where
+@[ipm_backtrack]
+instance intoWand_and_r (p q : Bool) [BI PROP] ioP ioQ (R1 R2 P' Q' : PROP)
+    [h : IntoWand p q R2 ioP P' ioQ Q'] : IntoWand p q iprop(R1 ∧ R2) ioP P' ioQ Q' where
   into_wand := (intuitionisticallyIf_mono and_elim_r).trans h.1
 
+-- The set_option is ok since this is an instance for an IPM class and thus can create mvars.
 set_option synthInstance.checkSynthOrder false in
-instance intoWand_forall (p q : Bool) [BI PROP] (Φ : α → PROP) (P Q : PROP) (x : α)
-    [h : IntoWand p q (Φ x) P Q] : IntoWand p q iprop(∀ x, Φ x) P Q where
+instance intoWand_forall (p q : Bool) [BI PROP] (Φ : α → PROP) ioP ioQ (P Q : PROP) (x : α)
+    [h : IntoWand p q (Φ x) ioP P ioQ Q] : IntoWand p q iprop(∀ x, Φ x) ioP P ioQ Q where
   into_wand := (intuitionisticallyIf_mono <| BI.forall_elim x).trans h.1
 
-instance intoWand_affinely (p q : Bool) [BI  PROP] (R P Q : PROP) [h : IntoWand p q R P Q] :
-    IntoWand p q iprop(<affine> R) iprop(<affine> P) iprop(<affine> Q) where
+instance intoWand_affinely (p q : Bool) [BI PROP] ioP ioQ (R P Q : PROP) [h : IntoWand p q R ioP P ioQ Q] :
+    IntoWand p q iprop(<affine> R) ioP iprop(<affine> P) ioQ iprop(<affine> Q) where
   into_wand := wand_intro <|
     (sep_congr intuitionisticallyIf_affinely intuitionisticallyIf_affinely).1.trans <|
     affinely_sep_2.trans <| affinely_mono <| wand_elim h.1
 
-instance intoWand_intuitionistically (p q : Bool) [BI PROP] (R P Q : PROP)
-    [h : IntoWand true q R P Q] : IntoWand p q iprop(□ R) P Q where
+instance intoWand_intuitionistically (p q : Bool) [BI PROP] ioP ioQ (R P Q : PROP)
+    [h : IntoWand true q R ioP P ioQ Q] : IntoWand p q iprop(□ R) ioP P ioQ Q where
   into_wand := (intuitionisticallyIf_mono h.1).trans intuitionisticallyIf_elim
 
-instance intoWand_intuitionistically_wand (p : Bool) [BI PROP] (P Q : PROP) :
-    IntoWand p true iprop(□ P -∗ Q) P Q where
-  into_wand := intuitionisticallyIf_elim
-
-instance intoWand_persistently_true (q : Bool) [BI PROP] (R P Q : PROP)
-    [h : IntoWand true q R P Q] : IntoWand true q iprop(<pers> R) P Q where
+instance intoWand_persistently_true (q : Bool) [BI PROP] ioP ioQ (R P Q : PROP)
+    [h : IntoWand true q R ioP P ioQ Q] : IntoWand true q iprop(<pers> R) ioP P ioQ Q where
   into_wand := intuitionistically_persistently.1.trans h.1
 
-instance intoWand_persistently_false (q : Bool) [BI PROP] (R P Q : PROP) [Absorbing R]
-    [h : IntoWand false q R P Q] : IntoWand false q iprop(<pers> R) P Q where
+instance intoWand_persistently_false (q : Bool) [BI PROP] ioP ioQ (R P Q : PROP) [Absorbing R]
+    [h : IntoWand false q R ioP P ioQ Q] : IntoWand false q iprop(<pers> R) ioP P ioQ Q where
   into_wand := persistently_elim.trans h.1
 
 -- FromForall
@@ -397,56 +380,74 @@ instance (priority := default - 10) intoAbsorbingly_default [BI PROP] (P : PROP)
     IntoAbsorbingly iprop(<absorb> P) P := ⟨.rfl⟩
 
 -- FromAssumption
-instance (priority := default + 100) fromAssumption_exact (p : Bool) [BI PROP] (P : PROP) :
-    FromAssumption p P P where
+instance (priority := default + 100) fromAssumption_exact (p : Bool) [BI PROP] ioP (P : PROP) :
+    FromAssumption p ioP P P where
   from_assumption := intuitionisticallyIf_elim
 
-instance (priority := default + 30) fromAssumption_persistently_r [BI PROP] (P Q : PROP)
-    [h : FromAssumption true P Q] : FromAssumption true P iprop(<pers> Q) where
+instance (priority := default + 30) fromAssumption_persistently_r [BI PROP] ioP (P Q : PROP)
+    [h : FromAssumption true ioP P Q] : FromAssumption true ioP P iprop(<pers> Q) where
   from_assumption := (persistent (P := iprop(□ P))).trans (persistently_mono h.1)
 
-instance (priority := default + 30) fromAssumption_affinely_r [BI PROP] (P Q : PROP)
-    [h : FromAssumption true P Q] : FromAssumption true P iprop(<affine> Q) where
+instance (priority := default + 30) fromAssumption_affinely_r [BI PROP] ioP (P Q : PROP)
+    [h : FromAssumption true ioP P Q] : FromAssumption true ioP P iprop(<affine> Q) where
   from_assumption := affinely_idem.2.trans <| affinely_mono h.1
 
-instance (priority := default + 30) fromAssumption_intuitionistically_r [BI PROP] (P Q : PROP)
-    [h : FromAssumption true P Q] : FromAssumption true P iprop(□ Q) where
+instance (priority := default + 30) fromAssumption_intuitionistically_r [BI PROP] ioP (P Q : PROP)
+    [h : FromAssumption true ioP P Q] : FromAssumption true ioP P iprop(□ Q) where
   from_assumption := intuitionistically_idem.2.trans <| intuitionistically_mono h.1
 
-instance (priority := default + 20) fromAssumption_absorbingly_r (p : Bool) [BI PROP] (P Q : PROP)
-    [h : FromAssumption p P Q] : FromAssumption p P iprop(<absorb> Q) where
+instance (priority := default + 20) fromAssumption_absorbingly_r (p : Bool) [BI PROP] ioP (P Q : PROP)
+    [h : FromAssumption p ioP P Q] : FromAssumption p ioP P iprop(<absorb> Q) where
   from_assumption := absorbingly_intro.trans <| absorbingly_mono h.1
 
 instance (priority := default + 20) fromAssumption_intuitionistically_l (p : Bool) [BI PROP]
-    (P Q : PROP) [h : FromAssumption true P Q] : FromAssumption p iprop(□ P) Q where
+    (P Q : PROP) [h : FromAssumption true .in P Q] : FromAssumption p .in iprop(□ P) Q where
   from_assumption := intuitionisticallyIf_intutitionistically.1.trans h.1
 
 instance (priority := default + 20) fromAssumption_intuitionistically_l_true (p : Bool) [BI PROP]
-    (P Q : PROP) [h : FromAssumption p P Q] : FromAssumption p iprop(□ P) Q where
+    (P Q : PROP) [h : FromAssumption p .in P Q] : FromAssumption p .in iprop(□ P) Q where
   from_assumption := (intuitionisticallyIf_comm' (q := true)).1.trans <|
     intuitionistically_elim.trans h.1
 
 instance (priority := default + 30) fromAssumption_persistently_l_true [BI PROP] (P Q : PROP)
-    [h : FromAssumption true P Q] : FromAssumption true iprop(<pers> P) Q where
+    [h : FromAssumption true .in P Q] : FromAssumption true .in iprop(<pers> P) Q where
   from_assumption := intuitionistically_persistently.1.trans h.1
 
 instance (priority := default + 30) fromAssumption_persistently_l_false [BI PROP] [BIAffine PROP]
-    (P Q : PROP) [h : FromAssumption true P Q] : FromAssumption false iprop(<pers> P) Q where
+    (P Q : PROP) [h : FromAssumption true .in P Q] : FromAssumption false .in iprop(<pers> P) Q where
   from_assumption := intuitionistically_iff_persistently.2.trans h.1
 
 instance (priority := default + 20) fromAssumption_affinely_l (p : Bool) [BI PROP] (P Q : PROP)
-    [h : FromAssumption p P Q] : FromAssumption p iprop(<affine> P) Q where
+    [h : FromAssumption p .in P Q] : FromAssumption p .in iprop(<affine> P) Q where
   from_assumption := (intuitionisticallyIf_mono affinely_elim).trans h.1
 
 set_option synthInstance.checkSynthOrder false in
 instance (priority := default + 10) fromAssumption_forall (p : Bool) [BI PROP] (Φ : α → PROP)
-    (x : α) (Q : PROP) [h : FromAssumption p (Φ x) Q] : FromAssumption p iprop(∀ x, Φ x) Q where
+    (x : α) (Q : PROP) [h : FromAssumption p .in (Φ x) Q] : FromAssumption p .in iprop(∀ x, Φ x) Q where
   from_assumption := (intuitionisticallyIf_mono <| forall_elim x).trans h.1
 
-instance fromAssumption_later [BI PROP] (p : Bool) (P Q : PROP)
-    [h : FromAssumption p P Q] : FromAssumption p P iprop(▷ Q) where
+instance fromAssumption_later [BI PROP] (p : Bool) ioP (P Q : PROP)
+    [h : FromAssumption p ioP P Q] : FromAssumption p ioP P iprop(▷ Q) where
   from_assumption := h.1.trans later_intro
 
+set_option synthInstance.checkSynthOrder false in
+@[ipm_backtrack]
+instance fromAssumption_and_l [BI PROP] (p : Bool) (P1 P2 Q : PROP)
+    [h : FromAssumption p .in P1 Q] : FromAssumption p .in iprop(P1 ∧ P2) Q where
+  from_assumption :=
+    match p, h with
+    | true, h => intuitionistically_and.mp.trans (and_elim_l.trans h.1)
+    | false, h => and_elim_l.trans h.1
+
+set_option synthInstance.checkSynthOrder false in
+@[ipm_backtrack]
+instance fromAssumption_and_r [BI PROP] (p : Bool) (P1 P2 Q : PROP)
+    [h : FromAssumption p .in P2 Q] : FromAssumption p .in iprop(P1 ∧ P2) Q where
+  from_assumption :=
+    match p, h with
+    | true, h => intuitionistically_and.mp.trans (and_elim_r.trans h.1)
+    | false, h => and_elim_r.trans h.1
+
 -- IntoPure
 instance intoPure_pure (φ : Prop) [BI PROP] : IntoPure (PROP := PROP) iprop(⌜φ⌝) φ := ⟨.rfl⟩
 
diff --git a/src/Iris/ProofMode/SynthInstance.lean b/src/Iris/ProofMode/SynthInstance.lean
new file mode 100644
index 00000000..b9ccac26
--- /dev/null
+++ b/src/Iris/ProofMode/SynthInstance.lean
@@ -0,0 +1,168 @@
+/-
+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
+
+/-
+This file implements a custom typeclass synthesis algorithm that is used for the proof mode typeclasses.
+This is necessary since proof mode typeclasses need to be able to instantiate and create new mvars, but the
+standard typeclass synthesis does not support this.
+
+See also https://leanprover.zulipchat.com/#narrow/channel/490604-iris-lean/topic/Issues.20with.20typeclasses.20in.20the.20proof.20mode/with/563410548 for discussion.
+
+In addition to the synthInstance family of functions, we provide the following attributes and annotations:
+
+The `ipm_class` attribute marks that a class should use the IPM synthesis defined in this file. For all other classes,
+the IPM synthesis falls back to standard synthesis, enabling one to use standard type classes as parameters for IPM type classes.
+Note that IPM synthesis is *not* triggered automatically for holes where the class is marked with `ipm_class`. Instead,
+the IPM synthesis needs to be explicitly invoked via the functions in this file.
+
+The `ipm_backtrack` attribute on an instance tells the IPM synthesis to backtrack if instance instance can be applied, but
+its preconditions fail to synthesize. This is not enabled by default to avoid accidental exponential blow-ups.
+
+The `InOut` type in Classes.lean is used to dynamically determine, which parameters are inputs and which are outputs. IPM synthesis
+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
+open Lean Elab Tactic Meta Qq BI Std
+
+def MessageData.withMCtx (mctx : MetavarContext) (d : MessageData) : MessageData :=
+  .lazy λ ctx => return MessageData.withContext {env := ctx.env, mctx := mctx, lctx := ctx.lctx, opts := ctx.opts} d
+
+initialize ipmClassesExt :
+    SimpleScopedEnvExtension Name (Std.HashSet Name)  ←
+  registerSimpleScopedEnvExtension {
+    addEntry := fun s n => s.insert n
+    initial := ∅
+  }
+
+syntax (name := ipm_class) "ipm_class" : attr
+
+/-- This attribute should be used for classes that use the special IPM synthInstance below. -/
+initialize registerBuiltinAttribute {
+  name := `ipm_class
+  descr := "proof mode class"
+  add := fun decl _stx _kind =>
+    ipmClassesExt.add decl
+}
+
+initialize ipmBacktrackExt :
+    SimpleScopedEnvExtension Name (Std.HashSet Name)  ←
+  registerSimpleScopedEnvExtension {
+    addEntry := fun s n => s.insert n
+    initial := ∅
+  }
+
+syntax (name := ipm_backtrack) "ipm_backtrack" : attr
+
+/-- This attribute marks instances on which the proof mode synthesis should backtrack. -/
+initialize registerBuiltinAttribute {
+  name := `ipm_backtrack
+  descr := "Enable backtracking for this instance"
+  add := fun decl _stx _kind =>
+    ipmBacktrackExt.add decl
+}
+
+
+private partial def synthInstanceMainCore (mvar : Expr) : MetaM (Option Unit) := do
+  withIncRecDepth do
+    let backtrackSet := ipmBacktrackExt.getState (← getEnv)
+    let mvarType  ← inferType mvar
+    let mvarType  ← instantiateMVars mvarType
+    if !(ipmClassesExt.getState (← getEnv)).contains mvarType.getAppFn.constName then
+      return ← withTraceNode `Meta.synthInstance (return m!"{exceptOptionEmoji ·} switch to normal synthInstance") do
+        let some e ← synthInstance? mvarType | return none
+        mvar.mvarId!.assign e
+        return some ()
+
+    let mctx0 ← getMCtx
+    withTraceNode `Meta.synthInstance (return m!"{exceptOptionEmoji ·} new goal {MessageData.withMCtx mctx0 m!"{mvarType}"} => {mvarType}") do
+    let instances ← SynthInstance.getInstances mvarType
+    let mctx      ← getMCtx
+    if instances.isEmpty then
+      return none
+    for inst in instances.reverse do
+      let (res, match?) ← withTraceNode `Meta.synthInstance
+        (λ r => withMCtx mctx do return MessageData.withMCtx mctx m!"{exceptOptionEmoji (r.map (·.1))} apply {inst.val} to {← instantiateMVars (← inferType mvar)}") do
+        setMCtx mctx
+        let some (mctx', subgoals) ← withAssignableSyntheticOpaque (SynthInstance.tryResolve mvar inst) | return (none, false)
+        setMCtx mctx'
+        for g in subgoals do
+          let some _ ← synthInstanceMainCore g | return (none, true)
+        return (some (), true)
+      if res.isSome then
+        return res
+      if (match? && !backtrackSet.contains inst.val.getAppFn.constName) then
+        trace[Meta.synthInstance] "no backtracking to other instances"
+        return res
+    return none
+
+private def synthInstanceMain (type : Expr) (_maxResultSize : Nat) : MetaM (Option Expr) :=
+  withCurrHeartbeats do
+     let mvar ← mkFreshExprMVar type
+     tryCatchRuntimeEx (do
+       let some _ ← synthInstanceMainCore mvar | return none
+       return mvar)
+       fun ex =>
+         if ex.isRuntime then
+           throwError "failed to synthesize{indentExpr type}\n{ex.toMessageData}{useDiagnosticMsg}"
+         else
+           throw ex
+
+private def synthInstanceCore? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (Option Expr) := do
+  let opts ← getOptions
+  let maxResultSize := maxResultSize?.getD (synthInstance.maxSize.get opts)
+  withTraceNode `Meta.synthInstance
+    (return m!"IPM: {exceptOptionEmoji ·} {← instantiateMVars type}") do
+  withConfig (fun config => { config with isDefEqStuckEx := true, transparency := TransparencyMode.instances,
+                                          foApprox := true, ctxApprox := true, constApprox := false, univApprox := false }) do
+  withInTypeClassResolution do
+    let type ← instantiateMVars type
+    -- TODO: if it becomes necessary, run whnf under the ∀ quantifiers of type
+    -- let type ← preprocess type
+    -- TODO: if it becomes necessary, create mvars for outParams
+    -- let normType ← preprocessOutParam type
+    let normType := type
+    -- key point: we don't create a new MCtxDepth here such that we can instantiate and create mvars
+    let result? ← synthInstanceMain normType maxResultSize
+    trace[Meta.synthInstance] "result {result?}"
+    return result?
+
+protected def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (Option (Expr × Std.HashSet MVarId)) := do profileitM Exception "typeclass inference " (← getOptions) (decl := type.getAppFn.constName?.getD .anonymous) do
+  -- we can be sure that e only depends on the mvars that actually appear in e
+  (← synthInstanceCore? type maxResultSize?).mapM λ e => do let e ← instantiateMVars e; return (e, ← e.getMVarDependencies)
+
+protected def trySynthInstance (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (LOption (Expr × Std.HashSet MVarId)) := do
+  catchInternalId isDefEqStuckExceptionId
+    (toLOptionM <| ProofMode.synthInstance? type maxResultSize?)
+    (fun _ => pure LOption.undef)
+
+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
+
+syntax (name := ipm_synth) "#ipm_synth " term : command
+
+@[command_elab ipm_synth]
+def ipm_synth_elab : Command.CommandElab
+  | `(#ipm_synth $term) =>
+        withoutModifyingEnv <| Command.runTermElabM fun _ => Term.withDeclName `_ipm_synth do
+        let e ← Term.elabTerm term none
+        Term.synthesizeSyntheticMVarsNoPostponing (ignoreStuckTC := true)
+        let e ← Term.levelMVarToParam (← instantiateMVars e)
+        match ← ProofMode.trySynthInstance e with
+        | .undef => logInfo "Undefined"
+        | .none => logInfo "None"
+        | .some (e, mvars) => do
+            logInfo m!"solution: {← inferType e}, new goals: {← mvars.toList.mapM (λ m => do return m!"{Expr.mvar m}: {← m.getType}")}"
+  | _ => throwUnsupportedSyntax
diff --git a/src/Iris/ProofMode/Tactics/Apply.lean b/src/Iris/ProofMode/Tactics/Apply.lean
index 9f4c2186..58c36120 100644
--- a/src/Iris/ProofMode/Tactics/Apply.lean
+++ b/src/Iris/ProofMode/Tactics/Apply.lean
@@ -4,23 +4,24 @@ Released under Apache 2.0 license as described in the file LICENSE.
 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 tac_apply [BI PROP] {p} {P Q P' Q1 R : PROP}
+theorem apply [BI PROP] {p} {P Q P' Q1 R : PROP}
     (h1 : P ⊣⊢ P' ∗ □?p Q) (h2 : P' ⊢ Q1)
-    [h3 : IntoWand p false Q Q1 R] : P ⊢ R :=
+    [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
   let ⟨_, hyps', _, out, p, _, pf⟩ := hyps.remove true uniq
   let A ← mkFreshExprMVarQ q($prop)
-  if let LOption.some _ ← trySynthInstanceQ q(IntoWand $p false $out $A $goal) then
+  if let some _ ← ProofMode.trySynthInstanceQAddingGoals gs q(IntoWand $p false $out .out $A .in $goal) then
      let pf' ← gs.addGoal hyps' A
-     return q(tac_apply $pf $pf')
+     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
@@ -31,14 +32,16 @@ elab "iapply" colGt pmt:pmTerm : tactic => do
   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
+  let ⟨uniq, _, hyps, pf⟩ ← iHave gs hyps pmt (← `(binderIdent|_)) true (mayPostpone := true)
   let ⟨e', _, _, out, p, _, pf'⟩ := hyps.remove true uniq
-  if let (some _, some _) := (← try? <| synthInstanceQ q(FromAssumption $p $out $goal),
-                              ← try? <| synthInstanceQ q(TCOr (Affine $e') (Absorbing $goal))) then
-    -- behave like iexact
-    mvar.assign q($(pf).trans (assumption (Q := $goal) $pf'))
-    replaceMainGoal (← gs.getGoals)
-  else
-    let pf' ← iApplyCore gs hyps goal uniq
-    mvar.assign q($(pf).trans $pf')
-    replaceMainGoal (← gs.getGoals)
+  if let some _ ← ProofMode.trySynthInstanceQAddingGoals gs 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
+  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 4d5953b3..b8671c13 100644
--- a/src/Iris/ProofMode/Tactics/Assumption.lean
+++ b/src/Iris/ProofMode/Tactics/Assumption.lean
@@ -10,7 +10,7 @@ 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 A Q] [TCOr (Affine P) (Absorbing Q)] :
+    [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
@@ -26,7 +26,7 @@ def assumptionLean {prop : Q(Type u)} (_bi : Q(BI $prop)) (ehyps goal : Q($prop)
 
       -- try to solve the goal
       try
-        let _ ← synthInstanceQ q(FromAssumption true $P $goal)
+        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 ()
@@ -41,6 +41,10 @@ elab "iassumption_lean" : tactic => do
   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))
@@ -50,9 +54,9 @@ variable {prop : Q(Type u)} (bi : Q(BI $prop)) (Q : Q($prop))
 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 $ty $Q)
+      synthInstance q(FromAssumption $b .in $ty $Q)
     | failure
-  let _ : Q(FromAssumption $b $ty $Q) := inst
+  let _ : Q(FromAssumption $b .in $ty $Q) := inst
   have : $out =Q iprop(□?$b $ty) := ⟨⟩
   match fastPath with
   | .absorbing _ => return q(assumption (Q := $Q) $pf)
@@ -75,9 +79,9 @@ def assumptionSlow (assume : Bool) :
     Pure.pure (.affine q(emp_affine))
   | out, .hyp _ _ _ b ty _ => do
     let fromAssum (_:Unit) := do
-      let _ ← synthInstanceQ q(FromAssumption $b $ty $Q)
+      let _ ← synthInstanceQ q(FromAssumption $b .in $ty $Q)
       let inst ← try? (synthInstanceQ q(Affine $out))
-      return .main q(FromAssumption.from_assumption) inst
+      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
diff --git a/src/Iris/ProofMode/Tactics/Basic.lean b/src/Iris/ProofMode/Tactics/Basic.lean
index bccbff3a..e5a63a23 100644
--- a/src/Iris/ProofMode/Tactics/Basic.lean
+++ b/src/Iris/ProofMode/Tactics/Basic.lean
@@ -5,6 +5,8 @@ Authors: Lars König, Mario Carneiro
 -/
 import Iris.ProofMode.Expr
 import Iris.ProofMode.Classes
+import Iris.ProofMode.Goals
+import Iris.ProofMode.SynthInstance
 
 namespace Iris.ProofMode
 open Lean Elab.Tactic Meta Qq BI Std
@@ -23,12 +25,12 @@ def istart (mvar : MVarId) : MetaM (MVarId × IrisGoal) := mvar.withContext do
   let prop ← mkFreshExprMVarQ q(Type u)
   let P ← mkFreshExprMVarQ q($prop)
   let bi ← mkFreshExprMVarQ q(BI $prop)
-  let _ ← synthInstanceQ q(ProofMode.AsEmpValid2 $goal $P)
+  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.as_emp_valid_2 $goal $subgoal)
+  mvar.assign q(ProofMode.asEmpValid_2 $goal $subgoal)
   pure (subgoal.mvarId!, irisGoal)
 
 elab "istart" : tactic => do
@@ -45,47 +47,9 @@ elab "istop" : tactic => do
   let some irisGoal := parseIrisGoal? goal | throwError "not in proof mode"
   mvar.setType irisGoal.strip
 
-theorem assumption [BI PROP] {p : Bool} {P P' A Q : PROP} [inst : FromAssumption p 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
-
-def binderIdentHasName (name : Name) (id : TSyntax ``binderIdent) : Bool :=
-  match id with
-  | `(binderIdent| $name':ident) => name'.getId == name
-  | _ => false
-
 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
-
-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
-  -- don't override an existing name, e.g. for ?_
-  if !name.isAnonymous then
-    m.setUserName name
-  g.goals.modify (·.push m)
-
-def Goals.getGoals {prop : Q(Type u)} {bi : Q(BI $prop)} (g : Goals bi) : MetaM (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)
-  return (nonDep ++ dep).toList
diff --git a/src/Iris/ProofMode/Tactics/Exact.lean b/src/Iris/ProofMode/Tactics/Exact.lean
index dd71eed7..0a8e5d34 100644
--- a/src/Iris/ProofMode/Tactics/Exact.lean
+++ b/src/Iris/ProofMode/Tactics/Exact.lean
@@ -1,25 +1,25 @@
 /-
 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.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
-  -- find hypothesis index
-  let mvar ← getMainGoal
+  let (mvar, { bi, hyps, goal, .. }) ← istart (← getMainGoal)
   mvar.withContext do
-  let g ← instantiateMVars <| ← mvar.getType
-  let some { hyps, goal, .. } := parseIrisGoal? g | throwError "not in proof mode"
+  let gs ← Goals.new bi
   let uniq ← hyps.findWithInfo hyp
   let ⟨e', _, _, out, p, _, pf⟩ := hyps.remove true uniq
 
-  let _ ← synthInstanceQ q(FromAssumption $p $out $goal)
+  let some _ ← ProofMode.trySynthInstanceQAddingGoals gs q(FromAssumption $p .in $out $goal)
+    | throwError "iexact: cannot unify {out} and {goal}"
   let _ ← synthInstanceQ q(TCOr (Affine $e') (Absorbing $goal))
 
   mvar.assign q(assumption (Q := $goal) $pf)
-  replaceMainGoal []
+  replaceMainGoal (← gs.getGoals)
diff --git a/src/Iris/ProofMode/Tactics/Exists.lean b/src/Iris/ProofMode/Tactics/Exists.lean
index eeef5484..d1ca14c0 100644
--- a/src/Iris/ProofMode/Tactics/Exists.lean
+++ b/src/Iris/ProofMode/Tactics/Exists.lean
@@ -1,30 +1,40 @@
 /-
 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.Tactics.Basic
 
 namespace Iris.ProofMode
 open Lean Elab Tactic Meta Qq BI
 
-theorem exists_intro' [BI PROP] {Φ : α → PROP} {P Q : PROP} [inst : FromExists Q Φ]
-    (a : α) (h : P ⊢ Φ a) : P ⊢ Q :=
-  h.trans <| (exists_intro a).trans inst.1
+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" x:term : tactic => do
+elab "iexists" xs:term,+ : tactic => do
   -- resolve existential quantifier with the given argument
 
   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
 
-  let v ← mkFreshLevelMVar
-  let α ← mkFreshExprMVarQ q(Sort v)
-  let Φ ← mkFreshExprMVarQ q($α → $prop)
-  let _ ← synthInstanceQ q(FromExists $goal $Φ)
-  let x ← elabTermEnsuringTypeQ (u := .succ .zero) x α
-  let m : Quoted q($e ⊢ $Φ $x) ← mkFreshExprSyntheticOpaqueMVar <|
-    IrisGoal.toExpr { prop, bi, hyps, goal := Expr.headBeta q($Φ $x), .. }
+  for x in xs.getElems do
+    have new_goal : Q($prop) := new_goal_and_pf.1
+    let new_goal_pf : Q($new_goal ⊢ $goal) := new_goal_and_pf.2
+    let v ← mkFreshLevelMVar
+    let α ← mkFreshExprMVarQ q(Sort v)
+    let Φ ← mkFreshExprMVarQ q($α → $prop)
+    let some _ ← ProofMode.trySynthInstanceQAddingGoals gs 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
+    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'⟩
 
-  mvar.assign q(exists_intro' (Q := $goal) $x $m)
-  replaceMainGoal [m.mvarId!]
+  let m : Q($e ⊢ $(new_goal_and_pf.1)) ← gs.addGoal 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 2802ab74..f9d6b169 100644
--- a/src/Iris/ProofMode/Tactics/Have.lean
+++ b/src/Iris/ProofMode/Tactics/Have.lean
@@ -10,13 +10,12 @@ import Iris.ProofMode.Tactics.Specialize
 namespace Iris.ProofMode
 open Lean Elab Tactic Meta Qq BI Std
 
-theorem have_as_emp_valid [BI PROP] {φ} {P Q : PROP}
-    [h1 : AsEmpValid2 φ P] (h : φ) : Q ⊢ Q ∗ P :=
-  sep_emp.2.trans (sep_mono_r (h1.1.mp h))
+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))
 
-
-def iHaveCore (gs : @Goals u prop bi) {e} (hyps : Hyps bi e)
-  (tm : Term) (name : TSyntax ``binderIdent) (keep : Bool) : TacticM (Name × (e' : _) × Hyps bi e' × Q($e ⊢ $e')) := do
+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
   if let some uniq ← try? <| hyps.findWithInfo ⟨tm⟩ then
     -- assertion from the Iris context
     let ⟨_, hyps, _, out', p, _, pf⟩ := hyps.remove (!keep) uniq
@@ -24,13 +23,12 @@ def iHaveCore (gs : @Goals u prop bi) {e} (hyps : Hyps bi e)
     return ⟨uniq', _, hyps, q($pf.1)⟩
   else
     -- lean hypothesis
-    let val ← instantiateMVars <| ← elabTerm tm none false
+    let val ← instantiateMVars <| ← elabTerm tm none mayPostpone
     let ty ← instantiateMVars <| ← inferType val
 
     let ⟨newMVars, _, _⟩ ← forallMetaTelescopeReducing ty
     let val := mkAppN val newMVars
     -- TOOD: should we call postprocessAppMVars?
-    -- TODO: should we call Term.synthesizeSyntheticMVarsNoPostponing?
     let newMVarIds ← newMVars.map Expr.mvarId! |>.filterM fun mvarId => not <$> mvarId.isAssigned
     let otherMVarIds ← getMVarsNoDelayed val
     let otherMVarIds := otherMVarIds.filter (!newMVarIds.contains ·)
@@ -41,14 +39,14 @@ def iHaveCore (gs : @Goals u prop bi) {e} (hyps : Hyps bi e)
     let ⟨0, ty, val⟩ ← inferTypeQ val | throwError m!"{val} is not a Prop"
 
     let hyp ← mkFreshExprMVarQ q($prop)
-    let some _ ← try? <| synthInstanceQ q(AsEmpValid2 $ty $hyp) | throwError m!"{ty} is not an entailment"
+    let some _ ← ProofMode.trySynthInstanceQAddingGoals gs 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_as_emp_valid $val)⟩
+    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) : TacticM (Name × (e' : _) × Hyps bi e' × Q($e ⊢ $e')) := do
-  let ⟨uniq, _, hyps', pf⟩ ← iHaveCore gs hyps pmt.term name keep
+  (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.terms pmt.spats
   return ⟨uniq, _, hyps'', q($(pf).trans $pf')⟩
 
diff --git a/src/Iris/ProofMode/Tactics/Intro.lean b/src/Iris/ProofMode/Tactics/Intro.lean
index 92b82de7..5d901a91 100644
--- a/src/Iris/ProofMode/Tactics/Intro.lean
+++ b/src/Iris/ProofMode/Tactics/Intro.lean
@@ -45,18 +45,17 @@ theorem wand_intro_spatial [BI PROP] {P Q A1 A2 : PROP}
 
 variable {prop : Q(Type u)} (bi : Q(BI $prop)) in
 partial def iIntroCore
-    {P} (hyps : Hyps bi P) (Q : Q($prop)) (pats : List iCasesPat)
-    (k : ∀ {P}, Hyps bi P → (Q : Q($prop)) → MetaM Q($P ⊢ $Q)) :
+    {P} (gs : Goals bi) (hyps : Hyps bi P) (Q : Q($prop)) (pats : List iCasesPat) :
     MetaM (Q($P ⊢ $Q)) := do
   match pats with
-  | [] => k hyps Q
+  | [] => gs.addGoal hyps Q
   | pat :: pats =>
     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)
     if let (.clear, some _) := (pat, fromImp) then
-      let pf ← iIntroCore hyps A2 pats k
+      let pf ← iIntroCore gs hyps A2 pats
       return q(imp_intro_drop (Q := $Q) $pf)
     else
     let alres ← try? (α := _ × (v : Level) × (α : Q(Sort v)) × (Φ : Q($α → $prop)) ×
@@ -72,29 +71,29 @@ partial def iIntroCore
         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 k
+        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 · A2 pats k)
+      let pf ← iCasesCore bi hyps A2 q(true) q(iprop(□ $B)) B ⟨⟩ pat (iIntroCore gs · 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 · A2 pats k)
+      let pf ← iCasesCore bi hyps A2 q(true) q(iprop(□ $B)) B ⟨⟩ pat (iIntroCore gs · 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 · A2 pats k)
+      let pf ← iCasesCore bi hyps A2 q(false) B B ⟨⟩ pat (iIntroCore gs · 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 · A2 pats k)
+      let pf ← iCasesCore bi hyps A2 q(false) A1 A1 ⟨⟩ pat (iIntroCore gs · A2 pats)
       return q(wand_intro_spatial (Q := $Q) $pf)
 
 
@@ -107,7 +106,7 @@ elab "iintro" pats:(colGt icasesPat)* : tactic => do
 
   -- process patterns
   let gs ← Goals.new bi
-  let pf ← iIntroCore bi hyps goal pats.toList <| gs.addGoal
+  let pf ← iIntroCore bi gs 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 f6a9cc8d..3e801937 100644
--- a/src/Iris/ProofMode/Tactics/LeftRight.lean
+++ b/src/Iris/ProofMode/Tactics/LeftRight.lean
@@ -15,15 +15,17 @@ theorem from_or_l [BI PROP] {P Q A1 A2 : PROP} [inst : FromOr Q A1 A2]
 elab "ileft" : tactic => do
   let (mvar, { u, prop, bi, e, hyps, goal }) ← istart (← getMainGoal)
   mvar.withContext do
+  let gs ← Goals.new bi
 
   -- choose left side of disjunction
   let A1 ← mkFreshExprMVarQ prop
   let A2 ← mkFreshExprMVarQ prop
-  let _ ← synthInstanceQ q(FromOr $goal $A1 $A2)
-  let m : Q($e ⊢ $A1) ← mkFreshExprSyntheticOpaqueMVar <|
-    IrisGoal.toExpr { u, prop, bi, hyps, goal := A1, .. }
+  let some _ ← ProofMode.trySynthInstanceQAddingGoals gs q(FromOr $goal $A1 $A2)
+    | throwError "ileft: {goal} is not a disjunction"
+
+  let m : Q($e ⊢ $A1) ← gs.addGoal hyps A1
   mvar.assign q(from_or_l (Q := $goal) $m)
-  replaceMainGoal [m.mvarId!]
+  replaceMainGoal (← gs.getGoals)
 
 theorem from_or_r [BI PROP] {P Q A1 A2 : PROP} [inst : FromOr Q A1 A2]
     (h1 : P ⊢ A2) : P ⊢ Q :=
@@ -32,12 +34,13 @@ theorem from_or_r [BI PROP] {P Q A1 A2 : PROP} [inst : FromOr Q A1 A2]
 elab "iright" : tactic => do
   let (mvar, { u, prop, bi, e, hyps, goal }) ← istart (← getMainGoal)
   mvar.withContext do
+  let gs ← Goals.new bi
 
   -- choose right side of disjunction
   let A1 ← mkFreshExprMVarQ prop
   let A2 ← mkFreshExprMVarQ prop
-  let _ ← synthInstanceQ q(FromOr $goal $A1 $A2)
-  let m : Q($e ⊢ $A2) ← mkFreshExprSyntheticOpaqueMVar <|
-    IrisGoal.toExpr { u, prop, bi, hyps, goal := A2, .. }
+  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
   mvar.assign q(from_or_r (Q := $goal) $m)
-  replaceMainGoal [m.mvarId!]
+  replaceMainGoal (← gs.getGoals)
diff --git a/src/Iris/ProofMode/Tactics/Pure.lean b/src/Iris/ProofMode/Tactics/Pure.lean
index 1cdfbbc9..abfb99cf 100644
--- a/src/Iris/ProofMode/Tactics/Pure.lean
+++ b/src/Iris/ProofMode/Tactics/Pure.lean
@@ -68,6 +68,7 @@ elab "ipure" colGt hyp:ident : tactic => do
   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
diff --git a/src/Iris/ProofMode/Tactics/Specialize.lean b/src/Iris/ProofMode/Tactics/Specialize.lean
index 2a55d055..70c23eac 100644
--- a/src/Iris/ProofMode/Tactics/Specialize.lean
+++ b/src/Iris/ProofMode/Tactics/Specialize.lean
@@ -15,22 +15,22 @@ structure SpecializeState {prop : Q(Type u)} (bi : Q(BI $prop)) (orig : Q($prop)
   (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 P3 : PROP}
+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 false Q P2 P3] [h4 : FromAssumption p P1 P2] :
-    A1 ⊢ A3 ∗ □?(p && q) P3 := by
+    [h3 : IntoWand q p Q .in P1 .out P2] :
+    A1 ⊢ A3 ∗ □?(p && q) P2 := by
   refine h1.trans <| (sep_mono_l h2.1).trans <| sep_assoc.1.trans (sep_mono_r ?_)
   cases p with
-  | false => exact (sep_mono_r h3.1).trans <| (sep_mono_l h4.1).trans wand_elim_r
+  | false => exact (sep_mono_r h3.1).trans <| wand_elim_r
   | true => exact
     (sep_mono intuitionisticallyIf_intutitionistically.2 intuitionisticallyIf_idem.2).trans <|
-    intuitionisticallyIf_sep_2.trans <| intuitionisticallyIf_mono <| (sep_mono_l h4.1).trans (wand_elim' h3.1)
+    intuitionisticallyIf_sep_2.trans <| intuitionisticallyIf_mono <| (wand_elim' h3.1)
 
 -- 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 P2 : PROP}
+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 P1 P2] : A1 ⊢ A3 ∗ P2 := by
+    [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
 
@@ -38,13 +38,13 @@ theorem specialize_forall [BI PROP] {p : Bool} {A1 A2 P : PROP} {α : Sort _} {
     [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_forall :
+def SpecializeState.process_forall (gs : @Goals u prop bi) :
     @SpecializeState u prop bi orig → Term → TermElabM (SpecializeState bi orig)
   | { e, hyps, p, out, pf }, arg => do
     let v ← mkFreshLevelMVar
     let α : Q(Sort v) ← mkFreshExprMVarQ q(Sort v)
     let Φ : Q($α → $prop) ← mkFreshExprMVarQ q($α → $prop)
-    let _ ← synthInstanceQ q(IntoForall $out $Φ)
+    let some _ ← ProofMode.trySynthInstanceQAddingGoals gs q(IntoForall $out $Φ) | throwError "ispecialize: {out} is not a forall"
     let x ← elabTermEnsuringTypeQ (u := .succ .zero) arg α
     have out' : Q($prop) := Expr.headBeta q($Φ $x)
     have : $out' =Q $Φ $x := ⟨⟩
@@ -59,11 +59,8 @@ def SpecializeState.process_wand (gs : @Goals u prop bi) :
     have : $out₁ =Q iprop(□?$p1 $out₁') := ⟨⟩
     have : $p2 =Q ($p1 && $p) := ⟨⟩
 
-    let out₁'' ← mkFreshExprMVarQ prop
     let out₂ ← mkFreshExprMVarQ prop
-    let LOption.some _ ← trySynthInstanceQ q(IntoWand $p false $out $out₁'' $out₂) |
-      throwError m!"ispecialize: {out} is not a wand"
-    let LOption.some _ ← trySynthInstanceQ q(FromAssumption $p1 $out₁' $out₁'') |
+    let some _ ← ProofMode.trySynthInstanceQAddingGoals gs 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 }
@@ -74,9 +71,9 @@ 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 LOption.some _ ← trySynthInstanceQ q(IntoWand $p false $out $out₁ $out₂) | throwError m!"ispecialize: {out} is not a wand"
+    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 pf := q(specialize_wand_subgoal $pf $h' $pf')
+    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)
@@ -85,7 +82,7 @@ def iSpecializeCore (gs : @Goals u prop bi) {e} (hyps : Hyps bi e)
     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 <| alls.foldlM SpecializeState.process_forall state
+  let state ← liftM <| alls.foldlM (SpecializeState.process_forall gs) state
   let state ← liftM <| spats.foldlM (SpecializeState.process_wand gs) state
 
   let hyps' := Hyps.add bi name uniq state.p state.out state.hyps
diff --git a/src/Iris/Tests.lean b/src/Iris/Tests.lean
index 233cdff2..a5dd1ca4 100644
--- a/src/Iris/Tests.lean
+++ b/src/Iris/Tests.lean
@@ -1 +1,3 @@
+import Iris.Tests.Instances
+import Iris.Tests.Notation
 import Iris.Tests.Tactics
diff --git a/src/Iris/Tests/Instances.lean b/src/Iris/Tests/Instances.lean
new file mode 100644
index 00000000..78dac4c0
--- /dev/null
+++ b/src/Iris/Tests/Instances.lean
@@ -0,0 +1,51 @@
+/-
+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.BI
+import Iris.ProofMode
+
+namespace Iris.Tests
+open BI ProofMode
+
+/- Test the backtracking of ipm_synth -/
+section backtracking
+
+variable [BI PROP] (P1 P2 Q : PROP) [FromAssumption p .in P1 Q] [FromAssumption p .in P2 Q]
+
+/- Test backtracking with both options. IPM backtracking search will search for right conjuncts before
+left conjuncts, because `fromAssumption_and_r` is declared after `fromAssumption_and_l`.
+This is the same behavior as regular typeclass search. -/
+/-- info: solution: FromAssumption p InOut.in iprop(P1 ∧ P2) Q, new goals: [] -/
+#guard_msgs in #ipm_synth (FromAssumption p .in iprop(P1 ∧ P2) Q)
+
+/- Test backtracking picking the left conjunct. -/
+/-- info: solution: FromAssumption p InOut.in iprop(P1 ∧ P2) P1, new goals: [] -/
+#guard_msgs in #ipm_synth (FromAssumption p .in iprop(P1 ∧ P2) P1)
+
+/- Test backtracking picking the right conjunct. -/
+/-- info: solution: FromAssumption p InOut.in iprop(P1 ∧ P2) P2, new goals: [] -/
+#guard_msgs in #ipm_synth (FromAssumption p .in iprop(P1 ∧ P2) P2)
+
+end backtracking
+
+/- Test creation and instantiation of mvars using of ipm_synth -/
+section mvars
+
+variable [BI PROP] (P1 P2 : Nat → PROP)
+
+/- Test creation of mvars -/
+/-- info: solution: IntoWand false false iprop(∀ x, P1 x -∗ P2 x) InOut.out (P1 ?m.24) InOut.out
+  (P2 ?m.24), new goals: [?m.24: Nat] -/
+#guard_msgs in #ipm_synth (IntoWand false false iprop(∀ a, P1 a -∗ P2 a) .out _ .out _)
+
+/- Test instantiation of forall quantifier -/
+/-- info: solution: IntoWand false false iprop(∀ x, P1 x -∗ P2 x) InOut.in (P1 1) InOut.out (P2 1), new goals: [] -/
+#guard_msgs in #ipm_synth (IntoWand false false iprop(∀ a, P1 a -∗ P2 a) .in (P1 1) .out _)
+
+/- Test instantiation of mvar created outside ipm_synth -/
+/-- info: solution: IntoWand false false iprop(P1 1 -∗ P2 1) InOut.in (P1 1) InOut.out (P2 1), new goals: [] -/
+#guard_msgs in #ipm_synth (IntoWand false false iprop(P1 _ -∗ P2 1) .in (P1 1) .out _)
+
+end mvars
diff --git a/src/Iris/Tests/Tactics.lean b/src/Iris/Tests/Tactics.lean
index 0a51a09c..800af982 100644
--- a/src/Iris/Tests/Tactics.lean
+++ b/src/Iris/Tests/Tactics.lean
@@ -118,22 +118,39 @@ end intro
 -- exists
 namespace «exists»
 
-theorem id [BI PROP] : ⊢ (∃ x, x : PROP) := by
+theorem id [BI PROP] : ⊢@{PROP} ∃ x, x := by
   iexists iprop(True)
   ipure_intro
   exact True.intro
 
-theorem f [BI PROP] : ⊢ (∃ (_x : Nat), True ∨ False : PROP) := by
+theorem f [BI PROP] : ⊢@{PROP} ∃ (_x : Nat), True ∨ False := by
   iexists 42
   ileft
   ipure_intro
   exact True.intro
 
-theorem pure [BI PROP] : ⊢ (⌜∃ x, x ∨ False⌝ : PROP) := by
+theorem pure [BI PROP] : ⊢@{PROP} ⌜∃ x, x ∨ False⌝ := by
   iexists True
   ipure_intro
   exact Or.inl True.intro
 
+
+theorem mvar [BI PROP] : ⊢@{PROP} ∃ x, ⌜x = 42⌝ := by
+  iexists ?y
+  ipure_intro
+  rfl
+
+theorem mvar_anon [BI PROP] : ⊢@{PROP} ∃ x, ⌜x = 42⌝ := by
+  iexists _
+  ipure_intro
+  rfl
+
+theorem mvar_two [BI PROP] : ⊢@{PROP} ∃ x y : Nat, ⌜x = y⌝ := by
+  iexists _, 1
+  ipure_intro
+  rfl
+
+
 end «exists»
 
 -- exact
@@ -228,9 +245,8 @@ theorem exact_lean [BI PROP] (Q : PROP) (H : ⊢ Q) : ⊢ Q := by
   iapply H
 
 theorem exact_lean' [BI PROP] (Q : PROP) : Q ⊢ (emp ∗ Q) ∗ emp := by
-  iapply (wand_intro (PROP:=PROP) sep_emp.mpr)
-  istop
-  apply affine
+  iapply (wand_intro sep_emp.mpr)
+  iemp_intro
 
 theorem exact_lean'' [BI PROP] (Q : PROP) (H : 0 = 0 → ⊢ Q) : ⊢ Q := by
   iapply H
@@ -238,10 +254,9 @@ theorem exact_lean'' [BI PROP] (Q : PROP) (H : 0 = 0 → ⊢ Q) : ⊢ Q := by
 
 theorem exact_lean''' [BI PROP] : ⊢@{PROP} ⌜1 = 1⌝ := by
   istart
-  iapply (pure_intro (PROP:=PROP) (P:=emp))
+  iapply (pure_intro (P:=emp))
   . rfl
-  istop
-  apply affine
+  iemp_intro
 
 theorem apply_lean [BI PROP] (P Q : PROP) (H : P ⊢ Q) (HP : ⊢ P) : ⊢ Q := by
   iapply H
@@ -254,7 +269,7 @@ theorem apply_lean' [BI PROP] (P Q : PROP) (H : ⊢ P -∗ Q) (HP : ⊢ P) : ⊢
 theorem apply_lean'' [BI PROP] (P Q : PROP) (H1 : P ⊢ Q) (H2 : Q ⊢ R) : P ⊢ R := by
   iintro HP
   iapply (wand_intro (emp_sep.mp.trans H2))
-  . istop; apply affine
+  . ipure_intro; trivial
   iapply H1 with HP
 
 theorem multiple_lean [BI PROP] (P Q R : PROP) (H : P ⊢ Q -∗ R) (HP : ⊢ P) : ⊢ Q -∗ R := by
@@ -271,10 +286,6 @@ theorem exact_forall [BI PROP] (P : α → PROP) (a : α) (H : ⊢ ∀ x, P x) :
   istart
   iapply H
 
-/--
-error: iapply: cannot apply P ?x to P a
--/
-#guard_msgs in -- TODO: allow tc search to instantiate mvars
 theorem exact_forall' [BI PROP] (P : α → PROP) (a : α) (H : ∀ x, ⊢ P x) : ⊢ P a := by
   iapply H
 
@@ -286,29 +297,28 @@ theorem apply_forall' [BI PROP] (P Q : α → PROP) (a b : α) : (∀ x, ∀ y,
   iintro H HP
   iapply H $! a, b with HP
 
-/- TODO: enable this when tc seach can create mvars
+/-- error: ispecialize: iprop(P a -∗ Q b) is not a forall -/
+#guard_msgs in
+theorem apply_forall_too_many [BI PROP] (P Q : α → PROP) (a b : α) : (∀ x, ∀ y, P x -∗ Q y) ⊢ P a -∗ Q b := by
+  iintro H HP
+  iapply H $! a, b, _ with HP
+
 theorem apply_forall2 [BI PROP] (P Q : α → PROP) (a b : α) : (∀ x, ∀ y, P x -∗ Q y) ⊢ P a -∗ Q b := by
   iintro H HP
   iapply H with HP
--/
 
-/--
-error: ispecialize: cannot instantiate iprop(P ?m.37 -∗ Q ?m.40) with P a
--/
-#guard_msgs in -- TODO: tc search should be able to instantiate mvars
 theorem apply_forall3 [BI PROP] (P Q : α → PROP) (a b : α) : (∀ x, ∀ y, P x -∗ Q y) ⊢ P a -∗ Q b := by
   iintro H HP
   iapply H $! ?_, ?_ with HP
 
-/- TODO: enable this when tc seach can create mvars
 theorem apply_forall4 [BI PROP] (P Q : α → PROP) (a b : α) : (∀ x, ∀ y, P x -∗ Q y) ⊢ P a -∗ Q b := by
   iintro H HP
   iapply H
--/
+  iapply HP
 
 theorem apply_forall_intuitionistic [BI PROP] (P Q : α → PROP) (a b : α) (H : ⊢ □ ∀ x, ∀ y, P x -∗ Q y) : P a ⊢ Q b := by
   iintro HP
-  iapply H $! a, b with HP
+  iapply H $! a with HP
 
 theorem apply_forall_intuitionistic' [BI PROP] (P Q : α → PROP) (a b : α) : (□ ∀ x, ∀ y, P x -∗ Q y) ⊢ P a -∗ Q b := by
   iintro H HP
@@ -321,6 +331,28 @@ theorem apply_two_wands [BI PROP] (P Q : Nat → PROP) :
   . iexact HP1
   . iexact HP2
 
+theorem apply_and_l [BI PROP] (P Q : Nat → PROP) :
+  ((P 1 -∗ P 2) ∧ (Q 1 -∗ Q 2)) ⊢ P 1 -∗ P 2 := by
+  iintro H HP1
+  iapply H
+  iexact HP1
+
+theorem apply_and_r [BI PROP] (P Q : Nat → PROP) :
+  ((P 1 -∗ P 2) ∧ (Q 1 -∗ Q 2)) ⊢ Q 1 -∗ Q 2 := by
+  iintro H HQ1
+  iapply H
+  iexact HQ1
+
+theorem apply_and_l_exact [BI PROP] (P Q : Nat → PROP) :
+  (P 1 ∧ Q 1) ⊢ P 1 := by
+  iintro H
+  iapply H
+
+theorem apply_and_r_exact [BI PROP] (P Q : Nat → PROP) :
+  (P 1 ∧ Q 1) ⊢ Q 1 := by
+  iintro H
+  iapply H
+
 end apply
 
 -- have
@@ -345,6 +377,10 @@ theorem exact_lean_forall3 [BI PROP] (Q : Nat → Nat → PROP) (H : ∀ x y, 
   case res => exact 1
   iexact HQ
 
+theorem exact_lean_forall4 [BI PROP] (Q : Nat → PROP) (H : ∀ x, ⊢ Q x) : ⊢ Q 1 := by
+  ihave HQ := H
+  iexact HQ
+
 theorem exact_lean_tc [BI PROP] (Q : Nat → PROP) (H : ∀ (P : PROP) [Persistent P], ⊢ P) : ⊢ Q 1 := by
   ihave HQ := H
   rotate_right 1; exact iprop(□ Q 1)