diff --git a/src/Iris/ProofMode/Classes.lean b/src/Iris/ProofMode/Classes.lean
index 61c4fd44..4150397b 100644
--- a/src/Iris/ProofMode/Classes.lean
+++ b/src/Iris/ProofMode/Classes.lean
@@ -16,7 +16,7 @@ declared as an `outParam`. Consequently, if type class instance search is suppos
 `AsEmpValid2` is used.
 -/
 
-class AsEmpValid1 (φ : outParam Prop) {PROP : Type _} (P : PROP) [BI PROP] where
+class AsEmpValid1 (φ : semiOutParam Prop) {PROP : Type _} (P : PROP) [BI PROP] where
   as_emp_valid : φ ↔ ⊢ P
 
 class AsEmpValid2 (φ : Prop) {PROP : outParam (Type _)} (P : outParam PROP) [BI PROP] where
@@ -40,6 +40,10 @@ 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)
+
 class FromImp [BI PROP] (P : PROP) (Q1 Q2 : outParam PROP) where
   from_imp : (Q1 → Q2) ⊢ P
 export FromImp (from_imp)
@@ -48,7 +52,7 @@ 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 P : PROP) (Q : outParam PROP) where
+class IntoWand [BI PROP] (p q : Bool) (R : PROP) (P Q : outParam PROP) where
   into_wand : □?p R ⊢ □?q P -∗ Q
 export IntoWand (into_wand)
 
@@ -106,7 +110,7 @@ class IntoAbsorbingly [BI PROP] (P : outParam PROP) (Q : PROP) where
 export IntoAbsorbingly (into_absorbingly)
 
 
-class FromAssumption (p : Bool) [BI PROP] (P Q : PROP) where
+class FromAssumption (p : Bool) [BI PROP] (P : semiOutParam PROP) (Q : PROP) where
   from_assumption : □?p P ⊢ Q
 export FromAssumption (from_assumption)
 
diff --git a/src/Iris/ProofMode/Instances.lean b/src/Iris/ProofMode/Instances.lean
index 42ad0aec..5141513c 100644
--- a/src/Iris/ProofMode/Instances.lean
+++ b/src/Iris/ProofMode/Instances.lean
@@ -26,6 +26,16 @@ instance asEmpValid1_equiv [BI PROP] (P Q : PROP) : AsEmpValid1 (P ⊣⊢ Q) ipr
 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
+
 -- FromImp
 instance fromImp_imp [BI PROP] (P1 P2 : PROP) : FromImp iprop(P1 → P2) P1 P2 := ⟨.rfl⟩
 -- FromWand
@@ -67,6 +77,10 @@ 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
   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
   into_wand := intuitionistically_persistently.1.trans h.1
@@ -429,6 +443,10 @@ instance (priority := default + 10) fromAssumption_forall (p : Bool) [BI PROP] (
     (x : α) (Q : PROP) [h : FromAssumption p (Φ x) Q] : FromAssumption p 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
+  from_assumption := h.1.trans later_intro
+
 -- IntoPure
 instance intoPure_pure (φ : Prop) [BI PROP] : IntoPure (PROP := PROP) iprop(⌜φ⌝) φ := ⟨.rfl⟩
 
diff --git a/src/Iris/ProofMode/Patterns.lean b/src/Iris/ProofMode/Patterns.lean
index ed428189..64b2e896 100644
--- a/src/Iris/ProofMode/Patterns.lean
+++ b/src/Iris/ProofMode/Patterns.lean
@@ -1 +1,3 @@
 import Iris.ProofMode.Patterns.CasesPattern
+import Iris.ProofMode.Patterns.ProofModeTerm
+import Iris.ProofMode.Patterns.SpecPattern
diff --git a/src/Iris/ProofMode/Patterns/ProofModeTerm.lean b/src/Iris/ProofMode/Patterns/ProofModeTerm.lean
new file mode 100644
index 00000000..0b45b19d
--- /dev/null
+++ b/src/Iris/ProofMode/Patterns/ProofModeTerm.lean
@@ -0,0 +1,34 @@
+/-
+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.SpecPattern
+
+namespace Iris.ProofMode
+open Lean
+
+declare_syntax_cat pmTerm
+
+syntax term : pmTerm
+syntax term "with" specPat,+ : pmTerm
+syntax term "$!" term,+ : pmTerm
+syntax term "$!" term,+ "with" 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⟩
+  | _ => Macro.throwUnsupported
+where
+  parseSpats (spats : Syntax.TSepArray `specPat ",") : MacroM (List SpecPat) :=
+      return (← spats.getElems.toList.mapM fun pat => SpecPat.parse pat.raw)
diff --git a/src/Iris/ProofMode/Patterns/SpecPattern.lean b/src/Iris/ProofMode/Patterns/SpecPattern.lean
new file mode 100644
index 00000000..27de2c17
--- /dev/null
+++ b/src/Iris/ProofMode/Patterns/SpecPattern.lean
@@ -0,0 +1,36 @@
+/-
+Copyright (c) 2025 Oliver Soeser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Oliver Soeser
+-/
+namespace Iris.ProofMode
+open Lean
+
+declare_syntax_cat specPat
+
+syntax binderIdent : specPat
+syntax "[" binderIdent,* "]" optional(" as " ident) : specPat
+
+inductive SpecPat
+  | ident (name : TSyntax ``binderIdent)
+  | idents (names : List (TSyntax ``binderIdent)) (goalName : Name)
+  deriving Repr, Inhabited
+
+partial def SpecPat.parse (pat : Syntax) : MacroM SpecPat := do
+  match go ⟨← expandMacros pat⟩ with
+  | none => Macro.throwUnsupported
+  | 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
+    | _ => none
+  | _ => none
+
+def headName (spats : List SpecPat) : Name :=
+  match spats.head? with
+    | some <| .ident _ => .anonymous
+    | some <| .idents _ name => name
+    | _ => .anonymous
diff --git a/src/Iris/ProofMode/Tactics.lean b/src/Iris/ProofMode/Tactics.lean
index 7758fa71..24a34423 100644
--- a/src/Iris/ProofMode/Tactics.lean
+++ b/src/Iris/ProofMode/Tactics.lean
@@ -1,4 +1,5 @@
 /- A description of the tactics can be found in `tactics.md`. -/
+import Iris.ProofMode.Tactics.Apply
 import Iris.ProofMode.Tactics.Assumption
 import Iris.ProofMode.Tactics.Basic
 import Iris.ProofMode.Tactics.Cases
@@ -9,6 +10,7 @@ import Iris.ProofMode.Tactics.Exists
 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
new file mode 100644
index 00000000..4bd97714
--- /dev/null
+++ b/src/Iris/ProofMode/Tactics/Apply.lean
@@ -0,0 +1,126 @@
+/-
+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.Split
+import Iris.ProofMode.Tactics.Pose
+
+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 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
+
+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⟩
+
+elab "iapply" colGt pmt:pmTerm : tactic => do
+  let pmt ← liftMacroM <| PMTerm.parse pmt
+  let mvar ← 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
diff --git a/src/Iris/ProofMode/Tactics/Basic.lean b/src/Iris/ProofMode/Tactics/Basic.lean
index 3c2d6c8a..5f060d58 100644
--- a/src/Iris/ProofMode/Tactics/Basic.lean
+++ b/src/Iris/ProofMode/Tactics/Basic.lean
@@ -53,9 +53,23 @@ 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
+  | _ => 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
+
+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 <|
+    IrisGoal.toExpr { prop, bi, hyps, goal, .. }
+  m.mvarId!.setUserName name
+  goals.modify (·.push m.mvarId!)
+  pure m
diff --git a/src/Iris/ProofMode/Tactics/Cases.lean b/src/Iris/ProofMode/Tactics/Cases.lean
index 4600e0ad..229e016d 100644
--- a/src/Iris/ProofMode/Tactics/Cases.lean
+++ b/src/Iris/ProofMode/Tactics/Cases.lean
@@ -286,11 +286,7 @@ elab "icases" colGt hyp:ident "with" colGt pat:icasesPat : tactic => do
 
   -- process pattern
   let goals ← IO.mkRef #[]
-  let pf2 ← iCasesCore bi hyps' goal b A A' h pat fun hyps => do
-    let m : Q($e ⊢ $goal) ← mkFreshExprSyntheticOpaqueMVar <|
-      IrisGoal.toExpr { u, prop, bi, hyps, goal, .. }
-    goals.modify (·.push m.mvarId!)
-    pure m
+  let pf2 ← iCasesCore bi hyps' goal b A A' h pat (λ hyps => goalTracker goals .anonymous hyps goal)
 
   mvar.assign q(($pf).1.trans $pf2)
   replaceMainGoal (← goals.get).toList
diff --git a/src/Iris/ProofMode/Tactics/Intro.lean b/src/Iris/ProofMode/Tactics/Intro.lean
index 8f52a6c2..a7394d24 100644
--- a/src/Iris/ProofMode/Tactics/Intro.lean
+++ b/src/Iris/ProofMode/Tactics/Intro.lean
@@ -102,16 +102,12 @@ elab "iintro" pats:(colGt icasesPat)* : tactic => do
   -- parse syntax
   let pats ← liftMacroM <| pats.mapM <| iCasesPat.parse
 
-  let (mvar, { prop, bi, hyps, goal, .. }) ← istart (← getMainGoal)
+  let (mvar, { bi, hyps, goal, .. }) ← istart (← getMainGoal)
   mvar.withContext do
 
   -- process patterns
   let goals ← IO.mkRef #[]
-  let pf ← iIntroCore bi hyps goal pats.toList fun {P} hyps goal => do
-    let m : Q($P ⊢ $goal) ← mkFreshExprSyntheticOpaqueMVar <|
-      IrisGoal.toExpr { prop, bi, hyps, goal, .. }
-    goals.modify (·.push m.mvarId!)
-    pure m
+  let pf ← iIntroCore bi hyps goal pats.toList <| goalTracker goals .anonymous
 
   mvar.assign pf
   replaceMainGoal (← goals.get).toList
diff --git a/src/Iris/ProofMode/Tactics/Pose.lean b/src/Iris/ProofMode/Tactics/Pose.lean
new file mode 100644
index 00000000..1e155c5d
--- /dev/null
+++ b/src/Iris/ProofMode/Tactics/Pose.lean
@@ -0,0 +1,70 @@
+/-
+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/Tests/Tactics.lean b/src/Iris/Tests/Tactics.lean
index 48c610a4..1191b5bd 100644
--- a/src/Iris/Tests/Tactics.lean
+++ b/src/Iris/Tests/Tactics.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Lars König
+Authors: Lars König, Oliver Soeser
 -/
 import Iris.BI
 import Iris.ProofMode
@@ -178,6 +178,142 @@ theorem lean_pure [BI PROP] (Q : PROP) : <affine> ⌜⊢ Q⌝ ⊢ Q := by
 
 end assumption
 
+-- apply
+namespace apply
+
+theorem exact [BI PROP] (Q : PROP) : Q ⊢ Q := by
+  iintro HQ
+  iapply HQ
+
+theorem apply [BI PROP] (P Q : PROP) : ⊢ P -∗ (P -∗ Q) -∗ Q := by
+  iintro HP H
+  iapply H with HP
+
+theorem multiple [BI PROP] (P Q R : PROP) : ⊢ P -∗ Q -∗ (P -∗ Q -∗ R) -∗ R := by
+  iintro HP HQ H
+  iapply H with HP, HQ
+
+theorem multiple' [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
+
+theorem exact_intuitionistic [BI PROP] (Q : PROP) : □ Q ⊢ Q := by
+  iintro □HQ
+  iapply HQ
+
+theorem apply_intuitionistic [BI PROP] (P Q : PROP) : ⊢ □ P -∗ (P -∗ Q) -∗ Q := by
+  iintro HP H
+  iapply H with HP
+
+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
+  case Q => iexact HQ
+  iexact HP
+
+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
+  iintro H HP
+  iapply H with HP
+
+theorem later_affine [BI PROP] [BIAffine PROP] (P Q : PROP) : ⊢ (▷ P → Q) -∗ P -∗ Q := by
+  iintro H HP
+  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)
+
+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
+  istart
+  iapply H
+  iapply HP
+
+theorem apply_lean' [BI PROP] (P Q : PROP) (H : ⊢ P -∗ Q) (HP : ⊢ P) : ⊢ Q := by
+  istart
+  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))
+  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 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 HP
+
+theorem exact_forall [BI PROP] (P : α → PROP) (a : α) (H : ⊢ ∀ x, P x) : ⊢ P a := by
+  istart
+  iapply H
+
+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
+  iintro HP
+  iapply H $! a, b with HP
+
+theorem apply_forall' [BI PROP] (P Q : α → PROP) (a b : α) : (∀ x, ∀ y, P x -∗ Q y) ⊢ P a -∗ Q b := by
+  iintro H HP
+  iapply H $! a, b with HP
+
+theorem apply_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
+
+theorem apply_forall_intuitionistic' [BI PROP] (P Q : α → PROP) (a b : α) : (□ ∀ x, ∀ y, P x -∗ Q y) ⊢ P a -∗ Q b := by
+  iintro H HP
+  iapply H $! a, b with HP
+
+end apply
+
+-- pose
+namespace pose
+
+theorem exact_lean [BI PROP] (Q : PROP) (H : ⊢ Q) : ⊢ Q := by
+  istart
+  ipose H as HQ
+  iapply HQ
+
+theorem apply_lean [BI PROP] (P Q : PROP) (H : P ⊢ Q) : ⊢ P -∗ Q := by
+  istart
+  ipose H as HPQ
+  iapply 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'
+  iapply H' with HP
+
+theorem apply_forall_intuitionistic [BI PROP] (P Q : α → PROP) (a b : α) (H : ⊢ □ ∀ x, ∀ y, P x -∗ Q y) : P a ⊢ Q b := by
+  iintro HP
+  ipose H $! a, b as H'
+  iapply H' with HP
+
+end pose
+
 -- ex falso
 namespace exfalso
 
diff --git a/tactics.md b/tactics.md
index 4b0d7b56..258b72d5 100644
--- a/tactics.md
+++ b/tactics.md
@@ -23,6 +23,8 @@
 | `ileft`<br>`iright`                    | Choose to prove the left (`ileft`) or right (`iright`) side of a disjunction in the goal.                                                                                                                                            |
 | `icases` *hyp* `with` *cases-pat*      | Destruct the hypothesis *hyp* using the cases pattern *cases-pat*.                                                                                                                                                                   |
 | `iintro` *cases-pats*                  | Introduce up to multiple hypotheses and destruct them using the cases patterns *cases-pats*.                                                                                                                                         |
+| `iapply` *pmTerm*                      | Match the conclusion of the current goal against the conclusion of the *pmTerm* and generates goals for each of its premises, moving all unused spatial hypotheses to the last premise.                                              |
+| `ipose` *pmTerm* `as` *name*           | Move *pmTerm* into the Iris context with the name *name*.                                                                                                                                                                               |
 
 ## Cases Patterns
 
@@ -44,3 +46,19 @@ P1 ∗ (□ P2 ∨ P2) ∗ (P3 ∧ P3')
 ⟨HP1, □HP2 | HP2, ⟨HP3, _⟩⟩
 -- (there are of course other valid patterns for destructing the shown hypothesis)
 ```
+
+## Specialization Patterns
+
+| Pattern                         | Description                                                                                                                                                                         |
+|---------------------------------|-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|
+| `H`                             | Use the hypothesis `H`, which should match the premise exactly.                                                                                                                                               |
+| `[H1, ..., HN]`                 | Generate a goal with the hypotheses `[H1, ..., HN]`                                                                                                                                                                |
+| `[H1, ..., HN]` as *str*        | Generate a goal named *str* with the hypotheses `[H1, ..., HN]`.                                                                                                                                                            |
+
+## Proof Mode Terms
+
+Proof mode terms (*pmTerm*) are of the form
+```
+(H $! t1 ... tn with "specPat1 ... specPatN")
+```
+where `H` is a hypothesis or Lean term whose conclusion is an entailment, `t1 ... tn` are Lean terms for the instantiation of universal quantifiers, and `specPat1 ... specPatN` are specialization patterns.
\ No newline at end of file