diff --git a/src/Iris/BI/BIBase.lean b/src/Iris/BI/BIBase.lean
index 61d3bd3e..0ffdca1a 100644
--- a/src/Iris/BI/BIBase.lean
+++ b/src/Iris/BI/BIBase.lean
@@ -38,6 +38,8 @@ def «exists» [BIBase PROP] {α : Sort _} (P : α → PROP) : PROP := sExists f
 /-- Entailment on separation logic propositions. -/
 macro:25 P:term:29 " ⊢ " Q:term:25 : term => ``(BIBase.Entails iprop($P) iprop($Q))
 
+macro:25 P:term:29 " ⊢@{ " PROP:term "} " Q:term:25 : term => ``(BIBase.Entails (PROP:=$PROP) iprop($P) iprop($Q))
+
 delab_rule BIBase.Entails
   | `($_ $P $Q) => do ``($(← unpackIprop P) ⊢ $(← unpackIprop Q))
 
@@ -170,13 +172,17 @@ structure BiEntails [BIBase PROP] (P Q : PROP) where
   mp : P ⊢ Q
   mpr : Q ⊢ P
 
+def EmpValid [BIBase PROP] (P : PROP) : Prop := emp ⊢ P
+
 /-- Entailment on separation logic propositions with an empty context. -/
-macro:25 "⊢ " P:term:25 : term => ``(emp ⊢ $P)
+macro:25 "⊢ " P:term:25 : term => ``(EmpValid iprop($P))
+macro:25 "⊢@{ " PROP:term " } " P:term:25 : term =>
+  ``(EmpValid (PROP:=$PROP) iprop($P))
 /-- Bidirectional entailment on separation logic propositions. -/
 macro:25 P:term:29 " ⊣⊢ " Q:term:29 : term => ``(BiEntails iprop($P) iprop($Q))
 
-delab_rule BIBase.Entails
-  | `($_ iprop(emp) $P) => do ``(⊢ $(← unpackIprop P))
+delab_rule BIBase.EmpValid
+  | `($_ $P) => do ``(⊢ $(← unpackIprop P))
 
 delab_rule BIBase.BiEntails
   | `($_ $P $Q) => do ``($(← unpackIprop P) ⊣⊢ $(← unpackIprop Q))
@@ -285,4 +291,3 @@ macro_rules
 
 delab_rule except0
   | `($_ $P) => do ``(iprop(◇ $(← unpackIprop P)))
-
diff --git a/src/Iris/BI/Lib/BUpdPlain.lean b/src/Iris/BI/Lib/BUpdPlain.lean
index b68d7c94..b525eeb8 100644
--- a/src/Iris/BI/Lib/BUpdPlain.lean
+++ b/src/Iris/BI/Lib/BUpdPlain.lean
@@ -48,26 +48,22 @@ theorem BUpdPlain_mono {P Q : PROP} : (P ⊢ Q) → (BUpdPlain P ⊢ BUpdPlain Q
     iapply H
     apply H
   iintro ⟨Ha, H2⟩
-  ispecialize Ha HQR
-  iapply Ha
+  iapply Ha $! HQR
   iapply H1
   iexact H2
 
 theorem BUpdPlain_idemp {P : PROP} : BUpdPlain (BUpdPlain P) ⊢ BUpdPlain P := by
   unfold BUpdPlain
   iintro Hp R H
-  ispecialize Hp R as HpR
-  iapply HpR
+  iapply Hp $! R
   iintro Hp
-  ispecialize Hp R as HpR2
-  iapply HpR2
+  iapply Hp $! R
   iassumption
 
 theorem BUpdPlain_frame_r {P Q : PROP} : BUpdPlain P ∗ Q ⊢ (BUpdPlain iprop(P ∗ Q)) := by
   unfold BUpdPlain
   iintro ⟨Hp, Hq⟩ R H
-  ispecialize Hp R as HpR
-  iapply HpR
+  iapply Hp $! R
   iintro Hp
   iapply H
   isplitl [Hp]
@@ -77,8 +73,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
-  ispecialize H P as HP
-  iapply HP
+  iapply H $! P
   exact wand_rfl
 
 /- BiBUpdPlainly entails the alternative definition -/
diff --git a/src/Iris/Examples/Proofs.lean b/src/Iris/Examples/Proofs.lean
index 65fed511..e61cb97c 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Φ
-  ispecialize HRΦ HR as HΦ
+  ihave HΦ := HRΦ with HR
   icases HΦ with ⟨x, _HΦ⟩
   iexists x
   isplitr
diff --git a/src/Iris/ProofMode/Expr.lean b/src/Iris/ProofMode/Expr.lean
index db4d1351..2f5d7cb7 100644
--- a/src/Iris/ProofMode/Expr.lean
+++ b/src/Iris/ProofMode/Expr.lean
@@ -22,12 +22,17 @@ def parseName? : Expr → Option (Name × Name × Expr)
 def mkNameAnnotation (name uniq : Name) (e : Expr) : Expr :=
   .mdata ⟨[(nameAnnotation, .ofName name), (uniqAnnotation, .ofName uniq)]⟩ e
 
+def getFreshName : TSyntax ``binderIdent → CoreM (Name × Syntax)
+  | `(binderIdent| $name:ident) => pure (name.getId, name)
+  | stx => return (← mkFreshUserName `x, stx)
+
 inductive Hyps {prop : Q(Type u)} (bi : Q(BI $prop)) : (e : Q($prop)) → Type where
   | emp (_ : $e =Q emp) : Hyps bi e
   | sep (tm elhs erhs : Q($prop)) (_ : $e =Q iprop($elhs ∗ $erhs))
         (lhs : Hyps bi elhs) (rhs : Hyps bi erhs) : Hyps bi e
   | hyp (tm : Q($prop)) (name uniq : Name) (p : Q(Bool)) (ty : Q($prop))
         (_ : $e =Q iprop(□?$p $ty)) : Hyps bi e
+deriving Repr
 
 instance : Inhabited (Hyps bi s) := ⟨.emp ⟨⟩⟩
 
@@ -56,6 +61,13 @@ def Hyps.mkHyp {prop : Q(Type u)} (bi : Q(BI $prop))
     (name uniq : Name) (p : Q(Bool)) (ty : Q($prop)) (e := q(iprop(□?$p $ty))) : Hyps bi e :=
   .hyp (mkIntuitionisticIf bi p (mkNameAnnotation name uniq ty)) name uniq p ty ⟨⟩
 
+-- TODO: should this ensure that adding a hypothesis to emp creates a
+-- hyp node instead of a sep node?
+def Hyps.add {prop : Q(Type u)} (bi : Q(BI $prop))
+    (name uniq : Name) (p : Q(Bool)) (ty : Q($prop)) {e} (h : Hyps bi e)
+    : Hyps bi q(iprop($e ∗ □?$p $ty)) :=
+  Hyps.mkSep h (.mkHyp bi name uniq p ty)
+
 partial def parseHyps? {prop : Q(Type u)} (bi : Q(BI $prop)) (expr : Expr) :
     Option ((s : Q($prop)) × Hyps bi s) := do
   if let some #[_, _, P, Q] := appM? expr ``sep then
@@ -107,6 +119,9 @@ def IrisGoal.strip : IrisGoal → Expr
 to have type `A : PROP` even though `PROP` is not a type. -/
 def HypMarker {PROP : Type _} (_A : PROP) : Prop := True
 
+/-- addLocalVarInfo associates the syntax `stx` (usually representing a hypothesis) with its type.
+This allows one to hover over the syntax and see the type. isBinder marks the place where the
+ hypothesis is introduced, e.g. for jump to definition. -/
 def addLocalVarInfo (stx : Syntax) (lctx : LocalContext)
     (expr : Expr) (expectedType? : Option Expr) (isBinder := false) : MetaM Unit := do
   Elab.withInfoContext' (pure ())
@@ -121,7 +136,18 @@ def addHypInfo (stx : Syntax) (name uniq : Name) (prop : Q(Type u)) (ty : Q($pro
   let ty := q(HypMarker $ty)
   addLocalVarInfo stx (lctx.mkLocalDecl ⟨uniq⟩ name ty) (.fvar ⟨uniq⟩) ty isBinder
 
+/-- Hyps.findWithInfo should be used on names obtained from the syntax of a tactic to highlight them correctly. -/
 def Hyps.findWithInfo {u prop bi} (hyps : @Hyps u prop bi s) (name : Ident) : MetaM Name := do
   let some (uniq, _, ty) := hyps.find? name.getId | throwError "unknown hypothesis"
   addHypInfo name name.getId uniq prop ty
   pure uniq
+
+/-- Hyps.addWithInfo should be used by tactics that introduce a hypothesis based on the name given by the user. -/
+def Hyps.addWithInfo {prop : Q(Type u)} (bi : Q(BI $prop))
+    (name : TSyntax ``binderIdent) (p : Q(Bool)) (ty : Q($prop)) {e} (h : Hyps bi e)
+    : MetaM (Name × Hyps bi q(iprop($e ∗ □?$p $ty))) := do
+  let uniq' ← mkFreshId
+  let (nameTo, nameRef) ← getFreshName name
+  addHypInfo nameRef nameTo uniq' prop ty (isBinder := true)
+  let hyps := Hyps.add bi nameTo uniq' p ty h
+  return ⟨uniq', hyps⟩
diff --git a/src/Iris/ProofMode/Patterns/SpecPattern.lean b/src/Iris/ProofMode/Patterns/SpecPattern.lean
index 27de2c17..c118734b 100644
--- a/src/Iris/ProofMode/Patterns/SpecPattern.lean
+++ b/src/Iris/ProofMode/Patterns/SpecPattern.lean
@@ -8,12 +8,13 @@ open Lean
 
 declare_syntax_cat specPat
 
-syntax binderIdent : specPat
-syntax "[" binderIdent,* "]" optional(" as " ident) : specPat
+syntax ident : 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 : TSyntax ``binderIdent)
-  | idents (names : List (TSyntax ``binderIdent)) (goalName : Name)
+  | ident (name : Ident)
+  | goal (names : List Ident) (goalName : Name)
   deriving Repr, Inhabited
 
 partial def SpecPat.parse (pat : Syntax) : MacroM SpecPat := do
@@ -22,15 +23,15 @@ partial def SpecPat.parse (pat : Syntax) : MacroM SpecPat := do
   | some pat => return pat
 where
   go : TSyntax `specPat → Option SpecPat
-  | `(specPat| $name:binderIdent) => some <| .ident name
-  | `(specPat| [$[$names:binderIdent],*]) => some <| .idents names.toList .anonymous
-  | `(specPat| [$[$names:binderIdent],*] as $goal:ident) => match goal.raw with
-    | .ident _ _ val _ => some <| .idents names.toList val
+  | `(specPat| $name:ident) => some <| .ident name
+  | `(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 <| .idents _ name => name
+    | some <| .goal _ name => name
     | _ => .anonymous
diff --git a/src/Iris/ProofMode/Tactics.lean b/src/Iris/ProofMode/Tactics.lean
index 24a34423..f02be568 100644
--- a/src/Iris/ProofMode/Tactics.lean
+++ b/src/Iris/ProofMode/Tactics.lean
@@ -7,10 +7,10 @@ import Iris.ProofMode.Tactics.Clear
 import Iris.ProofMode.Tactics.Exact
 import Iris.ProofMode.Tactics.ExFalso
 import Iris.ProofMode.Tactics.Exists
+import Iris.ProofMode.Tactics.Have
 import Iris.ProofMode.Tactics.Intro
 import Iris.ProofMode.Tactics.LeftRight
 import Iris.ProofMode.Tactics.Move
-import Iris.ProofMode.Tactics.Pose
 import Iris.ProofMode.Tactics.Pure
 import Iris.ProofMode.Tactics.Remove
 import Iris.ProofMode.Tactics.Rename
diff --git a/src/Iris/ProofMode/Tactics/Apply.lean b/src/Iris/ProofMode/Tactics/Apply.lean
index 4bd97714..9f4c2186 100644
--- a/src/Iris/ProofMode/Tactics/Apply.lean
+++ b/src/Iris/ProofMode/Tactics/Apply.lean
@@ -1,126 +1,44 @@
 /-
 Copyright (c) 2025 Oliver Soeser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Oliver Soeser
+Authors: Oliver Soeser, Michael Sammler
 -/
 import Iris.ProofMode.Patterns.ProofModeTerm
 import Iris.ProofMode.Tactics.Split
-import Iris.ProofMode.Tactics.Pose
+import Iris.ProofMode.Tactics.Have
 
 namespace Iris.ProofMode
 open Lean Elab Tactic Meta Qq BI Std
 
-theorem apply [BI PROP] {P Q1 Q2 R : PROP}
-    (h : P ⊢ Q1) [inst : IntoWand false false R Q1 Q2] : P ∗ R ⊢ Q2 :=
-  (sep_mono h inst.1).trans wand_elim_r
+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 :=
+      h1.1.trans (Entails.trans (sep_mono_l h2) (wand_elim' h3.1))
 
-theorem rec_apply [BI PROP] {P Q P' Q' Q1 Q2 R : PROP}
-    (h1 : P ⊣⊢ P' ∗ Q') (h2 : Q' ⊢ Q1) (h3 : P' ∗ Q2 ⊢ R)
-    [IntoWand false false Q Q1 Q2] : P ∗ Q ⊢ R :=
-  (sep_congr h1 .rfl).mp.trans <| sep_assoc.mp.trans <| (sep_mono_r <| apply h2).trans h3
+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
+     let pf' ← gs.addGoal hyps' A
+     return q(tac_apply $pf $pf')
 
-theorem apply_lean [BI PROP] {P Q R : PROP} (h1 : ⊢ Q) (h2 : P ∗ Q ⊢ R) : P ⊢ R :=
-  sep_emp.mpr.trans <| (sep_mono_r h1).trans h2
-
-variable {prop : Q(Type u)} {bi : Q(BI $prop)} in
-def specPatGoal
-    (A1 : Q($prop)) (hyps : Hyps bi e) (spats : List SpecPat)
-    (addGoal : ∀ {e}, Name → Hyps bi e → (goal : Q($prop)) → MetaM Q($e ⊢ $goal)) :
-    MetaM Q($e ⊢ $A1) := do
-  return ← if let (some <| .ident _, some inst) := (spats.head?,
-      ← try? (synthInstanceQ q(FromAssumption false $e $A1))) then
-    pure q(($inst).from_assumption)
-  else
-    addGoal (headName spats) hyps A1
-
-variable {prop : Q(Type u)} {bi : Q(BI $prop)} in
-def processSpecPats
-    (A1 : Q($prop)) (hypsl : Hyps bi el) (spats : List SpecPat)
-    (addGoal : ∀ {e}, Name → Hyps bi e → (goal : Q($prop)) → MetaM Q($e ⊢ $goal)) :
-    MetaM ((el' er' : Q($prop)) × Q($er' ⊢ $A1) × Hyps bi el' × Q($el ⊣⊢ $el' ∗ $er')) := do
-  let splitPat := fun name _ => match spats.head? with
-    | some <| .ident bIdent => binderIdentHasName name bIdent
-    | some <| .idents bIdents _ => bIdents.any <| binderIdentHasName name
-    | _ => false
-
-  let ⟨el', er', hypsl', hypsr', h'⟩ := Hyps.split bi splitPat hypsl
-  let m ← specPatGoal A1 hypsr' spats addGoal
-  return ⟨el', er', m, hypsl', h'⟩
-
-variable {prop : Q(Type u)} {bi : Q(BI $prop)} in
-partial def iApplyCore
-    (goal el er : Q($prop)) (hypsl : Hyps bi el) (spats : List SpecPat)
-    (addGoal : ∀ {e}, Name → Hyps bi e → (goal : Q($prop)) → MetaM Q($e ⊢ $goal)) :
-    MetaM (Q($el ∗ $er ⊢ $goal)) := do
-  let A1 ← mkFreshExprMVarQ q($prop)
-  let A2 ← mkFreshExprMVarQ q($prop)
-
-  let _ ← isDefEq er goal
-  if let (some _, some _) := (← try? <| synthInstanceQ q(FromAssumption false $er $goal),
-                              ← try? <| synthInstanceQ q(TCOr (Affine $el) (Absorbing $goal))) then
-    -- iexact case
-    return q(assumption (p := false) .rfl)
-  else if let some _ ← try? <| synthInstanceQ q(IntoWand false false $er $A1 $goal) then
-    -- iapply base case
-    let m ← specPatGoal A1 hypsl spats addGoal
-    return q(apply $m)
-  else if let some _ ← try? <| synthInstanceQ q(IntoWand false false $er $A1 $A2) then
-    -- iapply recursive case
-    let ⟨el', _, m, hypsl', h'⟩ ← processSpecPats A1 hypsl spats addGoal
-    let res : Q($el' ∗ $A2 ⊢ $goal) ← iApplyCore goal el' A2 hypsl' spats.tail addGoal
-    return q(rec_apply $h' $m $res)
-  else
-    throwError "iapply: cannot apply {er} to {goal}"
-
-theorem apply_forall [BI PROP] (x : α) (P : α → PROP) {Q : PROP}
-    [H1 : IntoForall Q P] (H2 : E ⊢ E' ∗ Q) : E ⊢ E' ∗ P x :=
-  Entails.trans H2 <| sep_mono_r <| H1.into_forall.trans <| forall_elim x
-
-partial def instantiateForalls' {prop : Q(Type u)} (e e' : Q($prop)) (bi : Q(BI $prop))
-    (out : Q($prop)) (pf : Q($e ⊢ $e' ∗ $out)) (terms : List Term) :
-    TacticM (Expr × Expr) := do
-  if let some t := terms.head? then
-    let texpr ← mkAppM' (← elabTerm t none) #[]
-    let ⟨_, ttype, texpr⟩ ← inferTypeQ texpr
-    let Φ ← mkFreshExprMVarQ q($ttype → $prop)
-    let _ ← synthInstanceQ q(IntoForall $out $Φ)
-    let res ← mkAppM' Φ #[texpr]
-    let pf' ← mkAppM ``apply_forall #[texpr, Φ, pf]
-    return ← instantiateForalls' e e' bi res pf' terms.tail
-  else
-    return ⟨out, pf⟩
+  let some ⟨_, hyps'', pf''⟩ ← try? <| iSpecializeCore gs hyps uniq [] [.goal [] .anonymous] | throwError m!"iapply: cannot apply {out} to {goal}"
+  let pf''' ← iApplyCore gs hyps'' goal uniq
+  return q($(pf'').trans $pf''')
 
 elab "iapply" colGt pmt:pmTerm : tactic => do
   let pmt ← liftMacroM <| PMTerm.parse pmt
-  let mvar ← getMainGoal
-
+  let (mvar, { bi, hyps, goal, .. }) ← istart (← getMainGoal)
   mvar.withContext do
-    let g ← instantiateMVars <| ← mvar.getType
-    let some { u, prop, e, bi, hyps, goal, .. } := parseIrisGoal? g | throwError "not in proof mode"
-    if let some uniq ← try? do pure (← hyps.findWithInfo ⟨pmt.term⟩) then
-      -- lemma from iris context
-      let ⟨e', hyps', out, _, _, _, pf⟩ := hyps.remove false uniq
-
-      let ⟨out, pf⟩ := ← instantiateForalls' e e' bi out q(($pf).mp) pmt.terms
-
-      let goals ← IO.mkRef #[]
-      let res ← iApplyCore goal e' out hyps' pmt.spats <| goalTracker goals
-      mvar.assign <| ← mkAppM ``Entails.trans #[pf, res]
-      replaceMainGoal (← goals.get).toList
-    else
-      -- lemma from lean context
-      let A1 ← mkFreshExprMVarQ q($prop)
-      let A2 ← mkFreshExprMVarQ q($prop)
-
-      let expected : Q(Prop) := if let some _ := ← try? <|
-        synthInstanceQ q(IntoWand false false $goal $A1 $A2)
-        then q($e ⊢ $A1 -∗ $A2) else q($e ⊢ $goal)
-
-      let expr ← mkAppM' (← elabTerm pmt.term (some expected)) #[]
-
-      let goals ← IO.mkRef #[]
-      let ⟨hyp, pf⟩ ← iPoseCore bi expr pmt.terms goals
-
-      let res ← iApplyCore goal e hyp hyps pmt.spats <| goalTracker goals
-      mvar.assign <| ← mkAppM ``apply_lean #[pf, res]
-      replaceMainGoal (← goals.get).toList
+  let gs ← Goals.new bi
+  let ⟨uniq, _, hyps, pf⟩ ← iHave gs hyps pmt (← `(binderIdent|_)) 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)
diff --git a/src/Iris/ProofMode/Tactics/Assumption.lean b/src/Iris/ProofMode/Tactics/Assumption.lean
index 6a1cbdf3..4d5953b3 100644
--- a/src/Iris/ProofMode/Tactics/Assumption.lean
+++ b/src/Iris/ProofMode/Tactics/Assumption.lean
@@ -20,8 +20,7 @@ def assumptionLean {prop : Q(Type u)} (_bi : Q(BI $prop)) (ehyps goal : Q($prop)
   mvar.withContext do
     let _ ← synthInstanceQ q(TCOr (Affine $ehyps) (Absorbing $goal))
     for h in ← getLCtx do
-      let some #[_, _, hh, (P : Q($prop))] := (← whnfR h.type).appM? ``Entails | continue
-      unless (← whnfR hh).isAppOfArity ``BI.emp 2 do continue
+      let some #[_, _, (P : Q($prop))] := (← whnfR h.type).appM? ``BIBase.EmpValid | continue
       have h : Q(⊢ $P) := .fvar h.fvarId
       -- let (name, type) := (h.userName, ← instantiateMVars h.type)
 
diff --git a/src/Iris/ProofMode/Tactics/Basic.lean b/src/Iris/ProofMode/Tactics/Basic.lean
index 5f060d58..bccbff3a 100644
--- a/src/Iris/ProofMode/Tactics/Basic.lean
+++ b/src/Iris/ProofMode/Tactics/Basic.lean
@@ -49,10 +49,6 @@ theorem assumption [BI PROP] {p : Bool} {P P' A Q : PROP} [inst : FromAssumption
   [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 getFreshName : TSyntax ``binderIdent → CoreM (Name × Syntax)
-  | `(binderIdent| $name:ident) => pure (name.getId, name)
-  | stx => return (← mkFreshUserName `x, stx)
-
 def binderIdentHasName (name : Name) (id : TSyntax ``binderIdent) : Bool :=
   match id with
   | `(binderIdent| $name':ident) => name'.getId == name
@@ -65,11 +61,31 @@ def selectHyp (ty : Expr) : ∀ {s}, @Hyps u prop bi s → MetaM (Name × Q(Bool
     pure (uniq, p, ty')
   | _, .sep _ _ _ _ lhs rhs => try selectHyp ty rhs catch _ => selectHyp ty lhs
 
-variable {prop : Q(Type u)} {bi : Q(BI $prop)} in
-def goalTracker {P} (goals : IO.Ref (Array MVarId)) (name : Name) (hyps : Hyps bi P)
-    (goal : Q($prop)) : MetaM Q($P ⊢ $goal) := do
-  let m : Q($P ⊢ $goal) ← mkFreshExprSyntheticOpaqueMVar <|
+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
-  goals.modify (·.push m.mvarId!)
+  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/Cases.lean b/src/Iris/ProofMode/Tactics/Cases.lean
index 2f4ad0f8..c146cfa7 100644
--- a/src/Iris/ProofMode/Tactics/Cases.lean
+++ b/src/Iris/ProofMode/Tactics/Cases.lean
@@ -207,6 +207,7 @@ partial def iCasesCore
     (pat : iCasesPat) (k : ∀ {P}, Hyps bi P → MetaM Q($P ⊢ $Q)) : MetaM (Q($P ∗ $A ⊢ $Q)) :=
   match pat with
   | .one name => do
+    -- TODO: use Hyps.addWithInfo here?
     let (name, ref) ← getFreshName name
     let uniq ← mkFreshId
     addHypInfo ref name uniq prop A' (isBinder := true)
@@ -285,8 +286,8 @@ elab "icases" colGt hyp:ident "with" colGt pat:icasesPat : tactic => do
   let ⟨_, hyps', A, A', b, h, pf⟩ := hyps.remove true uniq
 
   -- process pattern
-  let goals ← IO.mkRef #[]
-  let pf2 ← iCasesCore bi hyps' goal b A A' h pat (λ hyps => goalTracker goals .anonymous hyps goal)
+  let gs ← Goals.new bi
+  let pf2 ← iCasesCore bi hyps' goal b A A' h pat (λ hyps => gs.addGoal hyps goal)
 
   mvar.assign q(($pf).1.trans $pf2)
-  replaceMainGoal (← goals.get).toList
+  replaceMainGoal (← gs.getGoals)
diff --git a/src/Iris/ProofMode/Tactics/Have.lean b/src/Iris/ProofMode/Tactics/Have.lean
new file mode 100644
index 00000000..2802ab74
--- /dev/null
+++ b/src/Iris/ProofMode/Tactics/Have.lean
@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2025 Michael Sammler. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michael Sammler
+-/
+import Iris.ProofMode.Patterns.ProofModeTerm
+import Iris.ProofMode.Tactics.Basic
+import Iris.ProofMode.Tactics.Specialize
+
+namespace Iris.ProofMode
+open Lean Elab Tactic Meta Qq BI Std
+
+theorem have_as_emp_valid [BI PROP] {φ} {P Q : PROP}
+    [h1 : AsEmpValid2 φ P] (h : φ) : Q ⊢ Q ∗ P :=
+  sep_emp.2.trans (sep_mono_r (h1.1.mp h))
+
+
+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
+  if let some uniq ← try? <| hyps.findWithInfo ⟨tm⟩ then
+    -- assertion from the Iris context
+    let ⟨_, hyps, _, out', p, _, pf⟩ := hyps.remove (!keep) uniq
+    let ⟨uniq', hyps⟩ ← Hyps.addWithInfo bi name p out' hyps
+    return ⟨uniq', _, hyps, q($pf.1)⟩
+  else
+    -- lean hypothesis
+    let val ← instantiateMVars <| ← elabTerm tm none false
+    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 ·)
+    for mvar in newMVarIds ++ otherMVarIds do
+      gs.addPureGoal mvar
+
+    -- TODO: can we do this without re typechecking?
+    let ⟨0, ty, val⟩ ← inferTypeQ val | throwError m!"{val} is not a Prop"
+
+    let hyp ← mkFreshExprMVarQ q($prop)
+    let some _ ← try? <| synthInstanceQ q(AsEmpValid2 $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
+  return ⟨uniq, _, hyps'', q($(pf).trans $pf')⟩
+
+elab "ihave" colGt name:binderIdent " := " pmt:pmTerm  : tactic => do
+  let pmt ← liftMacroM <| PMTerm.parse pmt
+  let (mvar, { bi, hyps, goal, .. }) ← istart (← getMainGoal)
+  mvar.withContext do
+  let gs ← Goals.new bi
+  let ⟨_, _, hyps, pf⟩ ← iHave gs hyps pmt name true
+  let pf' ← gs.addGoal hyps goal
+  mvar.assign q(($pf).trans $pf')
+  replaceMainGoal (← gs.getGoals)
diff --git a/src/Iris/ProofMode/Tactics/Intro.lean b/src/Iris/ProofMode/Tactics/Intro.lean
index a7394d24..92b82de7 100644
--- a/src/Iris/ProofMode/Tactics/Intro.lean
+++ b/src/Iris/ProofMode/Tactics/Intro.lean
@@ -106,8 +106,8 @@ elab "iintro" pats:(colGt icasesPat)* : tactic => do
   mvar.withContext do
 
   -- process patterns
-  let goals ← IO.mkRef #[]
-  let pf ← iIntroCore bi hyps goal pats.toList <| goalTracker goals .anonymous
+  let gs ← Goals.new bi
+  let pf ← iIntroCore bi hyps goal pats.toList <| gs.addGoal
 
   mvar.assign pf
-  replaceMainGoal (← goals.get).toList
+  replaceMainGoal (← gs.getGoals)
diff --git a/src/Iris/ProofMode/Tactics/Pose.lean b/src/Iris/ProofMode/Tactics/Pose.lean
deleted file mode 100644
index 1e155c5d..00000000
--- a/src/Iris/ProofMode/Tactics/Pose.lean
+++ /dev/null
@@ -1,70 +0,0 @@
-/-
-Copyright (c) 2025 Oliver Soeser. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Oliver Soeser
--/
-import Iris.ProofMode.Patterns.ProofModeTerm
-import Iris.ProofMode.Tactics.Cases
-import Iris.Std
-
-namespace Iris.ProofMode
-open Lean Elab Tactic Meta Qq BI Std
-
-theorem pose [BI PROP] {P Q R : PROP}
-    (H1 : P ∗ Q ⊢ R) (H2 : ⊢ Q) : P ⊢ R :=
-  sep_emp.mpr.trans <| (sep_mono_r H2).trans H1
-
-theorem pose_forall [BI PROP] (x : α) (P : α → PROP) {Q : PROP}
-    [H1 : IntoForall Q P] (H2 : ⊢ Q) : ⊢ P x :=
-  Entails.trans H2 <| H1.into_forall.trans <| forall_elim x
-
-partial def instantiateForalls {prop : Q(Type u)} (bi : Q(BI $prop)) (hyp : Q($prop))
-    (pf : Q(⊢ $hyp)) (terms : List Term) : TacticM (Expr × Expr) := do
-  if let some t := terms.head? then
-    let texpr ← mkAppM' (← elabTerm t none) #[]
-    let ⟨_, ttype, texpr⟩ ← inferTypeQ texpr
-    let Φ ← mkFreshExprMVarQ q($ttype → $prop)
-    let _ ← synthInstanceQ q(IntoForall $hyp $Φ)
-    let res ← mkAppM' Φ #[texpr]
-    let pf' ← mkAppM ``pose_forall #[texpr, Φ, pf]
-    return ← instantiateForalls bi res pf' terms.tail
-  else
-    let pf ← mkAppM ``as_emp_valid_1 #[hyp, pf]
-    return ⟨hyp, pf⟩
-
-partial def handleDependentArrows {prop : Q(Type u)} (bi : Q(BI $prop)) (val : Expr) (goals : IO.Ref (Array MVarId)) : TacticM (Expr × Q(Prop)) := do
-  let p : Q(Prop) ← inferType val
-  if let .forallE _ binderType _ _ := p then
-    let m ← mkFreshExprMVar binderType
-    let val' := mkApp val m
-    goals.modify (·.push m.mvarId!)
-    return ← handleDependentArrows bi val' goals
-  else
-    return (val, p)
-
-def iPoseCore {prop : Q(Type u)} (bi : Q(BI $prop)) (val : Expr) (terms : List Term)
-    (goals : IO.Ref (Array MVarId)) : TacticM (Q($prop) × Expr) := do
-  let hyp ← mkFreshExprMVarQ q($prop)
-  let (v, p) ← handleDependentArrows bi val goals
-  if let some _ ← try? <| synthInstanceQ q(IntoEmpValid $p $hyp) then
-    return ← instantiateForalls bi hyp v terms
-  else
-    throwError "ipose: {val} is not an entailment"
-
-elab "ipose" colGt pmt:pmTerm "as" pat:(colGt icasesPat) : tactic => do
-  let pmt ← liftMacroM <| PMTerm.parse pmt
-  let pat ← liftMacroM <| iCasesPat.parse pat
-  let mvar ← getMainGoal
-
-  mvar.withContext do
-    let g ← instantiateMVars <| ← mvar.getType
-    let some { bi, hyps, goal, .. } := parseIrisGoal? g | throwError "not in proof mode"
-
-    let goals ← IO.mkRef #[]
-
-    let f ← getFVarId pmt.term
-    let ⟨hyp, pf⟩ := ← iPoseCore bi (.fvar f) pmt.terms goals
-
-    let m ← iCasesCore bi hyps goal q(false) hyp hyp ⟨⟩ pat (λ hyps => goalTracker goals .anonymous hyps goal)
-    mvar.assign <| ← mkAppM ``pose #[m, pf]
-    replaceMainGoal (← goals.get).toList
diff --git a/src/Iris/ProofMode/Tactics/Specialize.lean b/src/Iris/ProofMode/Tactics/Specialize.lean
index 668c190e..2a55d055 100644
--- a/src/Iris/ProofMode/Tactics/Specialize.lean
+++ b/src/Iris/ProofMode/Tactics/Specialize.lean
@@ -1,84 +1,105 @@
 /-
 Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Lars König, Mario Carneiro
+Authors: Lars König, Mario Carneiro, Michael Sammler
 -/
+import Iris.ProofMode.Patterns.ProofModeTerm
 import Iris.ProofMode.Tactics.Basic
 import Iris.ProofMode.Tactics.Remove
+import Iris.ProofMode.Tactics.Split
 
 namespace Iris.ProofMode
 open Lean Elab Tactic Meta Qq BI Std
 
 structure SpecializeState {prop : Q(Type u)} (bi : Q(BI $prop)) (orig : Q($prop)) where
-  (e : Q($prop)) (hyps : Hyps bi e) (b : Q(Bool)) (out : Q($prop))
-  pf : Q($orig ⊢ $e ∗ □?$b $out)
+  (e : Q($prop)) (hyps : Hyps bi e) (p : Q(Bool)) (out : Q($prop))
+  pf : Q($orig ⊢ $e ∗ □?$p $out)
 
-theorem specialize_wand [BI PROP] {q p : Bool} {A1 A2 A3 Q P1 P2 : PROP}
+theorem specialize_wand [BI PROP] {q p : Bool} {A1 A2 A3 Q P1 P2 P3 : PROP}
     (h1 : A1 ⊢ A2 ∗ □?q Q) (h2 : A2 ⊣⊢ A3 ∗ □?p P1)
-    [inst : IntoWand q p Q P1 P2] : A1 ⊢ A3 ∗ □?(p && q) P2 := by
+    [h3 : IntoWand q false Q P2 P3] [h4 : FromAssumption p P1 P2] :
+    A1 ⊢ A3 ∗ □?(p && q) P3 := 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 inst.1).trans wand_elim_r
+  | false => exact (sep_mono_r h3.1).trans <| (sep_mono_l h4.1).trans wand_elim_r
   | true => exact
     (sep_mono intuitionisticallyIf_intutitionistically.2 intuitionisticallyIf_idem.2).trans <|
-    intuitionisticallyIf_sep_2.trans <| intuitionisticallyIf_mono <| wand_elim' inst.1
+    intuitionisticallyIf_sep_2.trans <| intuitionisticallyIf_mono <| (sep_mono_l h4.1).trans (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}
+    (h1 : A1 ⊢ A2 ∗ □?q Q) (h2 : A2 ⊣⊢ A3 ∗ A4) (h3 : A4 ⊢ P1)
+    [inst : IntoWand q false Q P1 P2] : A1 ⊢ A3 ∗ P2 := by
+  refine h1.trans <| (sep_mono_l h2.1).trans <| sep_assoc.1.trans (sep_mono_r ((sep_mono_l h3).trans ?_))
+  exact (sep_mono_r inst.1).trans wand_elim_r
 
 theorem specialize_forall [BI PROP] {p : Bool} {A1 A2 P : PROP} {α : Sort _} {Φ : α → PROP}
     [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.process1 :
+def SpecializeState.process_forall :
     @SpecializeState u prop bi orig → Term → TermElabM (SpecializeState bi orig)
-  | { e, hyps, b, out, pf }, arg => do
-    let uniq ← match arg with
-      | `($x:ident) => try? (hyps.findWithInfo x)
-      | _ => pure none
-    if let some uniq := uniq then
-      -- if the argument is a hypothesis then specialize the wand
-      let ⟨e', hyps', out₁, out₁', b1, _, pf'⟩ := hyps.remove false uniq
-      let b2 := if b1.constName! == ``true then b else q(false)
-      have : $out₁ =Q iprop(□?$b1 $out₁') := ⟨⟩
-      have : $b2 =Q ($b1 && $b) := ⟨⟩
-
-      let out₂ ← mkFreshExprMVarQ prop
-      let _ ← synthInstanceQ q(IntoWand $b $b1 $out $out₁' $out₂)
-      let pf := q(specialize_wand $pf $pf')
-      return { e := e', hyps := hyps', b := b2, out := out₂, pf }
-    else
-      -- otherwise specialize the universal quantifier
-      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, b, out := out', pf := q(specialize_forall $pf $x) }
+  | { 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) }
 
-elab "ispecialize" hyp:ident args:(colGt term:max)* " as " name:binderIdent : tactic => do
-  let (mvar, { prop, bi, e, hyps, goal, .. }) ← istart (← getMainGoal)
-  mvar.withContext do
+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
+    let uniq ← hyps.findWithInfo i
+    let ⟨e', hyps', out₁, out₁', p1, _, pf'⟩ := hyps.remove false uniq
+    let p2 := if p1.constName! == ``true then p else q(false)
+    have : $out₁ =Q iprop(□?$p1 $out₁') := ⟨⟩
+    have : $p2 =Q ($p1 && $p) := ⟨⟩
 
-  -- find hypothesis index
-  let uniq ← hyps.findWithInfo hyp
-  let (nameTo, nameRef) ← getFreshName name
-  let ⟨_, hyps', _, out', b, _, pf⟩ := hyps.remove (hyp.getId == nameTo) uniq
+    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₁'') |
+      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 }
+  | { hyps, p, out, pf, .. }, .goal ns g => do
+    let mut uniqs : NameSet := {}
+    for name in ns do
+      uniqs := uniqs.insert (← hyps.findWithInfo name)
+    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 pf' ← gs.addGoal hypsr' out₁ g
+    let pf := q(specialize_wand_subgoal $pf $h' $pf')
+    return { e := el', hyps := hypsl', p := q(false), out := out₂, pf }
 
-  let state := { hyps := hyps', out := out', b, pf := q(($pf).1), .. }
+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
+  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
 
-  -- specialize hypothesis
-  let { e := ehyps, hyps, out, b, pf } ← liftM <| args.foldlM SpecializeState.process1 state
+  let hyps' := Hyps.add bi name uniq state.p state.out state.hyps
+  return ⟨_, hyps', state.pf⟩
 
-  let ⟨ehyp1, _⟩ := mkIntuitionisticIf bi b out
-  let uniq' ← mkFreshId
-  let hyp1 := .mkHyp bi nameTo uniq' b out ehyp1
-  addHypInfo nameRef nameTo uniq' prop out (isBinder := true)
-  let hyps' := hyps.mkSep hyp1
-  have pf : Q($e ⊢ $ehyps ∗ $ehyp1) := pf
-  let m : Q($ehyps ∗ $ehyp1 ⊢ $goal) ← mkFreshExprSyntheticOpaqueMVar <|
-    IrisGoal.toExpr { prop, bi, hyps := hyps', goal, .. }
-  mvar.assign q(($pf).trans $m)
-  replaceMainGoal [m.mvarId!]
-
-macro "ispecialize" hyp:ident args:(colGt term:max)* : tactic =>
-  `(tactic| ispecialize $hyp $args* as $hyp:ident)
+elab "ispecialize" colGt pmt:pmTerm : tactic => do
+  let pmt ← liftMacroM <| PMTerm.parse pmt
+  let (mvar, { bi, hyps, goal, .. }) ← istart (← getMainGoal)
+  mvar.withContext do
+  let gs ← Goals.new bi
+  -- hypothesis must be in the context, otherwise use pose proof
+  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 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 a34a0456..0a51a09c 100644
--- a/src/Iris/Tests/Tactics.lean
+++ b/src/Iris/Tests/Tactics.lean
@@ -208,7 +208,7 @@ theorem apply_intuitionistic [BI PROP] (P Q : PROP) : ⊢ □ P -∗ (P -∗ Q)
 
 theorem multiple_intuitionistic [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 with [], [HQ] as Q
   case Q => iexact HQ
   iexact HP
 
@@ -216,7 +216,7 @@ theorem later [BI PROP] (P Q : PROP) : ⊢ (▷ P -∗ Q) -∗ P -∗ Q := by
   iintro H HP
   iapply H with HP
 
-theorem affine [BI PROP] [BIAffine PROP] (P Q : PROP) : ⊢ (P → Q) -∗ <pers> P -∗ Q := by
+theorem test_affine [BI PROP] [BIAffine PROP] (P Q : PROP) : ⊢ (P → Q) -∗ <pers> P -∗ Q := by
   iintro H HP
   iapply H with HP
 
@@ -225,50 +225,57 @@ theorem later_affine [BI PROP] [BIAffine PROP] (P Q : PROP) : ⊢ (▷ P → Q)
   iapply H with HP
 
 theorem exact_lean [BI PROP] (Q : PROP) (H : ⊢ Q) : ⊢ Q := by
-  istart
   iapply H
 
 theorem exact_lean' [BI PROP] (Q : PROP) : Q ⊢ (emp ∗ Q) ∗ emp := by
-  istart
-  iapply (wand_intro sep_emp.mpr)
+  iapply (wand_intro (PROP:=PROP) sep_emp.mpr)
+  istop
+  apply affine
 
 theorem exact_lean'' [BI PROP] (Q : PROP) (H : 0 = 0 → ⊢ Q) : ⊢ Q := by
-  istart
   iapply H
   rfl
 
-theorem apply_lean [BI PROP] (P Q : PROP) (H : P ⊢ Q) (HP : ⊢ P) : ⊢ Q := by
+theorem exact_lean''' [BI PROP] : ⊢@{PROP} ⌜1 = 1⌝ := by
   istart
+  iapply (pure_intro (PROP:=PROP) (P:=emp))
+  . rfl
+  istop
+  apply affine
+
+theorem apply_lean [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
-  istart
-  iapply H with _
+  iapply H with []
   iapply HP
 
 theorem apply_lean'' [BI PROP] (P Q : PROP) (H1 : P ⊢ Q) (H2 : Q ⊢ R) : P ⊢ R := by
-  istart
   iintro HP
   iapply (wand_intro (emp_sep.mp.trans H2))
+  . istop; apply affine
   iapply H1 with HP
 
 theorem multiple_lean [BI PROP] (P Q R : PROP) (H : P ⊢ Q -∗ R) (HP : ⊢ P) : ⊢ Q -∗ R := by
   iintro HQ
-  iapply H with _, HQ
+  iapply H with [], HQ
   iapply HP
 
 theorem multiple_lean' [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) with [], HQ
   iapply HP
 
 theorem exact_forall [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
-  istart
   iapply H
 
 theorem apply_forall [BI PROP] (P Q : α → PROP) (a b : α) (H : ⊢ ∀ x, ∀ y, P x -∗ Q y) : P a ⊢ Q b := by
@@ -279,6 +286,26 @@ theorem apply_forall' [BI PROP] (P Q : α → PROP) (a b : α) : (∀ x, ∀ y,
   iintro H HP
   iapply H $! a, b with HP
 
+/- TODO: enable this when tc seach can create mvars
+theorem apply_forall2 [BI PROP] (P Q : α → PROP) (a b : α) : (∀ x, ∀ y, P x -∗ Q y) ⊢ P a -∗ Q b := by
+  iintro H HP
+  iapply H with HP
+-/
+
+/--
+error: ispecialize: cannot instantiate iprop(P ?m.37 -∗ Q ?m.40) with P a
+-/
+#guard_msgs in -- TODO: tc search should be able to instantiate mvars
+theorem apply_forall3 [BI PROP] (P Q : α → PROP) (a b : α) : (∀ x, ∀ y, P x -∗ Q y) ⊢ P a -∗ Q b := by
+  iintro H HP
+  iapply H $! ?_, ?_ with HP
+
+/- TODO: enable this when tc seach can create mvars
+theorem apply_forall4 [BI PROP] (P Q : α → PROP) (a b : α) : (∀ x, ∀ y, P x -∗ Q y) ⊢ P a -∗ Q b := by
+  iintro H HP
+  iapply H
+-/
+
 theorem apply_forall_intuitionistic [BI PROP] (P Q : α → PROP) (a b : α) (H : ⊢ □ ∀ x, ∀ y, P x -∗ Q y) : P a ⊢ Q b := by
   iintro HP
   iapply H $! a, b with HP
@@ -287,32 +314,79 @@ theorem apply_forall_intuitionistic' [BI PROP] (P Q : α → PROP) (a b : α) :
   iintro H HP
   iapply H $! a, b with HP
 
+theorem apply_two_wands [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
+
 end apply
 
--- pose
-namespace pose
+-- have
+namespace ihave
 
 theorem exact_lean [BI PROP] (Q : PROP) (H : ⊢ Q) : ⊢ Q := by
-  istart
-  ipose H as HQ
+  ihave HQ := H
+  iexact HQ
+
+theorem exact_lean_forall [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
+  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
+  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
+  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
+  ihave HQ := H iprop(□ Q _)
+  rotate_right 1; exact 1
+  iexact HQ
+
+theorem exact_spatial [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
-  istart
-  ipose H as HPQ
-  iapply HPQ
+  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
   iintro HP
-  ipose H $! a, b as H'
+  ihave H' := H $! a, b
   iapply H' with HP
 
+theorem apply_forall_spatial [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
+  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
   iintro HP
-  ipose H $! a, b as H'
+  ihave H' := H $! a, b
   iapply H' with HP
 
-end pose
+theorem apply_forall_intuitionistic_iris [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]
+  . iexact HP
+  iexact H'
+
+end ihave
 
 -- ex falso
 namespace exfalso
@@ -443,98 +517,114 @@ namespace specialize
 
 theorem wand_spatial [BI PROP] (Q : PROP) : P ⊢ (P -∗ Q) -∗ Q := by
   iintro HP HPQ
-  ispecialize HPQ HP as HQ
-  iexact HQ
+  ispecialize HPQ with HP
+  iexact HPQ
+
+theorem wand_spatial_subgoal [BI PROP] (Q : PROP) : P ⊢ (P -∗ Q) -∗ Q := by
+  iintro HP HPQ
+  ispecialize HPQ with [HP]
+  . iexact HP
+  iexact HPQ
+
+theorem wand_spatial_subgoal_named [BI PROP] (Q : PROP) : P ⊢ (P -∗ Q) -∗ Q := by
+  iintro HP HPQ
+  ispecialize HPQ with [HP] as G
+  case G => iexact HP
+  iexact HPQ
 
 theorem wand_intuitionistic [BI PROP] (Q : PROP) : □ P ⊢ □ (P -∗ Q) -∗ □ Q := by
   iintro □HP □HPQ
-  ispecialize HPQ HP as HQ
-  iexact HQ
+  ispecialize HPQ with HP
+  iexact HPQ
 
-theorem wand_intuitionistic_overwrite [BI PROP] (Q : PROP) : □ P ⊢ □ (□ P -∗ Q) -∗ □ Q := by
+theorem wand_intuitionistic_subgoal [BI PROP] (Q : PROP) : □ P ⊢ □ (P -∗ Q) -∗ Q := by
   iintro □HP □HPQ
-  ispecialize HPQ HP
+  ispecialize HPQ with []
+  . iexact HP
   iexact HPQ
 
 theorem wand_intuitionistic_required [BI PROP] (Q : PROP) : □ P ⊢ □ (□ P -∗ Q) -∗ □ Q := by
   iintro □HP □HPQ
-  ispecialize HPQ HP as HQ
-  iexact HQ
+  ispecialize HPQ with HP
+  iexact HPQ
 
 theorem wand_intuitionistic_spatial [BI PROP] (Q : PROP) : □ P ⊢ (P -∗ Q) -∗ Q := by
   iintro □HP HPQ
-  ispecialize HPQ HP as HQ
-  iexact HQ
+  ispecialize HPQ with HP
+  iexact HPQ
 
 theorem wand_intuitionistic_required_spatial [BI PROP] (Q : PROP) : □ P ⊢ (□ P -∗ Q) -∗ Q := by
   iintro □HP HPQ
-  ispecialize HPQ HP as HQ
-  iexact HQ
+  ispecialize HPQ with HP
+  iexact HPQ
 
 theorem wand_spatial_intuitionistic [BI PROP] (Q : PROP) : P ⊢ □ (P -∗ Q) -∗ Q := by
   iintro HP □HPQ
-  ispecialize HPQ HP as HQ
-  iexact HQ
+  ispecialize HPQ with HP
+  iexact HPQ
 
 theorem wand_spatial_multiple [BI PROP] (Q : PROP) : ⊢ P1 -∗ P2 -∗ (P1 -∗ P2 -∗ Q) -∗ Q := by
   iintro HP1 HP2 HPQ
-  ispecialize HPQ HP1 HP2 as HQ
-  iexact HQ
+  ispecialize HPQ with HP1, HP2
+  iexact HPQ
+
+theorem wand_spatial_multiple_subgoal [BI PROP] (Q : PROP) : ⊢ P1 -∗ P2 -∗ (P1 -∗ P2 -∗ Q) -∗ Q := by
+  iintro HP1 HP2 HPQ
+  ispecialize HPQ with [HP1], [HP2]
+  . iexact HP1
+  . iexact HP2
+  iexact HPQ
 
 theorem wand_intuitionistic_multiple [BI PROP] (Q : PROP) :
     ⊢ □ P1 -∗ □ P2 -∗ □ (P1 -∗ □ P2 -∗ Q) -∗ □ Q := by
   iintro □HP1 □HP2 □HPQ
-  ispecialize HPQ HP1 HP2 as HQ
-  iexact HQ
+  ispecialize HPQ with HP1, HP2
+  iexact HPQ
 
 theorem wand_multiple [BI PROP] (Q : PROP) :
     ⊢ P1 -∗ □ P2 -∗ P3 -∗ □ (P1 -∗ P2 -∗ P3 -∗ Q) -∗ Q := by
   iintro HP1 □HP2 HP3 HPQ
-  ispecialize HPQ HP1 HP2 HP3 as HQ
-  iexact HQ
+  ispecialize HPQ with HP1, HP2, HP3
+  iexact HPQ
 
 theorem forall_spatial [BI PROP] (Q : Nat → PROP) : ⊢ (∀ x, Q x) -∗ Q (y + 1) := by
   iintro HQ
-  ispecialize HQ (y + 1) as HQ
+  ispecialize HQ $! (y + 1)
   iexact HQ
 
 theorem forall_intuitionistic [BI PROP] (Q : Nat → PROP) : ⊢ □ (∀ x, Q x) -∗ □ Q y := by
   iintro □HQ
-  ispecialize HQ y as HQ'
-  iexact HQ'
-
-theorem forall_intuitionistic_overwrite [BI PROP] (Q : Nat → PROP) : ⊢ □ (∀ x, Q x) -∗ □ Q y := by
-  iintro □HQ
-  ispecialize HQ y as HQ
+  ispecialize HQ $! y
   iexact HQ
 
 theorem forall_spatial_intuitionistic [BI PROP] (Q : Nat → PROP) : ⊢ (∀ x, □ Q x) -∗ □ Q y := by
   iintro HQ
-  ispecialize HQ y as HQ
+  ispecialize HQ $! y
   iexact HQ
 
 theorem forall_spatial_multiple [BI PROP] (Q : Nat → Nat → PROP) :
     ⊢ (∀ x, ∀ y, Q x y) -∗ Q x y := by
   iintro HQ
-  ispecialize HQ x y as HQ'
-  iexact HQ'
+  ispecialize HQ $! x, y
+  iexact HQ
 
 theorem forall_intuitionistic_multiple [BI PROP] (Q : Nat → Nat → PROP) :
     ⊢ □ (∀ x, ∀ y, Q x y) -∗ □ Q x y := by
   iintro □HQ
-  ispecialize HQ x y as HQ'
-  iexact HQ'
+  ispecialize HQ $! x, y
+  iexact HQ
 
 theorem forall_multiple [BI PROP] (Q : Nat → Nat → PROP) : ⊢ (∀ x, □ (∀ y, Q x y)) -∗ □ Q x y := by
   iintro HQ
-  ispecialize HQ x y as HQ'
-  iexact HQ'
+  ispecialize HQ $! x, y
+  iexact HQ
 
 theorem multiple [BI PROP] (Q : Nat → PROP) :
     ⊢ □ P1 -∗ P2 -∗ (□ P1 -∗ (∀ x, P2 -∗ Q x)) -∗ Q y := by
   iintro □HP1 HP2 HPQ
-  ispecialize HPQ HP1 y HP2 as HQ
-  iexact HQ
+  ispecialize HPQ with HP1
+  ispecialize HPQ $! y with HP2
+  iexact HPQ
 
 end specialize