diff --git a/Iris/Iris/ProofMode/Classes.lean b/Iris/Iris/ProofMode/Classes.lean
index fdbe326cb..18868a05a 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
 
@@ -208,18 +208,27 @@ class IntoLaterN {PROP} [BI PROP] (only_head : Bool) (n : Nat) (P : PROP) (Q : o
 export IntoLaterN (into_laterN)
 
 /-- `CombineSepAs` combines two propositions `P` and `Q` into `R` -/
-@[ipm_class]
+@[ipm_class, rocq_alias CombineSepAs]
 class CombineSepAs [BI PROP] (P Q : PROP) (R : outParam PROP) where
   combine_sep_as : P ∗ Q ⊢ R
 export CombineSepAs (combine_sep_as)
 
 /-- `CombineSepGives` combines two propositions `P` and `Q` for a proposition
     with the `<pers>` modality -/
-@[ipm_class]
+@[ipm_class, rocq_alias CombineSepGives]
 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 481b3bcc5..8c74c91fc 100644
--- a/Iris/Iris/ProofMode/Expr.lean
+++ b/Iris/Iris/ProofMode/Expr.lean
@@ -189,6 +189,12 @@ partial def Hyps.intuitionisticIVarIds {u prop bi} :
   | _, .hyp _ _ ivar p _ _ => if isTrue p then [ivar] else []
   | _, .sep _ _ _ _ lhs rhs => lhs.intuitionisticIVarIds ++ rhs.intuitionisticIVarIds
 
+partial def Hyps.intuitionisticProps {u prop bi} :
+    ∀ {s}, @Hyps u prop bi s → List Q($prop)
+  | _, .emp _ => []
+  | _, .hyp tm _ _ p _ _ => if isTrue p then [tm] else []
+  | _, .sep _ _ _ _ lhs rhs => lhs.intuitionisticProps ++ rhs.intuitionisticProps
+
 variable (oldIVar : IVarId) (new : Name) {prop : Q(Type u)} {bi : Q(BI $prop)} in
 def Hyps.rename : ∀ {e}, Hyps bi e → Option (Hyps bi e)
   | _, .emp _ => none
@@ -484,6 +490,11 @@ structure IrisGoal where
 
 def isIrisGoal (expr : Expr) : Bool := isAppOfArity expr ``Entails' 4
 
+partial def isIrisGoalWithForalls (expr : Expr) : Bool :=
+  match expr.consumeMData with
+  | .forallE _ _ e _ => isIrisGoalWithForalls e
+  | e => isIrisGoal e
+
 def parseIrisGoal? (expr : Expr) : Option IrisGoal := do
   -- remove top-level metadata when matching on the goal
   let expr := expr.consumeMData
diff --git a/Iris/Iris/ProofMode/Instances.lean b/Iris/Iris/ProofMode/Instances.lean
index 53fecb860..762aca43c 100644
--- a/Iris/Iris/ProofMode/Instances.lean
+++ b/Iris/Iris/ProofMode/Instances.lean
@@ -7,6 +7,7 @@ module
 
 public import Iris.BI
 public import Iris.ProofMode.Classes
+public import Iris.ProofMode.ClassesMake
 public import Iris.ProofMode.ModalityInstances
 public import Iris.Std.TC
 public import Iris.Std.RocqPorting
@@ -917,3 +918,69 @@ 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_2.trans (persistently_mono h.combine_sep_gives)
+
+@[rocq_alias into_ih_entails]
+instance intoIH_entails [BI PROP] (P Q : PROP) : IntoIH (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_r h1.make_affinely.mpr).trans ?_
+    refine persistent_and_affinely_sep_r.2.trans ?_
+    exact pure_elim_r (fun hφ => h2.into_ih (hImp hφ))
+
+/-- Support for induction principles whose IH is guarded by `List.Forall`, e.g.
+    `∀ l, Forall P l → P (Tree l)` arising from nested inductive types like
+    `inductive ntree := Tree : List ntree → ntree`. -/
+@[rocq_alias into_ih_Forall]
+instance intoIH_listForall [BI PROP] (φ : α → Bool) (l : List α) (P : PROP) (Φ : α → PROP)
+    [h : ∀ x, IntoIH (φ x) P (Φ x)] :
+    IntoIH (l.all φ) P (bigSepL (fun _ a => iprop(□ Φ a)) l) where
+  into_ih := by
+    intro h1
+    induction l generalizing Φ with
+    | nil =>
+      simp [affine]
+    | cons x xs ih =>
+      simp [List.all, bigSepL] at h1 ⊢
+      rcases h1 with ⟨hx, hxs⟩
+      apply intuitionistically_sep_idem.mpr.trans
+      refine sep_mono ?_ ?_
+      · exact intuitionistically_intro' ((h x).into_ih hx)
+      · apply ih
+        apply (List.all_eq_true.mpr)
+        apply hxs
+
+/-- 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 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' ((h _ _).into_ih x)
+      · exact ih
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 533818f9f..0426e7b84 100644
--- a/Iris/Iris/ProofMode/Tactics/Induction.lean
+++ b/Iris/Iris/ProofMode/Tactics/Induction.lean
@@ -1,59 +1,498 @@
 /-
 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, 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
 
 namespace Iris.ProofMode
 
-public section
-open BI Std
+public meta section
+open BI Std Lean Elab Tactic Meta Qq
 
-/-
-  `IntoIH φ P Q` describes how to turn a pure induction hypothesis `φ` into a proofmode
-  hypothesis `Q` under an intuitionistic BI context `□ P`.
--/
-@[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_r h1.make_affinely.mpr).trans ?_
-    refine persistent_and_affinely_sep_r.2.trans ?_
-    exact pure_elim_r (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' (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_r (P := iprop(<pers> P)) (Q := Q))
+/--
+  The user of the `iinduction` tactic provides the proof for the induction
+  subgoal. Induction hypotheses are available for the user in the intuitionistic
+  context of the Iris proof state.
 
-public meta section
-open Lean Elab Tactic Meta Qq
+  Meanwhile, the actual induction subgoal generated by Lean with the `induction`
+  tactic has induction hypotheses in the regular context.
+
+  Given all hypotheses in the Iris proof state (represented by `P`) exist in
+  the intuitionistic context (that is, the spatial context is empty), we can
+  introduce another induction hypothesis generated by Lean into the
+  intuitionistic context.
+-/
+@[rocq_alias tac_revert_ih]
+theorem revert_IH [BI PROP] {P Q : PROP} {φ}
+    (ih : φ)
+    (h : R ⊢ □ P)
+    (inst : IntoIH φ P Q) :
+    R ⊢ □ (P ∗ □ Q) := calc
+  _ ⊢ □ P         := h
+  _ ⊢ □ P ∗ □ P   := intuitionistically_sep_dup.mp
+  _ ⊢ □ P ∗ □ □ P := sep_mono_r intuitionistically_idem.mpr
+  _ ⊢ □ P ∗ □ Q   := sep_mono_r <| intuitionistically_mono <| inst.into_ih ih
+  _ ⊢ □ P ∗ □ □ Q := sep_mono_r intuitionistically_idem.mpr
+  _ ⊢ □ (P ∗ □ Q) := intuitionistically_sep_2
+
+/--
+  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))
+
+/--
+  Given a collection of hypotheses (`hyps`) and a free variable `fvar`, return
+  the subset of intuitionistic hypotheses in `hyps` that contains the `fvar`
+  and all spatial hypotheses in the proof state.
+
+  This function is used for identifying the hypotheses in the Iris proof state
+  that must be reverted before applying Lean's built-in `induction` tactic.
+-/
+private def iHypsContaining {u} {prop : Q(Type $u)} {bi} {e : Q($prop)}
+    (hyps : Hyps bi e) (fvars : List FVarId) : List SelTarget :=
+  let ivars := hyps.intuitionisticIVarIds.filter <| fun ivar =>
+    match hyps.getDecl? ivar with
+    | some ⟨_, _, _, ty⟩ => fvars.any ty.containsFVar
+    | none => false
+
+  (ivars ++ hyps.spatialIVarIds).map ({ kind := .ipm ·, explicit := false })
+
+/--
+  Search for hypotheses in the regular Lean context that represent induction
+  hypotheses and return their IDs as a list.
+-/
+private def findIHs (m : MVarId) : ProofModeM (List FVarId) :=
+  m.withContext do
+    let lctx ← getLCtx
+    let mut ihs := []
+    for decl in lctx do
+      let type ← instantiateMVars decl.type
+      if isIrisGoalWithForalls type then
+        ihs := decl.fvarId :: ihs
+    return ihs.reverse
+
+/--
+  Used for every induction hypothesis generated by Lean upon using the built-in
+  `induction` tactic. This function is called by `addIHs` and returns
+  an instance of `InductionState` after handling one induction hypothesis.
+-/
+private def addIH {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
+    (st : @InductionState u prop bi e)
+    (φ : Q(Prop)) (p : Q($φ)) (hFVar : FVarId) :
+    ProofModeM (@InductionState u prop bi e) := do
+  let oldE := st.newE
+  let oldHyps : Hyps bi oldE := st.newHyps
+
+  -- Obtain the proposition to be introduced into the intuitionistic context
+  let Q ← mkFreshExprMVarQ q($prop)
+  let some inst ← ProofModeM.trySynthInstanceQ q(IntoIH $φ $oldE $Q)
+  | throwError "iinduction: type class synthesis with IntoIH failed"
+
+  -- Introduce the induction hypothesis into the intuitionistic context
+  let nameIdent := mkIdent <| ← hFVar.getUserName
+  let binderIdent ← `(binderIdent| $nameIdent:ident)
+  let ⟨_, newHyps⟩ ← Hyps.addWithInfo bi binderIdent q(true) Q oldHyps
+
+  return { newHyps, pf := q(revert_IH $p $st.pf $inst) }
+
+/--
+  Introduce a list of induction hypotheses into the intuitionistic context
+  of the Iris proof state. The list of `FVarId` values (`ihFVars`) should be
+  the list returned by `findIHs`. The function returns the final
+  `InductionState` with all induction hypotheses handled.
+
+  The argument `pfIntHyps` holds when the spatial context is empty, which
+  is indeed the case when all hypotheses therein have been reverted.
+-/
+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 : InductionState e := { newHyps := hyps, pf := q($pfIntHyps) }
+
+  -- Iteratively move the induction hypotheses into the intuitionistic context
+  for i in ihFVars do
+    let p := mkFVar i
+    let φ ← inferType <| mkFVar i
+    st ← addIH st φ p i
+
+  return st
+
+/--
+  Given hypothesis `hyps` representing `e` where every hypothesis exist in the
+  intuitionistic context, return the proof of `e ⊢ □ e`. Throw an error if
+  `hyps` contains hypotheses in the spatial context.
+-/
+private def buildPfIntHyps {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
+    (hyps : Hyps bi e) : ProofModeM Q($e ⊢ □ $e) :=
+  match hyps with
+  | .emp _ => pure q(intuitionistically_emp.mpr)
+  | .hyp _ _ _ p _ _ =>
+    match matchBool p with
+    | .inl _ => pure q(intuitionistically_idem.mpr)
+    | .inr _ =>
+      throwError "iinduction: spatial context is not empty after reverting hypotheses"
+  | .sep _ _ _ _ lhs rhs => do
+    let pfL ← buildPfIntHyps lhs
+    let pfR ← buildPfIntHyps rhs
+    pure q((sep_mono $pfL $pfR).trans intuitionistically_sep_2)
+
+/--
+  Tactic syntax for user-supplied alternative names.
+-/
+syntax inductionAlts := "| " binderIdent+ " => " tacticSeq
+
+/--
+  Parse the tactic syntax for user-supplied alternative names.
+
+  This function returns a triple, which includes:
+  1. the name of the constructor supplied by the user (`ctor.getId`),
+  2. the alternative names for that constructor (`vars`), and
+  3. the tactics for this induction subgoal.
+-/
+private def parseInductionAlts (alt : TSyntax `Iris.ProofMode.inductionAlts) :
+    TacticM (Name × Array (TSyntax `Lean.binderIdent) × TSyntax `Lean.Parser.Tactic.tacticSeq) := do
+  let `(inductionAlts| | $ctor:ident $vars:binderIdent* => $tac:tacticSeq) := alt
+  | throwError "iinduction: invalid syntax"
+  return ⟨ctor.getId, vars, tac⟩
+
+/--
+  Check whether a fully-qualified constructor name (e.g. `Nat.succ`) matches a
+  user-written short name (e.g. `succ`) or an already-qualified name.
+-/
+private def matchesCtorName (fullName : Name) (userShort : Name) : Bool :=
+  fullName == userShort || fullName.getString! == userShort.getString!
+
+/--
+  Throw an error if the user has supplied some but not all alternative names.
+-/
+private def throwMissingAlt {α} (ctor : Name) : ProofModeM α :=
+  throwError "iinduction: alternative `{ctor.getString!}` has not been provided"
+
+/--
+  Checks whether an invalid, missing and/or duplicate constructor names have
+  been supplied by the user. Throw an error if this is the case.
+-/
+private def checkCtors (ctors altCtors : List Name) : ProofModeM Unit := do
+  let mut errors : List String := []
+
+  -- Check for missing constructor names
+  let missingAltCtors :=
+    ctors.filter (not <| altCtors.any <| fun altCtor => matchesCtorName · altCtor)
+
+  -- Check for invalid constructor names
+  let invalidAltCtors :=
+    altCtors.filter (not <| ctors.any <| fun ctor => matchesCtorName ctor ·)
+
+  -- Check for duplicate constructor names
+  let dupAltCtors := (altCtors.filter <|
+    fun alt => altCtors.countP (matchesCtorName alt ·) > 1).eraseDupsBy matchesCtorName
+
+  if !missingAltCtors.isEmpty then
+    let missing := ", ".intercalate  <| missingAltCtors.map (s!"`{·}`")
+    errors := errors.concat s!"iinduction: missing alternative name(s): {missing}"
+  if !dupAltCtors.isEmpty then
+    let dups := ", ".intercalate  <| dupAltCtors.map (s!"`{·}`")
+    errors := errors.concat s!"iinduction: duplicate alternative name(s): {dups}"
+  if !invalidAltCtors.isEmpty then
+    let invalids := ", ".intercalate <| invalidAltCtors.map (s!"`{·}`")
+    errors := errors.concat s!"iinduction: invalid alternative name(s): {invalids}"
+
+  if !errors.isEmpty then
+    throwError m!"{"\n".intercalate errors}"
+
+/--
+  The main function handling the steps for the `iinduction` tactic.
+
+  1. Revert Iris hypotheses explicitly specified by the tactic user
+     (applicable when the `generalizing` syntax is used).
+  2. Revert all spatial hypotheses in the Iris proof state as well as the
+     relevant hypotheses in the intuitionistic context.
+  3. Revert pure Lean variables specified by the tactic user
+     (applicable when the `generalizing` syntax is used).
+  4. Prepare the arguments for `Lean.Meta.Tactic.induction`.
+  5. Apply `Lean.Meta.Tactic.induction` to obtain the induction subgoals.
+  6. For each subgoal, move the induction hypotheses from the regular Lean
+     context into the Iris intuitionistic context.
+  7. Introduce hypotheses reverted in steps 1 and 2 back into the Iris proof state.
+
+  The relevant intuitionistic hypotheses to which Step 2 refers are those
+  involving `fvar` or pure Lean variables in `genSelTargets`.
+-/
+private def iInductionCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
+    (hyps : Hyps bi e) (goal : Q($prop)) (fvar : FVarId)
+    (parsedAlts : Option <| Array <|
+      Name × Array (TSyntax `Lean.binderIdent) × TSyntax `Lean.Parser.Tactic.tacticSeq)
+    (altRecName : Option Name)
+    (genSelTargets : Option <| List SelTarget) :
+    ProofModeM Q($e ⊢ $goal) := do
+  -- Iris hypotheses to be reverted as specified by the user using the `generalizing` syntax
+  let explicitIrisTargets : List SelTarget :=
+    match genSelTargets with
+    | none => []
+    | some genSelTargets => genSelTargets.filter <| fun t => match t.kind with | .ipm _ => true | _ => false
+
+  -- `FVarID` values of pure hypothesis specified by the user using the `generalizing` syntax
+  let pureFVars : List FVarId :=
+    match genSelTargets with
+    | none => []
+    | some genSelTargets =>
+      genSelTargets.filterMap <| fun t => match t.kind with | .pure f => some f | _ => none
+
+  -- Iris hypotheses in the spatial context and relevant intuitionistic context
+  let spatialAndIntuitionisticTargets := iHypsContaining hyps <| pureFVars.concat fvar
+
+  let spatialAndIntuitionisticTargets :=
+    spatialAndIntuitionisticTargets.filter (not <| (explicitIrisTargets.map (·.kind)).contains ·.kind)
+
+  -- Pure hypotheses to be reverted as specified by the user using the `generalizing` syntax
+  let pureTargets : List SelTarget := pureFVars.map ({ kind := .pure ·, explicit := true })
+
+  -- Those in `explicitIrisTargets` get reverted first, so they are last in the list
+  let targets := pureTargets ++ spatialAndIntuitionisticTargets ++ explicitIrisTargets
+
+  -- Find the recursor name and constructor names of the inductive datatype
+  let fvarType ← whnf <| ← inferType <| mkFVar fvar
+  let ⟨recName, ctors⟩ ← match fvarType.getAppFn with
+  | .const indName _ =>
+    match (← getEnv).find? indName with
+    | some (.inductInfo val) =>
+        -- Use the user-supplied recursor name if available
+        let some recName ← match altRecName with
+          | none => getCustomEliminator? #[mkFVar fvar] true
+          | some altRecName => pure altRecName
+        | throwError "iinduction: unable to determine recursor name"
+        pure (recName, val.ctors)
+    | _ => throwError "iinduction: {indName} is not inductive"
+  | _ => throwError "iinduction: unable to determine inductive type"
+
+  let matcher :
+    Name →
+    Name × Array (TSyntax `Lean.binderIdent) × TSyntax `Lean.Parser.Tactic.tacticSeq →
+    Bool := fun ctor ⟨altCtor, _, _⟩ => matchesCtorName ctor altCtor
+
+  -- Check that all alternative names supplied by the user are valid
+  match parsedAlts with
+  | none => pure ()
+  | some parsedAlts => checkCtors ctors <| parsedAlts.toList.map Prod.fst
+
+  -- Define the names for variables and induction hypotheses if supplied by user
+  let varNames : Array AltVarNames ←
+    match parsedAlts with
+    | none =>
+      pure <| ctors.toArray.map <| fun _ => { explicit := true, varNames := [] }
+    | some parsedAlts => do
+      ctors.toArray.mapM <| fun ctor =>
+      match parsedAlts.find? <| matcher ctor with
+      | some (_, vars, _) =>
+        pure { explicit := true, varNames := vars.toList.map <|
+          fun v =>
+            match v.raw with
+            | `(binderIdent| $id:ident) => id.getId
+            | _ => Name.mkSimple "_" }
+      | none => throwMissingAlt ctor
+
+  let pf ← iRevertIntro hyps goal targets <|
+    fun hyps' goal' k => 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 ctors do
+        s.mvarId.withContext do
+          -- For pretty printing of arguments
+          match parsedAlts with
+          | none => pure ()
+          | some parsedAlts =>
+            match parsedAlts.find? <| matcher ctor with
+            | some ⟨_, vars, _⟩ =>
+              for ⟨fieldFVar, varStx⟩ in s.fields.toList.zip vars.toList do
+                if let `(binderIdent| $id:ident) := varStx then
+                  let lctx ← getLCtx
+                  let fieldType ← inferType fieldFVar
+                  addLocalVarInfo id lctx fieldFVar (some fieldType) true
+            | none => throwMissingAlt ctor
+
+          -- Obtain the type of the induction subgoal
+          let sType ← instantiateMVars <| ← s.mvarId.getType
+
+          let some irisGoal := parseIrisGoal? sType
+          -- This should not happen
+          | throwError "iinduction: fail to parse induction subgoal"
+
+          -- Find the induction hypotheses generated by Lean's `induction` tactic
+          let ihFVars ← findIHs s.mvarId
+
+          -- A proof that all hypotheses in the Iris goal exist in the intuitionistic context
+          let pfIntHyps ← buildPfIntHyps irisGoal.hyps
+
+          -- Introduce the induction hypothesis back into the Iris proof state
+          let st ← addIHs pfIntHyps irisGoal.hyps ihFVars
+
+          -- Generate the induction subgoal for the user
+          let pf' ← withoutFVars (u := 0) ihFVars.toArray <| k st.newHyps irisGoal.goal
+
+          -- Fill the metavariable for the induction subgoal generated by Lean
+          s.mvarId.assign <| q($(st.pf).trans <| intuitionistically_elim.trans $pf')
+
+          -- Handle user-supplied tactics for specific constructors
+          match parsedAlts with
+          | none => pure ()
+          | some parsedAlts =>
+            let biGoalMVar := (← getThe ProofModeM.State).goals.back!
+            modify <| fun s => { s with goals := s.goals.pop }
+
+            let some ⟨_, _, userTac⟩ := parsedAlts.find? <| matcher ctor
+            | throwMissingAlt ctor
+
+            -- Run the user tactic on the BI goal
+            let savedGoals ← getGoals
+            setGoals [biGoalMVar]
+            evalTactic userTac
+            let remaining ← getGoals
+            setGoals savedGoals
+            for r in remaining do addMVarGoal r
+
+      return m
+
+  return pf
+
+/--
+  Given a term expression, check whether it is a `FVarId` value. If so,
+  return it directly. Otherwise, generalise the term expressions before
+  returning its `FVarId`.
+-/
+private def termToFVar (x : TSyntax `term) : TacticM FVarId := do
+  let e ← withMainContext <| elabTerm x none
+  let e ← instantiateMVars e
+
+  if e.isFVar then
+    return e.fvarId!
+
+  let mvarId ← getMainGoal
+  let (fvars, newMVarId) ← mvarId.generalize #[{ expr := e }]
+  replaceMainGoal [newMVarId]
+
+  return fvars[0]!
+
+/--
+  Simple tactic with inaccessible names of variables and induction hypotheses
+  generated by Lean automatically.
+-/
+elab "iinduction" colGt x:term : tactic => do
+  let fvar ← termToFVar x
+
+  ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
+    let pf ← iInductionCore hyps goal fvar none none none
+    mvar.assign pf
+
+/-- Tactic with names of variables and induction hypotheses supplied by the user. -/
+elab "iinduction" colGt x:term "with" alts:(colGe inductionAlts)* : tactic => do
+  let fvar ← termToFVar x
+
+  -- Parse the list of alternative names supplied by the user
+  let parsedAlts ← alts.mapM parseInductionAlts
+
+  ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
+    let pf ← iInductionCore hyps goal fvar parsedAlts none none
+    mvar.assign pf
+
+/-- Tactic with the recursor name supplied by the user. -/
+elab "iinduction" colGt x:term "using" r:ident : tactic => do
+  let fvar ← termToFVar x
+
+  -- Parse the recursor name provided by the user
+  let recName := r.getId
+
+  ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
+    let pf ← iInductionCore hyps goal fvar none recName none
+    mvar.assign pf
+
+/-- Tactic with the recursor name and alternative names supplied by the user. -/
+elab "iinduction" colGt x:term "using" r:ident
+    "with" alts:(colGe inductionAlts)* : tactic => do
+  let fvar ← termToFVar x
+
+  -- Parse the recursor name provided by the user
+  let recName := r.getId
+  -- Parse the list of alternative names supplied by the user
+  let parsedAlts ← alts.mapM parseInductionAlts
+
+  ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
+    let pf ← iInductionCore hyps goal fvar parsedAlts recName none
+    mvar.assign pf
+
+elab "iinduction" colGt x:term "generalizing" genSelPats:(colGt selPat)+ : tactic => do
+  let fvar ← termToFVar x
+
+  ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
+    -- Parse the user-supplied list of variables to be generalised
+    let genSelPats ← liftMacroM <| SelPat.parse genSelPats
+    let genSelTargets ← SelPat.resolve hyps genSelPats
+
+    let pf ← iInductionCore hyps goal fvar none none genSelTargets
+    mvar.assign pf
+
+elab "iinduction" colGt x:term "generalizing" genSelPats:(colGt selPat)+
+    "with" alts:(colGe inductionAlts)* : tactic => do
+  let fvar ← termToFVar x
+
+  -- Parse the list of alternative names supplied by the user
+  let parsedAlts ← alts.mapM parseInductionAlts
+
+  ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
+    -- Parse the user-supplied list of variables to be generalised
+    let genSelPats ← liftMacroM <| SelPat.parse genSelPats
+    let genSelTargets ← SelPat.resolve hyps genSelPats
+
+    let pf ← iInductionCore hyps goal fvar parsedAlts none genSelTargets
+    mvar.assign pf
+
+elab "iinduction" colGt x:term "using" r:ident
+    "generalizing" genSelPats:(colGt selPat)+ : tactic => do
+  let fvar ← termToFVar x
+
+  -- Parse the recursor name provided by the user
+  let recName := r.getId
+
+  ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
+    -- Parse the user-supplied list of variables to be generalised
+    let genSelPats ← liftMacroM <| SelPat.parse genSelPats
+    let genSelTargets ← SelPat.resolve hyps genSelPats
+
+    let pf ← iInductionCore hyps goal fvar none recName genSelTargets
+    mvar.assign pf
+
+elab "iinduction" colGt x:term "using" r:ident
+    "generalizing" genSelPats:(colGt selPat)+ "with" alts:(colGe inductionAlts)* : tactic => do
+  let fvar ← termToFVar x
+
+  -- Parse the recursor name provided by the user
+  let recName := r.getId
+  -- Parse the list of alternative names supplied by the user
+  let parsedAlts ← alts.mapM parseInductionAlts
+
+  ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
+    -- Parse the user-supplied list of variables to be generalised
+    let genSelPats ← liftMacroM <| SelPat.parse genSelPats
+    let genSelTargets ← SelPat.resolve hyps genSelPats
+
+    let pf ← iInductionCore hyps goal fvar parsedAlts recName genSelTargets
+    mvar.assign pf
diff --git a/Iris/Iris/ProofMode/Tactics/RevertIntro.lean b/Iris/Iris/ProofMode/Tactics/RevertIntro.lean
index 380de3c6d..70d0e2e52 100644
--- a/Iris/Iris/ProofMode/Tactics/RevertIntro.lean
+++ b/Iris/Iris/ProofMode/Tactics/RevertIntro.lean
@@ -13,16 +13,16 @@ 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 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)
   (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
diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean
index edfb8d86c..754884e4c 100644
--- a/Iris/Iris/Tests/Tactics.lean
+++ b/Iris/Iris/Tests/Tactics.lean
@@ -2715,3 +2715,68 @@ example (P Q : PROP) :
   iloeb as IH
 
 end iloeb
+
+section iinduction
+
+/--
+  Tests `iinduction` with induction on natural numbers.
+
+  For natural numbers, `Nat.recAux` is used as the default recursor name. Hence,
+  the tactic is equivalent to `iinduction n using Nat.recAux generalizing %P HQ %R`.
+
+  Hypotheses in the spatial context necessarily become premises of the
+  induction hypothesis. The intuitionistic hypothesis `T n` is reverted
+  because it depends on `n`.
+
+  With the `generalizing` syntax, `P` and `R` are universally quantified
+  in the induction hypothesis. Given they occur in `HP` and `HR`, respectively,
+  the two propositions are included as premises of the induction hypothesis.
+
+  Meanwhile, `HQ` is included as a premise of the induction hypothesis without
+  `Q` being universally quantified.
+
+  Note that the following variants of the tactic all produce equivalent subgoals:
+  - `induction n generalizing %P HP HQ %R`
+  - `induction n generalizing %P HQ %R HR`
+  - `induction n generalizing %P HP HQ %R HR`
+  - the tactics above with any permutations of `generalizing` arguments.
+-/
+example [BI PROP] {P Q R S : PROP} {T : Nat → PROP} {n : Nat} :
+    ⊢ P -∗ □ Q -∗ □ R -∗ S -∗ □ T n -∗ ⌜n + 0 = n⌝ := by
+  iintro HP #HQ #HR HS #HT
+  iinduction n generalizing %P HQ %R with
+  -- Using the full name of the constructor (`Nat.zero`)
+  | Nat.zero  => itrivial
+  /- Using the short name of the constructor (`succ`), naming the induction
+     hypothesis as `ih`, but leaving the variable `n` inaccessible by using `_` -/
+  | succ _ ih => iframe; itrivial
+
+/- 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 user-supplied names -/
+/-- error: iinduction: missing alternative name(s): `Nat.succ`
+iinduction: duplicate alternative name(s): `zero`
+iinduction: invalid alternative name(s): `invalidA`, `invalidB`, `invalidC` -/
+#guard_msgs in
+example [BI PROP] {P Q R S T : PROP} {n : Nat} :
+    ⊢ P -∗ □ Q -∗ □ R -∗ S -∗ □ T -∗ ⌜n + 0 = n⌝ := by
+  iintro HP #HQ #HR HS #HT
+  iinduction n with
+  | invalidA  => done
+  | zero      => itrivial
+  | invalidB  => done
+  | Nat.zero  => itrivial
+  | invalidC  => done
+
+/-- Tests `iinduction` using a custom recursor name and expression -/
+example [BI PROP] {P R S : PROP} {Q T : Nat → PROP} {n : Nat} :
+    ⊢ P -∗ □ Q m -∗ □ R -∗ S -∗ □ T n -∗ ⌜n + m + 0 = n + m⌝ := by
+  iintro HP #HQ #HR HS #HT
+  iinduction n + m using Nat.strongRecOn
+  itrivial
+
+end iinduction