diff --git a/Iris/Iris/HeapLang/Lib/Quicksort.lean b/Iris/Iris/HeapLang/Lib/Quicksort.lean
index af85196f0..350260687 100644
--- a/Iris/Iris/HeapLang/Lib/Quicksort.lean
+++ b/Iris/Iris/HeapLang/Lib/Quicksort.lean
@@ -282,13 +282,12 @@ theorem quicksort_spec l ls Φ :
 theorem wp_makeList (l : List Int) (Φ : Val → IProp GF) :
     (∀ v, isList v l -∗ Φ v) -∗
     WP hl(&(makeList l)) {{ Φ }} := by
-  induction l generalizing Φ with
+  iintro HΦ
+  iinduction l generalizing %Φ HΦ with
   | nil =>
-    iintro HΦ
     unfold makeList
     iapply nil_spec $$ HΦ
   | cons l ls ih =>
-    iintro HΦ
     rw [makeList]
     wp_pures
     wp_bind &(makeList _)
diff --git a/Iris/Iris/Instances/Lib/FUpd.lean b/Iris/Iris/Instances/Lib/FUpd.lean
index b150420b0..453a85bd3 100644
--- a/Iris/Iris/Instances/Lib/FUpd.lean
+++ b/Iris/Iris/Instances/Lib/FUpd.lean
@@ -170,28 +170,26 @@ theorem lc_fupd_add_later {E1 E2 : CoPset} {P : IProp GF} : ⊢ £ 1 -∗ (▷ |
 @[rocq_alias lc_fupd_add_laterN]
 theorem lc_fupd_add_laterN (n : Nat) {E : CoPset} {P : IProp GF} :
     ⊢ £ n -∗ (▷^[n] |={E}=> P) -∗ |={E}=> P := by
-  induction n generalizing P with
+  iintro Hf Hupd
+  iinduction n with
   | zero =>
-    iintro _ H
     simp [BIBase.laterN]
-    iexact H
+    iexact Hupd
   | succ n IH =>
-    iintro Hf Hupd
     icases Hf with ⟨H1, Hf⟩
     iapply lc_fupd_add_later $$ H1
     inext
     iapply IH $$ [$] [$]
 
-@[rocq_alias lc_fupd_add_step_fupdN ]
+@[rocq_alias lc_fupd_add_step_fupdN]
 theorem lc_fupd_add_step_fupdN (E1 E2 E3: CoPset) (P : IProp GF) (n : Nat) :
-  £ n -∗ (|={E1}[E2]▷=>^[n] |={E1,E3}=> P) -∗ |={E1,E3}=> P := by
-  induction n generalizing P with
+    £ n -∗ (|={E1}[E2]▷=>^[n] |={E1,E3}=> P) -∗ |={E1,E3}=> P := by
+  iintro Hf Hupd
+  iinduction n with
   | zero =>
-    iintro _ H
     simp only [Nat.repeat]
-    iexact H
+    iexact Hupd
   | succ n IH =>
-    iintro Hf Hupd
     simp only [Nat.repeat]
     imod Hupd
     icases Hf with ⟨H1, Hf⟩
@@ -404,12 +402,12 @@ instance elimModal_fupd_fupd_finally p (E1 E2 : CoPset) (P Q : IProp GF) :
 @[rocq_alias step_fupdN_fupd_finally]
 theorem step_fupdN_fupd_finally (E1 E2 : CoPset) (n : Nat) (P : IProp GF) :
     (|={E1}[E2]▷=>^[n] |={E1|}=> P) ⊢ |={E1|}=> ▷^[n] ◇ P := by
-  induction n with
+  iintro HP
+  iinduction n with
   | zero =>
     simp only [Nat.repeat]
     exact fupd_finally_mono except0_intro
   | succ n IH =>
-    iintro HP
     simp only [Nat.repeat]
     imod HP
     iapply fupd_finally_mono (later_laterN n).mpr
diff --git a/Iris/Iris/ProgramLogic/Lifting.lean b/Iris/Iris/ProgramLogic/Lifting.lean
index edb0c6d85..28ce47eba 100644
--- a/Iris/Iris/ProgramLogic/Lifting.lean
+++ b/Iris/Iris/ProgramLogic/Lifting.lean
@@ -187,10 +187,9 @@ theorem wp_pure_step_fupd [Inhabited State] (E₂ : CoPset)
     [Hexec : PureExec φ n e₁ e₂] (Hφ : φ) :
     (|={E}[E₂]▷=>^[n] £ n -∗ WP e₂ @ s; E {{ Φ }}) ⊢ WP e₁ @ s; E {{ Φ }} := by
   replace Hexec := Hexec.pureExec Hφ
-  induction Hexec using Relation.Iterate.head_induction_on with
+  iinduction Hexec using Relation.Iterate.head_induction_on with simp only [Nat.repeat]
   | rfl =>
     iintro Hwp
-    simp only [Nat.repeat]
     rw (occs := [2]) [fupd_wp_iff.to_eq]
     icases lc_zero with >Hz
     iapply Hwp $$ Hz
@@ -202,7 +201,6 @@ theorem wp_pure_step_fupd [Inhabited State] (E₂ : CoPset)
       intro σ
       have _ : PrimStep.Reducible (e₁, σ) := by grind only [reducible_of_reducibleNoObs]
       grind [cases Stuckness]
-    simp only [Nat.repeat]
     iapply step_fupd_wand $$ Hwp
     iintro Hwp Hone
     iapply IH
diff --git a/Iris/Iris/ProofMode/Classes.lean b/Iris/Iris/ProofMode/Classes.lean
index ac2ca161b..f6aa701ac 100644
--- a/Iris/Iris/ProofMode/Classes.lean
+++ b/Iris/Iris/ProofMode/Classes.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, Michael Sammler, Alvin Tang
+Authors: Lars König, Michael Sammler, Yunsong Yang, Alvin Tang
 -/
 module
 
@@ -224,6 +224,15 @@ class CombineSepGives [BI PROP] (P Q : PROP) (R : outParam PROP) where
   combine_sep_gives : P ∗ Q ⊢ <pers> R
 export CombineSepGives (combine_sep_gives)
 
+/-
+  `IntoIH φ P Q` describes how to turn a pure induction hypothesis `φ` into a proofmode
+  hypothesis `Q` under an intuitionistic BI context `□ P`.
+-/
+@[ipm_class, rocq_alias IntoIH]
+class IntoIH [BI PROP] (φ : Prop) (P : PROP) (Q : outParam PROP) where
+  into_ih : φ → □ P ⊢ Q
+export IntoIH (into_ih)
+
 #rocq_ignore elim_inv_tc_opaque "No tc_opaque in Lean"
 #rocq_ignore elim_modal_tc_opaque "No tc_opaque in Lean"
 #rocq_ignore from_and_tc_opaque "No tc_opaque in Lean"
diff --git a/Iris/Iris/ProofMode/Expr.lean b/Iris/Iris/ProofMode/Expr.lean
index c9f86ea0b..e02b9ab2b 100644
--- a/Iris/Iris/ProofMode/Expr.lean
+++ b/Iris/Iris/ProofMode/Expr.lean
@@ -539,3 +539,21 @@ def Hyps.addWithInfo {prop : Q(Type u)} (bi : Q(BI $prop))
   addHypInfo nameRef nameTo ivar' prop ty (isBinder := true)
   let hyps := Hyps.add bi nameTo ivar' p ty h
   return ⟨ivar', hyps⟩
+
+/--
+  Given hypothesis `hyps` representing `e` where every hypothesis exist in the
+  intuitionistic context, return the proof of `e ⊢ □ e`. Return `none` if
+  `hyps` contains hypotheses in the spatial context.
+-/
+def Hyps.buildIntuitionisticProof {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
+    (hyps : Hyps bi e) : Option Q($e ⊢ □ $e) :=
+  match hyps with
+  | .emp _ => some q(intuitionistically_emp.mpr)
+  | .hyp _ _ _ p _ _ =>
+    match matchBool p with
+    | .inl _ => some q(intuitionistically_idem.mpr)
+    | .inr _ => none
+  | .sep _ _ _ _ lhs rhs => do
+    let pfL ← buildIntuitionisticProof lhs
+    let pfR ← buildIntuitionisticProof rhs
+    some q((sep_mono $pfL $pfR).trans intuitionistically_sep_mpr)
diff --git a/Iris/Iris/ProofMode/Instances.lean b/Iris/Iris/ProofMode/Instances.lean
index 8ebc6aa25..1cd553fc1 100644
--- a/Iris/Iris/ProofMode/Instances.lean
+++ b/Iris/Iris/ProofMode/Instances.lean
@@ -7,7 +7,9 @@ module
 
 public import Iris.BI
 public import Iris.ProofMode.Classes
+public import Iris.ProofMode.ClassesMake
 public import Iris.ProofMode.ModalityInstances
+public import Iris.ProofMode.Expr
 public import Iris.Std.TC
 public import Iris.Std.RocqPorting
 
@@ -918,3 +920,49 @@ instance combineSepGives_persistently [BI PROP] (Q1 Q2 P : PROP)
     [h : CombineSepGives Q1 Q2 P] :
     CombineSepGives iprop(<pers> Q1) iprop(<pers> Q2) iprop(<pers> P) where
   combine_sep_gives := persistently_sep_mpr.trans (persistently_mono h.combine_sep_gives)
+
+@[rocq_alias into_ih_entails]
+instance intoIH_entails [BI PROP] (P Q : PROP) : IntoIH (Entails' P Q) P Q where
+  into_ih := λ hpq => intuitionistically_elim.trans hpq
+
+@[rocq_alias into_ih_forall]
+instance (priority := default - 2) intoIH_forall [BI PROP] (φ : α → Prop) (P : PROP) (Φ : α → PROP)
+    [h : ∀ x, IntoIH (φ x) P (Φ x)] :
+    IntoIH (∀ x, φ x) P (BI.forall Φ) where
+  into_ih := by
+    intro hφ
+    apply forall_intro
+    intro x
+    exact (h x).into_ih (hφ x)
+
+@[rocq_alias into_ih_impl]
+instance (priority := default - 1) intoIH_imp [BI PROP] (φ ψ : Prop) (Δ P Q : PROP)
+    [h1 : MakeAffinely iprop(⌜φ⌝) P]
+    [h2 : IntoIH ψ Δ Q] :
+    IntoIH (φ → ψ) Δ iprop(P -∗ Q) where
+  into_ih := by
+    intro hImp
+    apply wand_intro
+    refine (sep_mono_right h1.make_affinely.mpr).trans ?_
+    refine persistent_and_affinely_sep_right.2.trans ?_
+    exact pure_elim_right (fun hφ => h2.into_ih (hImp hφ))
+
+#rocq_ignore into_ih_Forall "List.Forall does not exist in the core Lean libraries, and ∀ x ∈ l, p x is used instead"
+
+/-- Support for induction principles whose IH is guarded by `List.Forall₂`, e.g.
+    arising from mutual inductive types relating two lists element-wise. -/
+@[rocq_alias into_ih_Forall2]
+instance (priority := default - 2) intoIH_listForall₂ [BI PROP] (φ : α → β → Prop) (l1 : List α) (l2 : List β)
+    (P : PROP) (Φ : α → β → PROP)
+    [h : ∀ x1 x2, IntoIH (φ x1 x2) P (Φ x1 x2)] :
+    IntoIH (List.Forall₂ φ l1 l2) P (bigSepL2 (fun _ x1 x2 => iprop(□ Φ x1 x2)) l1 l2) where
+  into_ih := by
+    intro h
+    induction h with
+    | nil => simp [bigSepL2, affine]
+    | cons x xs ih =>
+      simp [bigSepL2] at ⊢
+      apply intuitionistically_sep_idem.mpr.trans
+      refine sep_mono ?_ ?_
+      · exact intuitionistically_intro_intuitionistically ((h _ _).into_ih x)
+      · exact ih
diff --git a/Iris/Iris/ProofMode/Porting.lean b/Iris/Iris/ProofMode/Porting.lean
index dad0da8f9..f239a4f0a 100644
--- a/Iris/Iris/ProofMode/Porting.lean
+++ b/Iris/Iris/ProofMode/Porting.lean
@@ -51,7 +51,7 @@ import Iris.Std.RocqPorting
 #rocq_concept proofmode "Tactics" "iCombine" ported "icombine"
 #rocq_concept proofmode "Tactics" "iIntros (basic)" ported "iintro"
 #rocq_concept proofmode "Tactics" "iIntros (all intro patterns)" missing ""
-#rocq_concept proofmode "Tactics" "iInduction" missing ""
+#rocq_concept proofmode "Tactics" "iInduction" ported "iinduction"
 #rocq_concept proofmode "Tactics" "iLöb" ported "iloeb"
 #rocq_concept proofmode "Tactics" "iAssert" ported "ihave _ : _"
 #rocq_concept proofmode "Tactics" "iRewrite" ported "irewrite"
diff --git a/Iris/Iris/ProofMode/ProofModeM.lean b/Iris/Iris/ProofMode/ProofModeM.lean
index f20e854f6..9ce7ac093 100644
--- a/Iris/Iris/ProofMode/ProofModeM.lean
+++ b/Iris/Iris/ProofMode/ProofModeM.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2025 Michael Sammler. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Michael Sammler, Zongyuan Liu, Yunsong Yang
+Authors: Michael Sammler, Zongyuan Liu, Yunsong Yang, Alvin Tang
 -/
 module
 
@@ -96,6 +96,30 @@ def addMVarGoal (m : MVarId) (name : Name := .anonymous) : ProofModeM Unit := do
     m.setUserName name
   modify ({goals := ·.goals.push m})
 
+/--
+  Creates a new proof goal with the given hypotheses (`hyps`), conclusion
+  (`goal`). Run a sequence of tactics with this proof goal and push all
+  subgoals into the proof state.
+
+  The function returns:
+  1. the metavariable of the initial goal,
+  2. a Boolean value indicating whether the `firstTactic` solves all goals,
+     `false` if `firstTactic` is `none`.
+-/
+def addBIGoalRunTactics {prop : Q(Type u)} {bi : Q(BI $prop)}
+    {e} (hyps : Hyps bi e) (goal : Q($prop)) (name : Name := .anonymous)
+    (firstTactic : Option <| TSyntax `tactic)
+    (tacticSeq : TSyntax `Lean.Parser.Tactic.tacticSeq) :
+    ProofModeM (Q($e ⊢ $goal) × Bool) := do
+  let m ← mkBIGoal hyps goal name
+  -- Run `firstTactic`, if available
+  let subgoals ← firstTactic.elim (pure [m.mvarId!]) (evalTacticAt · m.mvarId!)
+  -- Run the user tactics on each newly generated goal after running `firstTactic`
+  let mut subgoals' := []
+  for s in subgoals do
+    subgoals' := subgoals'.append <| ← evalTacticAt tacticSeq s
+  pure (m, firstTactic.isSome && subgoals.isEmpty)
+
 /-- Try to synthesize a typeclass instance, adding any created metavariables as proof mode goals. -/
 def ProofModeM.trySynthInstanceQ (α : Q(Sort v)) : ProofModeM (Option Q($α)) := do
   let LOption.some (e, mvars) ← ProofMode.trySynthInstance α | return none
diff --git a/Iris/Iris/ProofMode/Tactics.lean b/Iris/Iris/ProofMode/Tactics.lean
index 361255881..f74191c1c 100644
--- a/Iris/Iris/ProofMode/Tactics.lean
+++ b/Iris/Iris/ProofMode/Tactics.lean
@@ -12,6 +12,7 @@ public meta import Iris.ProofMode.Tactics.ExFalso
 public meta import Iris.ProofMode.Tactics.Exists
 public meta import Iris.ProofMode.Tactics.Frame
 public meta import Iris.ProofMode.Tactics.Have
+public meta import Iris.ProofMode.Tactics.Induction
 public meta import Iris.ProofMode.Tactics.Intro
 public meta import Iris.ProofMode.Tactics.LeftRight
 public meta import Iris.ProofMode.Tactics.Loeb
diff --git a/Iris/Iris/ProofMode/Tactics/Induction.lean b/Iris/Iris/ProofMode/Tactics/Induction.lean
index 7e9897c9f..554fe2833 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -1,59 +1,422 @@
 /-
 Copyright (c) 2026 Yunsong Yang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Yunsong Yang
+Authors: Yunsong Yang, Michael Sammler, Alvin Tang
 -/
 module
 
-public import Iris.ProofMode.ClassesMake
 public meta import Iris.ProofMode.Tactics.Basic
+public meta import Iris.ProofMode.Tactics.Assumption
+public meta import Iris.ProofMode.Tactics.Cases
+public meta import Iris.ProofMode.Patterns.CasesPattern
+public meta import Iris.ProofMode.ClassesMake
+public meta import Iris.ProofMode.Tactics.RevertIntro
+public meta import Iris.ProofMode.Tactics.Revert
+public meta import Lean.Meta.Tactic.TryThis
 
 namespace Iris.ProofMode
 
-public section
-open BI Std
+public meta section
+open BI Std Lean Elab Tactic Meta Qq Parser.Tactic
 
-/-
-  `IntoIH φ P Q` describes how to turn a pure induction hypothesis `φ` into a proofmode
-  hypothesis `Q` under an intuitionistic BI context `□ P`.
+syntax (name := iinduction) "iinduction " colGt term
+  (" using " ident)? (generalizingSelPats)? (inductionAlts)? : tactic
+
+/-- Information from the tactic user for an induction subgoal -/
+private structure Alt where
+  -- The name of the constructor
+  ctor : Name
+  -- The alternative names supplied by the tactic user
+  vars : Array <| TSyntax `Lean.binderIdent
+  -- User-supplied tactics for this case, `none` if a hole (`_` or `?_`) is given
+  tacs : Option <| TSyntax `Lean.Parser.Tactic.tacticSeq
+  -- The syntax, useful for error message printing
+  stx : TSyntax `Lean.Parser.Tactic.inductionAlt
+
+/-- Information from the tactic user for all induction subgoals -/
+private structure Alts where
+  -- User-supplied tactic to be applied before splitting into cases
+  tac : Option <| TSyntax `tactic
+  -- The alternative cases supplied by the user
+  alts : Array Alt
+  -- The wildcard case, if supplied by the user
+  wildcard : Option Alt
+  -- The syntax, useful for error message printing
+  stx : TSyntax `Lean.Parser.Tactic.inductionAlts
+
+/--
+  Given user-supplied alternative names and tactic sequences, parse the syntax
+  and return an `Alts` instance.
 -/
-@[ipm_class]
-class IntoIH [BI PROP] (φ : Prop) (P : PROP) (Q : outParam PROP) where
-  into_ih : φ → □ P ⊢ Q
-
--- TODO: two more instances [into_ih_Forall] and [into_ih_Forall2]
--- have not been implemented
-instance intoIH_entails [BI PROP] (P Q : PROP) : IntoIH (P ⊢ Q) P Q where
-  into_ih := λ hpq => intuitionistically_elim.trans hpq
-instance intoIH_forall [BI PROP] (φ : α → Prop) (P : PROP) (Φ : α → PROP)
-    [h : ∀ x, IntoIH (φ x) P (Φ x)] :
-    IntoIH (∀ x, φ x) P (BI.forall Φ) where
-  into_ih := by
-    intro hφ
-    apply forall_intro
-    intro x
-    exact (h x).into_ih (hφ x)
-instance intoIH_imp [BI PROP] (φ ψ : Prop) (Δ P Q : PROP)
-    [h1 : MakeAffinely iprop(⌜φ⌝) P]
-    [h2 : IntoIH ψ Δ Q] :
-    IntoIH (φ → ψ) Δ iprop(P -∗ Q) where
-  into_ih := by
-    intro hImp
-    apply wand_intro
-    refine (sep_mono_right h1.make_affinely.mpr).trans ?_
-    refine persistent_and_affinely_sep_right.2.trans ?_
-    exact pure_elim_right (fun hφ => h2.into_ih (hImp hφ))
-
-theorem ih_revert [BI PROP] {Δ P Q : PROP} {φ : Prop} (hφ : φ)
-    [hP : IntoIH φ Δ P]
-    (hΔ : Δ ⊢ □ Δ)
-    (hPQ : Δ ⊢ iprop(<pers> P → Q)) :
-    Δ ⊢ Q := by
-  have hP' : □ Δ ⊢ <pers> P :=
-    (intuitionistically_intro_intuitionistically (hP.into_ih hφ)).trans persistently_of_intuitionistically
-  have hAnd : □ Δ ⊢ iprop(<pers> P ∧ (<pers> P → Q)) :=
-    and_intro hP' <| intuitionistically_elim.trans hPQ
-  exact hΔ.trans <| hAnd.trans (imp_elim_right (P := iprop(<pers> P)) (Q := Q))
+private def parseInductionAlts (altsSyntax : TSyntax `Lean.Parser.Tactic.inductionAlts) :
+    TacticM Alts := do
+  -- For parsing the user-supplied names for variables and induction hypotheses
+  let parseVars (vars : Array Syntax) : TacticM (Array (TSyntax `Lean.binderIdent)) := do
+    vars.mapM fun v =>
+      match v with
+      | `(ident| $id:ident) => `(binderIdent| $id:ident)
+      | _                   => `(binderIdent| _)
 
-public meta section
-open Lean Elab Tactic Meta Qq
+  let mut parsedAlts := #[]
+
+  match altsSyntax with
+  | `(inductionAlts| with $[$tac]? $[$alts]*) =>
+    for alt in alts do
+      let (lhs, tacs) ← match alt with
+        | `(inductionAlt| $[$lhs:inductionAltLHS]* => $tac:tacticSeq) => pure (lhs, some tac)
+        | `(inductionAlt| $[$lhs:inductionAltLHS]* => $_:hole)
+        | `(inductionAlt| $[$lhs:inductionAltLHS]* => $_:syntheticHole) => pure (lhs, none)
+        | _ => throwErrorAt alt "iinduction: invalid syntax"
+
+      for l in lhs do
+        match l with
+        | `(inductionAltLHS| | $ctor:ident $[$vars]*)
+        | `(inductionAltLHS| | @ $ctor:ident $[$vars]*) =>
+          parsedAlts := parsedAlts.push ⟨ctor.getId, ← parseVars vars, tacs, alt⟩
+        | `(inductionAltLHS| | $_:hole $[$vars]*) =>
+          if parsedAlts.size < alts.size - 1 then
+            throwErrorAt alt
+              s!"iinduction: invalid occurrence of the wildcard alternative `| _ => ...`: ".append
+              "It must be the last alternative"
+          return ⟨tac, parsedAlts, some ⟨.anonymous, ← parseVars vars, tacs, alt⟩, altsSyntax⟩
+        | _ => throwErrorAt l "iinduction: invalid syntax"
+    return ⟨tac, parsedAlts, none, altsSyntax⟩
+  | _ => throwErrorAt altsSyntax "iinduction: invalid syntax"
+
+/--
+  This theorem is used for updating the proof in `InductionState` as `addIHs`
+  iterates through the list of induction hypotheses and introduces them from
+  the regular Lean context into the intuitionistic context.
+
+  The initial set of hypotheses that exist in the Iris context after applying
+  Lean's built-in induction step is represented by `P`. Since the spatial
+  context is empty (that is, all hypotheses exist in intuitionistic context),
+  `P ⊢ □ P` must hold.
+
+  The proposition `Q` represents these initial hypotheses as well as induction
+  hypotheses introduced into the intuitionistic context up until the most
+  recent `addIHs` iteration. At every iteration of `addIHs`, an induction
+  hypothesis `R` is obtained upon type class synthesis with `IntoIH`. The proof
+  for `InductionState` is obtained using this theorem accordingly.
+-/
+@[rocq_alias tac_revert_ih]
+theorem revert_IH [BI PROP] {P Q R : PROP} {φ}
+    (ih : φ)
+    (h1 : P ⊢ □ P)
+    (h2 : P ⊢ Q)
+    (inst : IntoIH φ P R) :
+    P ⊢ (Q ∗ □ R) := calc
+  _ ⊢ □ P         := h1
+  _ ⊢ □ P ∗ □ P   := intuitionistically_sep_dup.mp
+  _ ⊢ □ P ∗ □ □ P := sep_mono_right intuitionistically_idem.mpr
+  _ ⊢ □ P ∗ □ R   := sep_mono_right <| intuitionistically_mono <| inst.into_ih ih
+  _ ⊢ □ Q ∗ □ R   := sep_mono_left <| intuitionistically_mono h2
+  _ ⊢ Q ∗ □ R     := sep_mono_left intuitionistically_elim
+
+/--
+  Designed to be a mutable state such that `newHyps` contains induction
+  hypotheses generated by Lean's built-in induction.
+-/
+private structure InductionState {u} {prop : Q(Type u)} {bi} (origE : Q($prop)) where
+  {newE : Q($prop)}
+  (newHyps : Hyps bi newE)
+  (pf : Q($origE ⊢ $newE))
+
+/-- Introduce into the intuitionistic context of the Iris proof state. -/
+private def addIHs {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e : Q($prop)}
+    (pfIntHyps : Q($e ⊢ □ $e)) (hyps : Hyps bi e) (ihFVars : List FVarId) :
+    ProofModeM (@InductionState u prop bi e) := do
+
+  -- Initialise the mutable instance of `InductionState`
+  let mut st := { newHyps := hyps, pf := q(.rfl) }
+
+  -- Iteratively move the induction hypotheses into the intuitionistic context
+  for i in ihFVars do
+    let ⟨_u, (ϕ : Q(Prop)), (p : Q($ϕ))⟩ ← inferTypeQ <| mkFVar i
+
+    -- Obtain the proposition to be introduced into the intuitionistic context
+    let Q ← mkFreshExprMVarQ q($prop)
+    let some inst ← ProofModeM.trySynthInstanceQ q(IntoIH $ϕ $e $Q)
+    | throwError m!"iinduction: unable to perform type class synthesis with IntoIH for the induction hypothesis {ϕ}"
+
+    -- Introduce the induction hypothesis into the intuitionistic context
+    let nameIdent := mkIdent <| ← i.getUserName
+    let binderIdent ← `(binderIdent| $nameIdent:ident)
+    let ⟨_, newHyps⟩ ← Hyps.addWithInfo bi binderIdent q(true) Q st.newHyps
+    let pf := q(revert_IH $p $pfIntHyps $st.pf $inst)
+
+    st := { newHyps, pf }
+
+  return st
+
+private def throwMissingAlt {α} (ctor : Name) : ProofModeM α :=
+  throwError "iinduction: alternative `{ctor.getString!}` has not been provided"
+
+/--
+  Check that all the alternative names are valid and that there are no duplicates.
+  Otherwise, throw an error on the corresponding line.
+-/
+private def checkCtors (ctors : List Name) (parsedAlts : Alts) : ProofModeM Unit := do
+  let mut handledCtors : Std.HashSet Name := {}
+
+  for alt in parsedAlts.alts do
+    if !ctors.contains alt.ctor then
+      throwOrLogErrorAt alt.stx
+        m!"iinduction: invalid alternative name `{alt.ctor}`"
+
+    if handledCtors.contains alt.ctor then
+      throwOrLogErrorAt alt.stx
+        m!"iinduction: duplicate alternative name `{alt.ctor}`"
+
+    handledCtors := handledCtors.insert alt.ctor
+
+private def iInductionCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
+    (hyps : Hyps bi e) (goal : Q($prop)) (fvar : FVarId)
+    (parsedAlts : Option Alts) (altRecName : Option Name) (genSelTargets : List SelTarget) :
+    ProofModeM Q($e ⊢ $goal) := do
+  let targets := genSelTargets ++
+    (hyps.spatialIVarIds.map ({ kind := .ipm ·, explicit := false })).filter (not <| (genSelTargets.map (·.kind)).contains ·.kind)
+
+  -- Find the recursor name and constructor names of the inductive datatype
+  let fvarType ← liftM <| (inferType <| mkFVar fvar) >>= whnf
+  let recName ← match fvarType.getAppFn with
+  | .const indName _ =>
+    match (← getEnv).find? indName with
+    | some (.inductInfo _) =>
+      altRecName.elim
+        (getCustomEliminator? #[mkFVar fvar] true <&> (·.getD <| mkRecName indName))
+        pure
+    | _ => throwError "iinduction: {indName} is not inductive"
+  | _ => throwError "iinduction: unable to determine inductive type"
+
+  let matcher := fun ctor alt => alt.ctor != .anonymous && ctor == alt.ctor
+
+  -- Find the constructor names
+  let recCtors := ((← Lean.Meta.getElimInfo recName).altsInfo.map (·.name)).toList
+
+  -- Check that all alternative names supplied by the user are valid
+  parsedAlts.forM fun parsedAlts => do
+    checkCtors recCtors parsedAlts
+    if recCtors.length == parsedAlts.alts.size then
+      parsedAlts.wildcard.forM fun w =>
+        throwOrLogErrorAt w.stx "iinduction: wildcard alternative is not needed"
+
+  -- Define the names for variables and induction hypotheses if supplied by user
+  let varNames ←
+    match parsedAlts with
+    | none =>
+      pure <| recCtors.toArray.map <| fun _ => { explicit := true, varNames := [] }
+    | some parsedAlts => do
+      recCtors.toArray.mapM <| fun ctor =>
+      match parsedAlts.alts.find? (matcher ctor) <|> parsedAlts.wildcard with
+      | some alt =>
+        pure { explicit := true, varNames := alt.vars.toList.map <|
+          fun stx => match stx.raw with
+          | `(binderIdent| $id:ident) => id.getId
+          | _ => Name.mkSimple "_" }
+      | none =>
+        -- Defer the check if the first tactic for the `with` syntax is given
+        if parsedAlts.tac.isSome then
+          pure { explicit := true, varNames := [] }
+        else
+          throwMissingAlt ctor
+
+  let pf ← iRevertIntro hyps goal targets <|
+    fun hyps' goal' kIntro => do
+      -- Create a new metavariable for the proof goal upon reverting hypotheses
+      let m ← mkBIGoal hyps' goal'
+
+      -- Use built-in induction in Lean to generate the subgoals for induction
+      let subgoals ← m.mvarId!.withContext do
+        m.mvarId!.induction fvar recName varNames
+
+      -- Handle each subgoal generated by Lean's induction
+      for ⟨s, ctor⟩ in subgoals.toList.zip recCtors do
+        s.mvarId.withContext do
+          s.mvarId.setTag ctor
+            -- Obtain the type of the induction subgoal
+            let sType ← s.mvarId.getType >>= instantiateMVars
+
+            let some irisGoal := parseIrisGoal? sType
+            -- This should not happen
+            | throwOrLogError "iinduction: fail to parse induction subgoal"
+
+            -- Find the induction hypotheses generated by Lean's `induction` tactic
+            let ihFVars ← s.mvarId.withContext getLCtx >>=
+              (·.decls.toList.reduceOption.filterM
+                (instantiateMVars ·.type <&> (·.find? isIrisGoal |>.isSome)) <&>
+                (·.map (·.fvarId)))
+
+            -- A proof that all hypotheses in the Iris goal exist in the intuitionistic context
+            let some pfIntHyps := irisGoal.hyps.buildIntuitionisticProof
+            | throwOrLogError "iinduction: spatial context should be empty"
+
+            -- Introduce the induction hypothesis back into the Iris proof state
+            let st ← addIHs pfIntHyps irisGoal.hyps ihFVars
+
+            parsedAlts.forM fun parsedAlts => do
+              parsedAlts.alts.find? (matcher ctor) <|> parsedAlts.wildcard |>.forM
+                fun ⟨_, vars, _, stx⟩ => do
+                  -- Check that the number of arguments matches what are needed
+                  if vars.size > s.fields.size then
+                    throwOrLogErrorAt stx <|
+                      s!"iinduction: too many variable names provided at alternative `{ctor}`: ".append
+                      s!"{vars.size} provided, but {s.fields.size} expected"
+                  -- Label the arguments with their types, shown when the user hovers over them
+                  for ⟨fieldFVar, varStx⟩ in s.fields.zip vars do
+                    if let `(binderIdent| $id:ident) := varStx then
+                      let lctx ← getLCtx
+                      let fieldType ← inferType fieldFVar
+                      addLocalVarInfo id lctx fieldFVar fieldType true
+
+            let pf' ← withoutFVars (u := 0) ihFVars.toArray <| kIntro st.newHyps irisGoal.goal <|
+              fun hyps goal => do match parsedAlts with
+                -- Remove the induction hypotheses from the regular Lean context
+                | none => addBIGoal hyps goal ctor
+                | some parsedAlts =>
+                  -- Check if the alternative names for this constructor are supplied by the user
+                  match parsedAlts.alts.find? (matcher ctor) <|> parsedAlts.wildcard with
+                  | some ⟨_, _, tacticSeq, stx⟩ =>
+                    -- Generate the induction subgoal, label the induction subgoal with `ctor`
+                    match tacticSeq with
+                    | none => addBIGoal hyps goal ctor
+                    -- Run the tactics supplied by the user, if available
+                    | some tacticSeq =>
+                        let ⟨pf, allSolved⟩ ←
+                          addBIGoalRunTactics hyps goal ctor parsedAlts.tac tacticSeq
+                        -- Throw an error if the first tactic already solves the goal
+                        if allSolved then
+                          throwOrLogErrorAt stx
+                            s!"iinduction: alternative `{ctor.getString!}` is not needed"
+                        pure pf
+                  -- Alternative names not found, acceptable only when `firstTactic` solves it
+                  | none =>
+                    match parsedAlts.tac with
+                    -- No first tactic given, the alternative name is missing
+                    | none => throwMissingAlt ctor
+                    | some firstTactic =>
+                      let m ← mkBIGoal hyps goal ctor
+                      let subgoals ← evalTacticAt firstTactic m.mvarId!
+                      -- First tactic supplied by the user but does not completely solve this case
+                      if !subgoals.isEmpty then
+                        throwOrLogErrorAt parsedAlts.stx
+                          m!"iinduction: alternative `{ctor.getString!}` has not been provided"
+                      pure m
+
+            -- Fill the metavariable for the induction subgoal generated by Lean
+            s.mvarId.assign q($(st.pf).trans $pf')
+
+      return m
+
+  return pf
+
+private def generalizeTermWithFVar (x : TSyntax `term) : TacticM FVarId := do
+  let e ← withMainContext <| elabTerm x none
+  let e ← instantiateMVars e
+
+  -- Return the `FVarId` value directly if the term expresson is a free variable
+  if e.isFVar then
+    return e.fvarId!
+
+  -- Otherwise, generalise the term expression and return the `FVarId`
+  let mvarId ← getMainGoal
+  let (fvars, newMVarId) ← mvarId.generalize #[{ expr := e }]
+  replaceMainGoal [newMVarId]
+
+  return fvars[0]!
+
+/--
+  The `iinduction` tactic applies induction in the Iris Proof Mode in a similar
+  way as the `induction` tactic. Given an expression `e`, the application of
+  `iinduction e` performs the following steps:
+  1. Generalises the expression `e` using `Lean.Meta.Tactic.Generalize`.
+  2. Reverts all hypotheses in the spatial context, as well as those specified
+     in the `generalizing` clause.
+  3. Obtain the induction subgoals.
+  4. Moves all induction hypotheses into the intuitionstic context.
+  5. Introduce hypotheses reverted in steps 2 and 3 back into the Iris contexts.
+
+  Similar to the regular `induction` tactic, the following syntax is available.
+  - `iinduction e using r`: to specify the induction principle `r`.
+  - `iinduction e generalizing z₁ … zₙ`: to generalise `z₁ … zₙ`,
+    which is expressed as a selection pattern. Both Iris hypotheses and pure
+    Lean hypotheses can be generalised. Hypotheses dependent on any of
+    `z₁ … zₙ` or the induction target `e` must themselves be included in
+    the `generalizing` clause.
+  - `iinduction e generalizing! z₁ … zₙ`: similar to
+    `iinduction e generalizing z₁ … zₙ`, except that hypotheses dependent
+    on any of `z₁ … zₙ` or the induction target `e` are implicitly generalised.
+  - `iinduction e with tac | constr₁ => tac₁ | … | constrₙ => tacₙ`:
+    where `constr₁ … constrₙ` are names of the constructor, variables and
+    induction hypotheses, while `tac₁ … tacₙ` are the corresponding tactic
+    sequences. The optional first tactic `tac` is applied to all induction
+    subgoals.
+
+  As an example, consider the following Iris context, where `n : Nat`.
+
+  ```
+  ∗HP : P
+  □HQ : Q m
+  □HR : R
+  ∗HS : S
+  □HT : T n
+  ```
+
+  By applying `iinduction n generalizing HQ HT`, the hypotheses `HQ`
+  are additionally reverted and thus included as a wand premise in the induction
+  hypothesis. The hypothesis `HT` must also be reverted
+  because it involves the induction target `n`. Alternatively, one can use
+  `iinduction n generalizing! HQ` so that `HT` is generalised implicitly.
+
+  One can also generalise pure variables in the regular Lean context.
+  If there exists some pure/Iris hypotheses that is forward-dependent, they
+  should also be included in the `generalizing` clause. For the above example,
+  `iinduction n generalizing %m HQ HT` and `iinduction n generalizing! %m`
+  are equivalent.
+-/
+elab_rules : tactic
+  | `(tactic| iinduction $x $[using $r]? generalizing $genSelPats* $[$alts]?) => do
+    let fvar ← generalizeTermWithFVar x
+    -- Parse the recursor name provided by the user
+    let recName := r.map (·.getId)
+    -- Parse the list of alternative names supplied by the user
+    let parsedAlts ← alts.mapM parseInductionAlts
+
+    ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
+      let genSelTargets ← do
+        -- Parse the selection patterns for generalising hypotheses
+        let parsedGenSelPats ← liftMacroM <| SelPat.parse genSelPats
+        let genSelTargets ← SelPat.resolve hyps parsedGenSelPats
+        -- Check for dependencies with the hypotheses in the selection targets
+        checkDependentHyps "iinduction" hyps genSelTargets fvar genSelPats
+          (fun pats => `(tactic| iinduction $x $[using $r]? generalizing $pats* $[$alts]?))
+          (fun pats => `(tactic| iinduction $x $[using $r]? generalizing! $pats* $[$alts]?))
+        pure genSelTargets
+
+      let pf ← iInductionCore hyps goal fvar parsedAlts recName genSelTargets
+      mvar.assign pf
+  | `(tactic| iinduction $x $[using $r]? $[generalizing! $genSelPats*]? $[$alts]?) => do
+    let fvar ← generalizeTermWithFVar x
+    -- Parse the recursor name provided by the user
+    let recName := r.map (·.getId)
+    -- Parse the list of alternative names supplied by the user
+    let parsedAlts ← alts.mapM parseInductionAlts
+
+    ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
+      let mkGenSelTargets := fun genSelTargets => do
+        let ⟨_, missingIrisHyps, allPureFVarsSorted⟩ ←
+          getDependentHyps hyps genSelTargets fvar false
+        pure <| getCompleteSelTargets genSelTargets missingIrisHyps allPureFVarsSorted
+
+      let genSelTargets ←
+        match genSelPats with
+        | none => mkGenSelTargets []
+        | some genSelPats =>
+          -- Parse the selection patterns provided by the tactic user
+          let parsedGenSelPats ← liftMacroM <| SelPat.parse genSelPats
+          let genSelTargets ← SelPat.resolve hyps parsedGenSelPats
+          -- Include dependent hypotheses as well
+          mkGenSelTargets genSelTargets
+
+      let pf ← iInductionCore hyps goal fvar parsedAlts recName genSelTargets
+      mvar.assign pf
diff --git a/Iris/Iris/ProofMode/Tactics/Loeb.lean b/Iris/Iris/ProofMode/Tactics/Loeb.lean
index 06f28ca2a..dad78526e 100644
--- a/Iris/Iris/ProofMode/Tactics/Loeb.lean
+++ b/Iris/Iris/ProofMode/Tactics/Loeb.lean
@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fernando Leal
 -/
 module
+
+public import Iris.ProofMode.Tactics.Revert
 public import Iris.ProofMode.Tactics.RevertIntro
 
 namespace Iris.ProofMode
@@ -12,34 +14,62 @@ open Lean Meta Elab.Tactic Qq
 
 public meta section
 
+syntax (name := iloeb) "iloeb" " as " binderIdent (generalizingSelPats)? : tactic
+
+private def iLoebCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
+    (hyps : Hyps bi e) (goal : Q($prop)) (targets : List SelTarget)
+    (IH : TSyntax `Lean.binderIdent) : ProofModeM Q($e ⊢ $goal) :=
+  iRevertIntro hyps goal targets 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 · · addBIGoal)
+    return q($(pf').trans $pf)
+
 /--
   `iloeb as IH generalizing hs` applies Löb induction in the current goal
   using the induction hypothesis `IH`, optionally with other variables can be
-  generalized over through the `generalizing selPat*` syntax.
+  generalised over through the `generalizing selPat*` syntax. All spatial
+  hypothesis are generalised in the induction hypothesis. Hypotheses dependent
+  on those included in the selection pattern `hs` must also themselves be
+  included in `hs`.
 
-  All spatial hypothesis are generalized in the induction hypothesis.
+  `iloeb as IH generalizing! hs` is the same as `iloeb as IH generalizing hs`,
+  except that all hypotheses dependent on any hypothesis in the selection
+  pattern `hs` are implicitly reverted.
 -/
-elab "iloeb" " as " colGt IH:binderIdent " generalizing " hs:(colGt ppSpace selPat)* : tactic => do
-  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 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
-      return q($(pf').trans $pf)
-
-    mvid.assign expr
+elab_rules : tactic
+  | `(tactic| iloeb as $IH:binderIdent generalizing $hs:selPat*) => do
+    let pats ← Elab.liftMacroM <| SelPat.parse hs
 
-/--
-  `iloeb as IH` applies Löb induction in the current goal
-  using the induction hypothesis `IH`.
+    ProofModeM.runTactic fun mvid { hyps, goal, .. } => do
+      -- Parse the selection patterns provided by the tactic user
+      let targets : List SelTarget ← SelPat.resolve hyps (pats ++ [.spatial])
 
-  All spatial hypothesis are generalized in the induction hypothesis.
--/
-macro "iloeb" " as " colGt IH:binderIdent : tactic => `(tactic | iloeb as $IH generalizing)
+      -- Check for dependencies with the hypotheses in the selection targets
+      checkDependentHyps "iloeb" hyps targets none hs
+        (fun pats => `(tactic| iloeb as $IH generalizing $pats*))
+        (fun pats => `(tactic| iloeb as $IH generalizing! $pats*))
+
+      let expr ← iLoebCore hyps goal targets IH
+      mvid.assign expr
+  | `(tactic| iloeb as $IH:binderIdent $[generalizing! $hs:selPat*]?) => do
+    ProofModeM.runTactic fun mvid { hyps, goal, .. } => do
+      let targets ← do match hs with
+      | none =>
+        SelPat.resolve hyps [.spatial]
+      | some hs =>
+        -- Parse the selection patterns provided by the tactic user
+        let pats ← Elab.liftMacroM <| SelPat.parse hs
+        let targets ← SelPat.resolve hyps (pats ++ [.spatial])
+        -- Find all dependent hypotheses
+        let ⟨_, missingIrisHyps, allPureFVarsSorted⟩ ← getDependentHyps hyps targets none false
+        -- Obtain the selection targets, including dependent ones
+        pure <| getCompleteSelTargets targets missingIrisHyps allPureFVarsSorted
+
+      let expr ← iLoebCore hyps goal targets IH
+      mvid.assign expr
diff --git a/Iris/Iris/ProofMode/Tactics/Revert.lean b/Iris/Iris/ProofMode/Tactics/Revert.lean
index 7245dc91f..704529f9b 100644
--- a/Iris/Iris/ProofMode/Tactics/Revert.lean
+++ b/Iris/Iris/ProofMode/Tactics/Revert.lean
@@ -9,11 +9,21 @@ public import Iris.ProofMode.ClassesMake
 public meta import Iris.ProofMode.Patterns.SelPattern
 public meta import Iris.ProofMode.Tactics.Basic
 
+public meta import Iris.ProofMode.Tactics.Assumption
+public meta import Iris.ProofMode.Tactics.Cases
+public meta import Iris.ProofMode.Patterns.CasesPattern
+public meta import Lean.Meta.Tactic.TryThis
+
 namespace Iris.ProofMode
 
 public section
 open BI Std
 
+/- Syntax for `iinduction` and `iloeb` -/
+declare_syntax_cat generalizingSelPats
+syntax " generalizing " (ppSpace colGt selPat)* : generalizingSelPats
+syntax " generalizing! " (ppSpace colGt selPat)* : generalizingSelPats
+
 theorem wand_revert [BI PROP] {Δ Δ' P Q : PROP}
     (h1 : Δ ⊣⊢ Δ' ∗ P) (h2 : Δ' ⊢ P -∗ Q) : Δ ⊢ Q :=
   h1.mp.trans (wand_elim h2)
@@ -88,14 +98,142 @@ private def RevertState.revertLeanHyp
   let ldecl ← st.hyps.checkRemovableFVar "irevert" f none st.reverted.contains
   let v : Level ← Meta.getLevel ldecl.type
   have α : Q(Sort v) := ldecl.type
-  if ← Meta.isProp α then
+  if (← Meta.isProp α) && !st.goal.containsFVar f then
     have φ : Q(Prop) := α
     st.revertLeanPropHyp f φ
   else
     st.revertLeanForallHyp f α
 
-def iRevertCore (targets : List SelTarget) {u : Level}{prop: Q(Type $u)}{bi : Q(BI $prop)}{e : Q($prop)}(hyps : Hyps bi e)(goal: Q($prop))
-  (k : ∀ {e : Q($prop)}, Hyps bi e → (goal: Q($prop)) → ProofModeM Q($e ⊢ $goal) := addBIGoal) :
+def getDependentHyps {u} {prop : Q(Type $u)} {bi} {e : Q($prop)}
+    (hyps : Hyps bi e)
+    (explicitTargets : List SelTarget)
+    (inductionTarget : Option FVarId)
+    (includeSpatialHyps : Bool) :
+    ProofModeM <| List (FVarId × FVarId) × List (Name × IVarId × FVarId) × Array FVarId := do
+  let explicitIrisIVarIds := explicitTargets.filterMap
+    (match ·.kind with | .ipm ivar => some ivar | _ => none)
+  let explicitPureFVars :=
+    explicitTargets.filterMap
+    (match ·.kind with | .pure f => some f | _ => none) |>.append <|
+      inductionTarget.elim [] (.singleton ·)
+
+  -- Pairs of `FVarId` values `(f1, f2)` indicating `f1` depends on `f2`.
+  let mut missingPureHyps : List (FVarId × FVarId) := []
+
+  -- Check forward dependency of pure hypotheses
+  for fvar in explicitPureFVars.eraseDups do
+    let fwdDeps ← collectForwardDeps #[mkFVar fvar] false
+    for dep in fwdDeps do
+      let depId := dep.fvarId!
+      -- Skip `x` itself and variables already included in `explicitPureFVars`
+      if depId != fvar && !explicitPureFVars.contains depId then
+        -- Record the missing hypothesis to be generalised, if not already included
+        if !missingPureHyps.any (·.fst == depId) then
+          missingPureHyps := missingPureHyps.cons (depId, fvar)
+  missingPureHyps := missingPureHyps.reverse
+
+  let allPureFVars := explicitPureFVars ++ missingPureHyps.map (·.fst)
+
+  let irisHypsToBeChecked :=
+    hyps.intuitionisticIVarIds ++
+    if includeSpatialHyps then hyps.spatialIVarIds else []
+  -- Check forward dependency of Iris hypotheses
+  let missingIrisHyps : List (Name × IVarId × FVarId) :=
+    irisHypsToBeChecked.filterMap fun ivar =>
+      if explicitIrisIVarIds.contains ivar then none
+      else hyps.getDecl? ivar >>= fun ⟨name, _, _, ty⟩ =>
+        (allPureFVars.find? (ty.containsFVar ·)).map (name, ivar, ·)
+
+  -- Missing pure hypotheses does not include the induction target itself
+  let allPureFVars := allPureFVars.eraseDups.filter <|
+    fun fvar => inductionTarget.all (fvar != ·)
+
+  -- Sort the pure Lean hypothesis according to the dependency
+  let allPureFVarsSorted ← getLCtx <&> (·.sortFVarsByContextOrder allPureFVars.toArray)
+
+  return ⟨missingPureHyps, missingIrisHyps, allPureFVarsSorted⟩
+
+def getCompleteSelTargets (explicitTargets : List SelTarget)
+    (missingIrisHyps : List (Name × IVarId × FVarId))
+    (allPureVarsSorted : Array FVarId) :
+    List SelTarget :=
+  let pureTargets := allPureVarsSorted.toList.map ({ kind := .pure ·, explicit := true})
+  let explicitIrisTargets := explicitTargets.filter <|
+    fun t => match t.kind with | .ipm _ => true | _ => false
+  let implicitIrisTargets := missingIrisHyps.map <|
+    fun ⟨_, ivar, _⟩ => { kind := .ipm ivar, explicit := false }
+  pureTargets ++ explicitIrisTargets ++ implicitIrisTargets
+
+/--
+  Throw an error if there exists hypotheses that are depend on any hypothesis
+  in `explicitTargets` but are not themselves in the list.
+
+  The value `inductionTarget` can optionally be supplied. In this case,
+  hypotheses dependent on it should also be generalised.
+-/
+def checkDependentHyps {u} {prop : Q(Type $u)} {bi} {e : Q($prop)}
+    (tacticName : String) (hyps : Hyps bi e)
+    (explicitTargets : List SelTarget)
+    (inductionTarget : Option FVarId)
+    (selPats : TSyntaxArray `selPat)
+    (mkTacticExplicit mkTacticImplicit : TSyntaxArray `selPat → ProofModeM (TSyntax `tactic)) :
+    ProofModeM Unit := do
+  let ⟨missingPureHyps, missingIrisHyps, allPureFVarsSorted⟩ ←
+    getDependentHyps hyps explicitTargets inductionTarget true
+
+  -- Handle the printing of inaccessible names, if necessary
+  let ppHypName := fun name =>
+    if name.hasMacroScopes then
+      s!"`{name.eraseMacroScopes}` (inaccessible name)"
+    else s!"`{name.toString}`"
+
+  -- Add an error message if there exists some pure/Lean hypotheses that should also be generalised
+  if !missingPureHyps.isEmpty || !missingIrisHyps.isEmpty then
+    let leanLines ← missingPureHyps.mapM fun ⟨depId, srcId⟩ => do
+      let depDecl ← depId.getDecl
+      let srcDecl ← srcId.getDecl
+      return s!"• Lean hypothesis {ppHypName depDecl.userName} depends on {ppHypName srcDecl.userName}"
+    let irisLines ← missingIrisHyps.mapM fun ⟨depName, _, srcId⟩ => do
+      let srcDecl ← srcId.getDecl
+      return s!"• Iris hypothesis {ppHypName depName} depends on {ppHypName srcDecl.userName}"
+
+    let sortedPurePats : Array (TSyntax `selPat) ← allPureFVarsSorted.mapM fun fvarId => do
+      let decl ← fvarId.getDecl
+      let id := mkIdent <| .mkSimple decl.userName.toString
+      `(selPat| %$id:ident)
+
+    -- Build `selPat` syntax nodes for each missing item
+    let newIrisPats : Array (TSyntax `selPat) ←
+      missingIrisHyps.toArray.mapM fun ⟨name, _⟩ => `(selPat| $(mkIdent name):ident)
+
+    -- Check whether the new selecton pattern may contain any inaccessible names
+    let allNamesAccessible :=
+      (missingIrisHyps.all fun ⟨name, _, _⟩ => !name.hasMacroScopes) &&
+      !(← allPureFVarsSorted.anyM fun fvarId => do return (← fvarId.getDecl).userName.hasMacroScopes)
+
+    -- Find the old tactic syntax and generate the new one with missing hypotheses added
+    let oldTactic ← getRef
+
+    -- Suggest a fixed tactic with explicit generalisations
+    if allNamesAccessible then
+      let existingIrisPats := selPats.filter fun p =>
+        match p.raw with | `(selPat| %$_:ident) => false | _ => true
+      let extendedPats := sortedPurePats ++ existingIrisPats ++ newIrisPats
+      let newTactic ← mkTacticExplicit extendedPats
+      Lean.Meta.Tactic.TryThis.addSuggestion oldTactic newTactic
+
+    -- Suggest a fixed tactic with implicit generalisations
+    let newTactic ← mkTacticImplicit selPats
+    Lean.Meta.Tactic.TryThis.addSuggestion oldTactic newTactic
+
+    -- Log the error and attach the clickable suggestion
+    throwError m!"{tacticName}: The following hypotheses depend on variables in \
+      the `generalizing` clause but are not themselves included:\
+      \n{"\n".intercalate (leanLines ++ irisLines)}"
+
+def iRevertCore (targets : List SelTarget) {u : Level} {prop: Q(Type $u)}
+    {bi : Q(BI $prop)} {e : Q($prop)} (hyps : Hyps bi e) (goal: Q($prop))
+    (k : ∀ {e : Q($prop)}, Hyps bi e → (goal: Q($prop)) → ProofModeM Q($e ⊢ $goal) := addBIGoal) :
     ProofModeM Q($e ⊢ $goal) := do
   let init : RevertState e goal := { e, hyps, goal, pf := q(id) }
   let st ← targets.reverse.foldlM (init := init) fun st target => do
@@ -103,17 +241,46 @@ def iRevertCore (targets : List SelTarget) {u : Level}{prop: Q(Type $u)}{bi : Q(
       | .ipm ivar => st.revertProofModeHyp ivar
       | .pure fvar => st.revertLeanHyp fvar
 
-  let pf' : Q($(st.e) ⊢ $(st.goal)) ← withoutFVars (u:=0) st.reverted (k st.hyps st.goal)
+  let pf' : Q($(st.e) ⊢ $(st.goal)) ← withoutFVars (u := 0) st.reverted (k st.hyps st.goal)
   return q($(st.pf) $pf')
 
+syntax (name := irevert) "irevert " (colGt ppSpace selPat)+ : tactic
+syntax (name := irevert!) "irevert! " (colGt ppSpace selPat)+ : tactic
+
 /--
   `irevert pats` reverts the hypotheses specified by the selection pattern `pats`
-  from the Iris contexts back into the regular Lean context.
+  from context back into the proof goal. Pure/Iris hypotheses
+  dependent on any hypothesis specified by `pats` must also themselves be
+  included in the selection pattern.
+
+  `irevert! pats` is similar to `irevert pats`, except that pure/Iris hypotheses
+  dependent on any hypothesis specified by `pats` are automatically reverted.
 -/
-elab "irevert " pats:(colGt ppSpace selPat)+ : tactic => do
-  let pats ← liftMacroM <| SelPat.parse pats
+elab_rules : tactic
+  | `(tactic| irevert $pats:selPat*) => do
+    let parsedPats ← liftMacroM <| SelPat.parse pats
+
+    ProofModeM.runTactic fun mvar { hyps, goal, .. } => do
+      -- Parse the selection patterns provided by the tactic user
+      let targets ← SelPat.resolve hyps parsedPats
+
+      -- Check for dependencies with the hypotheses in the selection targets
+      checkDependentHyps "irevert" hyps targets none pats
+        (fun pats => `(tactic| irevert $pats*))
+        (fun pats => `(tactic| irevert! $pats*))
+
+      let expr ← iRevertCore targets hyps goal
+      mvar.assign expr
+  | `(tactic| irevert! $pats:selPat*) => do
+    let parsedPats ← liftMacroM <| SelPat.parse pats
+
+    ProofModeM.runTactic fun mvar { hyps, goal, .. } => do
+      -- Parse the selection patterns provided by the tactic user
+      let explicitTargets ← SelPat.resolve hyps parsedPats
+      -- Find all dependent hypotheses
+      let ⟨_, missingIrisHyps, allPureFVarsSorted⟩ ← getDependentHyps hyps explicitTargets none true
+      -- Obtain the selection targets, including dependent ones
+      let targets := getCompleteSelTargets explicitTargets missingIrisHyps allPureFVarsSorted
 
-  ProofModeM.runTactic fun mvar {hyps, goal, ..} => do
-    let targets ← SelPat.resolve hyps pats
-    let expr ← iRevertCore targets hyps goal
-    mvar.assign expr
+      let expr ← iRevertCore targets hyps goal
+      mvar.assign expr
diff --git a/Iris/Iris/ProofMode/Tactics/RevertIntro.lean b/Iris/Iris/ProofMode/Tactics/RevertIntro.lean
index 380de3c6d..e567c1b38 100644
--- a/Iris/Iris/ProofMode/Tactics/RevertIntro.lean
+++ b/Iris/Iris/ProofMode/Tactics/RevertIntro.lean
@@ -13,16 +13,21 @@ open Lean Meta Elab.Tactic Qq
 
 public meta section
 
-abbrev ProofModeContinuation (u : Level) :=
-  ∀ {prop : Q(Type u)} {bi : Q(BI $prop)} {e : Q($prop)}
-    (_hyps : Hyps bi e)(goal: Q($prop)),
+abbrev ProofModeContinuationIntro :=
+  ∀ {u : Level} {prop : Q(Type u)} {bi : Q(BI $prop)} {e : Q($prop)}
+    (_hyps : Hyps bi e) (goal: Q($prop)),
+    ProofModeM Q($e ⊢ $goal)
+
+abbrev ProofModeContinuationRevert :=
+  ∀ {u : Level} {prop : Q(Type u)} {bi : Q(BI $prop)} {e : Q($prop)}
+    (_hyps : Hyps bi e) (goal : Q($prop)), ProofModeContinuationIntro →
     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)
   (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)), ProofModeContinuationRevert →
     ProofModeM Q($e ⊢ $goal))
    : ProofModeM Q($e ⊢ $goal) := do
   let names : List (Syntax × IntroPat) ← hs.mapM fun
@@ -36,7 +41,7 @@ def iRevertIntro
       return (name, .intro <| (if ivar.persistent? then .intuitionistic else id) <| .one 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
+    k hyps goal fun hyps goal k' => do
+      iIntroCore hyps goal names k'
 
 initialize registerTraceClass `irevertintro
diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean
index fb8509a5f..0624ddcc6 100644
--- a/Iris/Iris/Tests/Tactics.lean
+++ b/Iris/Iris/Tests/Tactics.lean
@@ -377,19 +377,40 @@ example [BI PROP] (P : PROP) {x : Nat} : ⊢ P := by
   irevert %x
 
 /- Tests `irevert` failing with dependency -/
-/-- error: irevert: proofmode hypothesis H depends on x -/
+/-- info: Try this:
+  [apply] irevert %x %hp H
+---
+info: Try this:
+  [apply] irevert! %x
+---
+error: irevert: The following hypotheses depend on variables in the `generalizing` clause but are not themselves included:
+• Lean hypothesis `hp` depends on `x`
+• Iris hypothesis `H` depends on `x` -/
 #guard_msgs in
 example [BI PROP] (Φ : Bool → PROP) : ⊢ ∀ x, <affine> ⌜x = true⌝ -∗ Φ x -∗ Φ x := by
   iintro %x %hp H
   irevert %x
 
-/- Tests `irevert` failing with dependency -/
-/-- error: irevert: Lean hypothesis hp depends on x -/
+/-
+  Tests `irevert` failing with dependency, involving an inaccessible name
+-/
+/-- info: Try this:
+  [apply] irevert! %x H
+---
+error: irevert: The following hypotheses depend on variables in the `generalizing` clause but are not themselves included:
+• Lean hypothesis `x` (inaccessible name) depends on `x` -/
 #guard_msgs in
 example [BI PROP] (Φ : Bool → PROP) : ⊢ ∀ x, <affine> ⌜x = true⌝ -∗ Φ x -∗ Φ x := by
-  iintro %x %hp H
+  iintro %x %_ H
   irevert %x H
 
+/-- Tests `irevert!` which reverts `H2` and `H3` automatically -/
+example [BI PROP] (Φ : Bool → PROP) (x y : Bool) :
+    (∀ x, (Φ x -∗ Φ y) -∗ Φ x -∗ Φ y) ∗ (Φ x -∗ Φ y) ∗ Φ x ⊢ Φ y := by
+  iintro ⟨H1, H2, H3⟩
+  irevert! %x
+  iassumption
+
 end revert
 
 -- exists
@@ -2650,6 +2671,7 @@ end icombine
 section iloeb
 
 variable {PROP : Type u} [ι₁ : BI PROP] [ι₂ : BILoeb PROP]
+
 -- Tests `iloeb` basic
 /--
 error: unsolved goals
@@ -2775,4 +2797,407 @@ example (P Q : PROP) :
     ⊢ P -∗ Q := by
   iloeb as IH
 
+-- Tests `iloeb` where the `generalizing` clause has dependency
+/--
+info: Try this:
+  [apply] iloeb as IH generalizing %n %h1 %U HT
+---
+info: Try this:
+  [apply] iloeb as IH generalizing! %n
+---
+error: iloeb: The following hypotheses depend on variables in the `generalizing` clause but are not themselves included:
+• Lean hypothesis `h1` depends on `n`
+• Lean hypothesis `U` depends on `n`
+• Iris hypothesis `HT` depends on `n`
+-/
+#guard_msgs in
+example {n : Nat} {P T : Nat → PROP} {Q : Nat → Prop} {h1 : Q n} {U : (Q n) → Prop} :
+    ⊢ □ T n -∗ □ P n := by
+  iintro #HT
+  iloeb as IH generalizing %n
+
+-- Same test as above, involving inaccessible names
+/--
+info: Try this:
+  [apply] iloeb as IH generalizing! %n
+---
+error: iloeb: The following hypotheses depend on variables in the `generalizing` clause but are not themselves included:
+• Lean hypothesis `h1` depends on `n`
+• Lean hypothesis `x` (inaccessible name) depends on `n`
+• Iris hypothesis `x` (inaccessible name) depends on `n`
+-/
+#guard_msgs in
+example {n : Nat} {P T : Nat → PROP} {Q : Nat → Prop} {h1 : Q n} {_ : (Q n) → Prop} :
+    ⊢ □ T n -∗ □ P n := by
+  iintro #_
+  iloeb as IH generalizing %n
+
+-- Same test as above, except `generalizing!` is used
+/--
+error: unsolved goals
+PROP : Type u
+ι₁ : BI PROP
+ι₂ : BILoeb PROP
+P T : Nat → PROP
+Q : Nat → Prop
+n : Nat
+h1 : Q n
+x✝ : Q n → Prop
+⊢ ⏎
+  □IH : ▷ ∀ n, <affine> ⌜Q n⌝ -∗ ∀ x, □ T n -∗ □ P n
+  □x✝ : T n
+  ⊢ □ P n
+-/
+#guard_msgs in
+example {n : Nat} {P T : Nat → PROP} {Q : Nat → Prop} {h1 : Q n} {_ : (Q n) → Prop} :
+    ⊢ □ T n -∗ □ P n := by
+  iintro #_
+  iloeb as IH generalizing! %n
+
 end iloeb
+
+section iinduction
+
+/-- Inductively defined binary tree data structure -/
+inductive Tree (α : Type u) where
+  | leaf : Tree α
+  | node : Tree α → α → Tree α → Tree α
+  deriving Repr
+
+/--
+  Tests `iinduction` with simple induction on binary trees.
+  All propositions involved are in the intuitionistic context in this example.
+  Tests the use of a hole (`_`) for leaving a variable unnamed.
+-/
+example [BI PROP] {α} {t : Tree α} {P : Tree α → PROP} :
+    □ P .leaf -∗ □ (∀ l x r, P l -∗ P r -∗ P (.node l x r)) -∗ P t := by
+  iintro #H1 #H2
+  iinduction t with
+  | leaf => iexact H1
+  | node l _ r IH1 IH2 =>
+    iapply H2
+    · iexact IH1
+    · iexact IH2
+
+/-- A simple function on the inductive structure `Tree` -/
+def Tree.mirror : Tree α → Tree α
+  | .leaf => .leaf
+  | .node l x r => .node (.mirror r) x (.mirror l)
+
+/--
+  Tests `iinduction` with a pure hypothesis that involves `Tree.mirror`.
+-/
+example [BI PROP] {α} {t : Tree α} :
+  ⊢@{PROP} ⌜.mirror (.mirror t) = t⌝ := by
+  iinduction t with simp [Tree.mirror]
+  | leaf =>
+    itrivial
+  | node l x r ihl ihr =>
+    isplit
+    · iexact ihl
+    · iexact ihr
+
+/-- An inductively defined predicate on `Tree` -/
+def Tree.pred [BI PROP] (P : α → PROP) : Tree α → PROP
+  | .leaf => emp
+  | .node l x r => iprop(Tree.pred P l ∗ (P x ∗ Tree.pred P r))
+
+/--
+  Tests `iinduction` with spatial hypotheses that involve `Tree.mirror` and `Tree.pred`.
+-/
+example [BI PROP] {α} {t : Tree α} {P : α → PROP} :
+    Tree.pred P t -∗ Tree.pred P (.mirror t) := by
+  iintro H
+  iinduction t with simp [Tree.mirror, Tree.pred]
+  | leaf => itrivial
+  | node l x r ihl ihr =>
+    icases H with ⟨Hl, Hx, Hr⟩
+    iframe
+    isplitl [Hr]
+    · iapply ihr $$ Hr
+    · iapply ihl $$ Hl
+
+/--
+  Definition of n-tree and its induction principle from:
+  https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/.E2.9C.94.20Induction.20principle.20for.20nested.20inductive.20types/near/437905021
+-/
+inductive NTree (α : Type)
+| leaf
+| node : α → List (NTree α) → NTree α
+
+@[induction_eliminator]
+def NTree.induction_principle {α} (p : NTree α → Prop) (h_leaf : p leaf)
+  (h_node : (x : α) → (ts : List (NTree α)) → (ih : ∀ t ∈ ts, p t) → p (node x ts)) :
+  ∀ t : NTree α, p t :=
+  @NTree.rec α p (λ ts => ∀ t ∈ ts, p t) h_leaf h_node (List.forall_mem_nil p)
+    (λ _ _ h_head h_tail => List.forall_mem_cons.mpr (And.intro h_head h_tail))
+
+def NTree.id : NTree α → NTree α
+  | .leaf => .leaf
+  | .node x ts => .node x (ts.map .id)
+
+/-- Tests `iinduction` with the mutual induction principle -/
+example [BI PROP] {α} {t : NTree α} : ⊢@{PROP} ⌜t.id = t⌝ := by
+  iinduction t with simp [NTree.id]
+  | h_leaf => itrivial
+  | h_node x ts IH1 =>
+    iinduction ts with simp
+    | nil => itrivial
+    | cons t ts IH2 =>
+      isplit
+      · iapply IH1
+        itrivial
+      · iapply IH2
+        iintro !> %x H
+        iapply IH1
+        imodintro
+        iright
+        iexact H
+
+def NTree.childCount : NTree α → Nat
+  | .leaf => 0
+  | .node _ ts => ts.length
+
+/-- An binary relation defined using nested induction -/
+inductive NTree.Rel {α β} (R : α → β → Prop) : NTree α → NTree β → Prop
+  | leaf : Rel R .leaf .leaf
+  | node : ∀ a b ts₁ ts₂, R a b → List.Forall₂ (Rel R) ts₁ ts₂ → Rel R (.node a ts₁) (.node b ts₂)
+
+@[induction_eliminator]
+def NTree.Rel.induction_principle {α β} {R : α → β → Prop}
+    (p : ∀ {t1 : NTree α} {t2 : NTree β}, NTree.Rel R t1 t2 → Prop)
+    (h_base : p .leaf)
+    (h_step : ∀ a b ts1 ts2 ra f2,
+      List.Forall₂ (fun t1 t2 => ∀ h : NTree.Rel R t1 t2, p h) ts1 ts2 →
+      p (.node a b ts1 ts2 ra f2)) :
+    ∀ t1 t2 (h : NTree.Rel R t1 t2), p h :=
+  @NTree.Rel.rec α β R
+    (fun _ _ h => p h)
+    (fun a b _ => List.Forall₂ (fun t1 t2 => ∀ h : NTree.Rel R t1 t2, p h) a b)
+    h_base h_step .nil
+    (fun _ _ ih_h ih_hs => .cons (fun _ => ih_h) ih_hs)
+
+/-- Tests `iinduction` with induction that uses the type class instance `intoIH_listForall₂`. -/
+example [BI PROP] {α β} {R : α → β → Prop}
+    {t₁ : NTree α} {t₂ : NTree β} (H : NTree.Rel R t₁ t₂) :
+    ⊢@{PROP} ⌜NTree.childCount t₁ = NTree.childCount t₂⌝ := by
+  iinduction H with
+  | h_base =>
+    ipureintro
+    apply rfl
+  | h_step x1 x2 t1 t2 r IH1 IH2 =>
+    ipureintro
+    simp only [NTree.childCount]
+    induction IH1 with simp_all
+
+/--
+  Tests `iinduction` with simple induction on natural numbers.
+  Tries `iframe` to solve induction subgoals before splitting into cases.
+  Tests the `using` clause for custom recursor name.
+  Tests the use of a synthetic hole (`?_`) for delaying the induction subgoal.
+-/
+example [BI PROP] {n : Nat} {P : Nat → PROP} :
+    □ (∀ k, P k -∗ P (k + 1)) -∗ P 0 -∗ P n := by
+  iintro #H1 H2
+  iinduction n using Nat.rec with iframe
+  | succ n IH => ?_
+  iapply H1
+  iapply IH
+  iexact H2
+
+/--
+  Tests `iinduction` with induction on lists where it is necessary to
+  generalise some variables.
+  Tests the use of the wildcard (`_`) for remaining cases.
+-/
+example [BI PROP] {α} {xs : List α} {acc : List α} {P : List α → List α → PROP} :
+    □ (∀ acc, P [] acc) -∗
+    □ (∀ x xs acc, P xs (x :: acc) -∗ P (x :: xs) acc) -∗
+    P xs acc := by
+  iintro #Hnil #Hcons
+  iinduction xs generalizing %acc with
+  | cons x xs IH =>
+    iapply Hcons
+    iexact IH
+  | _ =>
+    iapply Hnil
+
+/- Tests `iinduction` with a non-inductive datatype. -/
+/-- error: iinduction: unable to determine inductive type -/
+#guard_msgs in
+example [BI PROP] {P : PROP} : ⊢ P := by
+  iinduction P
+
+/-
+  Tests `iinduction` with induction on natural numbers with invalid, duplicate
+  and missing user-supplied alternative names.
+-/
+/-- error: iinduction: invalid alternative name `invalidA`
+---
+error: iinduction: invalid alternative name `invalidB`
+---
+error: iinduction: duplicate alternative name `zero`
+---
+error: iinduction: alternative `succ` has not been provided -/
+#guard_msgs in
+example [BI PROP] {n : Nat} :
+    ⊢@{PROP} ⌜n + 0 = n⌝ := by
+  iinduction n with
+  | invalidA  => done
+  | zero      => itrivial
+  | invalidB  => done
+  | zero      => itrivial
+
+/- Tests `iinduction` with extra arguments supplied by the user -/
+/-- error: iinduction: too many variable names provided at alternative `succ`: 4 provided, but 2 expected -/
+#guard_msgs in
+example [BI PROP] {n : Nat} :
+    ⊢@{PROP} ⌜n + 0 = n⌝ := by
+  iinduction n with
+  | zero => itrivial
+  | succ n IH extra1 extra2 => itrivial
+
+/--
+  Tests `iinduction` using a custom recursor name (strong induction).
+  Tests induction on an expression `n + m`, which requires generalisation.
+  Tests the use of the same tactic sequences for multiple alternative names.
+  Note that `P` and `S` are reverted and thus included as wand premises
+  in the induction hypothesis.
+  Meanwhile, `T (n + m)` is also reverted because it involves the induction
+  target `n + m`.
+  The proposition `Q m` is reverted manually using the `generalizing` clause.
+  On the contrary, `R` is not reverted.
+-/
+example [BI PROP] {P R S : PROP} {Q T : Nat → PROP} {m n : Nat} :
+    ⊢ P -∗ □ Q m -∗ □ R -∗ S -∗ □ T (n + m) -∗ ⌜n + m + 0 = n + m⌝ := by
+  iintro HP #HQ #HR HS #HT
+  iinduction n + m using Nat.caseStrongRecOn generalizing %m HQ HT with
+  | zero | ind _ _ => itrivial
+
+/-
+  Tests `iinduction` with invalid use of the wildcard. The wildcard
+  should always be the last case.
+-/
+/-- error: iinduction: invalid occurrence of the wildcard alternative `| _ => ...`: It must be the last alternative -/
+#guard_msgs in
+example [BI PROP] {n : Nat} :
+    ⊢@{PROP} ⌜n + 0 = n⌝ := by
+  iinduction n with
+  | zero => itrivial
+  | _ => _
+  | succ n IH => itrivial
+
+/-
+  Tests `iinduction` with redundant use of the wildcard. The wildcard
+  is not required when all cases have already been handled.
+-/
+/-- error: iinduction: wildcard alternative is not needed -/
+#guard_msgs in
+example [BI PROP] {n : Nat} :
+    ⊢@{PROP} ⌜n + 0 = n⌝ := by
+  iinduction n with
+  | zero => itrivial
+  | succ n IH => itrivial
+  | _ => _
+
+/-
+  Tests `iinduction` with the tactic after `with` syntax.
+  One of the alternative names (`zero`) becomes redundant and therefore should
+  be detected by the tactic.
+-/
+/-- error: iinduction: alternative `zero` is not needed -/
+#guard_msgs in
+example [BI PROP] {P Q R S T : PROP} {n : Nat} :
+    ⊢ P -∗ □ Q -∗ □ R -∗ S -∗ □ T -∗ ⌜0 + 0 = 0⌝ -∗ ⌜n + 0 = n⌝ := by
+  iintro HP #HQ #HR HS #HT #H
+  iinduction n with (try iexact H)
+  | zero => itrivial  -- Redundant case
+  | succ n IH => itrivial
+
+/-
+  Tests `iinduction` with a tactic after `with` syntax.
+  One of the alternative names (`zero`) is redundant and therefore not required.
+  The tactic should not complain about any missing alternative names.
+-/
+example [BI PROP] {P Q R S T : PROP} {n : Nat} :
+    ⊢ P -∗ □ Q -∗ □ R -∗ S -∗ □ T -∗ ⌜0 + 0 = 0⌝ -∗ ⌜n + 0 = n⌝ := by
+  iintro HP #HQ #HR HS #HT #H
+  iinduction n with (try iexact H)
+  -- No complaints about missing `zero` case
+  | succ n IH => itrivial
+
+/-
+  Tests `iinduction` on `n` generalising `m`, where:
+  - *regular hypotheses* `h1 : T m` and `U1 : (T m) → Prop` depend on `m`;
+  - *regular hypotheses* `h2 : U1 h1` and `U2 : (U1 h1) → PROP` depends on `h1`,
+    which in turn depends on `m`;
+  - *Iris hypotheses* `□HQ : Q m` and `□HR : R m` depend on `m`;
+  - *Iris hypothesis* `□HS : S n` depends on the induction target `n`;
+  - *Iris hypothesis* `□HU2 : U2 h2` depends on `h2` and `U2`, which depends
+    depend on `h1`, which in turn depends on `m`.
+  This requires manual resolution.
+-/
+/-- info: Try this:
+  [apply] iinduction n generalizing %m %h1 %U1 %h2 %U2 HQ HR HS HU2 with
+  | zero
+  | succ n IH => itrivial
+---
+info: Try this:
+  [apply] iinduction n generalizing! %m with
+  | zero
+  | succ n IH => itrivial
+---
+error: iinduction: The following hypotheses depend on variables in the `generalizing` clause but are not themselves included:
+• Lean hypothesis `h1` depends on `m`
+• Lean hypothesis `U1` depends on `m`
+• Lean hypothesis `h2` depends on `m`
+• Lean hypothesis `U2` depends on `m`
+• Iris hypothesis `HQ` depends on `m`
+• Iris hypothesis `HR` depends on `m`
+• Iris hypothesis `HS` depends on `n`
+• Iris hypothesis `HU2` depends on `h2` -/
+#guard_msgs in
+example [BI PROP] {P : PROP} {m n : Nat} {Q R S : Nat → PROP} {T : Nat → Prop}
+    {h1 : T m} {U1 : (T m) → Prop} {h2 : U1 h1} {U2 : (U1 h1) → PROP} :
+    ⊢ P -∗ □ Q m -∗ □ R m -∗ □ S n -∗ □ U2 h2 -∗ ⌜n + 0 = n⌝ := by
+  iintro HP #HQ #HR #HS #HU2
+  iinduction n generalizing %m with
+  | zero
+  | succ n IH => itrivial
+
+/--
+  The same example with `generalizing!` clause does not require any manual
+  resolution of dependencies.
+-/
+example [BI PROP] {P : PROP} {m n : Nat} {Q R S : Nat → PROP} {T : Nat → Prop}
+    {h1 : T m} {U1 : (T m) → Prop} {h2 : U1 h1} {U2 : (U1 h1) → PROP} :
+    ⊢ P -∗ □ Q m -∗ □ R m -∗ □ S n -∗ □ U2 h2 -∗ ⌜n + 0 = n⌝ := by
+  iintro HP #HQ #HR #HS #HU2
+  iinduction n generalizing! %m with
+  | zero
+  | succ n IH => itrivial
+
+/- Similar test as above, except that some hypotheses have inaccessible names. -/
+/-- info: Try this:
+  [apply] iinduction n generalizing! %m with
+  | zero
+  | succ n IH => itrivial
+---
+error: iinduction: The following hypotheses depend on variables in the `generalizing` clause but are not themselves included:
+• Lean hypothesis `h1` depends on `m`
+• Lean hypothesis `U1` depends on `m`
+• Lean hypothesis `h2` depends on `m`
+• Lean hypothesis `U2` depends on `m`
+• Lean hypothesis `x` (inaccessible name) depends on `n`
+• Iris hypothesis `x` (inaccessible name) depends on `h2` -/
+#guard_msgs in
+example [BI PROP] {P : PROP} {m n : Nat} {T : Nat → Prop}
+    {h1 : T m} {_ : T n} {U1 : (T m) → Prop}
+    {h2 : U1 h1} {U2 : (U1 h1) → PROP} :
+    ⊢ P -∗ □ U2 h2 -∗ ⌜n + 0 = n⌝ := by
+  iintro HP #_
+  iinduction n generalizing %m with
+  | zero
+  | succ n IH => itrivial
+
+end iinduction
diff --git a/Iris/tactics.md b/Iris/tactics.md
index f9e465ec0..6b4f2cc97 100644
--- a/Iris/tactics.md
+++ b/Iris/tactics.md
@@ -12,7 +12,8 @@ The proof mode maintains three contexts: the *pure* (Lean) context, the *intuiti
 - `irename` *H* `=>` *H'* — Rename the hypothesis *H* to *H'*.
 - `irename :` *term* `=>` *H'* — Rename the hypothesis whose statement matches *term* to *H'*.
 - `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.
+- `irevert` [*selPats*](#selection-patterns) — Revert the selected hypotheses (proof mode or pure Lean hypotheses) into the goal. An Iris hypothesis *H* in *selPats* is reverted as a wand premise. If a pure hypothesis *H* in *selPats* has a type `φ` such that `φ : Prop`, then *H* is reverted as a premise. If *x* in *selPats* has a type `α` such that `α` is non-`Prop`, then *x* is reverted as a universally quantified variable. For every hypothesis *H* being reverted, all hypotheses dependent on *H* must also be reverted.
+- `irevert!` [*selPats*](#selection-patterns) — similar to `irevert` [*selPats*](#selection-patterns), except that for every hypothesis in *selPats*, hypotheses dependent on *H* are also implicitly reverted.
 - `ipure` *H* — Move the pure hypothesis *H* into the Lean context.
 - `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`.
@@ -57,7 +58,11 @@ The proof mode maintains three contexts: the *pure* (Lean) context, the *intuiti
 ## Rewriting and Induction
 
 - `irewrite [`*rules*`]` (`at` *H* | `at ⊢`)? — Rewrite with internal equalities (`≡`). Each rule is a [*pmTerm*](#proof-mode-terms), optionally prefixed with `←` for right-to-left rewriting. Rewrites in the goal by default or in hypothesis *H*. Supports `(occs := ...)` config. Example: `irewrite [← Heq $$ %b] at H`.
-- `iloeb as` *IH* (`generalizing` [*selPats*](#selection-patterns))? — Löb induction: adds the induction hypothesis *IH* (guarded by `▷`) to the intuitionistic context. All spatial hypotheses — plus anything selected by [*selPats*](#selection-patterns), including pure variables via `%x` — are generalized into the induction hypothesis.
+- `iloeb as` *IH* (`generalizing` [*selPats*](#selection-patterns))? — Löb induction: adds the induction hypothesis *IH* (guarded by `▷`) to the intuitionistic context. All spatial hypotheses — plus anything selected by [*selPats*](#selection-patterns), including pure variables via `%x` — are generalized into the induction hypothesis. For every hypothesis *H* in *selPats*, all hypotheses dependent on *H* must also be included in *selPats*.
+- `iloeb as` *IH* `generalizing!` [*selPats*](#selection-patterns) — same as `iloeb as` *IH* `generalizing` [*selPats*](#selection-patterns), except that for every hypothesis *H* in [*selPats*](#selection-patterns), all hypotheses dependent on *H* are implicitly also generalised.
+- `iinduction` *e* (`using` *r*)? (`with` (*tac*)? `|` *constr₁* `=>` *tac₁* `|` ... `|` *constrₙ* `=>` *tacₙ*)? — All spatial hypotheses, as well as pure/intuitionistic hypotheses dependent on *e*, are generalised and included as premises in the induction hypotheses. The induction principle is determined by the recursor name *r*, if given, or otherwise the default induction principle is chosen. The `with` clause enables alternative names to be given to variables and induction hypotheses. Each of *constr₁*, ..., *constrₙ* is the constructor name followed by the alternative names. Alternative names can be replaced with holes (`_`) for them to remain inaccessible. Each of *tac₁*, ..., *tacₙ* is either a tactic sequence for the induction subgoal or a hole (`_` or `?_`); the latter defers the induction subgoal. The tactic *tac* is optionally given, which is the first tactic applied to all induction subgoals.
+- `iinduction` *e* (`using` *r*)? `generalizing` [*selPats*](#selection-patterns) (`with` (*tac*)? `|` *constr₁* `=>` *tac₁* `|` ... `|` *constrₙ* `=>` *tacₙ*)? — Same as above, except that the hypotheses specified by [*selPats*](#selection-patterns) are also generalised. For every hypothesis *H* in [*selPats*](#selection-patterns), all hypotheses dependent on *H* or *e* must also be included in [*selPats*](#selection-patterns).
+- `iinduction` *e* (`using` *r*)? `generalizing!` [*selPats*](#selection-patterns) (`with` (*tac*)? `|` *constr₁* `=>` *tac₁* `|` ... `|` *constrₙ* `=>` *tacₙ*)? — Same as above, except that for every hypothesis *H* in *selPats*, hypotheses dependent on *H* or *e* are implicitly generalised.
 
 ## Solving Simple Goals