diff --git a/src/Iris/BI/Lib/BUpdPlain.lean b/src/Iris/BI/Lib/BUpdPlain.lean
index b525eeb8..1cdd96e2 100644
--- a/src/Iris/BI/Lib/BUpdPlain.lean
+++ b/src/Iris/BI/Lib/BUpdPlain.lean
@@ -34,8 +34,7 @@ theorem BUpdPlain_intro {P : PROP} : P ⊢ BUpdPlain P := by
   iintro Hp
   unfold BUpdPlain
   iintro _ H
-  iapply H
-  iexact Hp
+  iapply H $$ Hp
 
 theorem BUpdPlain_mono {P Q : PROP} : (P ⊢ Q) → (BUpdPlain P ⊢ BUpdPlain Q) := by
   intros H
@@ -43,27 +42,24 @@ theorem BUpdPlain_mono {P Q : PROP} : (P ⊢ Q) → (BUpdPlain P ⊢ BUpdPlain Q
   iintro R HQR
   iintro Hp
   have H1 : ⊢ iprop(Q -∗ ■ HQR) -∗ iprop(P -∗ ■ HQR) := by
-    iintro H
-    iintro Hp
+    iintro H Hp
     iapply H
     apply H
   iintro ⟨Ha, H2⟩
-  iapply Ha $! HQR
-  iapply H1
-  iexact H2
+  iapply Ha
+  iapply H1 $$ H2
 
 theorem BUpdPlain_idemp {P : PROP} : BUpdPlain (BUpdPlain P) ⊢ BUpdPlain P := by
   unfold BUpdPlain
   iintro Hp R H
-  iapply Hp $! R
+  iapply Hp
   iintro Hp
-  iapply Hp $! R
-  iassumption
+  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
-  iapply Hp $! R
+  iapply Hp
   iintro Hp
   iapply H
   isplitl [Hp]
@@ -73,7 +69,7 @@ theorem BUpdPlain_frame_r {P Q : PROP} : BUpdPlain P ∗ Q ⊢ (BUpdPlain iprop(
 theorem BUpdPlain_plainly {P : PROP} : BUpdPlain iprop(■ P) ⊢ (■ P) := by
   unfold BUpdPlain
   iintro H
-  iapply H $! P
+  iapply H
   exact wand_rfl
 
 /- BiBUpdPlainly entails the alternative definition -/
diff --git a/src/Iris/Examples/Proofs.lean b/src/Iris/Examples/Proofs.lean
index e61cb97c..106fac2e 100644
--- a/src/Iris/Examples/Proofs.lean
+++ b/src/Iris/Examples/Proofs.lean
@@ -13,7 +13,7 @@ theorem proof_example_1 [BI PROP] (P Q R : PROP) (Φ : α → PROP) :
   P ∗ Q ∗ □ R ⊢ □ (R -∗ ∃ x, Φ x) -∗ ∃ x, Φ x ∗ P ∗ Q
 := by
   iintro ⟨HP, HQ, □HR⟩ □HRΦ
-  ihave HΦ := HRΦ with HR
+  ihave HΦ := HRΦ $$ HR
   icases HΦ with ⟨x, _HΦ⟩
   iexists x
   isplitr
diff --git a/src/Iris/ProofMode/Classes.lean b/src/Iris/ProofMode/Classes.lean
index 4150397b..eb9f3f4d 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 as_emp_valid_1 [BI PROP] (P : PROP) [AsEmpValid .into φ P] : φ → ⊢ P :=
+  AsEmpValid.as_emp_valid.1 rfl
+theorem as_emp_valid_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..2ac3ce6e
--- /dev/null
+++ b/src/Iris/ProofMode/Goals.lean
@@ -0,0 +1,45 @@
+/-
+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 5141513c..c191e3c4 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
@@ -103,6 +86,13 @@ instance intoForall_intuitionistically [BI PROP] (P : PROP) (Φ : α → PROP)
     [h : IntoForall P Φ] : IntoForall iprop(□ P) (fun a => iprop(□ (Φ a))) where
   into_forall := (intuitionistically_mono h.1).trans intuitionistically_forall_1
 
+instance intoForall_wand_pure [BI PROP] (P Q : PROP) Φ
+    [h : FromPure a P Φ] : IntoForall iprop(P -∗ Q) (fun _ : Φ => Q) where
+  into_forall := forall_intro λ hΦ =>
+    emp_sep.2.trans <| (sep_mono_l <|
+      (affinelyIf_emp.mpr.trans (affinelyIf_mono (pure_intro hΦ))).trans
+        h.1).trans wand_elim_r
+
 -- FromExists
 instance (priority := default + 10) fromExists_exists [BI PROP] (Φ : α → PROP) :
     FromExists iprop(∃ a, Φ a) Φ := ⟨.rfl⟩
@@ -397,56 +387,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/Patterns/ProofModeTerm.lean b/src/Iris/ProofMode/Patterns/ProofModeTerm.lean
index 0b45b19d..17fdc605 100644
--- a/src/Iris/ProofMode/Patterns/ProofModeTerm.lean
+++ b/src/Iris/ProofMode/Patterns/ProofModeTerm.lean
@@ -11,23 +11,17 @@ open Lean
 declare_syntax_cat pmTerm
 
 syntax term : pmTerm
-syntax term "with" specPat,+ : pmTerm
-syntax term "$!" term,+ : pmTerm
-syntax term "$!" term,+ "with" specPat,+ : pmTerm
+syntax term "$$" specPat,+ : pmTerm
 
 structure PMTerm where
   term : Term
-  terms : List Term
   spats : List SpecPat
   deriving Repr, Inhabited
 
 partial def PMTerm.parse (term : Syntax) : MacroM PMTerm := do
   match ← expandMacros term with
-  | `(pmTerm| $trm:term) => return ⟨trm, [], []⟩
-  | `(pmTerm| $trm:term with $spats,*) => return ⟨trm, [], ← parseSpats spats⟩
-  | `(pmTerm| $trm:term $! $ts,*) => return ⟨trm, ts.getElems.toList, []⟩
-  | `(pmTerm| $trm:term $! $ts,* with $spats,*) =>
-    return ⟨trm, ts.getElems.toList, ← parseSpats spats⟩
+  | `(pmTerm| $trm:term) => return ⟨trm, []⟩
+  | `(pmTerm| $trm:term $$ $spats,*) => return ⟨trm, ← parseSpats spats⟩
   | _ => Macro.throwUnsupported
 where
   parseSpats (spats : Syntax.TSepArray `specPat ",") : MacroM (List SpecPat) :=
diff --git a/src/Iris/ProofMode/Patterns/SpecPattern.lean b/src/Iris/ProofMode/Patterns/SpecPattern.lean
index c118734b..a482ca60 100644
--- a/src/Iris/ProofMode/Patterns/SpecPattern.lean
+++ b/src/Iris/ProofMode/Patterns/SpecPattern.lean
@@ -9,11 +9,13 @@ open Lean
 declare_syntax_cat specPat
 
 syntax ident : specPat
+syntax "%" term : specPat
 syntax "[" ident,* "]" optional(" as " ident) : specPat
 
 -- see https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris/proofmode/spec_patterns.v?ref_type=heads#L15
 inductive SpecPat
   | ident (name : Ident)
+  | pure (t : Term)
   | goal (names : List Ident) (goalName : Name)
   deriving Repr, Inhabited
 
@@ -24,14 +26,9 @@ partial def SpecPat.parse (pat : Syntax) : MacroM SpecPat := do
 where
   go : TSyntax `specPat → Option SpecPat
   | `(specPat| $name:ident) => some <| .ident name
+  | `(specPat| % $term:term) => some <| .pure term
   | `(specPat| [$[$names:ident],*]) => some <| .goal names.toList .anonymous
   | `(specPat| [$[$names:ident],*] as $goal:ident) => match goal.raw with
     | .ident _ _ val _ => some <| .goal names.toList val
     | _ => none
   | _ => none
-
-def headName (spats : List SpecPat) : Name :=
-  match spats.head? with
-    | some <| .ident _ => .anonymous
-    | some <| .goal _ name => name
-    | _ => .anonymous
diff --git a/src/Iris/ProofMode/SynthInstance.lean b/src/Iris/ProofMode/SynthInstance.lean
new file mode 100644
index 00000000..f5f9dac8
--- /dev/null
+++ b/src/Iris/ProofMode/SynthInstance.lean
@@ -0,0 +1,132 @@
+/-
+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
+
+/- TODO: How to call these functions? ProofMode.synthInstance, ipmSynthInstance, synthIPMInstance, synthInstanceIPM? -/
+
+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 mctx0 ← getMCtx
+      let (res, match?) ← withTraceNode `Meta.synthInstance
+        (λ r => withMCtx mctx0 do return MessageData.withMCtx mctx0 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: Should we run whnf under the ∀ quantifiers of type?
+    -- let type ← preprocess type
+    -- TODO: should we 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
diff --git a/src/Iris/ProofMode/Tactics/Apply.lean b/src/Iris/ProofMode/Tactics/Apply.lean
index 9f4c2186..c5de621a 100644
--- a/src/Iris/ProofMode/Tactics/Apply.lean
+++ b/src/Iris/ProofMode/Tactics/Apply.lean
@@ -4,6 +4,7 @@ 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
 
@@ -12,17 +13,17 @@ open Lean Elab Tactic Meta Qq BI Std
 
 theorem tac_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')
 
-  let some ⟨_, hyps'', pf''⟩ ← try? <| iSpecializeCore gs hyps uniq [] [.goal [] .anonymous] | throwError m!"iapply: cannot apply {out} to {goal}"
+  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
   return q($(pf'').trans $pf''')
 
@@ -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..fd99d134 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,7 +25,7 @@ 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) ←
@@ -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..76d3a55e 100644
--- a/src/Iris/ProofMode/Tactics/Have.lean
+++ b/src/Iris/ProofMode/Tactics/Have.lean
@@ -11,12 +11,12 @@ 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))
+    [h1 : AsEmpValid .into φ P] (h : φ) : Q ⊢ Q ∗ P :=
+  sep_emp.2.trans (sep_mono_r (as_emp_valid_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 +24,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,15 +40,15 @@ 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)⟩
 
 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
-  let ⟨_, hyps'', pf'⟩ ← iSpecializeCore gs hyps' uniq pmt.terms pmt.spats
+  (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
   return ⟨uniq, _, hyps'', q($(pf).trans $pf')⟩
 
 elab "ihave" colGt name:binderIdent " := " pmt:pmTerm  : tactic => do
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..082192a7 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,18 +38,6 @@ 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 :
-    @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 x ← elabTermEnsuringTypeQ (u := .succ .zero) arg α
-    have out' : Q($prop) := Expr.headBeta q($Φ $x)
-    have : $out' =Q $Φ $x := ⟨⟩
-    return { e, hyps, p, out := out', pf := q(specialize_forall $pf $x) }
-
 def SpecializeState.process_wand (gs : @Goals u prop bi) :
     @SpecializeState u prop bi orig → SpecPat → TermElabM (SpecializeState bi orig)
   | { hyps, p, out, pf, .. }, .ident i => do
@@ -59,14 +47,22 @@ 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 }
+  | { e, hyps, p, out, pf, .. }, .pure t => do
+    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 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
+    return { e, hyps, p, out := out', pf := q(specialize_forall $pf $x) }
   | { hyps, p, out, pf, .. }, .goal ns g => do
     let mut uniqs : NameSet := {}
     for name in ns do
@@ -74,18 +70,17 @@ 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)
-  (uniq : Name) (alls : List Term) (spats : List SpecPat) : TacticM ((e' : _) × Hyps bi e' × Q($e ⊢ $e')) := do
+  (uniq : Name) (spats : List SpecPat) : TacticM ((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 <| alls.foldlM SpecializeState.process_forall state
   let state ← liftM <| spats.foldlM (SpecializeState.process_wand gs) state
 
   let hyps' := Hyps.add bi name uniq state.p state.out state.hyps
@@ -99,7 +94,7 @@ elab "ispecialize" colGt pmt:pmTerm : tactic => do
   -- hypothesis must be in the context, otherwise use pose proof
   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.terms pmt.spats
+  let ⟨_, hyps', pf⟩ ← iSpecializeCore gs hyps uniq pmt.spats
   let pf' ← gs.addGoal hyps' goal
   mvar.assign q(($pf).trans $pf')
   replaceMainGoal (← gs.getGoals)
diff --git a/src/Iris/Tests/Tactics.lean b/src/Iris/Tests/Tactics.lean
index 0a51a09c..669bbb20 100644
--- a/src/Iris/Tests/Tactics.lean
+++ b/src/Iris/Tests/Tactics.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Lars König, Oliver Soeser
+Authors: Lars König, Oliver Soeser, Michael Sammler
 -/
 import Iris.BI
 import Iris.ProofMode
@@ -12,7 +12,8 @@ open Iris.BI
 /- This file contains tests with various scenarios for all available tactics. -/
 
 -- start stop
-theorem start_stop [BI PROP] (Q : PROP) (H : Q ⊢ Q) : Q ⊢ Q := by
+/-- Tests `istart` and `istop` for entering and exiting proof mode -/
+example [BI PROP] (Q : PROP) (H : Q ⊢ Q) : Q ⊢ Q := by
   istart
   iintro _HQ
   istop
@@ -21,23 +22,27 @@ theorem start_stop [BI PROP] (Q : PROP) (H : Q ⊢ Q) : Q ⊢ Q := by
 -- rename
 namespace rename
 
-theorem rename [BI PROP] (Q : PROP) : Q ⊢ Q := by
+/-- Tests basic hypothesis renaming with `irename` -/
+example [BI PROP] (Q : PROP) : Q ⊢ Q := by
   iintro HQ
   irename HQ => H
   iexact H
 
-theorem rename_by_type [BI PROP] (Q : PROP) : □ P ∗ Q ⊢ Q := by
+/-- Tests renaming a hypothesis by its type -/
+example [BI PROP] (P Q : PROP) : □ P ∗ Q ⊢ Q := by
   iintro ⟨_HP, HQ⟩
   irename: Q => H
   iexact H
 
-theorem rename_twice [BI PROP] (Q : PROP) : Q ⊢ Q := by
+/-- Tests renaming a hypothesis twice -/
+example [BI PROP] (Q : PROP) : Q ⊢ Q := by
   iintro HQ
   irename HQ => H
   irename H => HQ
   iexact HQ
 
-theorem rename_id [BI PROP] (Q : PROP) : Q ⊢ Q := by
+/-- Tests renaming a hypothesis to itself (no-op) -/
+example [BI PROP] (Q : PROP) : Q ⊢ Q := by
   iintro HQ
   irename HQ => HQ
   iexact HQ
@@ -47,13 +52,15 @@ end rename
 -- clear
 namespace clear
 
-theorem intuitionistic [BI PROP] (Q : PROP) : □ P ⊢ Q -∗ Q := by
+/-- Tests clearing an intuitionistic hypothesis with `iclear` -/
+example [BI PROP] (Q : PROP) : □ P ⊢ Q -∗ Q := by
   iintro □HP
   iintro HQ
   iclear HP
   iexact HQ
 
-theorem spatial [BI PROP] (Q : PROP) : <affine> P ⊢ Q -∗ Q := by
+/-- Tests clearing a spatial affine hypothesis with `iclear` -/
+example [BI PROP] (Q : PROP) : <affine> P ⊢ Q -∗ Q := by
   iintro HP
   iintro HQ
   iclear HP
@@ -64,52 +71,64 @@ end clear
 -- intro
 namespace intro
 
-theorem spatial [BI PROP] (Q : PROP) : Q ⊢ Q := by
+/-- Tests introducing a spatial hypothesis -/
+example [BI PROP] (Q : PROP) : Q ⊢ Q := by
   iintro HQ
   iexact HQ
 
-theorem intuitionistic [BI PROP] (Q : PROP) : □ Q ⊢ Q := by
+/-- Tests introducing an intuitionistic hypothesis with the `□` pattern -/
+example [BI PROP] (Q : PROP) : □ Q ⊢ Q := by
   iintro □HQ
   iexact HQ
 
-theorem as_intuitionistic [BI PROP] (Q : PROP) : <affine> <pers> Q ⊢ Q := by
+/-- Tests introducing an affine persistent proposition as intuitionistic -/
+example [BI PROP] (Q : PROP) : <affine> <pers> Q ⊢ Q := by
   iintro □HQ
   iexact HQ
 
-theorem as_intuitionistic_in_spatial [BI PROP] (Q : PROP) : ⊢ <pers> Q → Q := by
+/-- Tests introducing a persistent implication in the spatial context -/
+example [BI PROP] (Q : PROP) : ⊢ <pers> Q → Q := by
   iintro HQ
   iexact HQ
 
-theorem drop [BI PROP] (Q : PROP) : ⊢ P → Q -∗ Q := by
+/-- Tests dropping a hypothesis in an implication with the `-` pattern -/
+example [BI PROP] (Q : PROP) : ⊢ P → Q -∗ Q := by
   iintro - HQ
   iexact HQ
 
-theorem drop_after [BI PROP] (Q : PROP) : ⊢ Q -∗ P → Q := by
+/-- Tests dropping a hypothesis in an implication in a non-empty context -/
+example [BI PROP] (Q : PROP) : ⊢ Q -∗ P → Q := by
   iintro HQ -
   iexact HQ
 
-theorem «forall» [BI PROP] : ⊢ ∀ x, ⌜x = 0⌝ → (⌜x = 0⌝ : PROP) := by
+/-- Tests introducing an universally quantified variable -/
+example [BI PROP] : ⊢@{PROP} ∀ x, ⌜x = 0⌝ → ⌜x = 0⌝ := by
   iintro x
   iintro H
   iexact H
 
-theorem pure [BI PROP] [BIAffine PROP] (Q : PROP) : ⊢ ⌜φ⌝ -∗ Q -∗ Q := by
+/-- Tests introducing and extracting a pure hypothesis in affine BI -/
+example [BI PROP] [BIAffine PROP] φ (Q : PROP) : ⊢ ⌜φ⌝ -∗ Q -∗ Q := by
   iintro ⌜Hφ⌝ HQ
   iexact HQ
 
-theorem pattern [BI PROP] (Q : PROP) : □ (P1 ∨ P2) ∗ Q ⊢ Q := by
+/-- Tests introducing with disjunction pattern inside intuitionistic -/
+example [BI PROP] (P1 P2 Q : PROP) : □ (P1 ∨ P2) ∗ Q ⊢ Q := by
   iintro ⟨□(_HP1 | _HP2), HQ⟩
   <;> iexact HQ
 
-theorem multiple_spatial [BI PROP] (Q : PROP) : ⊢ <affine> P -∗ Q -∗ Q := by
+/-- Tests introducing multiple spatial hypotheses -/
+example [BI PROP] (P Q : PROP) : ⊢ <affine> P -∗ Q -∗ Q := by
   iintro _HP HQ
   iexact HQ
 
-theorem multiple_intuitionistic [BI PROP] (Q : PROP) : ⊢ □ P -∗ □ Q -∗ Q := by
+/-- Tests introducing multiple intuitionistic hypotheses -/
+example [BI PROP] (Q : PROP) : ⊢ □ P -∗ □ Q -∗ Q := by
   iintro □_HP □HQ
   iexact HQ
 
-theorem multiple_patterns [BI PROP] (Q : PROP) : ⊢ □ (P1 ∧ P2) -∗ Q ∨ Q -∗ Q := by
+/-- Tests introducing with complex nested patterns -/
+example [BI PROP] (Q : PROP) : ⊢ □ (P1 ∧ P2) -∗ Q ∨ Q -∗ Q := by
   iintro □⟨_HP1, ∗_HP2⟩ (HQ | HQ)
   <;> iexact HQ
 
@@ -118,36 +137,62 @@ end intro
 -- exists
 namespace «exists»
 
-theorem id [BI PROP] : ⊢ (∃ x, x : PROP) := by
+/-- Tests `iexists` with a BI proposition -/
+example [BI PROP] : ⊢@{PROP} ∃ x, x := by
   iexists iprop(True)
   ipure_intro
   exact True.intro
 
-theorem f [BI PROP] : ⊢ (∃ (_x : Nat), True ∨ False : PROP) := by
+/-- Tests `iexists` with a natural number -/
+example [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
+/-- Tests `iexists` with Prop -/
+example [BI PROP] : ⊢@{PROP} ⌜∃ x, x ∨ False⌝ := by
   iexists True
   ipure_intro
   exact Or.inl True.intro
 
+
+/-- Tests `iexists` with a named metavariable -/
+example [BI PROP] : ⊢@{PROP} ∃ x, ⌜x = 42⌝ := by
+  iexists ?y
+  ipure_intro
+  rfl
+
+/-- Tests `iexists` with anonymous metavariable -/
+example [BI PROP] : ⊢@{PROP} ∃ x, ⌜x = 42⌝ := by
+  iexists _
+  ipure_intro
+  rfl
+
+/-- Tests `iexists` with two quantifiers -/
+example [BI PROP] : ⊢@{PROP} ∃ x y : Nat, ⌜x = y⌝ := by
+  iexists _, 1
+  ipure_intro
+  rfl
+
+
 end «exists»
 
 -- exact
 namespace exact
 
-theorem exact [BI PROP] (Q : PROP) : Q ⊢ Q := by
+/-- Tests basic `iexact` -/
+example [BI PROP] (Q : PROP) : Q ⊢ Q := by
   iintro HQ
   iexact HQ
 
-theorem def_eq [BI PROP] (Q : PROP) : <affine> <pers> Q ⊢ □ Q := by
+/-- Tests `iexact` with affine pers to intuitionistic -/
+example [BI PROP] (Q : PROP) : <affine> <pers> Q ⊢ □ Q := by
   iintro HQ
   iexact HQ
 
-theorem intuitionistic [BI PROP] (Q : PROP) : □ Q ⊢ Q := by
+/-- Tests `iexact` with intuitionistic hypothesis -/
+example [BI PROP] (Q : PROP) : □ Q ⊢ Q := by
   iintro HQ
   iexact HQ
 
@@ -156,23 +201,28 @@ end exact
 -- assumption
 namespace assumption
 
-theorem exact [BI PROP] (Q : PROP) : Q ⊢ Q := by
+/-- Tests `iassumption` for exact match -/
+example [BI PROP] (Q : PROP) : Q ⊢ Q := by
   iintro _HQ
   iassumption
 
-theorem from_assumption [BI PROP] (Q : PROP) : <affine> <pers> Q ⊢ □ Q := by
+/-- Tests `iassumption` with affine pers to intuitionistic -/
+example [BI PROP] (Q : PROP) : <affine> <pers> Q ⊢ □ Q := by
   iintro _HQ
   iassumption
 
-theorem intuitionistic [BI PROP] (Q : PROP) : □ Q ⊢ Q := by
+/-- Tests `iassumption` with intuitionistic hypothesis -/
+example [BI PROP] (Q : PROP) : □ Q ⊢ Q := by
   iintro □_HQ
   iassumption
 
-theorem lean [BI PROP] (Q : PROP) (H : ⊢ Q) : <affine> P ⊢ Q := by
+/-- Tests `iassumption` using a Lean hypothesis -/
+example [BI PROP] (Q : PROP) (H : ⊢ Q) : <affine> P ⊢ Q := by
   iintro _HP
   iassumption
 
-theorem lean_pure [BI PROP] (Q : PROP) : <affine> ⌜⊢ Q⌝ ⊢ Q := by
+/-- Tests `iassumption` with Lean hypothesis first introduced -/
+example [BI PROP] (Q : PROP) : <affine> ⌜⊢ Q⌝ ⊢ Q := by
   iintro ⌜H⌝
   iassumption
 
@@ -181,208 +231,279 @@ end assumption
 -- apply
 namespace apply
 
-theorem exact [BI PROP] (Q : PROP) : Q ⊢ Q := by
+/-- Tests `iapply` with exact match -/
+example [BI PROP] (Q : PROP) : Q ⊢ Q := by
   iintro HQ
   iapply HQ
 
-theorem apply [BI PROP] (P Q : PROP) : ⊢ P -∗ (P -∗ Q) -∗ Q := by
+/-- Tests `iapply` with wand -/
+example [BI PROP] (P Q : PROP) : ⊢ P -∗ (P -∗ Q) -∗ Q := by
   iintro HP H
-  iapply H with HP
+  iapply H $$ HP
 
-theorem multiple [BI PROP] (P Q R : PROP) : ⊢ P -∗ Q -∗ (P -∗ Q -∗ R) -∗ R := by
+/-- Tests `iapply` with multiple hypotheses -/
+example [BI PROP] (P Q R : PROP) : ⊢ P -∗ Q -∗ (P -∗ Q -∗ R) -∗ R := by
   iintro HP HQ H
-  iapply H with HP, HQ
+  iapply H $$ HP, HQ
 
-theorem multiple' [BI PROP] (P Q R S : PROP) : ⊢ (P -∗ Q) -∗ P -∗ R -∗ (Q -∗ R -∗ S) -∗ S := by
+/-- Tests `iapply` with nested wand application -/
+example [BI PROP] (P Q R S : PROP) : ⊢ (P -∗ Q) -∗ P -∗ R -∗ (Q -∗ R -∗ S) -∗ S := by
   iintro HPQ HP HR H
-  iapply H with [HPQ, HP], HR
-  iapply HPQ with HP
+  iapply H $$ [HPQ, HP], HR
+  iapply HPQ $$ HP
 
-theorem exact_intuitionistic [BI PROP] (Q : PROP) : □ Q ⊢ Q := by
+/-- Tests `iapply` with intuitionistic exact -/
+example [BI PROP] (Q : PROP) : □ Q ⊢ Q := by
   iintro □HQ
   iapply HQ
 
-theorem apply_intuitionistic [BI PROP] (P Q : PROP) : ⊢ □ P -∗ (P -∗ Q) -∗ Q := by
+/-- Tests `iapply` with intuitionistic wand argument -/
+example [BI PROP] (P Q : PROP) : ⊢ □ P -∗ (P -∗ Q) -∗ Q := by
   iintro HP H
-  iapply H with HP
+  iapply H $$ HP
 
-theorem multiple_intuitionistic [BI PROP] (P Q R : PROP) : ⊢ □ P -∗ Q -∗ □ (P -∗ Q -∗ □ R) -∗ R := by
+/-- Tests `iapply` with multiple intuitionistic hypotheses and subgoals -/
+example [BI PROP] (P Q R : PROP) : ⊢ □ P -∗ Q -∗ □ (P -∗ Q -∗ □ R) -∗ R := by
   iintro □HP HQ □H
-  iapply H with [], [HQ] as Q
+  iapply H $$ [], [HQ] as Q
   case Q => iexact HQ
   iexact HP
 
-theorem later [BI PROP] (P Q : PROP) : ⊢ (▷ P -∗ Q) -∗ P -∗ Q := by
+/-- Tests `iapply` with later modality -/
+example [BI PROP] (P Q : PROP) : ⊢ (▷ P -∗ Q) -∗ P -∗ Q := by
   iintro H HP
-  iapply H with HP
+  iapply H $$ HP
 
-theorem test_affine [BI PROP] [BIAffine PROP] (P Q : PROP) : ⊢ (P → Q) -∗ <pers> P -∗ Q := by
+/-- Tests `iapply` with implication -/
+example [BI PROP] [BIAffine PROP] (P Q : PROP) : ⊢ (P → Q) -∗ <pers> P -∗ Q := by
   iintro H HP
-  iapply H with HP
+  iapply H $$ HP
 
-theorem later_affine [BI PROP] [BIAffine PROP] (P Q : PROP) : ⊢ (▷ P → Q) -∗ P -∗ Q := by
+/-- Tests `iapply` with later and implication -/
+example [BI PROP] [BIAffine PROP] (P Q : PROP) : ⊢ (▷ P → Q) -∗ P -∗ Q := by
   iintro H HP
-  iapply H with HP
+  iapply H $$ HP
 
-theorem exact_lean [BI PROP] (Q : PROP) (H : ⊢ Q) : ⊢ Q := by
+/-- Tests `iapply` with Lean hypothesis -/
+example [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
+/-- Tests `iapply` with lemma -/
+example [BI PROP] (Q : PROP) : Q ⊢ (emp ∗ Q) ∗ emp := by
+  iapply (wand_intro sep_emp.mpr)
+  iemp_intro
 
-theorem exact_lean'' [BI PROP] (Q : PROP) (H : 0 = 0 → ⊢ Q) : ⊢ Q := by
+/-- Tests `iapply` with pure sidecondition -/
+example [BI PROP] (Q : PROP) (H : 0 = 0 → ⊢ Q) : ⊢ Q := by
   iapply H
   rfl
 
-theorem exact_lean''' [BI PROP] : ⊢@{PROP} ⌜1 = 1⌝ := by
+/-- Tests `iapply` with lemma with sidecondition -/
+example [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
+/-- Tests `iapply` with entailment as Lean hypothesis -/
+example [BI PROP] (P Q : PROP) (H : P ⊢ Q) (HP : ⊢ P) : ⊢ Q := by
   iapply H
   iapply HP
 
-theorem apply_lean' [BI PROP] (P Q : PROP) (H : ⊢ P -∗ Q) (HP : ⊢ P) : ⊢ Q := by
-  iapply H with []
+/-- Tests `iapply` with wand entailment as Lean hypothesis -/
+example [BI PROP] (P Q : PROP) (H : ⊢ P -∗ Q) (HP : ⊢ P) : ⊢ Q := by
+  iapply H $$ []
   iapply HP
 
-theorem apply_lean'' [BI PROP] (P Q : PROP) (H1 : P ⊢ Q) (H2 : Q ⊢ R) : P ⊢ R := by
+/-- Tests `iapply` with constructed term -/
+example [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
-  iapply H1 with HP
+  . ipure_intro; trivial
+  iapply H1 $$ HP
 
-theorem multiple_lean [BI PROP] (P Q R : PROP) (H : P ⊢ Q -∗ R) (HP : ⊢ P) : ⊢ Q -∗ R := by
+/-- Tests `iapply` with Lean wand entailment and subgoal -/
+example [BI PROP] (P Q R : PROP) (H : P ⊢ Q -∗ R) (HP : ⊢ P) : ⊢ Q -∗ R := by
   iintro HQ
-  iapply H with [], HQ
+  iapply H $$ [], HQ
   iapply HP
 
-theorem multiple_lean' [BI PROP] (P Q R : PROP) (H : P ∗ Q ⊢ R) (HP : ⊢ P) : ⊢ Q -∗ R := by
+/-- Tests `iapply` with lemma and subgoal -/
+example [BI PROP] (P Q R : PROP) (H : P ∗ Q ⊢ R) (HP : ⊢ P) : ⊢ Q -∗ R := by
   iintro HQ
-  iapply (wand_intro H) with [], HQ
+  iapply (wand_intro H) $$ [], HQ
   iapply HP
 
-theorem exact_forall [BI PROP] (P : α → PROP) (a : α) (H : ⊢ ∀ x, P x) : ⊢ P a := by
+/-- Tests `iapply` with forall -/
+example [BI PROP] (P : α → PROP) (a : α) (H : ⊢ ∀ x, P x) : ⊢ P a := by
   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
+/-- Tests `iapply` with Lean forall -/
+example [BI PROP] (P : α → PROP) (a : α) (H : ∀ x, ⊢ P x) : ⊢ P a := by
   iapply H
 
-theorem apply_forall [BI PROP] (P Q : α → PROP) (a b : α) (H : ⊢ ∀ x, ∀ y, P x -∗ Q y) : P a ⊢ Q b := by
+/-- Tests `iapply` with forall specialization -/
+example [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, %b, HP
 
-theorem apply_forall' [BI PROP] (P Q : α → PROP) (a b : α) : (∀ x, ∀ y, P x -∗ Q y) ⊢ P a -∗ Q b := by
+/-- Tests `iapply` with forall specialization from hypothesis -/
+example [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
+  iapply H $$ %a, %b, HP
 
-/- TODO: enable this when tc seach can create mvars
-theorem apply_forall2 [BI PROP] (P Q : α → PROP) (a b : α) : (∀ x, ∀ y, P x -∗ Q y) ⊢ P a -∗ Q b := by
+/-- Tests `iapply` with tactic -/
+example [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
--/
+  iapply H $$ %by exact a, %b, [HP]
+  iapply 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
+/-- error: ispecialize: iprop(P a -∗ Q b) is not a lean premise -/
+#guard_msgs in
+example [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
+  iapply H $$ %a, %b, %_, 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
+/-- Tests `iapply` using unification for foralls -/
+example [BI PROP] (P Q : α → PROP) (a b : α) : (∀ x, ∀ y, P x -∗ Q y) ⊢ P a -∗ Q b := by
+  iintro H HP
+  iapply H $$ HP
+
+/-- Tests `iapply` using manually created metavariables -/
+example [BI PROP] (P Q : α → PROP) (a b : α) : (∀ x, ∀ y, P x -∗ Q y) ⊢ P a -∗ Q b := by
+  iintro H HP
+  iapply H $$ %?_, %?_, HP
+
+/-- Tests `iapply` using unification in two steps, instantiating metavars  -/
+example [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
+/-- Tests `iapply` with intuitionistic forall from Lean -/
+example [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, HP
 
-theorem apply_forall_intuitionistic' [BI PROP] (P Q : α → PROP) (a b : α) : (□ ∀ x, ∀ y, P x -∗ Q y) ⊢ P a -∗ Q b := by
+/-- Tests `iapply` with intuitionistic forall from hypothesis -/
+example [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
+  iapply H $$ %a, %b, HP
 
-theorem apply_two_wands [BI PROP] (P Q : Nat → PROP) :
+/-- Tests `iapply` with two wands and subgoals -/
+example [BI PROP] (P Q : Nat → PROP) :
   (P 1 -∗ P 2 -∗ Q 1) ⊢ □ P 1 -∗ P 2 -∗ Q 1 := by
   iintro H □HP1 HP2
   iapply H
   . iexact HP1
   . iexact HP2
 
+/-- Tests `iapply` selecting left conjunct -/
+example [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
+
+/-- Tests `iapply` selecting right conjunct -/
+example [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
+
+/-- Tests `iapply` selecting left conjunct (exact match) -/
+example [BI PROP] (P Q : Nat → PROP) :
+  (P 1 ∧ Q 1) ⊢ P 1 := by
+  iintro H
+  iapply H
+
+/-- Tests `iapply` selecting right conjunct (exact match) -/
+example [BI PROP] (P Q : Nat → PROP) :
+  (P 1 ∧ Q 1) ⊢ Q 1 := by
+  iintro H
+  iapply H
+
 end apply
 
 -- have
 namespace ihave
 
-theorem exact_lean [BI PROP] (Q : PROP) (H : ⊢ Q) : ⊢ Q := by
+/-- Tests `ihave` with Lean hypothesis -/
+example [BI PROP] (Q : PROP) (H : ⊢ Q) : ⊢ Q := by
   ihave HQ := H
   iexact HQ
 
-theorem exact_lean_forall [BI PROP] (Q : Nat → PROP) (H : ∀ x, ⊢ Q x) : ⊢ Q 1 := by
+/-- Tests `ihave` with forall specialization via case -/
+example [BI PROP] (Q : Nat → PROP) (H : ∀ x, ⊢ Q x) : ⊢ Q 1 := by
   ihave HQ := H
   case x => exact 1
   iapply HQ
 
-theorem exact_lean_forall2 [BI PROP] (Q : Nat → PROP) (H : ∀ x, ⊢ Q x) : ⊢ Q 1 := by
+/-- Tests `ihave` with forall specialization via named hole -/
+example [BI PROP] (Q : Nat → PROP) (H : ∀ x, ⊢ Q x) : ⊢ Q 1 := by
   ihave HQ := H ?res
   case res => exact 1
   iexact HQ
 
-theorem exact_lean_forall3 [BI PROP] (Q : Nat → Nat → PROP) (H : ∀ x y, ⊢ Q x y) : ⊢ Q 1 1 := by
+/-- Tests `ihave` with two named holes -/
+example [BI PROP] (Q : Nat → Nat → PROP) (H : ∀ x y, ⊢ Q x y) : ⊢ Q 1 1 := by
   ihave HQ := H ?res ?res
   case res => exact 1
   iexact HQ
 
-theorem exact_lean_tc [BI PROP] (Q : Nat → PROP) (H : ∀ (P : PROP) [Persistent P], ⊢ P) : ⊢ Q 1 := by
+/-- Tests `ihave` creating metavars -/
+example [BI PROP] (Q : Nat → PROP) (H : ∀ x, ⊢ Q x) : ⊢ Q 1 := by
+  ihave HQ := H
+  iexact HQ
+
+/-- Tests `ihave` with typeclass argument (failing search) -/
+example [BI PROP] (Q : Nat → PROP) (H : ∀ (P : PROP) [Persistent P], ⊢ P) : ⊢ Q 1 := by
   ihave HQ := H
   rotate_right 1; exact iprop(□ Q 1)
   . apply inferInstance
   iexact HQ
 
-theorem exact_lean_tc2 [BI PROP] (Q : Nat → PROP) (H : ∀ (P : PROP) [Persistent P], ⊢ P) : ⊢ Q 1 := by
+/-- Tests `ihave` with typeclass argument (successful search) -/
+example [BI PROP] (Q : Nat → PROP) (H : ∀ (P : PROP) [Persistent P], ⊢ P) : ⊢ Q 1 := by
   ihave HQ := H iprop(□ Q _)
   rotate_right 1; exact 1
   iexact HQ
 
-theorem exact_spatial [BI PROP] (Q : PROP) : Q ⊢ Q := by
+/-- Tests `ihave` from spatial hypothesis -/
+example [BI PROP] (Q : PROP) : Q ⊢ Q := by
   iintro H
   ihave HQ := H
   iexact HQ
 
-theorem apply_lean [BI PROP] (P Q : PROP) (H : P ⊢ Q) : ⊢ P -∗ Q := by
+/-- Tests `ihave` with Lean entailment -/
+example [BI PROP] (P Q : PROP) (H : P ⊢ Q) : ⊢ P -∗ Q := by
   ihave HPQ := H
   iexact HPQ
 
-theorem apply_forall [BI PROP] (P Q : α → PROP) (a b : α) (H : ⊢ ∀ x, ∀ y, P x -∗ Q y) : P a ⊢ Q b := by
+/-- Tests `ihave` with forall specialization from Lean -/
+example [BI PROP] (P Q : α → PROP) (a b : α) (H : ⊢ ∀ x, ∀ y, P x -∗ Q y) : P a ⊢ Q b := by
   iintro HP
-  ihave H' := H $! a, b
-  iapply H' with HP
+  ihave H' := H $$ %a, %b
+  iapply H' $$ HP
 
-theorem apply_forall_spatial [BI PROP] (P Q : α → PROP) (a b : α) : (∀ x, ∀ y, P x -∗ Q y) ⊢ P a -∗ Q b := by
+/-- Tests `ihave` with forall specialization from hypothesis -/
+example [BI PROP] (P Q : α → PROP) (a b : α) : (∀ x, ∀ y, P x -∗ Q y) ⊢ P a -∗ Q b := by
   iintro H HP
-  ihave H' := H $! a, b with HP
+  ihave H' := H $$ %a, %b, HP
   iexact H'
 
-theorem apply_forall_intuitionistic [BI PROP] (P Q : α → PROP) (a b : α) (H : ⊢ □ ∀ x, ∀ y, P x -∗ Q y) : P a ⊢ Q b := by
+/-- Tests `ihave` with intuitionistic forall specialization from Lean -/
+example [BI PROP] (P Q : α → PROP) (a b : α) (H : ⊢ □ ∀ x, ∀ y, P x -∗ Q y) : P a ⊢ Q b := by
   iintro HP
-  ihave H' := H $! a, b
-  iapply H' with HP
+  ihave H' := H $$ %a, %b
+  iapply H' $$ HP
 
-theorem apply_forall_intuitionistic_iris [BI PROP] (P Q : α → PROP) (a b : α) : (□ ∀ x, ∀ y, P x -∗ Q y) ⊢ P a -∗ Q b := by
+/-- Tests `ihave` with intuitionistic forall specialization and subgoal -/
+example [BI PROP] (P Q : α → PROP) (a b : α) : (□ ∀ x, ∀ y, P x -∗ Q y) ⊢ P a -∗ Q b := by
   iintro H HP
-  ihave H' := H $! a, b with [HP]
+  ihave H' := H $$ %a, %b, [HP]
   . iexact HP
   iexact H'
 
@@ -391,15 +512,18 @@ end ihave
 -- ex falso
 namespace exfalso
 
-theorem false_intro [BI PROP] (Q : PROP) : False ⊢ Q := by
+/-- Tests false elimination via empty pattern -/
+example [BI PROP] (Q : PROP) : False ⊢ Q := by
   iintro ⟨⟩
 
-theorem false [BI PROP] (P : PROP) : □ P ⊢ False -∗ Q := by
+/-- Tests `iexfalso` with false hypothesis -/
+example [BI PROP] (P : PROP) : □ P ⊢ False -∗ Q := by
   iintro _HP HF
   iexfalso
   iexact HF
 
-theorem pure [BI PROP] (P : PROP) (HF : False) : ⊢ P := by
+/-- Tests `iexfalso` with pure false from Lean -/
+example [BI PROP] (P : PROP) (HF : False) : ⊢ P := by
   istart
   iexfalso
   ipure_intro
@@ -410,13 +534,15 @@ end exfalso
 -- pure
 namespace pure
 
-theorem move [BI PROP] (Q : PROP) : <affine> ⌜φ⌝ ⊢ Q -∗ Q := by
+/-- Tests `ipure` to move pure hypothesis to Lean context -/
+example [BI PROP] (Q : PROP) : <affine> ⌜φ⌝ ⊢ Q -∗ Q := by
   iintro Hφ
   iintro HQ
   ipure Hφ
   iexact HQ
 
-theorem move_multiple [BI PROP] (Q : PROP) : <affine> ⌜φ1⌝ ⊢ <affine> ⌜φ2⌝ -∗ Q -∗ Q := by
+/-- Tests `ipure` with multiple pure hypotheses -/
+example [BI PROP] (Q : PROP) : <affine> ⌜φ1⌝ ⊢ <affine> ⌜φ2⌝ -∗ Q -∗ Q := by
   iintro Hφ1
   iintro Hφ2
   iintro HQ
@@ -424,7 +550,8 @@ theorem move_multiple [BI PROP] (Q : PROP) : <affine> ⌜φ1⌝ ⊢ <affine> ⌜
   ipure Hφ2
   iexact HQ
 
-theorem move_conjunction [BI PROP] (Q : PROP) : (⌜φ1⌝ ∧ <affine> ⌜φ2⌝) ⊢ Q -∗ Q := by
+/-- Tests `ipure` with conjunction containing pure -/
+example [BI PROP] (Q : PROP) : (⌜φ1⌝ ∧ <affine> ⌜φ2⌝) ⊢ Q -∗ Q := by
   iintro Hφ
   iintro HQ
   ipure Hφ
@@ -435,20 +562,23 @@ end pure
 -- intuitionistic
 namespace intuitionistic
 
-theorem move [BI PROP] (P : PROP) : □ P ⊢ Q -∗ Q := by
+/-- Tests `iintuitionistic` to move hypothesis to intuitionistic context -/
+example [BI PROP] (P : PROP) : □ P ⊢ Q -∗ Q := by
   iintro HP
   iintro HQ
   iintuitionistic HP
   iexact HQ
 
-theorem move_multiple [BI PROP] (P : PROP) : □ P ⊢ □ Q -∗ Q := by
+/-- Tests `iintuitionistic` with multiple hypotheses -/
+example [BI PROP] (P : PROP) : □ P ⊢ □ Q -∗ Q := by
   iintro HP
   iintro HQ
   iintuitionistic HP
   iintuitionistic HQ
   iexact HQ
 
-theorem move_twice [BI PROP] (P : PROP) : □ P ⊢ Q -∗ Q := by
+/-- Tests `iintuitionistic` applied twice to same hypothesis -/
+example [BI PROP] (P : PROP) : □ P ⊢ Q -∗ Q := by
   iintro HP
   iintro HQ
   iintuitionistic HP
@@ -460,20 +590,23 @@ end intuitionistic
 -- spatial
 namespace spatial
 
-theorem move [BI PROP] (P : PROP) : □ P ⊢ □ Q -∗ Q := by
+/-- Tests `ispatial` to move hypothesis to spatial context -/
+example [BI PROP] (P : PROP) : □ P ⊢ □ Q -∗ Q := by
   iintro □HP
   iintro □HQ
   ispatial HP
   iexact HQ
 
-theorem move_multiple [BI PROP] (P : PROP) : □ P ⊢ □ Q -∗ Q := by
+/-- Tests `ispatial` with multiple hypotheses -/
+example [BI PROP] (P : PROP) : □ P ⊢ □ Q -∗ Q := by
   iintro □HP
   iintro □HQ
   ispatial HP
   ispatial HQ
   iexact HQ
 
-theorem move_twice [BI PROP] (P : PROP) : □ P ⊢ □ Q -∗ Q := by
+/-- Tests `ispatial` applied twice to same hypothesis -/
+example [BI PROP] (P : PROP) : □ P ⊢ □ Q -∗ Q := by
   iintro □HP
   iintro □HQ
   ispatial HP
@@ -485,10 +618,12 @@ end spatial
 -- emp intro
 namespace empintro
 
-theorem simple [BI PROP] : ⊢ (emp : PROP) := by
+/-- Tests `iemp_intro` for proving emp -/
+example [BI PROP] : ⊢@{PROP} emp := by
   iemp_intro
 
-theorem affine_env [BI PROP] (P : PROP) : <affine> P ⊢ emp := by
+/-- Tests `iemp_intro` with affine environment -/
+example [BI PROP] (P : PROP) : <affine> P ⊢ emp := by
   iintro _HP
   iemp_intro
 
@@ -497,15 +632,18 @@ end empintro
 -- pure intro
 namespace pureintro
 
-theorem simple [BI PROP] : ⊢ (⌜True⌝ : PROP) := by
+/-- Tests `ipure_intro` for True -/
+example [BI PROP] : ⊢@{PROP} ⌜True⌝ := by
   ipure_intro
   exact True.intro
 
-theorem or [BI PROP] : ⊢ True ∨ (False : PROP) := by
+/-- Tests `ipure_intro` for disjunction -/
+example [BI PROP] : ⊢@{PROP} True ∨ False := by
   ipure_intro
   apply Or.inl True.intro
 
-theorem with_proof [BI PROP] (H : A → B) (P Q : PROP) : <affine> P ⊢ <pers> Q → ⌜A⌝ → ⌜B⌝ := by
+/-- Tests `ipure_intro` with context -/
+example [BI PROP] (H : A → B) (P Q : PROP) : <affine> P ⊢ <pers> Q → ⌜A⌝ → ⌜B⌝ := by
   iintro _HP □_HQ
   ipure_intro
   exact H
@@ -515,128 +653,178 @@ end pureintro
 -- specialize
 namespace specialize
 
-theorem wand_spatial [BI PROP] (Q : PROP) : P ⊢ (P -∗ Q) -∗ Q := by
+/-- Tests `ispecialize` with spatial wand -/
+example [BI PROP] (Q : PROP) : P ⊢ (P -∗ Q) -∗ Q := by
   iintro HP HPQ
-  ispecialize HPQ with HP
+  ispecialize HPQ $$ HP
   iexact HPQ
 
-theorem wand_spatial_subgoal [BI PROP] (Q : PROP) : P ⊢ (P -∗ Q) -∗ Q := by
+/-- Tests `ispecialize` with subgoal -/
+example [BI PROP] (Q : PROP) : P ⊢ (P -∗ Q) -∗ Q := by
   iintro HP HPQ
-  ispecialize HPQ with [HP]
+  ispecialize HPQ $$ [HP]
   . iexact HP
   iexact HPQ
 
-theorem wand_spatial_subgoal_named [BI PROP] (Q : PROP) : P ⊢ (P -∗ Q) -∗ Q := by
+/-- Tests `ispecialize` with named subgoal -/
+example [BI PROP] (Q : PROP) : P ⊢ (P -∗ Q) -∗ Q := by
   iintro HP HPQ
-  ispecialize HPQ with [HP] as G
+  ispecialize HPQ $$ [HP] as G
   case G => iexact HP
   iexact HPQ
 
-theorem wand_intuitionistic [BI PROP] (Q : PROP) : □ P ⊢ □ (P -∗ Q) -∗ □ Q := by
+/-- Tests `ispecialize` with intuitionistic wand -/
+example [BI PROP] (Q : PROP) : □ P ⊢ □ (P -∗ Q) -∗ □ Q := by
   iintro □HP □HPQ
-  ispecialize HPQ with HP
+  ispecialize HPQ $$ HP
   iexact HPQ
 
-theorem wand_intuitionistic_subgoal [BI PROP] (Q : PROP) : □ P ⊢ □ (P -∗ Q) -∗ Q := by
+/-- Tests `ispecialize` with intuitionistic wand and subgoal -/
+example [BI PROP] (Q : PROP) : □ P ⊢ □ (P -∗ Q) -∗ Q := by
   iintro □HP □HPQ
-  ispecialize HPQ with []
+  ispecialize HPQ $$ []
   . iexact HP
   iexact HPQ
 
-theorem wand_intuitionistic_required [BI PROP] (Q : PROP) : □ P ⊢ □ (□ P -∗ Q) -∗ □ Q := by
+/-- Tests `ispecialize` with intuitionistic wand requiring intuitionistic argument -/
+example [BI PROP] (Q : PROP) : □ P ⊢ □ (□ P -∗ Q) -∗ □ Q := by
   iintro □HP □HPQ
-  ispecialize HPQ with HP
+  ispecialize HPQ $$ HP
   iexact HPQ
 
-theorem wand_intuitionistic_spatial [BI PROP] (Q : PROP) : □ P ⊢ (P -∗ Q) -∗ Q := by
+/-- Tests `ispecialize` with intuitionistic premise and spatial wand -/
+example [BI PROP] (Q : PROP) : □ P ⊢ (P -∗ Q) -∗ Q := by
   iintro □HP HPQ
-  ispecialize HPQ with HP
+  ispecialize HPQ $$ HP
   iexact HPQ
 
-theorem wand_intuitionistic_required_spatial [BI PROP] (Q : PROP) : □ P ⊢ (□ P -∗ Q) -∗ Q := by
+/-- Tests `ispecialize` with intuitionistic premise required by spatial wand -/
+example [BI PROP] (Q : PROP) : □ P ⊢ (□ P -∗ Q) -∗ Q := by
   iintro □HP HPQ
-  ispecialize HPQ with HP
+  ispecialize HPQ $$ HP
   iexact HPQ
 
-theorem wand_spatial_intuitionistic [BI PROP] (Q : PROP) : P ⊢ □ (P -∗ Q) -∗ Q := by
+/-- Tests `ispecialize` with spatial premise and intuitionistic wand -/
+example [BI PROP] (Q : PROP) : P ⊢ □ (P -∗ Q) -∗ Q := by
   iintro HP □HPQ
-  ispecialize HPQ with HP
+  ispecialize HPQ $$ HP
   iexact HPQ
 
-theorem wand_spatial_multiple [BI PROP] (Q : PROP) : ⊢ P1 -∗ P2 -∗ (P1 -∗ P2 -∗ Q) -∗ Q := by
+/-- Tests `ispecialize` with multiple spatial arguments -/
+example [BI PROP] (Q : PROP) : ⊢ P1 -∗ P2 -∗ (P1 -∗ P2 -∗ Q) -∗ Q := by
   iintro HP1 HP2 HPQ
-  ispecialize HPQ with HP1, HP2
+  ispecialize HPQ $$ HP1, HP2
   iexact HPQ
 
-theorem wand_spatial_multiple_subgoal [BI PROP] (Q : PROP) : ⊢ P1 -∗ P2 -∗ (P1 -∗ P2 -∗ Q) -∗ Q := by
+/-- Tests `ispecialize` with multiple subgoals -/
+example [BI PROP] (Q : PROP) : ⊢ P1 -∗ P2 -∗ (P1 -∗ P2 -∗ Q) -∗ Q := by
   iintro HP1 HP2 HPQ
-  ispecialize HPQ with [HP1], [HP2]
+  ispecialize HPQ $$ [HP1], [HP2]
   . iexact HP1
   . iexact HP2
   iexact HPQ
 
-theorem wand_intuitionistic_multiple [BI PROP] (Q : PROP) :
+/-- Tests `ispecialize` with multiple intuitionistic arguments -/
+example [BI PROP] (Q : PROP) :
     ⊢ □ P1 -∗ □ P2 -∗ □ (P1 -∗ □ P2 -∗ Q) -∗ □ Q := by
   iintro □HP1 □HP2 □HPQ
-  ispecialize HPQ with HP1, HP2
+  ispecialize HPQ $$ HP1, HP2
   iexact HPQ
 
-theorem wand_multiple [BI PROP] (Q : PROP) :
+/-- Tests `ispecialize` with mixed spatial and intuitionistic arguments -/
+example [BI PROP] (Q : PROP) :
     ⊢ P1 -∗ □ P2 -∗ P3 -∗ □ (P1 -∗ P2 -∗ P3 -∗ Q) -∗ Q := by
   iintro HP1 □HP2 HP3 HPQ
-  ispecialize HPQ with HP1, HP2, HP3
+  ispecialize HPQ $$ HP1, HP2, HP3
   iexact HPQ
 
-theorem forall_spatial [BI PROP] (Q : Nat → PROP) : ⊢ (∀ x, Q x) -∗ Q (y + 1) := by
+/-- Tests `ispecialize` with forall in spatial context -/
+example [BI PROP] (Q : Nat → PROP) : ⊢ (∀ x, Q x) -∗ Q (y + 1) := by
   iintro HQ
-  ispecialize HQ $! (y + 1)
+  ispecialize HQ $$ %(y + 1)
   iexact HQ
 
-theorem forall_intuitionistic [BI PROP] (Q : Nat → PROP) : ⊢ □ (∀ x, Q x) -∗ □ Q y := by
+/-- Tests `ispecialize` with forall in intuitionistic context -/
+example [BI PROP] (Q : Nat → PROP) : ⊢ □ (∀ x, Q x) -∗ □ Q y := by
   iintro □HQ
-  ispecialize HQ $! y
+  ispecialize HQ $$ %y
   iexact HQ
 
-theorem forall_spatial_intuitionistic [BI PROP] (Q : Nat → PROP) : ⊢ (∀ x, □ Q x) -∗ □ Q y := by
+/-- Tests `ispecialize` with forall returning intuitionistic proposition -/
+example [BI PROP] (Q : Nat → PROP) : ⊢ (∀ x, □ Q x) -∗ □ Q y := by
   iintro HQ
-  ispecialize HQ $! y
+  ispecialize HQ $$ %y
   iexact HQ
 
-theorem forall_spatial_multiple [BI PROP] (Q : Nat → Nat → PROP) :
+/-- Tests `ispecialize` with multiple forall in spatial context -/
+example [BI PROP] (Q : Nat → Nat → PROP) :
     ⊢ (∀ x, ∀ y, Q x y) -∗ Q x y := by
   iintro HQ
-  ispecialize HQ $! x, y
+  ispecialize HQ $$ %x, %y
   iexact HQ
 
-theorem forall_intuitionistic_multiple [BI PROP] (Q : Nat → Nat → PROP) :
+/-- Tests `ispecialize` with multiple forall in intuitionistic context -/
+example [BI PROP] (Q : Nat → Nat → PROP) :
     ⊢ □ (∀ x, ∀ y, Q x y) -∗ □ Q x y := by
   iintro □HQ
-  ispecialize HQ $! x, y
+  ispecialize HQ $$ %x, %y
   iexact HQ
 
-theorem forall_multiple [BI PROP] (Q : Nat → Nat → PROP) : ⊢ (∀ x, □ (∀ y, Q x y)) -∗ □ Q x y := by
+/-- Tests `ispecialize` with nested forall and intuitionistic -/
+example [BI PROP] (Q : Nat → Nat → PROP) : ⊢ (∀ x, □ (∀ y, Q x y)) -∗ □ Q x y := by
   iintro HQ
-  ispecialize HQ $! x, y
+  ispecialize HQ $$ %x, %y
   iexact HQ
 
-theorem multiple [BI PROP] (Q : Nat → PROP) :
+/-- Tests `ispecialize` with mixed forall and wand specialization -/
+example [BI PROP] (Q : Nat → PROP) :
     ⊢ □ P1 -∗ P2 -∗ (□ P1 -∗ (∀ x, P2 -∗ Q x)) -∗ Q y := by
   iintro □HP1 HP2 HPQ
-  ispecialize HPQ with HP1
-  ispecialize HPQ $! y with HP2
+  ispecialize HPQ $$ HP1, %y, HP2
   iexact HPQ
 
+/-- Tests `ispecialize` with pure True wand using `.intro` -/
+example [BI PROP] (P : PROP) :
+    ⊢ (True -∗ P) -∗ P := by
+  iintro H
+  ispecialize H $$ %.intro
+  iexact H
+
+/-- Tests `ispecialize` with pure wand using tactic -/
+example [BI PROP] (P : PROP) :
+    ⊢ (True -∗ P) -∗ P := by
+  iintro H
+  ispecialize H $$ %(by grind)
+  iexact H
+
+/-- Tests `ispecialize` alternating pure and spatial arguments -/
+example [BI PROP] (P Q : PROP) :
+    ⊢ (∀ x, P -∗ ⌜x = 1⌝ -∗ Q) -∗ P -∗ Q := by
+  iintro H HP
+  ispecialize H $$ %_, HP, %rfl
+  iexact H
+
+/-- Tests `ispecialize` with pure subgoal -/
+example [BI PROP] (P Q : PROP) :
+    ⊢ (∀ x, P -∗ ⌜x = 1⌝ -∗ Q) -∗ P -∗ Q := by
+  iintro H HP
+  ispecialize H $$ %_, HP, %_
+  · rfl
+  iexact H
+
 end specialize
 
 -- split
 namespace split
 
-theorem and [BI PROP] (Q : PROP) : Q ⊢ Q ∧ Q := by
+/-- Tests `isplit` for conjunction -/
+example [BI PROP] (Q : PROP) : Q ⊢ Q ∧ Q := by
   iintro HQ
   isplit
   <;> iexact HQ
 
-theorem sep_left [BI PROP] [BIAffine PROP] (Q : PROP) : ⊢ P -∗ Q -∗ R -∗ P ∗ Q := by
+/-- Tests `isplitl` with explicit left hypotheses -/
+example [BI PROP] [BIAffine PROP] (Q : PROP) : ⊢ P -∗ Q -∗ R -∗ P ∗ Q := by
   iintro HP
   iintro HQ
   iintro _HR
@@ -644,7 +832,8 @@ theorem sep_left [BI PROP] [BIAffine PROP] (Q : PROP) : ⊢ P -∗ Q -∗ R -∗
   · iexact HP
   · iexact HQ
 
-theorem sep_right [BI PROP] [BIAffine PROP] (Q : PROP) : ⊢ P -∗ Q -∗ R -∗ P ∗ Q := by
+/-- Tests `isplitr` with explicit right hypotheses -/
+example [BI PROP] [BIAffine PROP] (Q : PROP) : ⊢ P -∗ Q -∗ R -∗ P ∗ Q := by
   iintro HP
   iintro HQ
   iintro _HR
@@ -652,7 +841,8 @@ theorem sep_right [BI PROP] [BIAffine PROP] (Q : PROP) : ⊢ P -∗ Q -∗ R -
   · iexact HP
   · iexact HQ
 
-theorem sep_left_all [BI PROP] [BIAffine PROP] (Q : PROP) : ⊢ P -∗ □ Q -∗ R -∗ P ∗ Q := by
+/-- Tests `isplitl` without argument -/
+example [BI PROP] [BIAffine PROP] (Q : PROP) : ⊢ P -∗ □ Q -∗ R -∗ P ∗ Q := by
   iintro HP
   iintro □HQ
   iintro _HR
@@ -660,7 +850,8 @@ theorem sep_left_all [BI PROP] [BIAffine PROP] (Q : PROP) : ⊢ P -∗ □ Q -
   · iexact HP
   · iexact HQ
 
-theorem sep_right_all [BI PROP] [BIAffine PROP] (Q : PROP) : ⊢ □ P -∗ Q -∗ R -∗ P ∗ Q := by
+/-- Tests `isplitr` without argument -/
+example [BI PROP] [BIAffine PROP] (Q : PROP) : ⊢ □ P -∗ Q -∗ R -∗ P ∗ Q := by
   iintro □HP
   iintro HQ
   iintro _HR
@@ -673,17 +864,20 @@ end split
 -- left / right
 namespace leftright
 
-theorem left [BI PROP] (P : PROP) : P ⊢ P ∨ Q := by
+/-- Tests `ileft` -/
+example [BI PROP] (P : PROP) : P ⊢ P ∨ Q := by
   iintro HP
   ileft
   iexact HP
 
-theorem right [BI PROP] (Q : PROP) : Q ⊢ P ∨ Q := by
+/-- Tests `iright` -/
+example [BI PROP] (Q : PROP) : Q ⊢ P ∨ Q := by
   iintro HQ
   iright
   iexact HQ
 
-theorem complex [BI PROP] (P Q : PROP) : ⊢ P -∗ Q -∗ P ∗ (R ∨ Q ∨ R) := by
+/-- Tests nested disjunction with left and right -/
+example [BI PROP] (P Q : PROP) : ⊢ P -∗ Q -∗ P ∗ (R ∨ Q ∨ R) := by
   iintro HP HQ
   isplitl [HP]
   · iassumption
@@ -696,177 +890,212 @@ end leftright
 -- cases
 namespace cases
 
-theorem rename [BI PROP] (P : PROP) : P ⊢ P := by
+/-- Tests `icases` for simple renaming -/
+example [BI PROP] (P : PROP) : P ⊢ P := by
   iintro HP
   icases HP with H
   iexact H
 
-theorem clear [BI PROP] (P Q : PROP) : ⊢ P -∗ <affine> Q -∗ P := by
+/-- Tests `icases` to clear hypothesis -/
+example [BI PROP] (P Q : PROP) : ⊢ P -∗ <affine> Q -∗ P := by
   iintro HP
   iintro HQ
   icases HQ with -
   iexact HP
 
-theorem and [BI PROP] (Q : PROP) : □ (P1 ∧ P2 ∧ Q) ⊢ Q := by
+/-- Tests `icases` with nested conjunction -/
+example [BI PROP] (Q : PROP) : □ (P1 ∧ P2 ∧ Q) ⊢ Q := by
   iintro □HP
   icases HP with ⟨_HP1, _HP2, HQ⟩
   iexact HQ
 
-theorem and_intuitionistic [BI PROP] (Q : PROP) : □ P ∧ Q ⊢ Q := by
+/-- Tests `icases` with intuitionistic conjunction -/
+example [BI PROP] (Q : PROP) : □ P ∧ Q ⊢ Q := by
   iintro HPQ
   icases HPQ with ⟨_HP, HQ⟩
   iexact HQ
 
-theorem and_persistent_left [BI PROP] (Q : PROP) : <pers> Q ∧ <affine> P ⊢ Q := by
+/-- Tests `icases` on conjunction with persistent left -/
+example [BI PROP] (Q : PROP) : <pers> Q ∧ <affine> P ⊢ Q := by
   iintro HQP
   icases HQP with ⟨□HQ, _HP⟩
   iexact HQ
 
-theorem and_persistent_right [BI PROP] (Q : PROP) : Q ∧ <pers> P ⊢ Q := by
+/-- Tests `icases` on conjunction with persistent right -/
+example [BI PROP] (Q : PROP) : Q ∧ <pers> P ⊢ Q := by
   iintro HQP
   icases HQP with ⟨HQ, _HP⟩
   iexact HQ
 
-theorem sep [BI PROP] [BIAffine PROP] (Q : PROP) : P1 ∗ P2 ∗ Q ⊢ Q := by
+/-- Tests `icases` with nested separating conjunction -/
+example [BI PROP] [BIAffine PROP] (Q : PROP) : P1 ∗ P2 ∗ Q ⊢ Q := by
   iintro HPQ
   icases HPQ with ⟨_HP1, _HP2, HQ⟩
   iexact HQ
 
-theorem disjunction [BI PROP] (Q : PROP) : Q ⊢ <affine> (P1 ∨ P2 ∨ P3) -∗ Q := by
+/-- Tests `icases` with nested disjunction -/
+example [BI PROP] (Q : PROP) : Q ⊢ <affine> (P1 ∨ P2 ∨ P3) -∗ Q := by
   iintro HQ
   iintro HP
   icases HP with (_HP1 | _HP2 | _HP3)
   <;> iexact HQ
 
-theorem conjunction_and_disjunction [BI PROP] [BIAffine PROP] (Q : PROP) :
+/-- 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
   iintro HP
   icases HP with ⟨_HP11 | _HP12 | _HP13, HP2, HP31 | HP32 | HP33, HQ⟩
   <;> iexact HQ
 
-theorem move_to_pure [BI PROP] (Q : PROP) : ⊢ <affine> ⌜⊢ Q⌝ -∗ Q := by
+/-- Tests `icases` moving pure to Lean context with ⌜⌝ -/
+example [BI PROP] (Q : PROP) : ⊢ <affine> ⌜⊢ Q⌝ -∗ Q := by
   iintro HQ
   icases HQ with ⌜HQ⌝
   istop
   exact HQ
 
-theorem move_to_pure_ascii [BI PROP] (Q : PROP) : ⊢ <affine> ⌜⊢ Q⌝ -∗ Q := by
+/-- Tests `icases` moving pure to Lean context with % -/
+example [BI PROP] (Q : PROP) : ⊢ <affine> ⌜⊢ Q⌝ -∗ Q := by
   iintro HQ
   icases HQ with %HQ
   istop
   exact HQ
 
-theorem move_to_intuitionistic [BI PROP] (Q : PROP) : ⊢ □ Q -∗ Q := by
+/-- Tests `icases` moving to intuitionistic with □ -/
+example [BI PROP] (Q : PROP) : ⊢ □ Q -∗ Q := by
   iintro HQ
   icases HQ with □HQ
   iexact HQ
 
-theorem move_to_intuitionistic_ascii [BI PROP] (Q : PROP) : ⊢ □ Q -∗ Q := by
+/-- Tests `icases` moving to intuitionistic with # -/
+example [BI PROP] (Q : PROP) : ⊢ □ Q -∗ Q := by
   iintro HQ
   icases HQ with #HQ
   iexact HQ
 
-theorem move_to_spatial [BI PROP] (Q : PROP) : ⊢ □ Q -∗ Q := by
+/-- Tests `icases` moving to spatial with ∗ -/
+example [BI PROP] (Q : PROP) : ⊢ □ Q -∗ Q := by
   iintro □HQ
   icases HQ with ∗HQ
   iexact HQ
 
-theorem move_to_spatial_ascii [BI PROP] (Q : PROP) : ⊢ □ Q -∗ Q := by
+/-- Tests `icases` moving to spatial with * -/
+example [BI PROP] (Q : PROP) : ⊢ □ Q -∗ Q := by
   iintro □HQ
   icases HQ with *HQ
   iexact HQ
 
-theorem move_to_pure_conjunction [BI PROP] (Q : PROP) : ⊢ <affine> ⌜φ⌝ ∗ Q -∗ Q := by
+/-- Tests `icases` with pure in conjunction -/
+example [BI PROP] (Q : PROP) : ⊢ <affine> ⌜φ⌝ ∗ Q -∗ Q := by
   iintro HφQ
   icases HφQ with ⟨⌜Hφ⌝, HQ⟩
   iexact HQ
 
-theorem move_to_pure_disjunction [BI PROP] (Q : PROP) :
+/-- Tests `icases` with pure in disjunction -/
+example [BI PROP] (Q : PROP) :
     ⊢ <affine> ⌜φ1⌝ ∨ <affine> ⌜φ2⌝ -∗ Q -∗ Q := by
   iintro Hφ
   iintro HQ
   icases Hφ with (⌜Hφ1⌝ | ⌜Hφ2⌝)
   <;> iexact HQ
 
-theorem move_to_intuitionistic_conjunction [BI PROP] (Q : PROP) : ⊢ □ P ∗ Q -∗ Q := by
+/-- Tests `icases` with intuitionistic in conjunction -/
+example [BI PROP] (Q : PROP) : ⊢ □ P ∗ Q -∗ Q := by
   iintro HPQ
   icases HPQ with ⟨□_HP, HQ⟩
   iexact HQ
 
-theorem move_to_intuitionistic_disjunction [BI PROP] (Q : PROP) : ⊢ □ Q ∨ Q -∗ Q := by
+/-- Tests `icases` with intuitionistic in disjunction -/
+example [BI PROP] (Q : PROP) : ⊢ □ Q ∨ Q -∗ Q := by
   iintro HQQ
   icases HQQ with (□HQ | HQ)
   <;> iexact HQ
 
-theorem move_to_spatial_conjunction [BI PROP] (Q : PROP) : ⊢ □ (P ∧ Q) -∗ Q := by
+/-- Tests `icases` moving to spatial inside intuitionistic conjunction -/
+example [BI PROP] (Q : PROP) : ⊢ □ (P ∧ Q) -∗ Q := by
   iintro □HPQ
   icases HPQ with ⟨_HP, ∗HQ⟩
   iexact HQ
 
-theorem move_to_spatial_disjunction [BI PROP] (Q : PROP) : ⊢ □ (Q ∨ Q) -∗ Q := by
+/-- Tests `icases` with or inside intuitionistic, moving one to spatial -/
+example [BI PROP] (Q : PROP) : ⊢ □ (Q ∨ Q) -∗ Q := by
   iintro □HPQ
   icases HPQ with (HQ | ∗HQ)
   <;> iexact HQ
 
-theorem move_to_intuitionistic_and_back_conjunction [BI PROP] (Q : PROP) : ⊢ □ (P ∧ Q) -∗ Q := by
+/-- Tests `icases` moving whole hypothesis to intuitionistic then destructing -/
+example [BI PROP] (Q : PROP) : ⊢ □ (P ∧ Q) -∗ Q := by
   iintro HPQ
   icases HPQ with □⟨_HP, ∗HQ⟩
   iexact HQ
 
-theorem move_to_intuitionistic_and_back_disjunction [BI PROP] (Q : PROP) : ⊢ □ (Q ∨ Q) -∗ Q := by
+/-- Tests `icases` with or, moving whole to intuitionistic -/
+example [BI PROP] (Q : PROP) : ⊢ □ (Q ∨ Q) -∗ Q := by
   iintro HPQ
   icases HPQ with □(HQ | ∗HQ)
   <;> iexact HQ
 
-theorem conjunction_clear [BI PROP] [BIAffine PROP] (Q : PROP) : Q ∗ P ⊢ Q := by
+/-- Tests `icases` clearing in conjunction -/
+example [BI PROP] [BIAffine PROP] (Q : PROP) : Q ∗ P ⊢ Q := by
   iintro HQP
   icases HQP with ⟨HQ, -⟩
   iexact HQ
 
-theorem disjunction_clear [BI PROP] [BIAffine PROP] (Q : PROP) : Q ⊢ P1 ∨ P2 -∗ Q := by
+/-- Tests `icases` clearing in disjunction -/
+example [BI PROP] [BIAffine PROP] (Q : PROP) : Q ⊢ P1 ∨ P2 -∗ Q := by
   iintro HQ
   iintro HP
   icases HP with (- | _HP2)
   <;> iexact HQ
 
-theorem and_destruct_spatial_right [BI PROP] (Q : PROP) : P ∧ Q ⊢ Q := by
+/-- Tests `icases` destructing conjunction left -/
+example [BI PROP] (Q : PROP) : P ∧ Q ⊢ Q := by
   iintro HPQ
   icases HPQ with ⟨-, HQ⟩
   iexact HQ
 
-theorem and_destruct_spatial_left [BI PROP] (Q : PROP) : Q ∧ P ⊢ Q := by
+/-- Tests `icases` destructing conjunction right -/
+example [BI PROP] (Q : PROP) : Q ∧ P ⊢ Q := by
   iintro HQP
   icases HQP with ⟨HQ, -⟩
   iexact HQ
 
-theorem and_clear_spatial_multiple [BI PROP] (Q : PROP) : P1 ∧ P2 ∧ Q ∧ P3 ⊢ Q := by
+/-- Tests `icases` destructing multiple conjunctions  -/
+example [BI PROP] (Q : PROP) : P1 ∧ P2 ∧ Q ∧ P3 ⊢ Q := by
   iintro HPQ
   icases HPQ with ⟨-, -, HQ, -⟩
   iexact HQ
 
-theorem and_destruct_intuitionistic_right [BI PROP] (Q : PROP) : □ (P ∧ Q) ⊢ Q := by
+/-- Tests `icases` destructing intuitionistic conjunction, clearing left -/
+example [BI PROP] (Q : PROP) : □ (P ∧ Q) ⊢ Q := by
   iintro □HPQ
   icases HPQ with ⟨-, HQ⟩
   iexact HQ
 
-theorem and_destruct_intuitionistic_left [BI PROP] (Q : PROP) : □ (Q ∧ P) ⊢ Q := by
+/-- Tests `icases` destructing intuitionistic conjunction, clearing right -/
+example [BI PROP] (Q : PROP) : □ (Q ∧ P) ⊢ Q := by
   iintro □HQP
   icases HQP with ⟨HQ, -⟩
   iexact HQ
 
-theorem and_clear_intuitionistic_multiple [BI PROP] (Q : PROP) : □ (P1 ∧ P2 ∧ Q ∧ P3) ⊢ Q := by
+/-- Tests `icases` destructing multiple intuitionistic conjunctions -/
+example [BI PROP] (Q : PROP) : □ (P1 ∧ P2 ∧ Q ∧ P3) ⊢ Q := by
   iintro □HPQ
   icases HPQ with ⟨-, -, HQ, -⟩
   iexact HQ
 
-theorem «exists» [BI PROP] (Q : Nat → PROP) : (∃ x, Q x) ⊢ ∃ x, Q x ∨ False := by
+/-- Tests `icases` with existential -/
+example [BI PROP] (Q : Nat → PROP) : (∃ x, Q x) ⊢ ∃ x, Q x ∨ False := by
   iintro ⟨x, H⟩
   iexists x
   ileft
   iexact H
 
-theorem exists_intuitionistic [BI PROP] (Q : Nat → PROP) : □ (∃ x, Q x) ⊢ ∃ x, □ Q x ∨ False := by
+/-- Tests `icases` with intuitionistic existential -/
+example [BI PROP] (Q : Nat → PROP) : □ (∃ x, Q x) ⊢ ∃ x, □ Q x ∨ False := by
   iintro ⟨x, □H⟩
   iexists x
   ileft
   iexact H
+
+end cases