diff --git a/Iris/Iris/ProofMode/Expr.lean b/Iris/Iris/ProofMode/Expr.lean
index c9f86ea0b..8b75781df 100644
--- a/Iris/Iris/ProofMode/Expr.lean
+++ b/Iris/Iris/ProofMode/Expr.lean
@@ -140,12 +140,13 @@ def Hyps.mkHyp {prop : Q(Type u)} (bi : Q(BI $prop))
     (name : Name) (ivar : IVarId) (p : Q(Bool)) (ty : Q($prop)) (e := q(iprop(□?$p $ty))) : Hyps bi e :=
   .hyp (mkIntuitionisticIf bi p (mkNameAnnotation name ivar ty)) name ivar 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 : Name) (ivar : IVarId) (p : Q(Bool)) (ty : Q($prop)) {e} (h : Hyps bi e)
-    : Hyps bi q(iprop($e ∗ □?$p $ty)) :=
-  Hyps.mkSep h (.mkHyp bi name ivar p ty)
+    : (e' : Q($prop)) × Hyps bi e' × Q(iprop($e ∗ □?$p $ty ⊣⊢ $e')) :=
+  match h with
+  -- Adding a hypothesis to `emp` creates a `.hyp` node instead of a `.sep` node
+  | .emp _ => ⟨_, .mkHyp bi name ivar p ty, q(emp_sep)⟩
+  | _ => ⟨_, .mkSep h (.mkHyp bi name ivar p ty), q(.rfl)⟩
 
 partial def parseHyps? {prop : Q(Type u)} (bi : Q(BI $prop)) (expr : Expr) :
     Option ((s : Q($prop)) × Hyps bi s) := do
@@ -533,9 +534,9 @@ def Hyps.findWithInfo {u prop bi} (hyps : @Hyps u prop bi s) (name : Ident) : Me
 /-- 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 (IVarId × Hyps bi q(iprop($e ∗ □?$p $ty))) := do
+    : MetaM (IVarId × (e' : Q($prop)) × Hyps bi e' × Q(iprop($e ∗ □?$p $ty ⊣⊢ $e'))) := do
   let ivar' ← mkFreshIVarId (isTrue p)
   let (nameTo, nameRef) ← getFreshName name
   addHypInfo nameRef nameTo ivar' prop ty (isBinder := true)
-  let hyps := Hyps.add bi nameTo ivar' p ty h
-  return ⟨ivar', hyps⟩
+  let ⟨e', hyps, pf⟩ := Hyps.add bi nameTo ivar' p ty h
+  return ⟨ivar', e', hyps, pf⟩
diff --git a/Iris/Iris/ProofMode/Patterns/CasesPattern.lean b/Iris/Iris/ProofMode/Patterns/CasesPattern.lean
index 2013eb220..f789b258b 100644
--- a/Iris/Iris/ProofMode/Patterns/CasesPattern.lean
+++ b/Iris/Iris/ProofMode/Patterns/CasesPattern.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, Alvin Tang
 -/
 module
 
@@ -15,50 +15,74 @@ open Lean
 declare_syntax_cat icasesPat
 syntax icasesPatAlts := sepBy1(icasesPat, " | ")
 syntax binderIdent : icasesPat
+/-- Drop the hypothesis. -/
 syntax "-" : icasesPat
+/-- Frame the hypothesis and cancel it against the goal. -/
 syntax "$" : icasesPat
+/--
+  Destruct a (separating) conjunction or existential; an existential variable is
+  bound with `%x` where `x` is the name for it.
+-/
 syntax "⟨" icasesPatAlts,* "⟩" : icasesPat
+/-- Destruct a disjunction, one goal per disjunct. -/
 syntax "(" icasesPatAlts ")" : icasesPat
-syntax "%" binderIdent : icasesPat
+/-- Move the hypothesis to the pure Lean context and give it a name. -/
+syntax "%" rcasesPat : icasesPat
+/-- Move the hypothesis to the intuitionistic context and destruct the proposition. -/
 syntax "#" icasesPat : icasesPat
+/-- Move the hypothesis to the spatial context and destruct the proposition. -/
 syntax "∗" icasesPat : icasesPat
+/-- Eliminate the modality at the top of the hypothesis and destruct the remaining proposition. -/
 syntax ">" icasesPat : icasesPat
+/-- Introduce a pure equality and use it for rewriting in the backward direction. -/
+syntax "←" : icasesPat
+/-- Introduce a pure equality and use it for rewriting in the forward direction. -/
+syntax "→" : icasesPat
 
--- TODO: attach syntax to iCasesPat such that one can use withRef to
--- associate the errors with the right part of the syntax
 inductive iCasesPat
-  | one (name : TSyntax ``binderIdent)
-  | clear
-  | frame
-  | conjunction (args : List iCasesPat)
-  | disjunction (args : List iCasesPat)
-  | pure           (pat : TSyntax ``binderIdent)
-  | intuitionistic (pat : iCasesPat)
-  | spatial        (pat : iCasesPat)
-  | mod            (pat : iCasesPat)
+  | one (ref : Syntax) (name : TSyntax ``binderIdent)
+  | clear (ref : Syntax)
+  | frame (ref : Syntax)
+  | conjunction (ref : Syntax) (args : List iCasesPat)
+  | disjunction (ref : Syntax) (args : List iCasesPat)
+  | pure (ref : Syntax) (pat : TSyntax `rcasesPat)
+  | intuitionistic (ref : Syntax) (pat : iCasesPat)
+  | spatial (ref : Syntax) (pat : iCasesPat)
+  | mod (ref : Syntax) (pat : iCasesPat)
+  | rewrite (ref : Syntax) (forward : Bool)
   deriving Repr, Inhabited
 
+def iCasesPat.ref : iCasesPat → Syntax
+  | .one r _ | .clear r | .frame r | .conjunction r _ | .disjunction r _
+  | .pure r _ | .intuitionistic r _ | .spatial r _ | .mod r _ | .rewrite r _ => r
+
 partial def iCasesPat.parse (pat : TSyntax `icasesPat) : MacroM iCasesPat := do
   match go ⟨← expandMacros pat⟩ with
   | none => Macro.throwUnsupported
   | some pat => return pat
 where
-  go : TSyntax `icasesPat → Option iCasesPat
-  | `(icasesPat| $name:binderIdent) => some <| .one name
-  | `(icasesPat| -) => some <| .clear
-  | `(icasesPat| $) => some <| .frame
-  | `(icasesPat| ⟨$[$args],*⟩) => args.mapM goAlts |>.map (.conjunction ·.toList)
-  | `(icasesPat| %$pat:binderIdent) => some <| .pure pat
-  | `(icasesPat| #$pat) => go pat |>.map .intuitionistic
-  | `(icasesPat| ∗$pat) => go pat |>.map .spatial
-  | `(icasesPat| >$pat) => go pat |>.map .mod
-  | `(icasesPat| ($pat)) => goAlts pat
-  | _ => none
-  goAlts : TSyntax ``icasesPatAlts → Option iCasesPat
-  | `(icasesPatAlts| $args|*) =>
-    match args.getElems with
-    | #[arg] => go arg
-    | args   => args.mapM go |>.map (.disjunction ·.toList)
-  | _ => none
+  go (stx : TSyntax `icasesPat) : Option iCasesPat :=
+    let ref := stx.raw
+    match ref with
+    | `(icasesPat| $name:binderIdent) => some <| .one ref name
+    | `(icasesPat| -) => some <| .clear ref
+    | `(icasesPat| $) => some <| .frame ref
+    | `(icasesPat| ⟨$[$args],*⟩) => args.mapM goAlts |>.map (.conjunction ref ·.toList)
+    | `(icasesPat| %$pat:rcasesPat) => some <| .pure ref pat
+    | `(icasesPat| #$pat) => go pat |>.map <| .intuitionistic ref
+    | `(icasesPat| ∗$pat) => go pat |>.map <| .spatial ref
+    | `(icasesPat| >$pat) => go pat |>.map <| .mod ref
+    | `(icasesPat| ($pat)) => goAlts pat
+    | `(icasesPat| ←) => some <| .rewrite ref false
+    | `(icasesPat| →) => some <| .rewrite ref true
+    | _ => none
+  goAlts (stx : TSyntax ``icasesPatAlts) : Option iCasesPat :=
+    let ref := stx.raw
+    match stx with
+    | `(icasesPatAlts| $args|*) =>
+      match args.getElems with
+      | #[arg] => go arg
+      | args   => args.mapM go |>.map (.disjunction ref ·.toList)
+    | _ => none
 
 end Iris.ProofMode
diff --git a/Iris/Iris/ProofMode/Patterns/IntroPattern.lean b/Iris/Iris/ProofMode/Patterns/IntroPattern.lean
index 51fad31bb..59f2b99b4 100644
--- a/Iris/Iris/ProofMode/Patterns/IntroPattern.lean
+++ b/Iris/Iris/ProofMode/Patterns/IntroPattern.lean
@@ -1,11 +1,12 @@
 /-
 Copyright (c) 2025 Michael Sammler. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Michael Sammler
+Authors: Michael Sammler, Alvin Tang
 -/
 module
 
 public import Iris.ProofMode.Patterns.CasesPattern
+public import Iris.ProofMode.Patterns.SelPattern
 meta import Iris.Std.RocqPorting
 
 @[expose] public section
@@ -13,17 +14,44 @@ meta import Iris.Std.RocqPorting
 namespace Iris.ProofMode
 open Lean
 
+declare_syntax_cat selPatFrame
+syntax ("!" noWs)? selPat : selPatFrame
+
 declare_syntax_cat introPat
 
 syntax icasesPat : introPat
+/-- Introduce a modality, analogous to applying `imodintro`. -/
 syntax "!>" : introPat
+/-- Try to solve the goal using `itrivial`. -/
 syntax "//" : introPat
+/-- Apply simplification. -/
+syntax "/=" : introPat
+/-- Apply simplifcation (`/=`) and try solving the goal (`//`). -/
+syntax "//=" : introPat
+/-- Introduce all universal quantifiers. -/
+syntax "*" : introPat
+/-- Introduce all universal quantifiers, pure arrows and wands. -/
+syntax "**" : introPat
+/-- Introduces a pure proof goal, analogous to applying `ipureintro`. -/
+syntax "!%" : introPat
+/--
+  Given selection patterns `spats`, the introduction pattern `{ spats }`
+  *clears* the hypotheses chosen by `spats`. Prefix an element in the selection
+  patterns with `!` to *frame* the hypotheses instead.
+-/
+syntax "{" (colGt ppSpace selPatFrame)* ppSpace "}" : introPat
 
 @[rocq_alias intro_pat]
 inductive IntroPat
   | intro (case : iCasesPat)
   | trivial
   | modintro
+  | simp
+  | simptrivial
+  | all
+  | allwand
+  | pureintro
+  | clear (selPats : List <| Bool × SelPat)
   deriving Repr, Inhabited
 
 partial def IntroPat.parse (term : Syntax) : MacroM (Syntax × IntroPat) := do
@@ -31,7 +59,15 @@ partial def IntroPat.parse (term : Syntax) : MacroM (Syntax × IntroPat) := do
   | `(introPat| $case:icasesPat) => return (term, .intro (← iCasesPat.parse case))
   | `(introPat| //) => return (term, .trivial)
   | `(introPat| !>) => return (term, .modintro)
+  | `(introPat| /=) => return (term, .simp)
+  | `(introPat| //=) => return (term, .simptrivial)
+  | `(introPat| *) => return (term, .all)
+  | `(introPat| **) => return (term, .allwand)
+  | `(introPat| !%) => return (term, .pureintro)
+  | `(introPat| { $spats:selPatFrame* }) => return (term, .clear (← spats.toList.mapM parseSelPats))
   | _ => Macro.throwUnsupported
+  where parseSelPats (spat : TSyntax `selPatFrame) : MacroM <| Bool × SelPat := do
+    return ⟨!spat.raw[0].getArgs.isEmpty, ← SelPat.parseOne ⟨spat.raw[1]⟩⟩
 
 #rocq_ignore gallina_ident "Not necessary in Lean"
 #rocq_ignore intro_pat.big_conj "Not necessary in Lean"
diff --git a/Iris/Iris/ProofMode/Patterns/ProofModeTerm.lean b/Iris/Iris/ProofMode/Patterns/ProofModeTerm.lean
index 73eec6df9..468c94eb3 100644
--- a/Iris/Iris/ProofMode/Patterns/ProofModeTerm.lean
+++ b/Iris/Iris/ProofMode/Patterns/ProofModeTerm.lean
@@ -16,7 +16,7 @@ open Lean
 declare_syntax_cat pmTerm
 
 syntax term : pmTerm
-syntax term colGt " $$ " (colGt specPat)+ : pmTerm
+syntax term colGt " $$ " (colGt ppSpace specPat)+ : pmTerm
 
 @[rocq_alias iTrm]
 structure PMTerm where
diff --git a/Iris/Iris/ProofMode/Patterns/SelPattern.lean b/Iris/Iris/ProofMode/Patterns/SelPattern.lean
index 588426efb..8449df66a 100644
--- a/Iris/Iris/ProofMode/Patterns/SelPattern.lean
+++ b/Iris/Iris/ProofMode/Patterns/SelPattern.lean
@@ -15,9 +15,13 @@ open Lean Meta Std
 declare_syntax_cat selPat
 
 syntax ident : selPat
+/-- Choose all hypothesis from the pure context. -/
 syntax "%" : selPat
+/-- Choose a specific hypothesis from the pure context. -/
 syntax "%" noWs ident : selPat
+/-- Choose all hypotheses in the intuitionistic context. -/
 syntax "#" : selPat
+/-- Choose all hypotheses in the spatial context. -/
 syntax "∗" : selPat
 
 @[rocq_alias sel_pat]
@@ -69,6 +73,7 @@ def SelPat.resolveOne (hyps : Hyps bi e) : SelPat → ProofModeM (List SelTarget
       return [⟨.ipm ivar, true⟩]
   | .leanIdent name => do
       let ldecl ← getLocalDeclFromUserName name.getId
+      addLocalVarInfo name (← getLCtx) ldecl.toExpr ldecl.type
       return [⟨.pure ldecl.fvarId, true⟩]
   | .intuitionistic =>
       return hyps.intuitionisticIVarIds.map (⟨.ipm ·, false⟩)
diff --git a/Iris/Iris/ProofMode/Porting.lean b/Iris/Iris/ProofMode/Porting.lean
index dad0da8f9..3fcdea6d0 100644
--- a/Iris/Iris/ProofMode/Porting.lean
+++ b/Iris/Iris/ProofMode/Porting.lean
@@ -27,7 +27,7 @@ import Iris.Std.RocqPorting
 #rocq_concept proofmode "Tactics" "iAssumptionCoq" ignored "weird tactic"
 #rocq_concept proofmode "Tactics" "iExFalso" ported "iexfalso"
 #rocq_concept proofmode "Tactics" "iPure (basic)" ported "ipure"
-#rocq_concept proofmode "Tactics" "iPure (pure destructuring patterns)" missing "(also for other tactics using ipure)"
+#rocq_concept proofmode "Tactics" "iPure (pure destructuring patterns)" ported "ipure ... as ..."
 #rocq_concept proofmode "Tactics" "iEmpIntro" ported "iempintro"
 #rocq_concept proofmode "Tactics" "iPureIntro" ported "ipureintro"
 #rocq_concept proofmode "Tactics" "iFrame (basic)" ported "iframe"
@@ -59,7 +59,7 @@ import Iris.Std.RocqPorting
 #rocq_concept proofmode "Tactics" "iAccu" missing ""
 #rocq_concept proofmode "Tactics" "rules for trivial" ported "itrivial"
 
-#rocq_concept proofmode "Intro Patterns" missing ""
+#rocq_concept proofmode "Intro Patterns" ported ""
 #rocq_concept proofmode "Intro Patterns" "IIdent (pattern: H)" ported "pattern: H"
 #rocq_concept proofmode "Intro Patterns" "IFresh (pattern: ?)" ported "pattern: _"
 #rocq_concept proofmode "Intro Patterns" "IDrop (pattern: _)" ported "pattern: -"
@@ -70,15 +70,15 @@ import Iris.Std.RocqPorting
 #rocq_concept proofmode "Intro Patterns" "IIntuitionistic (pattern: #H)" ported "pattern: #H"
 #rocq_concept proofmode "Intro Patterns" "ISpatial (pattern: -#H)" ported "pattern: ∗H"
 #rocq_concept proofmode "Intro Patterns" "IModalElim (pattern: >H)" ported "pattern: >H"
-#rocq_concept proofmode "Intro Patterns" "IRewrite (pattern: ->/<-)" missing ""
-#rocq_concept proofmode "Intro Patterns" "IPureIntro (pattern: !%)" missing ""
+#rocq_concept proofmode "Intro Patterns" "IRewrite (pattern: ->/<-)" ported "pattern: →/←"
+#rocq_concept proofmode "Intro Patterns" "IPureIntro (pattern: !%)" ported "pattern: !%"
 #rocq_concept proofmode "Intro Patterns" "IModalIntro (pattern: !>)" ported "pattern: !>"
-#rocq_concept proofmode "Intro Patterns" "ISimpl (pattern: /=)" missing ""
+#rocq_concept proofmode "Intro Patterns" "ISimpl (pattern: /=)" ported "pattern: /="
 #rocq_concept proofmode "Intro Patterns" "IDone (pattern: //)" ported "pattern: //"
-#rocq_concept proofmode "Intro Patterns" "IForall (pattern: *)" missing ""
-#rocq_concept proofmode "Intro Patterns" "IAll (pattern: **)" missing ""
-#rocq_concept proofmode "Intro Patterns" "IClear (pattern: {selpat})" missing ""
-#rocq_concept proofmode "Intro Patterns" "IClearFrame (pattern: {$selpat})" missing ""
+#rocq_concept proofmode "Intro Patterns" "IForall (pattern: *)" ported "pattern: *"
+#rocq_concept proofmode "Intro Patterns" "IAll (pattern: **)" ported "pattern: **"
+#rocq_concept proofmode "Intro Patterns" "IClear (pattern: {selpat})" ported "pattern: { H, ... }"
+#rocq_concept proofmode "Intro Patterns" "IClearFrame (pattern: {$selpat})" ported "pattern: { !H, ... }"
 
 #rocq_concept proofmode "Specialization Patterns" missing ""
 #rocq_concept proofmode "Specialization Patterns" "SIdent (pattern: H)" ported "pattern: H"
diff --git a/Iris/Iris/ProofMode/Tactics/Cases.lean b/Iris/Iris/ProofMode/Tactics/Cases.lean
index 9f5ec3854..519cb2599 100644
--- a/Iris/Iris/ProofMode/Tactics/Cases.lean
+++ b/Iris/Iris/ProofMode/Tactics/Cases.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, Mario Carneiro, Michael Sammler, Yunsong Yang
+Authors: Lars König, Mario Carneiro, Michael Sammler, Yunsong Yang, Alvin Tang
 -/
 module
 
@@ -64,29 +64,31 @@ public meta section
 open Lean Elab Tactic Meta Qq Std
 
 private def iCasesEmptyConj {prop : Q(Type u)} (bi : Q(BI $prop))
-    {P} (_hyps : Hyps bi P) (p : Q(Bool)) (A goal : Q($prop)) :
+    {P} (_hyps : Hyps bi P) (p : Q(Bool)) (A goal : Q($prop)) (tacName : String) :
     ProofModeM (Q($P ∗ □?$p $A ⊢ $goal)) := do
   if let .defEq _ ← isDefEqQ A q(iprop(False)) then
     return q(false_elim')
   else
-    throwError "icases: cannot destruct {A} as an empty conjunct"
+    throwError "{tacName}: cannot destruct {A} as an empty conjunct"
 
 /-- Destruct an existential hypothesis [A] by introducing its witness and continuing with the body [B]. -/
-private def iCasesExists {prop : Q(Type u)} (bi : Q(BI $prop)) (name : TSyntax ``binderIdent)
-    (p : Q(Bool)) (P A goal : Q($prop))
+private def iCasesExists {prop : Q(Type u)} {bi : Q(BI $prop)} (pat : TSyntax `rcasesPat)
+    (p : Q(Bool)) (P A goal : Q($prop)) (tacName : String)
     (k : (B : Q($prop)) → ProofModeM Q($P ∗ □?$p $B ⊢ $goal)) :
     ProofModeM (Q($P ∗ □?$p $A ⊢ $goal)) := do
   let v ← mkFreshLevelMVar
   let α : Q(Sort v) ← mkFreshExprMVarQ q(Sort v)
   let Φ : Q($α → $prop) ← mkFreshExprMVarQ q($α → $prop)
   let .some _ ← ProofModeM.trySynthInstanceQ q(IntoExists $A $Φ)
-    | throwError "icases: {A} is not an existential quantifier"
-  let (name, ref) ← getFreshName name
-  withLocalDeclDQ name α fun x => do
-    addLocalVarInfo ref (← getLCtx) x α
-    have B : Q($prop) := Expr.headBeta q($Φ $x)
-    let pf : Q(∀ x, $P ∗ □?$p $Φ x ⊢ $goal) ← mkLambdaFVars #[x] <|← k B
-    return q(exists_elim' $pf)
+  | throwError "{tacName}: {A} is not an existential quantifier"
+  let pf : Q(∀ x, $P ∗ □?$p $Φ x ⊢ $goal) ←
+    iPureDestruct q(∀ x, $P ∗ □?$p $Φ x ⊢ $goal) pat fun g => do
+      let B : Q($prop) ← mkFreshExprMVarQ q($prop)
+      let eq ← isDefEq (← g.getType) q($P ∗ □?$p $B ⊢ $goal)
+      if !eq then
+        throwError "{tacName}: unexpected goal {goal} after intro pattern"
+      k (Expr.headBeta (← instantiateMVars B))
+  return q(exists_elim' $pf)
 
 /-- Destruct a conjunction hypothesis [A] and continue with only its left or right component. -/
 private def iCasesAndLR {prop : Q(Type u)} (bi : Q(BI $prop))
@@ -101,8 +103,8 @@ private def iCasesAndLR {prop : Q(Type u)} (bi : Q(BI $prop))
   else return some q(sep_and_elim_l $(← k A1))
 
 /-- Destruct a conjunction hypothesis [A] into two parts and continue with the left and right subpatterns in sequence. -/
-private def iCasesSep {prop : Q(Type u)} (bi : Q(BI $prop))
-    {P} (hyps : Hyps bi P) (p : Q(Bool)) (A goal : Q($prop))
+private def iCasesSep {prop : Q(Type u)} {bi : Q(BI $prop)}
+    {P} (hyps : Hyps bi P) (p : Q(Bool)) (A goal : Q($prop)) (tacName : String)
     (k : ∀ {P}, Hyps bi P → (goal : Q($prop)) → ProofModeM Q($P ⊢ $goal))
     (k1 k2 : ∀ {P}, Hyps bi P → (goal B : Q($prop)) →
       (∀ {P}, Hyps bi P → (goal : Q($prop)) → ProofModeM Q($P ⊢ $goal)) →
@@ -113,62 +115,62 @@ private def iCasesSep {prop : Q(Type u)} (bi : Q(BI $prop))
   match matchBool p with
   | .inl _ =>
     let .some _ ← ProofModeM.trySynthInstanceQ q(IntoAnd $p $A $A1 $A2)
-      | throwError "icases: cannot destruct {A}"
+      | throwError "{tacName}: cannot destruct {A}"
     let goal' := q(iprop(□ $A2 -∗ $goal))
     let pf ← k1 hyps goal' A1 fun hyps goal' => do
       let goal'' ← mkFreshExprMVarQ q($prop)
       let .some _ ← ProofModeM.trySynthInstanceQ q(FromWand $goal' .in iprop(□ $A2) $goal'')
-        | throwError "icases: internal error: {goal'} is not a wand"
+        | throwError "{tacName}: internal error: {goal'} is not a wand"
       let pf ← k2 hyps goal'' A2 k
       return q((wand_intro $pf).trans (from_wand .in (Q1:=iprop(□ $A2))))
     return q(and_elim_intuitionistic $pf)
   | .inr _ =>
     let .some _ ← ProofModeM.trySynthInstanceQ q(IntoSep $A $A1 $A2)
-      | throwError "icases: cannot destruct {A}"
+      | throwError "{tacName}: cannot destruct {A}"
     let goal' := q(iprop($A2 -∗ $goal))
     let pf ← k1 hyps goal' A1 fun hyps goal' => do
       let goal'' ← mkFreshExprMVarQ q($prop)
       let .some _ ← ProofModeM.trySynthInstanceQ q(FromWand $goal' .in $A2 $goal'')
-        | throwError "icases: internal error: {goal'} is not a wand"
+        | throwError "{tacName}: internal error: {goal'} is not a wand"
       let pf ← k2 hyps goal'' A2 k
       return q((wand_intro $pf).trans (from_wand .in (Q1:=$A2)))
     return q(sep_elim_spatial (A := $A) $pf)
 
 /-- Destruct a disjunction hypothesis [A] into two cases and continue separately on each branch. -/
-private def iCasesOr {prop : Q(Type u)} (bi : Q(BI $prop))
-    (p : Q(Bool)) (P A goal : Q($prop))
+private def iCasesOr {prop : Q(Type u)} {bi : Q(BI $prop)}
+    (p : Q(Bool)) (P A goal : Q($prop)) (tacName : String)
     (k1 k2 : (B : Q($prop)) → ProofModeM Q($P ∗ □?$p $B ⊢ $goal)) :
     ProofModeM (Q($P ∗ □?$p $A ⊢ $goal)) := do
   let A1 ← mkFreshExprMVarQ q($prop)
   let A2 ← mkFreshExprMVarQ q($prop)
   let .some _ ← ProofModeM.trySynthInstanceQ q(IntoOr $A $A1 $A2)
-    | throwError "icases: {A} is not a disjunction"
+    | throwError "{tacName}: {A} is not a disjunction"
   return q(or_elim' $(← k1 A1) $(← k2 A2))
 
 /--
 Destruct a persistent hypothesis [A] by turning it into an explicit [□ B] and continuing with
 the persistent body.
 -/
-private def iCasesIntuitionistic {prop : Q(Type u)} (_bi : Q(BI $prop))
-    (p : Q(Bool)) (P A goal : Q($prop))
+private def iCasesIntuitionistic {prop : Q(Type u)} {bi : Q(BI $prop)}
+    (p : Q(Bool)) (P A goal : Q($prop)) (tacName : String)
     (k : (B : Q($prop)) → ProofModeM Q($P ∗ □ $B ⊢ $goal)) :
     ProofModeM (Q($P ∗ □?$p $A ⊢ $goal)) := do
   let B ← mkFreshExprMVarQ q($prop)
   let .some _ ← ProofModeM.trySynthInstanceQ q(IntoPersistently $p $A $B)
-    | throwError "icases: {A} not persistent"
+    | throwError "{tacName}: {A} not persistent"
   match matchBool p with
   | .inl _ =>
     return q(intuitionistic_elim_intuitionistic $(← k B))
   | .inr _ =>
     let .some _ ← trySynthInstanceQ q(TCOr (Affine $A) (Absorbing $goal))
-      | throwError "icases: {A} not affine and the goal not absorbing"
+      | throwError "{tacName}: {A} not affine and the goal not absorbing"
     return q(intuitionistic_elim_spatial (A := $A) $(← k B))
 
 /--
 Destruct an affine/spatial hypothesis [A] by removing the affinely wrapper and continuing with
 the spatial body.
 -/
-private def iCasesSpatial {prop : Q(Type u)} (_bi : Q(BI $prop))
+private def iCasesSpatial {prop : Q(Type u)} {bi : Q(BI $prop)}
     (p : Q(Bool)) (P A goal : Q($prop))
     (k : (B : Q($prop)) → ProofModeM Q($P ∗ $B ⊢ $goal)) :
     ProofModeM (Q($P ∗ □?$p $A ⊢ $goal)) := do
@@ -195,65 +197,68 @@ possibly an updated goal.
 ## Returns
 A proof of `hyps ∗ □?p A ⊢ goal`.
 -/
-partial def iCasesCore {P} (hyps : Hyps bi P) (goal : Q($prop)) (pat : iCasesPat)
-    (p : Q(Bool)) (A : Q($prop))
+partial def iCasesCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {P}
+    (hyps : Hyps bi P) (goal : Q($prop)) (pat : iCasesPat)
+    (p : Q(Bool)) (A : Q($prop)) (tacName : String)
     (k : ∀ {P}, Hyps bi P → (goal' : Q($prop)) → ProofModeM Q($P ⊢ $goal') := addBIGoal) :
     ProofModeM (Q($P ∗ □?$p $A ⊢ $goal)) :=
+  withRef pat.ref do
   match pat with
-  | .one name => do
-    -- TODO: use Hyps.addWithInfo here?
-    let (name, ref) ← getFreshName name
-    let ivar ← mkFreshIVarId (isTrue p)
-    addHypInfo ref name ivar prop A (isBinder := true)
-    let hyp := .mkHyp bi name ivar p A
-    if let .emp _ := hyps then pure q(of_emp_sep $(← k hyp goal))
-    else k (.mkSep hyps hyp) goal
-
-  | .clear => do
-    let pf ← iClearCore bi q(iprop($P ∗ □?$p $A)) P p A goal q(.rfl)
+  | .one _ name => do
+    let ⟨_, _, hyps', pfEq⟩ ← Hyps.addWithInfo bi name p A hyps
+    let pf ← k hyps' goal
+    return q($(pfEq).mp.trans $pf)
+
+  | .clear _ =>
+    let pf ← iClearCoreOne bi q(iprop($P ∗ □?$p $A)) P p A goal q(.rfl) tacName
     pure q($pf $(← k hyps goal))
 
-  | .frame => do
-    let ⟨ivar, hyps'⟩ ← Hyps.addWithInfo bi (← `(binderIdent | _)) p A hyps
-    let res ← iFrame bi _ hyps' goal [⟨.ipm ivar, true⟩]
-    res.finish @k
+  | .frame _ =>
+    let ⟨ivar, _, hyps', pfEq⟩ ← Hyps.addWithInfo bi (← `(binderIdent | _)) p A hyps
+    let res ← iFrame hyps' goal [⟨.ipm ivar, true⟩]
+    let pf ← res.finish k
+    return q($(pfEq).mp.trans $pf)
 
-  | .conjunction [arg] | .disjunction [arg] => iCasesCore hyps goal arg p A @k
+  | .conjunction _ [arg] | .disjunction _ [arg] =>
+    iCasesCore hyps goal arg p A tacName k
 
-  | .disjunction [] => throwUnsupportedSyntax
+  | .disjunction _ [] => throwUnsupportedSyntax
 
-  | .conjunction [] => iCasesEmptyConj bi hyps p A goal
+  | .conjunction _ [] => iCasesEmptyConj bi hyps p A goal tacName
 
   -- pure conjunctions are always handled as existentials. There is `intoExist_and_pure` and
   -- `intoExist_sep_pure` to make this work as expected for pure assertions that are not explicit existentials.
-  | .conjunction (.pure arg :: args) => do
-    iCasesExists bi arg p P A goal (iCasesCore hyps goal (.conjunction args) p · k)
-  | .conjunction (arg :: args) => do
-    if arg matches .clear then
+  | .conjunction ref (.pure _ arg :: args) =>
+    iCasesExists arg p P A goal tacName (iCasesCore hyps goal (.conjunction ref args) p · tacName k)
+  | .conjunction ref (arg :: args) =>
+    if arg matches .clear _ then
       if let some pf ← iCasesAndLR bi p P A goal true λ B =>
-        iCasesCore hyps goal (.conjunction args) p B @k then return pf
-    if args matches [.clear] then
+        iCasesCore hyps goal (.conjunction ref args) p B tacName  k then return pf
+    if args matches [.clear _] then
       if let some pf ← iCasesAndLR bi p P A goal false λ B =>
-        iCasesCore hyps goal arg p B @k then return pf
-    iCasesSep bi hyps p A goal @k (iCasesCore · · arg p · ·)
-      (iCasesCore · · (.conjunction args) p · ·)
+        iCasesCore hyps goal arg p B tacName k then return pf
+    iCasesSep hyps p A goal tacName k (iCasesCore · · arg p · tacName ·)
+      (iCasesCore · · (.conjunction ref args) p · tacName ·)
 
-  | .disjunction (arg :: args) =>
-    iCasesOr bi p P A goal (iCasesCore hyps goal arg p · k)
-      (iCasesCore hyps goal (.disjunction args) p · k)
+  | .disjunction ref (arg :: args) =>
+    iCasesOr p P A goal tacName (iCasesCore hyps goal arg p · tacName k)
+      (iCasesCore hyps goal (.disjunction ref args) p · tacName k)
 
-  | .pure arg => do
-    iPureCore bi q(iprop($P ∗ □?$p $A)) P p A goal arg q(.rfl) λ _ _ => k hyps goal
+  | .pure _ arg =>
+    iPureCore q(iprop($P ∗ □?$p $A)) P p A goal arg q(.rfl) tacName <| k hyps goal
 
-  | .intuitionistic arg =>
-    iCasesIntuitionistic bi p P A goal (iCasesCore hyps goal arg q(true) · @k)
+  | .intuitionistic _ arg =>
+    iCasesIntuitionistic p P A goal tacName (iCasesCore hyps goal arg q(true) · tacName k)
 
-  | .spatial arg =>
-    iCasesSpatial bi p P A goal (iCasesCore hyps goal arg q(false) · @k)
+  | .spatial _ arg =>
+    iCasesSpatial p P A goal (iCasesCore hyps goal arg q(false) · tacName k)
 
-  | .mod arg =>
+  | .mod _ arg =>
     iModCore bi P goal p A λ p' A goal' =>
-      iCasesCore hyps goal' arg p' A @k
+      iCasesCore hyps goal' arg p' A tacName k
+
+  | .rewrite _ forward =>
+    iPureRewriteCore hyps p A goal tacName forward q(.rfl) k
 
 /--
   `icases pmt with pat` destructs `pmt : pmTerm` using the cases pattern `pat`.
@@ -262,7 +267,7 @@ elab "icases" keep:("+keep ")? colGt pmt:pmTerm " with " colGt pat:icasesPat : t
   -- parse syntax
   let pmt ← liftMacroM <| PMTerm.parse pmt
   let pat ← liftMacroM <| iCasesPat.parse pat
-  ProofModeM.runTactic λ mvar { bi, goal, hyps, .. } => do
+  ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
 
   -- We keep the persistent hypothesis if it is required by the user (+keep is set by ihave)
   -- or if we perform specialization
@@ -270,7 +275,7 @@ elab "icases" keep:("+keep ")? colGt pmt:pmTerm " with " colGt pat:icasesPat : t
     (try_dup_context := pat.should_try_dup_context)
 
   -- process pattern
-  let pf2 ← iCasesCore bi hyps goal pat p A
+  let pf2 ← iCasesCore hyps goal pat p A "icases"
 
   mvar.assign q(($pf).trans $pf2)
 
diff --git a/Iris/Iris/ProofMode/Tactics/Clear.lean b/Iris/Iris/ProofMode/Tactics/Clear.lean
index 8ec4be8a8..ffa84ac6b 100644
--- a/Iris/Iris/ProofMode/Tactics/Clear.lean
+++ b/Iris/Iris/ProofMode/Tactics/Clear.lean
@@ -25,14 +25,14 @@ theorem clear_intuitionistic [BI PROP] {P P' A Q : PROP}
 public meta section
 open Lean Elab Tactic Meta Qq
 
-def iClearCore {prop : Q(Type u)} (_bi : Q(BI $prop)) (e e' : Q($prop))
-    (p : Q(Bool)) (out goal : Q($prop))
-    (pf : Q($e ⊣⊢ $e' ∗ □?$p $out)) : ProofModeM Q(($e' ⊢ $goal) → $e ⊢ $goal) := do
+def iClearCoreOne {prop : Q(Type u)} (_bi : Q(BI $prop)) (e e' : Q($prop))
+    (p : Q(Bool)) (out goal : Q($prop)) (pf : Q($e ⊣⊢ $e' ∗ □?$p $out))
+    (tacName : String) : ProofModeM Q(($e' ⊢ $goal) → $e ⊢ $goal) := do
     match matchBool p with
     | .inl _ => return q(clear_intuitionistic (Q := $goal) $pf)
     | .inr _ =>
       let .some _ ← trySynthInstanceQ q(TCOr (Affine $out) (Absorbing $goal))
-        | throwError "iclear: {out} is not affine and the goal not absorbing"
+        | throwError "{tacName}: {out} is not affine and the goal not absorbing"
       return q(clear_spatial (A:=$out) $pf)
 
 private structure ClearState {u} {prop : Q(Type u)} {bi : Q(BI $prop)} (origE goal : Q($prop)) where
@@ -40,32 +40,40 @@ private structure ClearState {u} {prop : Q(Type u)} {bi : Q(BI $prop)} (origE go
   pf : Q(($e ⊢ $goal) → ($origE ⊢ $goal))
 
 private def ClearState.clearProofModeHyp {u prop bi origE goal} :
-    @ClearState u prop bi origE goal → IVarId →
+    @ClearState u prop bi origE goal → String → IVarId →
     ProofModeM (@ClearState u prop bi origE goal)
-  | { e, hyps, pf }, ivar => do
+  | { e, hyps, pf }, tacName, ivar => do
       let ⟨e', hyps', _, out', p, _, hrem⟩ := hyps.remove true ivar
-      let step ← iClearCore bi e e' p out' goal hrem
+      let step ← iClearCoreOne bi e e' p out' goal hrem tacName
       let pf' : Q(($e' ⊢ $goal) → ($origE ⊢ $goal)) := q(λ h => $pf ($step h))
       return {  e := e', hyps := hyps', pf := pf' }
 
-/--
-  `iclear pats` discards the hypotheses selected by the selection pattern `pats`.
--/
-elab "iclear " pats:(colGt ppSpace selPat)+ : tactic => do
-  let pats ← liftMacroM <| SelPat.parse pats
-
-  ProofModeM.runTactic λ mvar { e, hyps, goal, .. } => do
+def iClearCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
+    (hyps : Hyps bi e) (goal : Q($prop)) (pats : List SelPat)
+    (k : ∀ {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e : Q($prop)}
+      (_ : Hyps bi e) (goal : Q($prop)) (_ : Array FVarId), ProofModeM Q($e ⊢ $goal)) :
+    ProofModeM Q($e ⊢ $goal) := do
   let (ivars, fvars) := (← SelPat.resolve hyps pats).partitionMap fun
-    | {kind := .ipm ivar, ..} => .inl ivar
-    | {kind := .pure id,  ..} => .inr id
+  | {kind := .ipm ivar, ..} => .inl ivar
+  | {kind := .pure id,  ..} => .inr id
 
   -- Clear the selected Iris hypotheses first, updating the proof-mode context and proof term.
-  let mut st : ClearState e goal := { e, hyps, pf := q(fun h => h) }
-  for ivar in ivars do st ← st.clearProofModeHyp ivar
+  let mut st : ClearState e goal := { e, hyps, pf := q(id) }
+  for ivar in ivars do st ← st.clearProofModeHyp "iclear" ivar
 
   -- Lean locals are cleared afterwards; first ensure no remaining hypothesis or goal depends on them.
   for fvar in fvars do
     let _ ← st.hyps.checkRemovableFVar "iclear" fvar (some goal) fvars.contains
 
-  let pf' ← addBIGoalWithoutFVars st.hyps goal fvars.reverse.toArray
-  mvar.assign q($(st.pf) $pf')
+  let pf' ← k st.hyps goal fvars.reverse.toArray
+  return q($(st.pf) $pf')
+
+/--
+  `iclear pats` discards the hypotheses selected by the selection pattern `pats`.
+-/
+elab "iclear " pats:(colGt ppSpace selPat)+ : tactic => do
+  let pats ← liftMacroM <| SelPat.parse pats
+
+  ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
+    let pf ← iClearCore hyps goal pats (addBIGoalWithoutFVars · ·)
+    mvar.assign pf
diff --git a/Iris/Iris/ProofMode/Tactics/Combine.lean b/Iris/Iris/ProofMode/Tactics/Combine.lean
index 1b5cca40b..1fdd2cdbe 100644
--- a/Iris/Iris/ProofMode/Tactics/Combine.lean
+++ b/Iris/Iris/ProofMode/Tactics/Combine.lean
@@ -12,8 +12,8 @@ public meta import Iris.ProofMode.ClassesMake
 
 namespace Iris.ProofMode
 
-public meta section
-open Lean Elab Tactic Meta Qq BI Std
+public section
+open BI Std
 
 /-- Auxiliary lemma for combining two hypotheses using `CombineSepAs` -/
 theorem combine_as_step [BI PROP] {p1 p2 : Bool} {e e1 e2 out1 out2 out : PROP}
@@ -95,6 +95,9 @@ theorem combine_as_gives [BI PROP] {p : Bool} {newE e outAs outGives goal : PROP
   _ ⊢ newE ∗ □?p (outAs ∗ □ outGives)   := sep_mono_right intuitionisticallyIf_sep_mpr
   _ ⊢ goal := pfAsGives
 
+public meta section
+open Lean Elab Tactic Meta Qq BI Std
+
 /--
   The `icombine` tactic with the `as` syntax transforms the hypotheses
   corresponding to `origE` into `newE ∗ □?$p $outAs`, where `outAs` is the
@@ -228,7 +231,7 @@ elab "icombine " patSels:(colGt ppSpace selPat)*
     let hs ← iCombineParseSelPats hyps patSels
     let st ← iCombineCore hs hyps goal
 
-    let pf ← iCasesCore _ st.newHyps goal pat q($(st.p)) st.outAs addBIGoal
+    let pf ← iCasesCore st.newHyps goal pat q($(st.p)) st.outAs "icombine"
     mvar.assign q($(st.pfAs).trans $pf)
 
 /--
@@ -250,7 +253,7 @@ elab "icombine " patSels:(colGt ppSpace selPat)*
 
     match st.outGives, st.pfGives with
     | some outGives, pfGives =>
-      let pf ← iCasesCore _ hyps goal pat q(true) outGives addBIGoal
+      let pf ← iCasesCore hyps goal pat q(true) outGives "icombine"
       mvar.assign q($(pfGives).trans $pf)
     | none, _ => throwNoInstanceForGives
 
@@ -279,7 +282,7 @@ elab "icombine " patSels:(colGt ppSpace selPat)*
 
     match st.outGives, st.pfGives with
     | some outGives, pfGives =>
-      let pf ← iCasesCore _ st.newHyps goal (.conjunction [pat1, .intuitionistic pat2])
-        q($st.p) q(iprop($st.outAs ∗ □ $outGives)) addBIGoal
+      let pf ← iCasesCore st.newHyps goal (.conjunction pat1.ref [pat1, .intuitionistic pat2.ref pat2])
+        q($st.p) q(iprop($st.outAs ∗ □ $outGives)) "icombine"
       mvar.assign q(combine_as_gives $st.pfAs $pfGives $pf)
     | none, _ => throwNoInstanceForGives
diff --git a/Iris/Iris/ProofMode/Tactics/Frame.lean b/Iris/Iris/ProofMode/Tactics/Frame.lean
index af5be77c3..371bcadd4 100644
--- a/Iris/Iris/ProofMode/Tactics/Frame.lean
+++ b/Iris/Iris/ProofMode/Tactics/Frame.lean
@@ -86,7 +86,7 @@ private def FrameResult.step {u prop bi origE origGoal} :
     else
       return st
 
-def iFrame {prop : Q(Type u)} (bi : Q(BI $prop)) (e : Q($prop))
+def iFrame {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e : Q($prop)}
     (hyps : Hyps bi e) (goal : Q($prop)) (sels : List SelTarget) :
     ProofModeM (FrameResult bi e goal) := do
   let mut st : FrameResult bi e goal := { progress := false, e, hyps, goal, pf := q(frame_init) }
@@ -136,10 +136,10 @@ def FrameResult.finishClose {u prop bi origE origGoal} (res : @FrameResult u pro
 elab "iframe " pats:(colGt ppSpace selPat)+ : tactic => do
   let pats ← liftMacroM <| SelPat.parse pats
 
-  ProofModeM.runTactic λ mvar { bi, e, hyps, goal, .. } => do
+  ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
   let pats ← SelPat.resolve hyps pats
 
-  let res ← iFrame bi e hyps goal pats
+  let res ← iFrame hyps goal pats
   mvar.assign (← res.finish (addBIGoal · ·))
 
 /--
diff --git a/Iris/Iris/ProofMode/Tactics/Have.lean b/Iris/Iris/ProofMode/Tactics/Have.lean
index 3c97cd888..c40cf96a5 100644
--- a/Iris/Iris/ProofMode/Tactics/Have.lean
+++ b/Iris/Iris/ProofMode/Tactics/Have.lean
@@ -36,9 +36,9 @@ macro "ihave " colGt pat:icasesPat " := " pmt:pmTerm : tactic => `(tactic | icas
 elab "ihave " colGt pat:icasesPat " : " P:term " $$ " spat:specPat : tactic => do
   let spat ← liftMacroM <| SpecPat.parse spat
   let pat ← liftMacroM <| iCasesPat.parse pat
-  ProofModeM.runTactic λ mvar { prop, bi, hyps, goal, .. } => do
+  ProofModeM.runTactic λ mvar { prop, hyps, goal, .. } => do
   let P ← elabTermEnsuringTypeQ (← `(iprop($P))) prop
   --  establish `P` with `spat`
   let ⟨_, hyps', p, A, pf⟩ ← iSpecializeCore hyps q(true) q(iprop($P -∗ $P)) [spat] (try_dup_context := pat.should_try_dup_context)
-  let pf2 ← iCasesCore bi hyps' goal pat p A
+  let pf2 ← iCasesCore hyps' goal pat p A "ihave"
   mvar.assign q(ihave_assert (($pf).trans $pf2))
diff --git a/Iris/Iris/ProofMode/Tactics/Intro.lean b/Iris/Iris/ProofMode/Tactics/Intro.lean
index f6cf3fd62..e2e502742 100644
--- a/Iris/Iris/ProofMode/Tactics/Intro.lean
+++ b/Iris/Iris/ProofMode/Tactics/Intro.lean
@@ -1,12 +1,13 @@
 /-
 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, Michael Sammler
+Authors: Lars König, Mario Carneiro, Michael Sammler, Alvin Tang
 -/
 module
 
 public meta import Iris.ProofMode.Patterns.IntroPattern
 public meta import Iris.ProofMode.Tactics.Cases
+public meta import Iris.ProofMode.Tactics.Pure
 public meta import Iris.ProofMode.Tactics.ModIntro
 public meta import Iris.ProofMode.Tactics.Trivial
 
@@ -53,6 +54,34 @@ theorem wand_intro_spatial [BI PROP] {P Q A1 A2 : PROP}
 public meta section
 open Lean Elab Tactic Meta Qq BI Std
 
+/--
+  Used by `iIntroCore` for the cases `.intro (.pure …)`, `.intro (.rewrite …)`,
+  `.all` and `.allwand`.
+
+  The function `k'` is the fallback option when type class synthesis with `Q`
+  using `FromForall` fails. The fallback option is applicable only for
+  `.all` and `.allwand`.
+-/
+private def iIntroCoreForallIntro {u} {prop : Q(Type u)} {bi : Q(BI $prop)}
+    {P : Q($prop)} (ref : Syntax) (n : Option <| TSyntax ``binderIdent)
+    (Q : Q($prop)) (tacName : String) (k' : Option <| ProofModeM Q($P ⊢ $Q))
+    (k : Q($prop) → (B : Q($prop)) → ProofModeM Q($P ⊢ $B)) :
+    ProofModeM Q($P ⊢ $Q) := do
+  let ⟨n, _⟩ ← getFreshName <| n.getD (← `(binderIdent| _))
+  let v ← mkFreshLevelMVar
+  let α ← mkFreshExprMVarQ q(Sort v)
+  let Φ ← mkFreshExprMVarQ q($α → $prop)
+  match ← ProofModeM.trySynthInstanceQ q(FromForall $Q $Φ), k' with
+  | none, none =>
+    throwError "{tacName}: {Q} cannot be turned into a universal quantifier or pure hypothesis"
+  | none, some k' => k'
+  | some _, _ =>
+    withLocalDeclDQ n α fun x => do
+      addLocalVarInfo ref (← getLCtx) x α
+      have B : Q($prop) := Expr.headBeta q($Φ $x)
+      let pf : Q(∀ x, $P ⊢ $Φ x) ← mkLambdaFVars #[x] <|← k x B
+      return q(from_forall_intro $pf)
+
 /--
 Introduce the hypothesis specified by `pats` into the context given by `P` (structured  as `hyps`).
 The type of the current goal is given by `Q`.
@@ -60,72 +89,120 @@ The type of the current goal is given by `Q`.
 This function returns the proof of `P ⊢ Q` to be assigned. The new context is included in the
 `goals` directly by the tactic.
 -/
-partial def iIntroCore {prop : Q(Type u)} {bi : Q(BI $prop)}
-  {P} (hyps : Hyps bi P) (Q : Q($prop)) (pats : List (Syntax × IntroPat))
-  (k : ∀ {prop : Q(Type $u)} {bi : Q(BI $prop)} {e : Q($prop)}, Hyps bi e → (goal: Q($prop)) → ProofModeM Q($e ⊢ $goal) := addBIGoal) :
+partial def iIntroCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)}
+  {P} (hyps : Hyps bi P) (Q : Q($prop)) (pats : List (Syntax × IntroPat)) (tacName : String)
+  (k : ∀ {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e : Q($prop)}, Hyps bi e → (goal: Q($prop)) → ProofModeM Q($e ⊢ $goal) := addBIGoal) :
     ProofModeM (Q($P ⊢ $Q)) := do
   match pats with
   | [] => k hyps Q
-  | (ref, .modintro) :: pats =>
-    withRef ref do
-    iModIntroCore hyps Q (← `(_)) (iIntroCore · · pats k)
-  | (ref, .trivial) :: pats =>
-    withRef ref do
-    if let some r ← iTrivial hyps Q then
-      return r
-    else
-      iIntroCore hyps Q pats k
-  | (ref, .intro (.pure n)) :: pats =>
-    withRef ref do
-    let v ← mkFreshLevelMVar
-    let α ← mkFreshExprMVarQ q(Sort v)
-    let Φ ← mkFreshExprMVarQ q($α → $prop)
-    let .some _ ← ProofModeM.trySynthInstanceQ q(FromForall $Q $Φ)
-      | throwError "iintro: {Q} cannot be turned into a universal quantifier or pure hypothesis"
-    let (n, ref) ← getFreshName n
-    withLocalDeclDQ n α fun x => do
-      addLocalVarInfo ref (← getLCtx) x α
-      have B : Q($prop) := Expr.headBeta q($Φ $x)
-      have : $B =Q $Φ $x := ⟨⟩
-      let pf : Q(∀ x, $P ⊢ $Φ x) ← mkLambdaFVars #[x] <|← iIntroCore hyps B pats k
+  | (ref, pat) :: pats =>
+    withRef ref do match pat with
+    | .modintro =>
+      iModIntroCore hyps Q (← `(_)) tacName (iIntroCore · · pats tacName k)
+    | .trivial =>
+      if let some r ← iTrivial hyps Q then
+        return r
+      else
+        iIntroCore hyps Q pats tacName k
+    | .simp =>
+      let simpCtx ← Simp.mkContext (simpTheorems := #[← getSimpTheorems])
+      let ⟨Q', _⟩ ← Lean.Meta.dsimp Q simpCtx #[← Simp.getSimprocs]
+      iIntroCore hyps Q' pats tacName k
+    | .simptrivial =>
+      iIntroCore hyps Q ((ref, .simp) :: (ref, .trivial) :: pats) tacName k
+    | .all =>
+      iIntroCoreForallIntro ref none Q tacName
+        -- No more universally quantified variable to be introduced
+        (iIntroCore hyps Q pats tacName k)
+        -- Introduction of a universally quantified variable
+        (fun _ B => iIntroCore hyps B ((ref, .all) :: pats) tacName k)
+    | .allwand =>
+      let k' : ProofModeM Q($P ⊢ $Q) := do
+        let A1 ← mkFreshExprMVarQ q($prop)
+        let A2 ← mkFreshExprMVarQ q($prop)
+        let instFromImp ← ProofModeM.trySynthInstanceQ q(FromImp $Q $A1 $A2)
+        let instFromWand ← ProofModeM.trySynthInstanceQ q(FromWand $Q .out $A1 $A2)
+        let instPersistent ← ProofModeM.trySynthInstanceQ q(TCOr (Persistent $A1) (Intuitionistic $P))
+        match instFromWand, instFromImp, instPersistent with
+        -- Introduction of a wand premise or a pure premise, if possible
+        | some _, _, _ | _, some _, some _ =>
+          iIntroCore hyps Q ((ref, .intro (.one ref (← `(binderIdent| _)))) :: (ref, .allwand) :: pats) tacName k
+        | _, _, _ =>
+          -- No more universally quantified variable or premise to be introduced
+          iIntroCore hyps Q pats tacName k
+      -- Introduction of a universally quantified variable
+      iIntroCoreForallIntro ref none Q tacName k'
+        (fun _ B => iIntroCore hyps B ((ref, .allwand) :: pats) tacName k)
+    | .pureintro =>
+      let ⟨pf, m⟩ ← iPureIntroCore bi P Q tacName
+      if pats.isEmpty then
+        addMVarGoal m
+      else
+        let ⟨newM, g⟩ ← startProofMode m
+        let pf' ← newM.withContext <| iIntroCore g.hyps g.goal pats tacName k
+        newM.assign pf'
+      return pf
+    | .clear selPats =>
+      match selPats with
+      | [] => iIntroCore hyps Q pats tacName k
+      | ⟨false, s⟩ :: selPats =>
+        iClearCore hyps Q [s]
+          fun hyps' goal' fvars => withoutFVars (u := 0) fvars
+            <| iIntroCore hyps' goal' ((ref, .clear selPats) :: pats) tacName k
+      | ⟨true, s⟩ :: selPats =>
+        let res ← s.resolveOne hyps >>= iFrame hyps Q
+        res.finish (iIntroCore · · ((ref, .clear selPats) :: pats) tacName k)
+    | .intro (.rewrite _ direction) =>
+      iIntroCoreForallIntro ref none Q tacName none <|
+        fun x B => iPureRewriteCoreAux hyps B x direction tacName (iIntroCore · · pats tacName k)
+    | .intro (.pure _ pat) =>
+      let v ← mkFreshLevelMVar
+      let α ← mkFreshExprMVarQ q(Sort v)
+      let Φ ← mkFreshExprMVarQ q($α → $prop)
+      let .some _ ← ProofModeM.trySynthInstanceQ q(FromForall $Q $Φ)
+      | throwError "{tacName}: {Q} cannot be turned into a universal quantifier or pure hypothesis"
+      let pf : Q(∀ x, $P ⊢ $Φ x) ← iPureDestruct q(∀ x, $P ⊢ $Φ x) pat fun g => do
+        let B : Q($prop) ← mkFreshExprMVarQ q($prop)
+        let eq ← isDefEq (← g.getType) q($P ⊢ $B)
+        if !eq then throwError "{tacName}: internal error: unexpected goal after intro pattern"
+        iIntroCore hyps (Expr.headBeta (← instantiateMVars B)) pats tacName k
       return q(from_forall_intro (Q := $Q) $pf)
-  | (ref, .intro pat) :: pats =>
-    withRef ref do
-    let A1 ← mkFreshExprMVarQ q($prop)
-    let A2 ← mkFreshExprMVarQ q($prop)
-    let fromImp ← ProofModeM.trySynthInstanceQ q(FromImp $Q $A1 $A2)
-    if let (.clear, some _) := (pat, fromImp) then
-      let pf ← iIntroCore hyps A2 pats k
-      return q(imp_intro_drop (Q := $Q) $pf)
-    else
-    let B ← mkFreshExprMVarQ q($prop)
-    match pat, fromImp with
-    | .intuitionistic pat, some _ =>
-      let .some _ ← ProofModeM.trySynthInstanceQ q(IntoPersistently false $A1 $B)
-        | throwError "iintro: {A1} not persistent"
-      let pf ← iCasesCore bi hyps A2 pat q(true) B (iIntroCore · · pats k)
-      return q(imp_intro_intuitionistic (Q := $Q) $pf)
-    | .intuitionistic pat, none =>
-      let .some _ ← ProofModeM.trySynthInstanceQ q(FromWand $Q .out $A1 $A2)
-        | throwError "iintro: {Q} not a wand"
-      let .some _ ← ProofModeM.trySynthInstanceQ q(IntoPersistently false $A1 $B)
-        | throwError "iintro: {A1} not persistent"
-      let .some _ ← trySynthInstanceQ q(TCOr (Affine $A1) (Absorbing $A2))
-        | throwError "iintro: {A1} not affine and the goal not absorbing"
-      let pf ← iCasesCore bi hyps A2 pat q(true) B (iIntroCore · · pats k)
-      return q(wand_intro_intuitionistic (A1 := $A1) (Q := $Q) $pf)
-    | _, some _ =>
-      -- should always succeed
-      let _ ← ProofModeM.synthInstanceQ q(FromAffinely $B $A1)
-      let .some _ ← trySynthInstanceQ q(TCOr (Persistent $A1) (Intuitionistic $P))
-        | throwError "iintro: {A1} is not persistent and spatial context is non-empty"
-      let pf ← iCasesCore bi hyps A2 pat q(false) B (iIntroCore · · pats k)
-      return q(imp_intro_spatial (Q := $Q) $pf)
-    | _, none =>
-      let .some _ ← ProofModeM.trySynthInstanceQ q(FromWand $Q .out $A1 $A2)
-        | throwError "iintro: {Q} not a wand"
-      let pf ← iCasesCore bi hyps A2 pat q(false) A1 (iIntroCore · · pats k)
-      return q(wand_intro_spatial (A1 := $A1) (Q := $Q) $pf)
+    | .intro pat =>
+      let A1 ← mkFreshExprMVarQ q($prop)
+      let A2 ← mkFreshExprMVarQ q($prop)
+      let fromImp ← ProofModeM.trySynthInstanceQ q(FromImp $Q $A1 $A2)
+      if let (.clear _, some _) := (pat, fromImp) then
+        let pf ← iIntroCore hyps A2 pats tacName k
+        return q(imp_intro_drop (Q := $Q) $pf)
+      else
+      let B ← mkFreshExprMVarQ q($prop)
+      match pat, fromImp with
+      | .intuitionistic _ pat, some _ =>
+        let .some _ ← ProofModeM.trySynthInstanceQ q(IntoPersistently false $A1 $B)
+          | throwError "{tacName}: {A1} not persistent"
+        let pf ← iCasesCore hyps A2 pat q(true) B tacName (iIntroCore · · pats tacName k)
+        return q(imp_intro_intuitionistic (Q := $Q) $pf)
+      | .intuitionistic _ pat, none =>
+        let .some _ ← ProofModeM.trySynthInstanceQ q(FromWand $Q .out $A1 $A2)
+          | throwError "{tacName}: {Q} not a wand"
+        let .some _ ← ProofModeM.trySynthInstanceQ q(IntoPersistently false $A1 $B)
+          | throwError "{tacName}: {A1} not persistent"
+        let .some _ ← trySynthInstanceQ q(TCOr (Affine $A1) (Absorbing $A2))
+          | throwError "{tacName}: {A1} not affine and the goal not absorbing"
+        let pf ← iCasesCore hyps A2 pat q(true) B tacName (iIntroCore · · pats tacName k)
+        return q(wand_intro_intuitionistic (A1 := $A1) (Q := $Q) $pf)
+      | _, some _ =>
+        -- should always succeed
+        let _ ← ProofModeM.synthInstanceQ q(FromAffinely $B $A1)
+        let .some _ ← trySynthInstanceQ q(TCOr (Persistent $A1) (Intuitionistic $P))
+          | throwError "{tacName}: {A1} is not persistent and spatial context is non-empty"
+        let pf ← iCasesCore hyps A2 pat q(false) B tacName (iIntroCore · · pats tacName k)
+        return q(imp_intro_spatial (Q := $Q) $pf)
+      | _, none =>
+        let .some _ ← ProofModeM.trySynthInstanceQ q(FromWand $Q .out $A1 $A2)
+          | throwError "{tacName}: {Q} not a wand"
+        let pf ← iCasesCore hyps A2 pat q(false) A1 tacName (iIntroCore · · pats tacName k)
+        return q(wand_intro_spatial (A1 := $A1) (Q := $Q) $pf)
 
 /--
   `iintro pats` introduces hypotheses using the introduction pattern `pats`.
@@ -135,6 +212,6 @@ elab "iintro " pats:(colGt ppSpace introPat)* : tactic => do
   let pats ← liftMacroM <| pats.mapM <| IntroPat.parse
 
   ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
-  let pf ← iIntroCore hyps goal pats.toList
+  let pf ← iIntroCore hyps goal pats.toList "iintro"
 
   mvar.assign pf
diff --git a/Iris/Iris/ProofMode/Tactics/Loeb.lean b/Iris/Iris/ProofMode/Tactics/Loeb.lean
index 06f28ca2a..be5cebbd0 100644
--- a/Iris/Iris/ProofMode/Tactics/Loeb.lean
+++ b/Iris/Iris/ProofMode/Tactics/Loeb.lean
@@ -23,15 +23,15 @@ elab "iloeb" " as " colGt IH:binderIdent " generalizing " hs:(colGt ppSpace selP
   let pats ← Elab.liftMacroM <| SelPat.parse hs
   ProofModeM.runTactic fun mvid {hyps, goal, ..} => do
     let targets : List SelTarget ← SelPat.resolve hyps (pats ++ [.spatial])
-    let expr ← iRevertIntro hyps goal targets fun {prop _ _} hyps goal k => do
+    let expr ← iRevertIntro hyps goal targets "iloeb" fun {prop _ _} hyps goal k => do
       let some _ ← ProofModeM.trySynthInstanceQ q(BI.BILoeb $prop)
         | throwError m!"iloeb: no `{←ppExpr q(BI.BILoeb $prop)}` instance found"
       let pf := q(BI.loeb_wand_intuitionistically (P := $goal))
       let pf' ← do
         -- We have applied BI.loeb_wand_intuitionistically
         let goal := q(iprop(□ (□ ▷ $goal -∗ $goal)))
-        iModIntroCore hyps goal (← `(_)) fun hyps goal => do
-        iIntroCore hyps goal [(IH, .intro <| .intuitionistic <| .one IH)] k
+        iModIntroCore hyps goal (← `(_)) "iloeb" fun hyps goal => do
+        iIntroCore hyps goal [(IH, .intro <| .intuitionistic IH <| .one IH IH)] "iloeb" k
       return q($(pf').trans $pf)
 
     mvid.assign expr
diff --git a/Iris/Iris/ProofMode/Tactics/ModIntro.lean b/Iris/Iris/ProofMode/Tactics/ModIntro.lean
index 9ac73cfde..9044f765f 100644
--- a/Iris/Iris/ProofMode/Tactics/ModIntro.lean
+++ b/Iris/Iris/ProofMode/Tactics/ModIntro.lean
@@ -159,7 +159,8 @@ where go {e}
 # Returns
 Proof term of `hyps ⊢ goal`
 -/
-def iModIntroCore {e} (hyps : @Hyps u prop bi e) (goal : Q($prop)) (sel : TSyntax `term)
+def iModIntroCore {e} (hyps : @Hyps u prop bi e) (goal : Q($prop))
+  (sel : TSyntax `term) (tacName : String)
   (k : ∀ {prop' bi' P}, @Hyps u prop' bi' P → ∀ Q : Q($prop'), ProofModeM Q($P ⊢ $Q) := addBIGoal)
    : ProofModeM (Q($e ⊢ $goal)) := do
     let prop' : Q(Type u) ← mkFreshExprMVarQ q(Type u)
@@ -170,7 +171,7 @@ def iModIntroCore {e} (hyps : @Hyps u prop bi e) (goal : Q($prop)) (sel : TSynta
     let Q ← mkFreshExprMVarQ q($prop')
     -- `M Q ⊢ goal`
     let .some _ ← ProofModeM.trySynthInstanceQ q(@FromModal $prop' $prop $bi' $bi $Φ $M $sel $goal $Q)
-      | throwError "imodintro: {goal} is not a modality{if sel.isMVar then m!"" else m!" matching {sel}"}"
+      | throwError "{tacName}: {goal} is not a modality{if sel.isMVar then m!"" else m!" matching {sel}"}"
     -- show the side condition
     let hΦ ← iSolveSidecondition q($Φ)
     -- perform modality actions, get transformed context `hyps'` and `pf : hyps ⊢ M hyps'`
@@ -186,7 +187,7 @@ def iModIntroCore {e} (hyps : @Hyps u prop bi e) (goal : Q($prop)) (sel : TSynta
 -/
 elab "imodintro " colGt sel:term : tactic => do
   ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
-  let pf ← iModIntroCore hyps goal sel
+  let pf ← iModIntroCore hyps goal sel "imodintro"
 
   mvar.assign pf
 
diff --git a/Iris/Iris/ProofMode/Tactics/Pure.lean b/Iris/Iris/ProofMode/Tactics/Pure.lean
index 6901ce5a2..ff23b600b 100644
--- a/Iris/Iris/ProofMode/Tactics/Pure.lean
+++ b/Iris/Iris/ProofMode/Tactics/Pure.lean
@@ -29,41 +29,141 @@ theorem pure_elim_intuitionistic [BI PROP] {P P' A Q : PROP} {φ : Prop}
     [IntoPure A φ] (h : P ⊣⊢ P' ∗ □ A) (h' : φ → P' ⊢ Q) : P ⊢ Q :=
   pure_elim_spatial h h'
 
+theorem pure_intro_affine [BI PROP] {Q : PROP} {φ : Prop}
+    (h : FromPure true Q .out φ) [Affine P] (hφ : φ) : P ⊢ Q :=
+  (affine.trans (eq_true hφ ▸ affinely_true.2)).trans h.1
+
+theorem pure_intro_spatial [BI PROP] {Q : PROP} {φ : Prop}
+    (h : FromPure false Q .out φ) (hφ : φ) : P ⊢ Q :=
+  (pure_intro hφ).trans h.1
+
 public meta section
 open Lean Elab Tactic Meta Qq
 
-def iPureCore {prop : Q(Type u)} (_bi : Q(BI $prop))
-    (P P' : Q($prop)) (p : Q(Bool)) (A Q : Q($prop)) (name : TSyntax ``binderIdent) (pf : Q($P ⊣⊢ $P' ∗ □?$p $A))
-    (k : (φ : Q(Prop)) → Q($φ) → ProofModeM (Q($P' ⊢ $Q))) : ProofModeM (Q($P ⊢ $Q)) := do
+/--
+  Apply a destruction pattern for pure hypotheses.
+  Then, apply the function `k` to all subgoals generated by the destruction.
+-/
+def iPureDestruct (ty : Q(Prop)) (pat : TSyntax `rcasesPat)
+    (k : MVarId → ProofModeM Expr) : ProofModeM Q($ty) := do
+  let m : Q($ty) ← mkFreshExprSyntheticOpaqueMVar ty
+  let gs ← withRef pat <| Lean.Elab.Tactic.RCases.rintro #[pat] none m.mvarId!
+  for g in gs do
+    g.withContext do g.assign (← k g)
+  instantiateMVars m
+
+/--
+  Rewrite an Iris entailment using the pure Lean equality `h`,
+  removing it from the context afterwards.
+-/
+def iPureRewriteCoreAux {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
+    (hyps : Hyps bi e) (goal : Q($prop)) (h : Expr) (forward : Bool) (tacName : String)
+    (k : ∀ {e'}, Hyps bi e' → (goal' : Q($prop)) → ProofModeM Q($e' ⊢ $goal')) :
+    ProofModeM Q($e ⊢ $goal) := do
+  let target := q($(hyps.tm) ⊢ $goal)
+  let g ← mkFreshExprSyntheticOpaqueMVar target <&> (·.mvarId!)
+  let ⟨newE, eq, []⟩ ← g.rewrite target h !forward
+  | throwError "{tacName}: rewriting should not give additional subgoals"
+  let some #[_, _, newTm, newGoal] := newE.consumeMData.appM? ``BIBase.Entails
+  | throwError "{tacName}: unable to parse the Iris entailment {newE}"
+  let some ⟨_, hyps'⟩ := parseHyps? bi newTm
+  | throwError "{tacName}: unable to parse the Iris context {newTm}"
+  let gNew ← g.replaceTargetEq newE eq
+  -- Apply the continuation function to the new proof goal after rewriting
+  (withoutFVars (u := 0) #[h.fvarId!] <| k hyps' newGoal) >>= (gNew.assign ·)
+  instantiateMVars (.mvar g)
+
+/-- Transform a proof of `φ → (P' ⊢ Q)` into that of `P ⊢ Q`. -/
+def iPureCoreBuildProof {prop : Q(Type u)} {bi : Q(BI $prop)}
+    {P P' : Q($prop)} {p : Q(Bool)} {A Q : Q($prop)} (φ : Q(Prop))
+    (inst : Q(IntoPure $A $φ))
+    (pf : Q($P ⊣⊢ $P' ∗ □?$p $A)) (f : Q($φ → ($P' ⊢ $Q))) (tacName : String) :
+    ProofModeM Q($P ⊢ $Q) := do
+  match matchBool p with
+  | .inl _ => return q(pure_elim_intuitionistic $pf $f)
+  | .inr _ =>
+    let .some _ ← trySynthInstanceQ q(TCOr (Affine $A) (Absorbing $Q))
+    | throwError "{tacName}: {A} is not affine and the goal not absorbing"
+    return q(pure_elim_spatial (A := $A) $pf $f)
+
+/--
+  Introduce a pure equality into the Lean context, use it for rewriting and
+  discard the equality hypothesis.
+-/
+def iPureRewriteCore {prop : Q(Type u)} {bi : Q(BI $prop)} {P P' : Q($prop)}
+    (hyps : Hyps bi P') (p : Q(Bool)) (A Q : Q($prop)) (tacName : String)
+    (forward : Bool) (pf : Q($P ⊣⊢ $P' ∗ □?$p $A))
+    (k : ∀ {e'}, Hyps bi e' → (goal' : Q($prop)) → ProofModeM Q($e' ⊢ $goal')) :
+    ProofModeM Q($P ⊢ $Q) := do
   let φ : Q(Prop) ← mkFreshExprMVarQ q(Prop)
-  let .some _ ← ProofModeM.trySynthInstanceQ q(IntoPure $A $φ)
-    | throwError "ipure: {A} is not pure"
-
-  let (name, ref) ← getFreshName name
-  withLocalDeclDQ name φ fun h => do
-    addLocalVarInfo ref (← getLCtx) h φ
-    let m ← k φ h
-    let f : Q($φ → $P' ⊢ $Q) ← mkLambdaFVars #[h] m
-
-    match matchBool p with
-    | .inl _ =>
-      return (q(pure_elim_intuitionistic $pf $f))
-    | .inr _ =>
-      let .some _ ← trySynthInstanceQ q(TCOr (Affine $A) (Absorbing $Q))
-        | throwError "ipure: {A} is not affine and the goal not absorbing"
-      return q(pure_elim_spatial (A:=$A) $pf $f)
+  let .some inst ← ProofModeM.trySynthInstanceQ q(IntoPure $A $φ)
+  | throwError "{tacName}: {A} is not pure"
+  let m : Q($φ → ($P' ⊢ $Q)) ← mkFreshExprSyntheticOpaqueMVar q($φ → ($P' ⊢ $Q))
+  let (h, g) ← m.mvarId!.intro1
+  let f ← do
+    g.withContext do g.assign (← iPureRewriteCoreAux hyps Q (.fvar h) forward tacName k)
+    instantiateMVars m
+  return ← iPureCoreBuildProof φ inst pf f tacName
+
+def iPureCore {prop : Q(Type u)} {bi : Q(BI $prop)}
+    (P P' : Q($prop)) (p : Q(Bool)) (A Q : Q($prop)) (purePat : TSyntax `rcasesPat)
+    (pf : Q($P ⊣⊢ $P' ∗ □?$p $A)) (tacName : String)
+    (k : ProofModeM Q($P' ⊢ $Q)) : ProofModeM Q($P ⊢ $Q) := do
+  let φ : Q(Prop) ← mkFreshExprMVarQ q(Prop)
+  let some inst ← ProofModeM.trySynthInstanceQ q(IntoPure $A $φ)
+  | throwError "{tacName}: {A} is not pure"
+  let f ← iPureDestruct q($φ → ($P' ⊢ $Q)) purePat <| fun _ => k
+  return ← iPureCoreBuildProof φ inst pf f tacName
+
+def iPureIntroCore {u} {prop : Q(Type u)} (_bi : Q(BI $prop))
+    (e goal : Q($prop)) (tacName : String) :
+    ProofModeM <| Q($e ⊢ $goal) × MVarId := do
+  let b : Q(Bool) ← mkFreshExprMVarQ q(Bool)
+  let φ : Q(Prop) ← mkFreshExprMVarQ q(Prop)
+  let .some h ← ProofModeM.trySynthInstanceQ q(FromPure $b $goal .out $φ)
+  | throwError "{tacName}: {goal} is not pure"
+  let m : Q($φ) ← mkFreshExprSyntheticOpaqueMVar (← instantiateMVars φ)
+
+  let pf : Q($e ⊢ $goal) ← do
+    match ← whnf b with
+    | .const ``true _ =>
+      have : $b =Q true := ⟨⟩
+      let .some _ ← trySynthInstanceQ q(Affine $e)
+        | throwError "{tacName}: context is not affine"
+      pure q(pure_intro_affine (P := $e) (Q := $goal) $h $m)
+    | .const ``false _ =>
+      have : $b =Q false := ⟨⟩
+      pure q(pure_intro_spatial (P := $e) (Q := $goal) $h $m)
+    -- the following indicates a bug in the typeclass instances that generate b
+    | _ => throwError "{tacName}: bug in typeclass instances, cannot reduce {b} to true or false"
+
+  return ⟨pf, m.mvarId!⟩
 
 /--
   `ipure H` moves a pure hypothesis `H` from the Iris context into the regular
   Lean context.
 -/
 elab "ipure " colGt hyp:ident : tactic => do
-  ProofModeM.runTactic λ mvar { bi, e, hyps, goal, .. } => do
+  ProofModeM.runTactic λ mvar { e, hyps, goal, .. } => do
 
   let ivar ← hyps.findWithInfo hyp
   let ⟨e', hyps', _, out', p, _, pf⟩ := hyps.remove true ivar
 
-  let pf ← iPureCore bi e e' p out' goal (← `(binderIdent| $hyp:ident)) pf fun _ _ => addBIGoal hyps' goal
+  let pf ← iPureCore e e' p out' goal (← `(rcasesPat| $hyp:ident)) pf "ipure" <| addBIGoal hyps' goal
+
+  mvar.assign pf
+
+/--
+  `ipure H as pat` moves a pure hypothesis `H` from the Iris context into the
+  regular Lean context and destructs it using the `rcases` destruction pattern.
+-/
+elab "ipure " colGt hyp:ident " as " pat:rcasesPat : tactic => do
+  ProofModeM.runTactic λ mvar { e, hyps, goal, .. } => do
+
+  let ivar ← hyps.findWithInfo hyp
+  let ⟨e', hyps', _, out', p, _, pf⟩ := hyps.remove true ivar
+
+  let pf ← iPureCore e e' p out' goal pat pf "ipure" <| addBIGoal hyps' goal
 
   mvar.assign pf
 
@@ -78,38 +178,14 @@ elab "iempintro" : tactic => do
     | throwError "iempintro: context is not affine"
   mvar.assign q(affine (P := $e))
 
-theorem pure_intro_affine [BI PROP] {Q : PROP} {φ : Prop}
-    (h : FromPure true Q .out φ) [Affine P] (hφ : φ) : P ⊢ Q :=
-  (affine.trans (eq_true hφ ▸ affinely_true.2)).trans h.1
-
-theorem pure_intro_spatial [BI PROP] {Q : PROP} {φ : Prop}
-    (h : FromPure false Q .out φ) (hφ : φ) : P ⊢ Q :=
-  (pure_intro hφ).trans h.1
-
 /--
   `ipureintro` turns a goal of the form `⌜φ⌝` into the Lean goal `φ`.
 -/
 elab "ipureintro" : tactic => do
-  ProofModeM.runTactic λ mvar { e, goal, .. } => do
-
-  let b : Q(Bool) ← mkFreshExprMVarQ q(Bool)
-  let φ : Q(Prop) ← mkFreshExprMVarQ q(Prop)
-  let .some h ← ProofModeM.trySynthInstanceQ q(FromPure $b $goal .out $φ)
-    | throwError "ipureintro: {goal} is not pure"
-  let m : Q($φ) ← mkFreshExprMVar (← instantiateMVars φ)
-  addMVarGoal m.mvarId!
-
-  match ← whnf b with
-  | .const ``true _ =>
-    have : $b =Q true := ⟨⟩
-    let .some _ ← trySynthInstanceQ q(Affine $e)
-      | throwError "ipureintro: context is not affine"
-    mvar.assign q(pure_intro_affine (P := $e) (Q := $goal) $h $m)
-  | .const ``false _ =>
-    have : $b =Q false := ⟨⟩
-    mvar.assign q(pure_intro_spatial (P := $e) (Q := $goal) $h $m)
-  -- the following indicates a bug in the typeclass instances that generate b
-  | _ => throwError "ipureintro: bug in typeclass instances, cannot reduce {b} to true or false"
+  ProofModeM.runTactic λ mvar { bi, e, goal, .. } => do
+    let ⟨pf, m⟩ ← iPureIntroCore bi e goal "ipureintro"
+    addMVarGoal m
+    mvar.assign pf
 
 -- TODO: what is the best lean automation tactic to call here?
 -- `assumption` is necessary if the goal contains mvars
diff --git a/Iris/Iris/ProofMode/Tactics/RevertIntro.lean b/Iris/Iris/ProofMode/Tactics/RevertIntro.lean
index 380de3c6d..7817dc308 100644
--- a/Iris/Iris/ProofMode/Tactics/RevertIntro.lean
+++ b/Iris/Iris/ProofMode/Tactics/RevertIntro.lean
@@ -13,30 +13,30 @@ open Lean Meta Elab.Tactic Qq
 
 public meta section
 
-abbrev ProofModeContinuation (u : Level) :=
-  ∀ {prop : Q(Type u)} {bi : Q(BI $prop)} {e : Q($prop)}
+abbrev ProofModeContinuation :=
+  ∀ {u : Level} {prop : Q(Type u)} {bi : Q(BI $prop)} {e : Q($prop)}
     (_hyps : Hyps bi e)(goal: Q($prop)),
     ProofModeM Q($e ⊢ $goal)
 
 def iRevertIntro
   {prop: Q(Type u)} {bi : Q(BI $prop)} {e : Q($prop)} (hyps : Hyps bi e) (goal: Q($prop))
-  (hs : List SelTarget)
+  (hs : List SelTarget) (tacName : String)
   (k : ∀ {prop : Q(Type u)} {bi : Q(BI $prop)} {e : Q($prop)}
-    (_hyps : Hyps bi e) (goal: Q($prop)), ProofModeContinuation u →
+    (_hyps : Hyps bi e) (goal: Q($prop)), ProofModeContinuation →
     ProofModeM Q($e ⊢ $goal))
    : ProofModeM Q($e ⊢ $goal) := do
   let names : List (Syntax × IntroPat) ← hs.mapM fun
     | {kind := .pure id, ..} => do
       let name ← Lean.mkIdent <$> id.getUserName
-      let ident ← `(binderIdent| $name:ident)
-      return (name, .intro <| .pure ident)
+      let purePat ← `(rcasesPat| $name:ident)
+      return (name, .intro <| .pure purePat purePat)
     | {kind := .ipm ivar, ..} =>  do
       let name ← Lean.mkIdent <$> (hyps.getUserName? ivar).getM
       let ident ← `(binderIdent| $name:ident)
-      return (name, .intro <| (if ivar.persistent? then .intuitionistic else id) <| .one ident)
+      return (name, .intro <| (if ivar.persistent? then .intuitionistic ident else id) <| .one ident ident)
   trace[irevertintro] s!"Calling `iRevertIntro` with {names.map (·.1)} on context {←ppExpr <| IrisGoal.toExpr {hyps, goal ..}}"
   iRevertCore hs hyps goal fun hyps goal => do
   k hyps goal fun hyps goal => do
-  iIntroCore hyps goal names
+  iIntroCore hyps goal names tacName
 
 initialize registerTraceClass `irevertintro
diff --git a/Iris/Iris/ProofMode/Tactics/Specialize.lean b/Iris/Iris/ProofMode/Tactics/Specialize.lean
index 88c7c68da..6af7ef139 100644
--- a/Iris/Iris/ProofMode/Tactics/Specialize.lean
+++ b/Iris/Iris/ProofMode/Tactics/Specialize.lean
@@ -108,7 +108,7 @@ private def processWand :
     let out₂ ← mkFreshExprMVarQ prop
     let some _ ← ProofModeM.trySynthInstanceQ q(IntoWand $p false $out .out $out₁ .out $out₂)
       | throwError m!"ispecialize: {out} is not a wand"
-    let res ← iFrame bi _ hypsr' out₁ (frameIVars.map (⟨.ipm ·, true⟩))
+    let res ← iFrame hypsr' out₁ (frameIVars.map (⟨.ipm ·, true⟩))
     let pf'' ← res.finish λ hyps goal => do
       if trivial then
         let some r ← iTrivial hyps goal
@@ -127,7 +127,7 @@ private def processWand :
     let out₂ ← mkFreshExprMVarQ prop
     let some _ ← ProofModeM.trySynthInstanceQ q(IntoWand $p false $out .out $out₁ .out $out₂)
       | throwError m!"ispecialize: {out} is not a wand"
-    let res ← iFrame bi _ hyps out₁ (← SelPat.resolve hyps [.spatial, .intuitionistic])
+    let res ← iFrame hyps out₁ (← SelPat.resolve hyps [.spatial, .intuitionistic])
     let ⟨_, hyps', pf'⟩ ← res.finishClose
     return { e := _, hyps := hyps', p := q(false), out := out₂, pf := q(specialize_wand_autoframe $out₂ $pf $pf') }
 
@@ -141,8 +141,7 @@ TODO: This also needs to check that there are no modality addition patterns in `
 @[rocq_alias intro_pat_intuitionistic, rocq_alias use_tac_specialize_intuitionistic_helper]
 def iCasesPat.should_try_dup_context (pat : iCasesPat) : Bool :=
   match pat with
-  | .intuitionistic _ => true
-  | .pure _ => true
+  | .intuitionistic _ _ | .pure _ _ | .rewrite _ _ => true
   | _ => false
 
 /-- Specialize a proposition `A` by applying a sequence of specialization patterns.
@@ -195,6 +194,6 @@ elab "ispecialize " colGt pmt:pmTerm : tactic => do
     | throwError "ispecialize: cannot find argument"
 
   let ⟨_, hyps'', pb, B, pf'⟩ ← iSpecializeCore hyps' p out pmt.spats
-  let hyps''' := Hyps.add bi name ivar pb B hyps''
+  let ⟨_, hyps''', pfEq⟩ := Hyps.add bi name ivar pb B hyps''
   let pf'' ← addBIGoal hyps''' goal
-  mvar.assign q(($pf).1.trans <| $(pf').trans <| $pf'')
+  mvar.assign q(($pf).1.trans <| $(pf').trans <| $(pfEq).mp.trans $pf'')
diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean
index fb8509a5f..92b564eac 100644
--- a/Iris/Iris/Tests/Tactics.lean
+++ b/Iris/Iris/Tests/Tactics.lean
@@ -273,6 +273,89 @@ example [BI PROP] (P Q : PROP) : ⊢ P → Q := by
 example [BI PROP] (P : PROP) : P -∗ P → P := by
   iintro HP1 HP2
 
+/- Tests `iintro` using the introduction pattern `⟨⟩` to solve the goal -/
+example [BI PROP] (P : PROP) : False ∗ □ P ⊢@{PROP} P := by
+  iintro ⟨⟨⟩, #_⟩
+
+@[simp]
+private def def1 := 3
+
+/- Tests `iintro` using the introduction pattern for simplification (`/=`) -/
+example [BI PROP] (P Q : PROP) : ⊢@{PROP} if def1 = 3 then P -∗ P else Q := by
+  iintro /= HP
+  iexact HP
+
+/- Tests `iintro` where the lack of simplification (`/=`) causes a failure -/
+/-- error: iintro: if def1 = 3 then iprop(P -∗ P) else Q not a wand -/
+#guard_msgs in
+example [BI PROP] (P Q : PROP) : ⊢@{PROP} if def1 = 3 then P -∗ P else Q := by
+  iintro HP
+
+/- Tests `iintro` with the pattern for simplification and solving trivial goals (`//=`) -/
+example [BI PROP] : ⊢@{PROP} if def1 = 3 then True else False := by
+  iintro //=
+
+/- Tests `iintro` with the pattern for ∀-introduction (`*`) -/
+example {Val : Type} [BI PROP] (P Q : Val → PROP) :
+    ⊢@{PROP} ∀ x y, P x -∗ Q y -∗ P x ∗ Q y := by
+  iintro * _ _
+  iframe
+
+/-- Tests `iintro` with the pattern for repeating ∀-introduction and premise introduction (`**`) -/
+example {Val : Type} {ϕ : Prop} [BI PROP] (P : Val → Val → PROP) (Q : Val → PROP) :
+    ⊢@{PROP} ∀ x y, P x y -∗ ∀ z, (⌜ϕ⌝ → Q z -∗ P x y ∗ Q z ∗ ⌜ϕ⌝) := by
+  iintro **
+  iframe
+  ipureintro
+  assumption
+
+/-- Tests `iintro` with the pattern for introducing a pure goal and exiting the proof mode (`!%`) -/
+example [BI PROP] (P Q : PROP) : ⊢ □ P -∗ □ Q -∗ ⌜n = n⌝ := by
+  iintro - - !%
+  rfl
+
+/- Tests `iintro` with pure introduction failure -/
+/-- error: iintro: Q is not pure -/
+#guard_msgs in
+example [BI PROP] (P Q : PROP) : P ⊢ Q := by
+  iintro HP !%
+
+/-- Tests `iintro` with introduction patterns coming after `!%` -/
+example {ϕ : Prop} [BI PROP] : ⊢@{PROP} ⌜⌜ϕ⌝ ⊢@{PROP} ⌜ϕ⌝⌝ := by
+  iintro !% %_ !%
+  assumption
+
+/-- Tests `iintro` with an introduction pattern for clearing and framing hypotheses (`{ selPats* }`) -/
+example [BI PROP] (P Q R S T : PROP) (ϕ : Prop) :
+    ⊢ □ ⌜ϕ⌝ -∗ P -∗ Q -∗ <affine> R -∗ □ S -∗ □ T -∗ P ∗ Q ∗ T := by
+  iintro %hϕ HP HQ {!HP} HR #HS #HT {HR %hϕ %ϕ !# #}
+  iexact HQ
+
+/-- Tests `iintro` with introduction patterns for rewriting pure equalities -/
+example [BI PROP] (m n : Nat) (a b c : Prop) :
+    m = 2 → 3 = n → ⊢@{PROP} ⌜a = b⌝ -∗ ⌜b = c⌝ -∗ ⌜m.succ = n ∧ a = c⌝ := by
+  iintro → ← ← →
+  ipureintro
+  and_intros <;> rfl
+
+/-
+  Tests `iintro` with an introduction pattern for rewriting but the
+  hypothesis is not a pure equality
+-/
+/-- error: Invalid rewrite argument: Expected an equality or iff proof or
+definition name, but `x✝` is a proof of
+  P -/
+#guard_msgs in
+example [BI PROP] (P : Prop) : ⊢@{PROP} ⌜P⌝ -∗ True := by
+  iintro →
+
+/-- Tests `iintro` with non-trivial `rcases` destruction patterns -/
+example [BI PROP] (a b c1 c2 c3 : Prop) (P : Prop → Prop) :
+    ⊢@{PROP} □ ⌜((a = b ∧ (b ∨ (c1 ∧ c2 ∧ c3))) ∧ ∃ x, P x)⌝ -∗ ⌜a ∨ c1⌝ ∗ ⌜∃ x, P x⌝ := by
+  iintro %⟨⟨rfl, ((hb : a) | ⟨hc, _, -⟩)⟩, @⟨d : Prop, hd⟩⟩ !%
+  · grind
+  · grind
+
 end intro
 
 -- revert
@@ -905,6 +988,13 @@ example [BI PROP] (Q : PROP) : (⌜φ1⌝ ∧ <affine> ⌜φ2⌝) ⊢ Q -∗ Q :
   ipure Hφ
   iexact HQ
 
+/-- Tests `ipure` with an `rcases` destruction pattern -/
+example [BI PROP] (Q : PROP) : (⌜φ1⌝ ∧ <affine> ⌜φ2⌝) ⊢ Q -∗ Q := by
+  iintro Hφ
+  iintro HQ
+  ipure Hφ as ⟨hφ1, -⟩
+  iexact HQ
+
 /-- Tests `ipure` with implication containing pure -/
 example [BI PROP] (Q : PROP) : <affine> (⌜φ1⌝ ∧ ⌜φ2⌝ → ⌜φ3⌝)  ⊢ Q -∗ Q := by
   iintro Hφ
@@ -1703,6 +1793,47 @@ example [BI PROP] (Q : PROP) : □ Q ⊢ Q := by
   iintro H
   icases H with ⟨HA, HB⟩
 
+/-- Tests `icases` with a case destruction pattern for rewriting pure equalities -/
+example [BI PROP] (m n : Nat) (a b c : Prop) :
+    ⊢@{PROP} ⌜m = 2⌝ -∗ ⌜3 = n⌝ -∗ ⌜a = b⌝ -∗ ⌜b = c⌝ -∗ ⌜m.succ = n ∧ a = c⌝ := by
+  iintro #H1 H2 #H3 H4
+  icases H1 with →
+  icases H2 with ←
+  icases H3 with ←
+  icases H4 with →
+  ipureintro
+  and_intros <;> rfl
+
+/-
+  Tests `icases` with a case destruction pattern for rewriting but the
+  hypothesis is not a pure equality.
+-/
+/-- error: Invalid rewrite argument: Expected an equality or iff proof or
+definition name, but `a✝` is a proof of
+  P -/
+#guard_msgs in
+example [BI PROP] (P : Prop) : ⊢@{PROP} ⌜P⌝ -∗ True := by
+  iintro HP
+  icases HP with →
+
+/-
+  Tests `icases` with a case destruction pattern for rewriting but the
+  hypothesis is not a pure hypothesis.
+-/
+/-- error: icases: P is not pure -/
+#guard_msgs in
+example [BI PROP] (P : PROP) : ⊢@{PROP} P -∗ True := by
+  iintro HP
+  icases HP with →
+
+/-- Tests `icases` with non-trivial `rcases` destruction patterns -/
+example [BI PROP] (a b c1 c2 c3 : Prop) (P : Prop → Prop) :
+    ⊢@{PROP} □ ⌜((a = b ∧ (b ∨ (c1 ∧ c2 ∧ c3))) ∧ ∃ x, P x)⌝ -∗ ⌜a ∨ c1⌝ ∗ ⌜∃ x, P x⌝ := by
+  iintro Hpure
+  icases Hpure with %⟨⟨rfl, ((hb : a) | ⟨hc, _, -⟩)⟩, @⟨d : Prop, hd⟩⟩
+  · ipureintro <;> grind
+  · ipureintro <;> grind
+
 end cases
 
 section imodintro
@@ -2638,13 +2769,21 @@ example {GF m n} [LcGS .hasLC GF] :
   icombine H1 H2 H3 H4 as Hnew
   iexact Hnew
 
-/-- Tests `icombine` for combining two tokens -/
+/-- Tests `icombine` for combining two tokens. -/
 example {GF} [TokenG GF] {γ} :
     ⊢@{IProp GF} token γ -∗ token γ -∗ False := by
   iintro H1 H2
   icombine H1 H2 gives H
   iexact H
 
+/- Tests `icombine` with an invalid destruction pattern. -/
+/-- error: icombine: cannot destruct iprop(<absorb> <affine> (P ∗ Q)) -/
+#guard_msgs in
+example [BI PROP] {P Q R : PROP} [CombineSepGives P Q R] :
+    ⊢ <absorb> <affine> P -∗ <absorb> <affine> Q -∗ <absorb> <affine> (P ∗ Q) ∗ <pers> R := by
+  iintro HP HQ
+  icombine HP HQ as ⟨HNew1, _⟩ gives HNew2
+
 end icombine
 
 section iloeb
diff --git a/Iris/tactics.md b/Iris/tactics.md
index f9e465ec0..a1c73ae49 100644
--- a/Iris/tactics.md
+++ b/Iris/tactics.md
@@ -14,6 +14,7 @@ The proof mode maintains three contexts: the *pure* (Lean) context, the *intuiti
 - `iclear` [*selPats*](#selection-patterns) — Discard the hypotheses selected by [*selPats*](#selection-patterns).
 - `irevert` [*selPats*](#selection-patterns) — Revert the selected hypotheses (proof mode or pure Lean hypotheses) into the goal.
 - `ipure` *H* — Move the pure hypothesis *H* into the Lean context.
+- `ipure` *H* `as` *rcasesPat* — Move the pure hypothesis *H* into the Lean context and destruct it with the `rcases` pattern.
 - `iintuitionistic` *H* — Move *H* to the intuitionistic context. Equivalent to `icases H with #H`.
 - `ispatial` *H* — Move *H* to the spatial context. Equivalent to `icases H with ∗H`.
 
@@ -73,10 +74,11 @@ The proof mode maintains three contexts: the *pure* (Lean) context, the *intuiti
 - `$` — Frame the hypothesis: immediately cancel it against the goal (like `iframe`).
 - `⟨`*pat₁*`,` ... `,` *patₙ*`⟩` — Destruct a (separating) conjunction or existential; an existential variable is bound with `%`*x*, e.g. `⟨%x, H⟩`.
 - `(`*pat₁* `|` ... `|` *patₙ*`)` — Destruct a disjunction, one goal per disjunct. Parentheses can be omitted when nested inside `⟨⟩`.
-- `%`*name* — Move the (pure) hypothesis into the Lean context as *name*.
+- `%`*rcasesPat* — Move the (pure) hypothesis into the Lean context and destruct it with the `rcases` pattern *rcasesPat*.
 - `#`*pat* — Move the hypothesis to the intuitionistic context, then destruct with *pat*.
 - `∗`*pat* — Move the hypothesis to the spatial context, then destruct with *pat*.
 - `>`*pat* — Eliminate the modality at the top of the hypothesis, then destruct with *pat*.
+- `←`/`→` — Rewrite using a pure Lean equality and then remove the equality from the context.
 
 Example:
 ```lean
@@ -91,8 +93,14 @@ Example:
 - [*casesPat*](#cases-patterns) — Introduce a hypothesis and destruct it with [*casesPat*](#cases-patterns). In particular, `%x` introduces a universally quantified variable or pure premise into the Lean context.
 - `!>` — Introduce the modality at the top of the goal (like `imodintro`).
 - `//` — Try to close the goal with `itrivial` (and continue with the remaining patterns if it fails).
-
-Example: `iintro %x ⟨HP, #HQ⟩ !> //`.
+- `*` — Introduce all universal quantifiers.
+- `**` — Introduce all universal quantifiers, pure arrows, and wands.
+- `!%` — Introduce a pure proof goal and exit the proof mode.
+- `/=` — Apply simplification.
+- `//=` — Apply simplification and try solving the goal using `itrivial`. This is a shorthand for `/=` and `//`.
+- `{` [*selPats*](#selection-patterns) `}` — Clear the selection hypotheses chosen by the selection patterns *selPats*. Each element in *selPats* can be prefixed with `!` so that the chosen hypotheses are framed instead.
+
+Example: `iintro %x ⟨HP, #HQ⟩ !> {HR !HS #} → //`.
 
 ## Selection Patterns