diff --git a/src/Iris.lean b/src/Iris.lean
index 2bd468667..96f2ce5c3 100644
--- a/src/Iris.lean
+++ b/src/Iris.lean
@@ -1,7 +1,9 @@
-import Iris.Algebra
-import Iris.BI
-import Iris.Examples
-import Iris.Instances
-import Iris.ProofMode
-import Iris.Std
-import Iris.Tests
+module
+
+public import Iris.Algebra
+public import Iris.BI
+public import Iris.Examples
+public import Iris.Instances
+public import Iris.ProofMode
+public import Iris.Std
+public import Iris.Tests
diff --git a/src/Iris/Algebra.lean b/src/Iris/Algebra.lean
index 30043dc56..3ad44600b 100644
--- a/src/Iris/Algebra.lean
+++ b/src/Iris/Algebra.lean
@@ -1,15 +1,17 @@
-import Iris.Algebra.Agree
-import Iris.Algebra.CMRA
-import Iris.Algebra.COFESolver
-import Iris.Algebra.DFrac
-import Iris.Algebra.Excl
-import Iris.Algebra.Frac
-import Iris.Algebra.GenMap
-import Iris.Algebra.LocalUpdates
-import Iris.Algebra.IProp
-import Iris.Algebra.OFE
-import Iris.Algebra.Updates
-import Iris.Algebra.UPred
-import Iris.Algebra.Heap
-import Iris.Algebra.View
-import Iris.Algebra.HeapView
+module
+
+public import Iris.Algebra.Agree
+public import Iris.Algebra.CMRA
+public import Iris.Algebra.COFESolver
+public import Iris.Algebra.DFrac
+public import Iris.Algebra.Excl
+public import Iris.Algebra.Frac
+public import Iris.Algebra.GenMap
+public import Iris.Algebra.LocalUpdates
+public import Iris.Algebra.IProp
+public import Iris.Algebra.OFE
+public import Iris.Algebra.Updates
+public import Iris.Algebra.UPred
+public import Iris.Algebra.Heap
+public import Iris.Algebra.View
+public import Iris.Algebra.HeapView
diff --git a/src/Iris/Algebra/Agree.lean b/src/Iris/Algebra/Agree.lean
index 5d22ba2e2..d765dde22 100644
--- a/src/Iris/Algebra/Agree.lean
+++ b/src/Iris/Algebra/Agree.lean
@@ -3,9 +3,12 @@ Copyright (c) 2025 Leo Stefanesco. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leo Stefanesco, Puming Liu
 -/
+module
 
-import Iris.Algebra.CMRA
-import Iris.Algebra.OFE
+public import Iris.Algebra.CMRA
+public import Iris.Algebra.OFE
+
+@[expose] public section
 
 namespace Iris
 
diff --git a/src/Iris/Algebra/Auth.lean b/src/Iris/Algebra/Auth.lean
index 899a32c4c..e0a230a1b 100644
--- a/src/Iris/Algebra/Auth.lean
+++ b/src/Iris/Algebra/Auth.lean
@@ -3,8 +3,10 @@ Copyright (c) 2025 Alexander Bai. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alexander Bai
 -/
-import Iris.Algebra.View
-import Iris.Algebra.LocalUpdates
+module
+
+public import Iris.Algebra.View
+public import Iris.Algebra.LocalUpdates
 
 /-!
 # Authoritative Camera
@@ -14,6 +16,8 @@ The authoritative camera has 2 types of elements:
 -  and the fragment `◯ b`
 -/
 
+@[expose] public section
+
 open Iris
 
 open OFE CMRA UCMRA View
diff --git a/src/Iris/Algebra/CMRA.lean b/src/Iris/Algebra/CMRA.lean
index f81f9b54d..cd763fa6b 100644
--- a/src/Iris/Algebra/CMRA.lean
+++ b/src/Iris/Algebra/CMRA.lean
@@ -3,7 +3,11 @@ Copyright (c) 2025 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Сухарик (@suhr), Markus de Medeiros, Puming Liu
 -/
-import Iris.Algebra.OFE
+module
+
+public import Iris.Algebra.OFE
+
+@[expose] public section
 
 namespace Iris
 open OFE
diff --git a/src/Iris/Algebra/COFESolver.lean b/src/Iris/Algebra/COFESolver.lean
index 9e9cacf30..9a84d8f57 100644
--- a/src/Iris/Algebra/COFESolver.lean
+++ b/src/Iris/Algebra/COFESolver.lean
@@ -3,7 +3,11 @@ Copyright (c) 2025 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import Iris.Algebra.OFE
+module
+
+public import Iris.Algebra.OFE
+
+@[expose] public section
 
 namespace Iris.COFE.OFunctor
 open OFE
diff --git a/src/Iris/Algebra/DFrac.lean b/src/Iris/Algebra/DFrac.lean
index 44cb62ddc..002336a38 100644
--- a/src/Iris/Algebra/DFrac.lean
+++ b/src/Iris/Algebra/DFrac.lean
@@ -3,12 +3,15 @@ Copyright (c) 2025 Markus de Medeiros. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus de Medeiros, Mario Carneiro
 -/
+module
 
-import Iris.Algebra.CMRA
-import Iris.Algebra.OFE
-import Iris.Algebra.Frac
-import Iris.Algebra.Updates
-import Iris.Algebra.LocalUpdates
+public import Iris.Algebra.CMRA
+public import Iris.Algebra.OFE
+public import Iris.Algebra.Frac
+public import Iris.Algebra.Updates
+public import Iris.Algebra.LocalUpdates
+
+@[expose] public section
 
 namespace Iris
 
diff --git a/src/Iris/Algebra/Excl.lean b/src/Iris/Algebra/Excl.lean
index 5d11e3ca9..b5def0463 100644
--- a/src/Iris/Algebra/Excl.lean
+++ b/src/Iris/Algebra/Excl.lean
@@ -3,8 +3,11 @@ Copyright (c) 2025 Oliver Soeser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Soeser, Mario Carneiro
 -/
+module
 
-import Iris.Algebra.CMRA
+public import Iris.Algebra.CMRA
+
+@[expose] public section
 
 namespace Iris
 
diff --git a/src/Iris/Algebra/Frac.lean b/src/Iris/Algebra/Frac.lean
index 3f94d9058..1e640c368 100644
--- a/src/Iris/Algebra/Frac.lean
+++ b/src/Iris/Algebra/Frac.lean
@@ -3,9 +3,10 @@ Copyright (c) 2025 Markus de Medeiros. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus de Medeiros, Shreyas Srinivas, Mario Carneiro
 -/
+module
 
-import Iris.Algebra.CMRA
-import Iris.Algebra.OFE
+public import Iris.Algebra.CMRA
+public import Iris.Algebra.OFE
 
 /-!
 # The Frac CMRA
@@ -14,6 +15,8 @@ This CMRA captures the notion of fractional ownership of another resource.
 Traditionally the underlying set is assumed to be the half open interval $$(0,1]$$.
 -/
 
+@[expose] public section
+
 namespace Iris
 
 class Fraction (α : Type _) extends Add α where
diff --git a/src/Iris/Algebra/GenMap.lean b/src/Iris/Algebra/GenMap.lean
index b375256d6..49654aca7 100644
--- a/src/Iris/Algebra/GenMap.lean
+++ b/src/Iris/Algebra/GenMap.lean
@@ -3,9 +3,13 @@ Copyright (c) 2025 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus de Medeiros
 -/
-import Iris.Algebra.OFE
-import Iris.Algebra.CMRA
-import Iris.Algebra.Updates
+module
+
+public import Iris.Algebra.OFE
+public import Iris.Algebra.CMRA
+public import Iris.Algebra.Updates
+
+@[expose] public section
 
 namespace Iris
 open OFE
diff --git a/src/Iris/Algebra/Heap.lean b/src/Iris/Algebra/Heap.lean
index 9925dff95..7f0c272cf 100644
--- a/src/Iris/Algebra/Heap.lean
+++ b/src/Iris/Algebra/Heap.lean
@@ -3,11 +3,14 @@ Copyright (c) 2025 Markus de Medeiros. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus de Medeiros, Puming Liu
 -/
+module
 
-import Iris.Algebra.CMRA
-import Iris.Algebra.OFE
-import Iris.Std.Set
-import Iris.Std.PartialMap
+public import Iris.Algebra.CMRA
+public import Iris.Algebra.OFE
+public import Iris.Std.Set
+public import Iris.Std.PartialMap
+
+@[expose] public section
 
 open Iris Std
 
diff --git a/src/Iris/Algebra/HeapView.lean b/src/Iris/Algebra/HeapView.lean
index 988e3d31f..a5c877bae 100644
--- a/src/Iris/Algebra/HeapView.lean
+++ b/src/Iris/Algebra/HeapView.lean
@@ -3,10 +3,12 @@ Copyright (c) 2025 Markus de Medeiros. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus de Medeiros, Puming Liu
 -/
-import Iris.Algebra.Heap
-import Iris.Algebra.View
-import Iris.Algebra.DFrac
-import Iris.Algebra.Frac
+module
+
+public import Iris.Algebra.Heap
+public import Iris.Algebra.View
+public import Iris.Algebra.DFrac
+public import Iris.Algebra.Frac
 
 /-!
 # Heap Views
@@ -28,6 +30,8 @@ It provides authoritative and fragmental ownership over heap elements with fract
 * `HeapView.update_replace`: Replacement update lemma
 -/
 
+@[expose] public section
+
 open Iris
 
 section heapView
diff --git a/src/Iris/Algebra/IProp.lean b/src/Iris/Algebra/IProp.lean
index 743ded04b..2b3afa62e 100644
--- a/src/Iris/Algebra/IProp.lean
+++ b/src/Iris/Algebra/IProp.lean
@@ -3,13 +3,16 @@ Copyright (c) 2025 Markus de Medeiros. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus de Medeiros
 -/
+module
 
-import Iris.Algebra.CMRA
-import Iris.Algebra.OFE
-import Iris.Algebra.UPred
-import Iris.Algebra.GenMap
-import Iris.Algebra.COFESolver
-import Init.Data.Vector
+public import Iris.Algebra.CMRA
+public import Iris.Algebra.OFE
+public import Iris.Algebra.UPred
+public import Iris.Algebra.GenMap
+public import Iris.Algebra.COFESolver
+public import Init.Data.Vector
+
+@[expose] public section
 
 namespace Iris
 
diff --git a/src/Iris/Algebra/LocalUpdates.lean b/src/Iris/Algebra/LocalUpdates.lean
index 346b6ef6c..1888c892c 100644
--- a/src/Iris/Algebra/LocalUpdates.lean
+++ b/src/Iris/Algebra/LocalUpdates.lean
@@ -3,7 +3,11 @@ Copyright (c) 2025 Сухарик. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Сухарик (@suhr), Mario Carneiro
 -/
-import Iris.Algebra.CMRA
+module
+
+public import Iris.Algebra.CMRA
+
+@[expose] public section
 
 namespace Iris
 
diff --git a/src/Iris/Algebra/Numbers.lean b/src/Iris/Algebra/Numbers.lean
index 2682cc91f..0225d1a8b 100644
--- a/src/Iris/Algebra/Numbers.lean
+++ b/src/Iris/Algebra/Numbers.lean
@@ -3,10 +3,11 @@ Copyright (c) 2025 Shreyas Srinivas. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Shreyas Srinivas, Markus de Medeiros
 -/
+module
 
-import Iris.Algebra.CMRA
-import Iris.Algebra.OFE
-import Iris.Algebra.LocalUpdates
+public import Iris.Algebra.CMRA
+public import Iris.Algebra.OFE
+public import Iris.Algebra.LocalUpdates
 
 /-! ## Numbers CMRA
 Simple CMRA's for commutative monoids.
@@ -17,6 +18,8 @@ There are three variants:
 - "No core": there is no core (eg. (PNat, +))
 -/
 
+@[expose] public section
+
 open Std
 
 class IdentityFree (α : Type _) [Add α] where
diff --git a/src/Iris/Algebra/OFE.lean b/src/Iris/Algebra/OFE.lean
index 95af9ff26..f94debd39 100644
--- a/src/Iris/Algebra/OFE.lean
+++ b/src/Iris/Algebra/OFE.lean
@@ -3,6 +3,9 @@ Copyright (c) 2023 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
+module
+
+@[expose] public section
 
 namespace Iris
 
diff --git a/src/Iris/Algebra/UPred.lean b/src/Iris/Algebra/UPred.lean
index 6890ff206..806e9b599 100644
--- a/src/Iris/Algebra/UPred.lean
+++ b/src/Iris/Algebra/UPred.lean
@@ -3,9 +3,12 @@ Copyright (c) 2025 Markus de Medeiros. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus de Medeiros
 -/
+module
 
-import Iris.Algebra.CMRA
-import Iris.Algebra.OFE
+public import Iris.Algebra.CMRA
+public import Iris.Algebra.OFE
+
+@[expose] public section
 
 namespace Iris
 open CMRA
diff --git a/src/Iris/Algebra/Updates.lean b/src/Iris/Algebra/Updates.lean
index b506f62e7..688b6622c 100644
--- a/src/Iris/Algebra/Updates.lean
+++ b/src/Iris/Algebra/Updates.lean
@@ -3,7 +3,11 @@ Copyright (c) 2025 Сухарик. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Сухарик (@suhr)
 -/
-import Iris.Algebra.CMRA
+module
+
+public import Iris.Algebra.CMRA
+
+@[expose] public section
 
 namespace Iris
 
diff --git a/src/Iris/Algebra/View.lean b/src/Iris/Algebra/View.lean
index 37a879c88..ee563a2e3 100644
--- a/src/Iris/Algebra/View.lean
+++ b/src/Iris/Algebra/View.lean
@@ -3,13 +3,17 @@ Copyright (c) 2025 Markus de Medeiros. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus de Medeiros, Puming Liu
 -/
-import Iris.Algebra.CMRA
-import Iris.Algebra.OFE
-import Iris.Algebra.Frac
-import Iris.Algebra.DFrac
-import Iris.Algebra.Agree
-import Iris.Algebra.Updates
-import Iris.Algebra.LocalUpdates
+module
+
+public import Iris.Algebra.CMRA
+public import Iris.Algebra.OFE
+public import Iris.Algebra.Frac
+public import Iris.Algebra.DFrac
+public import Iris.Algebra.Agree
+public import Iris.Algebra.Updates
+public import Iris.Algebra.LocalUpdates
+
+@[expose] public section
 
 open Iris
 
diff --git a/src/Iris/BI.lean b/src/Iris/BI.lean
index 3bea992cc..89a666f0d 100644
--- a/src/Iris/BI.lean
+++ b/src/Iris/BI.lean
@@ -1,8 +1,10 @@
-import Iris.BI.Classes
-import Iris.BI.DerivedLaws
-import Iris.BI.DerivedLawsLater
-import Iris.BI.Extensions
-import Iris.BI.Instances
-import Iris.BI.BI
-import Iris.BI.Notation
-import Iris.BI.Updates
+module
+
+public import Iris.BI.Classes
+public import Iris.BI.DerivedLaws
+public import Iris.BI.DerivedLawsLater
+public import Iris.BI.Extensions
+public import Iris.BI.Instances
+public import Iris.BI.BI
+public import Iris.BI.Notation
+public import Iris.BI.Updates
diff --git a/src/Iris/BI/BI.lean b/src/Iris/BI/BI.lean
index 0f91953fc..7feb1184d 100644
--- a/src/Iris/BI/BI.lean
+++ b/src/Iris/BI/BI.lean
@@ -3,8 +3,12 @@ Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lars König, Mario Carneiro
 -/
-import Iris.Algebra.OFE
-import Iris.BI.BIBase
+module
+
+public import Iris.Algebra.OFE
+public import Iris.BI.BIBase
+
+@[expose] public section
 
 namespace Iris
 open Iris.Std OFE
diff --git a/src/Iris/BI/BIBase.lean b/src/Iris/BI/BIBase.lean
index 8a98aa3f0..85d118556 100644
--- a/src/Iris/BI/BIBase.lean
+++ b/src/Iris/BI/BIBase.lean
@@ -3,11 +3,15 @@ Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lars König, Mario Carneiro
 -/
-import Iris.BI.Notation
-import Iris.Std.Classes
-import Iris.Std.DelabRule
-import Iris.Std.Rewrite
-import Iris.Std.BigOp
+module
+
+public meta import Iris.BI.Notation
+public import Iris.Std.Classes
+public meta import Iris.Std.DelabRule
+public meta import Iris.Std.Rewrite
+public import Iris.Std.BigOp
+
+@[expose] public section
 
 namespace Iris.BI
 open Iris.Std
diff --git a/src/Iris/BI/Classes.lean b/src/Iris/BI/Classes.lean
index 5d645601b..a41627fbb 100644
--- a/src/Iris/BI/Classes.lean
+++ b/src/Iris/BI/Classes.lean
@@ -3,7 +3,11 @@ Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lars König, Mario Carneiro
 -/
-import Iris.BI.BI
+module
+
+public import Iris.BI.BI
+
+@[expose] public section
 
 namespace Iris.BI
 
diff --git a/src/Iris/BI/DerivedLaws.lean b/src/Iris/BI/DerivedLaws.lean
index 289aad33c..3f85c92af 100644
--- a/src/Iris/BI/DerivedLaws.lean
+++ b/src/Iris/BI/DerivedLaws.lean
@@ -3,12 +3,16 @@ Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lars König, Mario Carneiro, Markus de Medeiros, Michael Sammler
 -/
-import Iris.BI.Classes
-import Iris.BI.Extensions
-import Iris.BI.BI
-import Iris.Std.Classes
-import Iris.Std.Rewrite
-import Iris.Std.TC
+module
+
+public import Iris.BI.Classes
+public import Iris.BI.Extensions
+public import Iris.BI.BI
+public import Iris.Std.Classes
+public import Iris.Std.Rewrite
+public import Iris.Std.TC
+
+@[expose] public section
 
 namespace Iris.BI
 open Iris.Std BI
diff --git a/src/Iris/BI/DerivedLawsLater.lean b/src/Iris/BI/DerivedLawsLater.lean
index e5e6528d6..e2acf9060 100644
--- a/src/Iris/BI/DerivedLawsLater.lean
+++ b/src/Iris/BI/DerivedLawsLater.lean
@@ -3,13 +3,17 @@ Copyright (c) 2026 Michael Sammler. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michael Sammler
 -/
-import Iris.BI.Classes
-import Iris.BI.Extensions
-import Iris.BI.BI
-import Iris.BI.DerivedLaws
-import Iris.Std.Classes
-import Iris.Std.Rewrite
-import Iris.Std.TC
+module
+
+public import Iris.BI.Classes
+public import Iris.BI.Extensions
+public import Iris.BI.BI
+public import Iris.BI.DerivedLaws
+public import Iris.Std.Classes
+public import Iris.Std.Rewrite
+public import Iris.Std.TC
+
+@[expose] public section
 
 namespace Iris.BI
 open Iris.Std BI
diff --git a/src/Iris/BI/Extensions.lean b/src/Iris/BI/Extensions.lean
index b78e5186a..97d34564d 100644
--- a/src/Iris/BI/Extensions.lean
+++ b/src/Iris/BI/Extensions.lean
@@ -3,8 +3,12 @@ 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
 -/
-import Iris.BI.Classes
-import Iris.BI.BI
+module
+
+public import Iris.BI.Classes
+public import Iris.BI.BI
+
+@[expose] public section
 
 namespace Iris.BI
 
diff --git a/src/Iris/BI/Instances.lean b/src/Iris/BI/Instances.lean
index 37e3c0620..74e7cde7d 100644
--- a/src/Iris/BI/Instances.lean
+++ b/src/Iris/BI/Instances.lean
@@ -3,11 +3,15 @@ Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lars König, Mario Carneiro
 -/
-import Iris.BI.Classes
-import Iris.BI.DerivedLaws
-import Iris.BI.Extensions
-import Iris.BI.BI
-import Iris.Std.Classes
+module
+
+public import Iris.BI.Classes
+public import Iris.BI.DerivedLaws
+public import Iris.BI.Extensions
+public import Iris.BI.BI
+public import Iris.Std.Classes
+
+@[expose] public section
 
 namespace Iris.BI
 open Iris.Std
diff --git a/src/Iris/BI/Lib/BUpdPlain.lean b/src/Iris/BI/Lib/BUpdPlain.lean
index d54ad1737..ad34ccb60 100644
--- a/src/Iris/BI/Lib/BUpdPlain.lean
+++ b/src/Iris/BI/Lib/BUpdPlain.lean
@@ -1,10 +1,14 @@
-import Iris.Std
-import Iris.BI
-import Iris.Algebra.Updates
-import Iris.ProofMode.Classes
-import Iris.ProofMode.Tactics
-import Iris.ProofMode.Display
-import Iris.ProofMode.InstancesUpdates
+module
+
+public import Iris.Std
+public import Iris.BI
+public import Iris.Algebra.Updates
+public import Iris.ProofMode.Classes
+public import Iris.ProofMode.Tactics
+public import Iris.ProofMode.Display
+public import Iris.ProofMode.InstancesUpdates
+
+@[expose] public section
 
 namespace Iris
 open Iris.Std BI
diff --git a/src/Iris/BI/Lib/Fixpoint.lean b/src/Iris/BI/Lib/Fixpoint.lean
index 42eb56cc9..eb78350c4 100644
--- a/src/Iris/BI/Lib/Fixpoint.lean
+++ b/src/Iris/BI/Lib/Fixpoint.lean
@@ -3,9 +3,12 @@ Copyright (c) 2026 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus de Medeiros
 -/
+module
 
-import Iris.BI
-import Iris.ProofMode
+public import Iris.BI
+public import Iris.ProofMode
+
+@[expose] public section
 
 namespace Iris
 open Iris.Std BI OFE
diff --git a/src/Iris/BI/Notation.lean b/src/Iris/BI/Notation.lean
index 825a36c06..177fc7516 100644
--- a/src/Iris/BI/Notation.lean
+++ b/src/Iris/BI/Notation.lean
@@ -3,7 +3,11 @@ 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
 -/
-import Lean.PrettyPrinter.Delaborator
+module
+
+public meta import Lean.PrettyPrinter.Delaborator
+
+public meta section
 
 namespace Iris.BI
 open Lean Lean.Macro
diff --git a/src/Iris/BI/Plainly.lean b/src/Iris/BI/Plainly.lean
index c8b49fb4f..f4020b475 100644
--- a/src/Iris/BI/Plainly.lean
+++ b/src/Iris/BI/Plainly.lean
@@ -3,11 +3,14 @@ Copyright (c) 2025 Markus de Medeiros. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus de Medeiros
 -/
+module
 
-import Iris.BI.Classes
-import Iris.BI.BI
-import Iris.BI.DerivedLaws
-import Iris.Algebra
+public import Iris.BI.Classes
+public import Iris.BI.BI
+public import Iris.BI.DerivedLaws
+public import Iris.Algebra
+
+@[expose] public section
 
 namespace Iris
 open BI
diff --git a/src/Iris/BI/Updates.lean b/src/Iris/BI/Updates.lean
index bb78296b1..5a595a539 100644
--- a/src/Iris/BI/Updates.lean
+++ b/src/Iris/BI/Updates.lean
@@ -3,13 +3,16 @@ Copyright (c) 2025 Markus de Medeiros. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus de Medeiros
 -/
+module
 
-import Iris.BI.BI
-import Iris.BI.BIBase
-import Iris.BI.Classes
-import Iris.BI.DerivedLaws
-import Iris.Algebra
-import Iris.BI.Plainly
+public import Iris.BI.BI
+public import Iris.BI.BIBase
+public import Iris.BI.Classes
+public import Iris.BI.DerivedLaws
+public import Iris.Algebra
+public import Iris.BI.Plainly
+
+@[expose] public section
 
 namespace Iris
 open Iris.Std BI
diff --git a/src/Iris/Examples.lean b/src/Iris/Examples.lean
index a831b63e6..1c5929295 100644
--- a/src/Iris/Examples.lean
+++ b/src/Iris/Examples.lean
@@ -1 +1,3 @@
-import Iris.Examples.Proofs
+module
+
+public import Iris.Examples.Proofs
diff --git a/src/Iris/Examples/IProp.lean b/src/Iris/Examples/IProp.lean
index 93bce0df6..b4f4b5054 100644
--- a/src/Iris/Examples/IProp.lean
+++ b/src/Iris/Examples/IProp.lean
@@ -3,11 +3,15 @@ Copyright (c) 2025 Markus de Medeiros. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus de Medeiros
 -/
-import Iris.BI
-import Iris.ProofMode
-import Iris.Instances.IProp
-import Iris.Algebra
-import Iris.Std.HeapInstances
+module
+
+public import Iris.BI
+public import Iris.ProofMode
+public import Iris.Instances.IProp
+public import Iris.Algebra
+public import Iris.Std.HeapInstances
+
+@[expose] public section
 
 namespace Iris.Examples
 open Iris.BI COFE
diff --git a/src/Iris/Examples/Proofs.lean b/src/Iris/Examples/Proofs.lean
index e742de19d..cdada7968 100644
--- a/src/Iris/Examples/Proofs.lean
+++ b/src/Iris/Examples/Proofs.lean
@@ -3,8 +3,12 @@ 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
 -/
-import Iris.BI
-import Iris.ProofMode
+module
+
+public import Iris.BI
+public import Iris.ProofMode
+
+@[expose] public section
 
 namespace Iris.Examples
 open Iris.BI
diff --git a/src/Iris/Examples/Resources.lean b/src/Iris/Examples/Resources.lean
index b771fb97d..2973a9696 100644
--- a/src/Iris/Examples/Resources.lean
+++ b/src/Iris/Examples/Resources.lean
@@ -3,11 +3,15 @@ Copyright (c) 2025 Markus de Medeiros. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus de Medeiros
 -/
-import Iris.ProofMode
-import Iris.Algebra.IProp
-import Iris.Instances.UPred.Instance
-import Iris.Instances.IProp.Instance
-import Iris.Algebra.Agree
+module
+
+public import Iris.ProofMode
+public import Iris.Algebra.IProp
+public import Iris.Instances.UPred.Instance
+public import Iris.Instances.IProp.Instance
+public import Iris.Algebra.Agree
+
+@[expose] public section
 
 namespace Iris.Examples
 open Iris.BI COFE
diff --git a/src/Iris/Instances.lean b/src/Iris/Instances.lean
index 995cfb742..52446176e 100644
--- a/src/Iris/Instances.lean
+++ b/src/Iris/Instances.lean
@@ -1,2 +1,4 @@
-import Iris.Instances.Classical
-import Iris.Instances.Data
+module
+
+public import Iris.Instances.Classical
+public import Iris.Instances.Data
diff --git a/src/Iris/Instances/Classical.lean b/src/Iris/Instances/Classical.lean
index dfcc4702a..d31ec3b2f 100644
--- a/src/Iris/Instances/Classical.lean
+++ b/src/Iris/Instances/Classical.lean
@@ -1,2 +1,4 @@
-import Iris.Instances.Classical.Instance
-import Iris.Instances.Classical.Notation
+module
+
+public import Iris.Instances.Classical.Instance
+public import Iris.Instances.Classical.Notation
diff --git a/src/Iris/Instances/Classical/Instance.lean b/src/Iris/Instances/Classical/Instance.lean
index 78a8aef51..442274b41 100644
--- a/src/Iris/Instances/Classical/Instance.lean
+++ b/src/Iris/Instances/Classical/Instance.lean
@@ -3,9 +3,13 @@ Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lars König
 -/
-import Iris.BI
-import Iris.Instances.Data
-import Iris.Std.Equivalence
+module
+
+public import Iris.BI
+public import Iris.Instances.Data
+public import Iris.Std.Equivalence
+
+@[expose] public section
 
 namespace Iris.Instances.Classical
 open Iris.BI Iris.Instances.Data Std
diff --git a/src/Iris/Instances/Classical/Notation.lean b/src/Iris/Instances/Classical/Notation.lean
index 51e1c1143..1d21dd449 100644
--- a/src/Iris/Instances/Classical/Notation.lean
+++ b/src/Iris/Instances/Classical/Notation.lean
@@ -3,7 +3,11 @@ 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
 -/
-import Iris.Instances.Classical.Instance
+module
+
+public import Iris.Instances.Classical.Instance
+
+@[expose] public section
 
 namespace Iris.Instances.Classical
 open Iris.Instances.Data
diff --git a/src/Iris/Instances/Data.lean b/src/Iris/Instances/Data.lean
index d7db7d9d8..c975aca9d 100644
--- a/src/Iris/Instances/Data.lean
+++ b/src/Iris/Instances/Data.lean
@@ -1,2 +1,4 @@
-import Iris.Instances.Data.SetNotation
-import Iris.Instances.Data.State
+module
+
+public import Iris.Instances.Data.SetNotation
+public import Iris.Instances.Data.State
diff --git a/src/Iris/Instances/Data/SetNotation.lean b/src/Iris/Instances/Data/SetNotation.lean
index 0eed8b344..0155d488a 100644
--- a/src/Iris/Instances/Data/SetNotation.lean
+++ b/src/Iris/Instances/Data/SetNotation.lean
@@ -3,6 +3,9 @@ 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
 -/
+module
+
+@[expose] public section
 
 namespace Iris.Instances.Data
 
diff --git a/src/Iris/Instances/Data/State.lean b/src/Iris/Instances/Data/State.lean
index 02bf804dd..d78fc998b 100644
--- a/src/Iris/Instances/Data/State.lean
+++ b/src/Iris/Instances/Data/State.lean
@@ -3,7 +3,11 @@ 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
 -/
-import Iris.Instances.Data.SetNotation
+module
+
+public import Iris.Instances.Data.SetNotation
+
+@[expose] public section
 
 namespace Iris.Instances.Data
 
diff --git a/src/Iris/Instances/IProp.lean b/src/Iris/Instances/IProp.lean
index 0e63032ba..30a27a1be 100644
--- a/src/Iris/Instances/IProp.lean
+++ b/src/Iris/Instances/IProp.lean
@@ -1 +1,3 @@
-import Iris.Instances.IProp.Instance
+module
+
+public import Iris.Instances.IProp.Instance
diff --git a/src/Iris/Instances/IProp/Instance.lean b/src/Iris/Instances/IProp/Instance.lean
index 60a17cdfe..e7e2f7647 100644
--- a/src/Iris/Instances/IProp/Instance.lean
+++ b/src/Iris/Instances/IProp/Instance.lean
@@ -3,10 +3,13 @@ Copyright (c) 2025 Markus de Medeiros. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus de Medeiros, Zongyuan Liu, Remy Seassau
 -/
+module
 
-import Iris.BI
-import Iris.Algebra
-import Iris.Instances.UPred
+public import Iris.BI
+public import Iris.Algebra
+public import Iris.Instances.UPred
+
+@[expose] public section
 namespace Iris
 
 open COFE
diff --git a/src/Iris/Instances/UPred.lean b/src/Iris/Instances/UPred.lean
index 8930d2dc3..68821abe0 100644
--- a/src/Iris/Instances/UPred.lean
+++ b/src/Iris/Instances/UPred.lean
@@ -1 +1,3 @@
-import Iris.Instances.UPred.Instance
+module
+
+public import Iris.Instances.UPred.Instance
diff --git a/src/Iris/Instances/UPred/Instance.lean b/src/Iris/Instances/UPred/Instance.lean
index d62fd1c4e..5d1da7373 100644
--- a/src/Iris/Instances/UPred/Instance.lean
+++ b/src/Iris/Instances/UPred/Instance.lean
@@ -3,13 +3,16 @@ Copyright (c) 2025 Markus de Medeiros. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus de Medeiros, Mario Carneiro
 -/
+module
 
-import Iris.BI
-import Iris.Algebra.OFE
-import Iris.Algebra.CMRA
-import Iris.Algebra.UPred
-import Iris.Algebra.Updates
-import Iris.BI.Lib.BUpdPlain
+public import Iris.BI
+public import Iris.Algebra.OFE
+public import Iris.Algebra.CMRA
+public import Iris.Algebra.UPred
+public import Iris.Algebra.Updates
+public import Iris.BI.Lib.BUpdPlain
+
+@[expose] public section
 
 section UPredInstance
 
diff --git a/src/Iris/ProofMode.lean b/src/Iris/ProofMode.lean
index f2462941b..34761f9c8 100644
--- a/src/Iris/ProofMode.lean
+++ b/src/Iris/ProofMode.lean
@@ -1,12 +1,14 @@
-import Iris.ProofMode.Classes
-import Iris.ProofMode.ClassesMake
-import Iris.ProofMode.Display
-import Iris.ProofMode.Expr
-import Iris.ProofMode.Instances
-import Iris.ProofMode.InstancesLater
-import Iris.ProofMode.InstancesMake
-import Iris.ProofMode.InstancesPlainly
-import Iris.ProofMode.InstancesUpdates
-import Iris.ProofMode.Patterns
-import Iris.ProofMode.Tactics
-import Iris.ProofMode.UnifHints
+module
+
+public import Iris.ProofMode.Classes
+public import Iris.ProofMode.ClassesMake
+public meta import Iris.ProofMode.Display
+public meta import Iris.ProofMode.Expr
+public import Iris.ProofMode.Instances
+public import Iris.ProofMode.InstancesLater
+public import Iris.ProofMode.InstancesMake
+public import Iris.ProofMode.InstancesPlainly
+public import Iris.ProofMode.InstancesUpdates
+public import Iris.ProofMode.Patterns
+public meta import Iris.ProofMode.Tactics
+public import Iris.ProofMode.UnifHints
diff --git a/src/Iris/ProofMode/Classes.lean b/src/Iris/ProofMode/Classes.lean
index 7ab75b303..4d3c4cbb4 100644
--- a/src/Iris/ProofMode/Classes.lean
+++ b/src/Iris/ProofMode/Classes.lean
@@ -3,9 +3,13 @@ Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lars König, Michael Sammler
 -/
-import Iris.BI
-import Iris.ProofMode.SynthInstance
-import Iris.ProofMode.Modalities
+module
+
+public import Iris.BI
+public meta import Iris.ProofMode.SynthInstance
+public import Iris.ProofMode.Modalities
+
+@[expose] public section
 
 namespace Iris.ProofMode
 open Iris.BI
diff --git a/src/Iris/ProofMode/ClassesMake.lean b/src/Iris/ProofMode/ClassesMake.lean
index 235e4781e..c28ae6e21 100644
--- a/src/Iris/ProofMode/ClassesMake.lean
+++ b/src/Iris/ProofMode/ClassesMake.lean
@@ -3,8 +3,12 @@ Copyright (c) 2026 Michael Sammler. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michael Sammler
 -/
-import Iris.BI
-import Iris.ProofMode.SynthInstance
+module
+
+public import Iris.BI
+public meta import Iris.ProofMode.SynthInstance
+
+@[expose] public section
 
 namespace Iris.ProofMode
 open Iris.BI
diff --git a/src/Iris/ProofMode/Display.lean b/src/Iris/ProofMode/Display.lean
index 627c56926..cdb21e64c 100644
--- a/src/Iris/ProofMode/Display.lean
+++ b/src/Iris/ProofMode/Display.lean
@@ -3,10 +3,14 @@ Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lars König, Mario Carneiro
 -/
-import Iris.BI.Notation
-import Iris.ProofMode.Expr
+module
 
-import Lean.PrettyPrinter.Delaborator
+public meta import Iris.BI.Notation
+public meta import Iris.ProofMode.Expr
+
+public meta import Lean.PrettyPrinter.Delaborator
+
+public meta section
 
 namespace Iris.ProofMode
 open Iris.BI Qq
diff --git a/src/Iris/ProofMode/Expr.lean b/src/Iris/ProofMode/Expr.lean
index 88e49762a..612ff9081 100644
--- a/src/Iris/ProofMode/Expr.lean
+++ b/src/Iris/ProofMode/Expr.lean
@@ -3,17 +3,22 @@ Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lars König, Mario Carneiro, Michael Sammler
 -/
-import Qq
-import Iris.BI
-import Iris.ProofMode.Classes
-import Iris.Std
+module
+
+public meta import Qq
+public import Iris.BI
+public import Iris.ProofMode.Classes
+public import Iris.Std
+public meta import Iris.Std.Expr
+
+public meta section
 
 namespace Iris.ProofMode
 open Iris.BI Iris.Std
 open Lean Lean.Expr Lean.Meta Qq
 
-@[match_pattern] def nameAnnotation := `name
-@[match_pattern] def uniqAnnotation := `uniq
+@[expose, match_pattern] def nameAnnotation := `name
+@[expose, match_pattern] def uniqAnnotation := `uniq
 
 def parseName? : Expr → Option (Name × Name × Expr)
   | .mdata ⟨[(nameAnnotation, .ofName name), (uniqAnnotation, .ofName uniq)]⟩ e => do
@@ -112,32 +117,32 @@ def Hyps.select (ty : Expr) : ∀ {s}, @Hyps u prop bi s → MetaM (Name × Q(Bo
   | _, .sep _ _ _ _ lhs rhs => try Hyps.select ty rhs catch _ => Hyps.select ty lhs
 
 
-private theorem intuitionistically_sep_dup [BI PROP] {P : PROP} : □ P ⊣⊢ □ P ∗ □ P :=
+theorem intuitionistically_sep_dup [BI PROP] {P : PROP} : □ P ⊣⊢ □ P ∗ □ P :=
   intuitionistically_sep_idem.symm
 
-private theorem sep_emp_rev [BI PROP] {P : PROP} : P ⊣⊢ P ∗ emp := sep_emp.symm
+theorem sep_emp_rev [BI PROP] {P : PROP} : P ⊣⊢ P ∗ emp := sep_emp.symm
 
-private theorem emp_sep_rev [BI PROP] {P : PROP} : P ⊣⊢ emp ∗ P := emp_sep.symm
+theorem emp_sep_rev [BI PROP] {P : PROP} : P ⊣⊢ emp ∗ P := emp_sep.symm
 
 section split
 
-private theorem split_es [BI PROP] {Q Q1 Q2 : PROP} (h : Q ⊣⊢ Q1 ∗ Q2) : emp ∗ Q ⊣⊢ Q1 ∗ Q2 :=
+theorem split_es [BI PROP] {Q Q1 Q2 : PROP} (h : Q ⊣⊢ Q1 ∗ Q2) : emp ∗ Q ⊣⊢ Q1 ∗ Q2 :=
   emp_sep.trans h
-private theorem split_ls [BI PROP] {P Q Q1 Q2 : PROP} (h : Q ⊣⊢ Q1 ∗ Q2) : P ∗ Q ⊣⊢ (P ∗ Q1) ∗ Q2 :=
+theorem split_ls [BI PROP] {P Q Q1 Q2 : PROP} (h : Q ⊣⊢ Q1 ∗ Q2) : P ∗ Q ⊣⊢ (P ∗ Q1) ∗ Q2 :=
   (sep_congr_r h).trans sep_assoc.symm
-private theorem split_rs [BI PROP] {P Q Q1 Q2 : PROP} (h : Q ⊣⊢ Q1 ∗ Q2) : P ∗ Q ⊣⊢ Q1 ∗ (P ∗ Q2) :=
+theorem split_rs [BI PROP] {P Q Q1 Q2 : PROP} (h : Q ⊣⊢ Q1 ∗ Q2) : P ∗ Q ⊣⊢ Q1 ∗ (P ∗ Q2) :=
   (sep_congr_r h).trans sep_left_comm
-private theorem split_se [BI PROP] {P P1 P2 : PROP} (h : P ⊣⊢ P1 ∗ P2) : P ∗ emp ⊣⊢ P1 ∗ P2 :=
+theorem split_se [BI PROP] {P P1 P2 : PROP} (h : P ⊣⊢ P1 ∗ P2) : P ∗ emp ⊣⊢ P1 ∗ P2 :=
   sep_emp.trans h
-private theorem split_sl [BI PROP] {P Q P1 P2 : PROP} (h : P ⊣⊢ P1 ∗ P2) : P ∗ Q ⊣⊢ (P1 ∗ Q) ∗ P2 :=
+theorem split_sl [BI PROP] {P Q P1 P2 : PROP} (h : P ⊣⊢ P1 ∗ P2) : P ∗ Q ⊣⊢ (P1 ∗ Q) ∗ P2 :=
   (sep_congr_l h).trans sep_right_comm
-private theorem split_sr [BI PROP] {P Q P1 P2 : PROP} (h : P ⊣⊢ P1 ∗ P2) : P ∗ Q ⊣⊢ P1 ∗ (P2 ∗ Q) :=
+theorem split_sr [BI PROP] {P Q P1 P2 : PROP} (h : P ⊣⊢ P1 ∗ P2) : P ∗ Q ⊣⊢ P1 ∗ (P2 ∗ Q) :=
   (sep_congr_l h).trans sep_assoc
-private theorem split_ss [BI PROP] {P Q P1 P2 Q1 Q2 : PROP}
+theorem split_ss [BI PROP] {P Q P1 P2 Q1 Q2 : PROP}
     (h1 : P ⊣⊢ P1 ∗ P2) (h2 : Q ⊣⊢ Q1 ∗ Q2) : P ∗ Q ⊣⊢ (P1 ∗ Q1) ∗ (P2 ∗ Q2) :=
   (sep_congr h1 h2).trans sep_sep_sep_comm
 
-private inductive SplitResult {prop : Q(Type u)} (bi : Q(BI $prop)) (e : Q($prop)) where
+inductive SplitResult {prop : Q(Type u)} (bi : Q(BI $prop)) (e : Q($prop)) where
   | emp (_ : $e =Q BI.emp)
   | left
   | right
@@ -145,7 +150,7 @@ private inductive SplitResult {prop : Q(Type u)} (bi : Q(BI $prop)) (e : Q($prop
           (pf : Q($e ⊣⊢ $elhs ∗ $erhs))
 
 variable {prop : Q(Type u)} (bi : Q(BI $prop)) (toRight : Name → Name → Bool) in
-private def Hyps.splitCore : ∀ {e}, Hyps bi e → SplitResult bi e
+def Hyps.splitCore : ∀ {e}, Hyps bi e → SplitResult bi e
   | _, .emp _ => .emp ⟨⟩
   | ehyp, h@(.hyp _ name uniq b ty _) =>
     match matchBool b with
@@ -188,23 +193,23 @@ structure RemoveHyp {prop : Q(Type u)} (bi : Q(BI $prop)) (e : Q($prop)) where
   (pf : Q($e ⊣⊢ $e' ∗ $out))
   deriving Inhabited
 
-private inductive RemoveHypCore {prop : Q(Type u)} (bi : Q(BI $prop)) (e : Q($prop)) (α : Type) where
+inductive RemoveHypCore {prop : Q(Type u)} (bi : Q(BI $prop)) (e : Q($prop)) (α : Type) where
   | none
   | one (a : α) (out' : Q($prop)) (p : Q(Bool)) (eq : $e =Q iprop(□?$p $out'))
   | main (a : α) (_ : RemoveHyp bi e)
 
-private theorem remove_l [BI PROP] {P P' Q R : PROP} (h : P ⊣⊢ P' ∗ R) :
+theorem remove_l [BI PROP] {P P' Q R : PROP} (h : P ⊣⊢ P' ∗ R) :
     P ∗ Q ⊣⊢ (P' ∗ Q) ∗ R :=
   (sep_congr_l h).trans sep_right_comm
 
-private theorem remove_r [BI PROP] {P Q Q' R : PROP} (h : Q ⊣⊢ Q' ∗ R) :
+theorem remove_r [BI PROP] {P Q Q' R : PROP} (h : Q ⊣⊢ Q' ∗ R) :
     P ∗ Q ⊣⊢ (P ∗ Q') ∗ R :=
   (sep_congr_r h).trans sep_assoc.symm
 
 variable [Monad m] {prop : Q(Type u)} (bi : Q(BI $prop)) (rp : Bool)
   (check : Name → Name → Q(Bool) → Q($prop) → m (Option α)) in
 /-- If `rp` is true, the hyp will be removed even if it is in the intuitionistic context. -/
-private def Hyps.removeCore : ∀ {e}, Hyps bi e → m (RemoveHypCore bi e α)
+def Hyps.removeCore : ∀ {e}, Hyps bi e → m (RemoveHypCore bi e α)
   | _, .emp _ => pure .none
   | e, h@(.hyp _ name uniq p ty _) => do
     if let some a ← check name uniq p ty then
diff --git a/src/Iris/ProofMode/Instances.lean b/src/Iris/ProofMode/Instances.lean
index 6163d839d..a7227b276 100644
--- a/src/Iris/ProofMode/Instances.lean
+++ b/src/Iris/ProofMode/Instances.lean
@@ -3,10 +3,14 @@ Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lars König, Mario Carneiro
 -/
-import Iris.BI
-import Iris.ProofMode.Classes
-import Iris.ProofMode.ModalityInstances
-import Iris.Std.TC
+module
+
+public import Iris.BI
+public import Iris.ProofMode.Classes
+public import Iris.ProofMode.ModalityInstances
+public import Iris.Std.TC
+
+@[expose] public section
 
 namespace Iris.ProofMode
 open Iris.BI Iris.Std
diff --git a/src/Iris/ProofMode/InstancesLater.lean b/src/Iris/ProofMode/InstancesLater.lean
index cf80210d9..affa072ed 100644
--- a/src/Iris/ProofMode/InstancesLater.lean
+++ b/src/Iris/ProofMode/InstancesLater.lean
@@ -3,11 +3,15 @@ Copyright (c) 2026 Michael Sammler. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michael Sammler
 -/
-import Iris.BI
-import Iris.ProofMode.Classes
-import Iris.ProofMode.ClassesMake
-import Iris.ProofMode.ModalityInstances
-import Iris.Std.TC
+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
+
+@[expose] public section
 
 namespace Iris.ProofMode
 open Iris.BI Iris.Std
diff --git a/src/Iris/ProofMode/InstancesMake.lean b/src/Iris/ProofMode/InstancesMake.lean
index a70cbaf34..2edcfb174 100644
--- a/src/Iris/ProofMode/InstancesMake.lean
+++ b/src/Iris/ProofMode/InstancesMake.lean
@@ -3,8 +3,12 @@ Copyright (c) 2026 Michael Sammler. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michael Sammler
 -/
-import Iris.BI
-import Iris.ProofMode.ClassesMake
+module
+
+public import Iris.BI
+public import Iris.ProofMode.ClassesMake
+
+@[expose] public section
 
 namespace Iris.ProofMode
 open Iris.BI
diff --git a/src/Iris/ProofMode/InstancesPlainly.lean b/src/Iris/ProofMode/InstancesPlainly.lean
index ffa3f7cec..7769451c9 100644
--- a/src/Iris/ProofMode/InstancesPlainly.lean
+++ b/src/Iris/ProofMode/InstancesPlainly.lean
@@ -3,10 +3,14 @@ Copyright (c) 2026 Michael Sammler. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michael Sammler
 -/
-import Iris.BI
-import Iris.ProofMode.Classes
-import Iris.ProofMode.ModalityInstances
-import Iris.Std.TC
+module
+
+public import Iris.BI
+public import Iris.ProofMode.Classes
+public import Iris.ProofMode.ModalityInstances
+public import Iris.Std.TC
+
+@[expose] public section
 
 namespace Iris.ProofMode
 open Iris.BI Iris.Std
diff --git a/src/Iris/ProofMode/InstancesUpdates.lean b/src/Iris/ProofMode/InstancesUpdates.lean
index 9571edf6c..c50e2b1f4 100644
--- a/src/Iris/ProofMode/InstancesUpdates.lean
+++ b/src/Iris/ProofMode/InstancesUpdates.lean
@@ -3,9 +3,13 @@ Copyright (c) 2026 Michael Sammler. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michael Sammler
 -/
-import Iris.BI
-import Iris.ProofMode.Classes
-import Iris.Std.TC
+module
+
+public import Iris.BI
+public import Iris.ProofMode.Classes
+public import Iris.Std.TC
+
+@[expose] public section
 
 namespace Iris.ProofMode
 open Iris.BI Iris.Std
diff --git a/src/Iris/ProofMode/Modalities.lean b/src/Iris/ProofMode/Modalities.lean
index 48125cf87..5aef8677d 100644
--- a/src/Iris/ProofMode/Modalities.lean
+++ b/src/Iris/ProofMode/Modalities.lean
@@ -3,7 +3,11 @@ Copyright (c) 2025 Markus de Medeiros. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus de Medeiros, Michael Sammler
 -/
-import Iris.BI
+module
+
+public import Iris.BI
+
+@[expose] public section
 
 namespace Iris.ProofMode
 open Iris.BI
diff --git a/src/Iris/ProofMode/ModalityInstances.lean b/src/Iris/ProofMode/ModalityInstances.lean
index e532e6ece..57b0f0866 100644
--- a/src/Iris/ProofMode/ModalityInstances.lean
+++ b/src/Iris/ProofMode/ModalityInstances.lean
@@ -3,10 +3,14 @@ Copyright (c) 2025 Markus de Medeiros. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus de Medeiros, Michael Sammler
 -/
-import Iris.BI
-import Iris.BI.DerivedLaws
-import Iris.ProofMode.Modalities
-import Iris.ProofMode.Classes
+module
+
+public import Iris.BI
+public import Iris.BI.DerivedLaws
+public import Iris.ProofMode.Modalities
+public import Iris.ProofMode.Classes
+
+@[expose] public section
 
 namespace Iris.ProofMode
 open Iris.BI
diff --git a/src/Iris/ProofMode/Patterns.lean b/src/Iris/ProofMode/Patterns.lean
index 3125976c8..09f22c48d 100644
--- a/src/Iris/ProofMode/Patterns.lean
+++ b/src/Iris/ProofMode/Patterns.lean
@@ -1,4 +1,6 @@
-import Iris.ProofMode.Patterns.CasesPattern
-import Iris.ProofMode.Patterns.IntroPattern
-import Iris.ProofMode.Patterns.ProofModeTerm
-import Iris.ProofMode.Patterns.SpecPattern
+module
+
+public import Iris.ProofMode.Patterns.CasesPattern
+public import Iris.ProofMode.Patterns.IntroPattern
+public import Iris.ProofMode.Patterns.ProofModeTerm
+public import Iris.ProofMode.Patterns.SpecPattern
diff --git a/src/Iris/ProofMode/Patterns/CasesPattern.lean b/src/Iris/ProofMode/Patterns/CasesPattern.lean
index 90d7072b9..77d3b0f23 100644
--- a/src/Iris/ProofMode/Patterns/CasesPattern.lean
+++ b/src/Iris/ProofMode/Patterns/CasesPattern.lean
@@ -3,7 +3,11 @@ 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
 -/
-import Lean.Data.Name
+module
+
+public import Lean.Data.Name
+
+@[expose] public section
 
 namespace Iris.ProofMode
 open Lean
diff --git a/src/Iris/ProofMode/Patterns/IntroPattern.lean b/src/Iris/ProofMode/Patterns/IntroPattern.lean
index 64780e78a..cb0477e6c 100644
--- a/src/Iris/ProofMode/Patterns/IntroPattern.lean
+++ b/src/Iris/ProofMode/Patterns/IntroPattern.lean
@@ -3,7 +3,11 @@ Copyright (c) 2025 Michael Sammler. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michael Sammler
 -/
-import Iris.ProofMode.Patterns.CasesPattern
+module
+
+public import Iris.ProofMode.Patterns.CasesPattern
+
+@[expose] public section
 
 namespace Iris.ProofMode
 open Lean
diff --git a/src/Iris/ProofMode/Patterns/ProofModeTerm.lean b/src/Iris/ProofMode/Patterns/ProofModeTerm.lean
index 51e6b974d..2657e6df7 100644
--- a/src/Iris/ProofMode/Patterns/ProofModeTerm.lean
+++ b/src/Iris/ProofMode/Patterns/ProofModeTerm.lean
@@ -3,7 +3,11 @@ Copyright (c) 2025 Oliver Soeser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Soeser
 -/
-import Iris.ProofMode.Patterns.SpecPattern
+module
+
+public import Iris.ProofMode.Patterns.SpecPattern
+
+@[expose] public section
 
 namespace Iris.ProofMode
 open Lean
diff --git a/src/Iris/ProofMode/Patterns/SpecPattern.lean b/src/Iris/ProofMode/Patterns/SpecPattern.lean
index a482ca60c..ac5c12527 100644
--- a/src/Iris/ProofMode/Patterns/SpecPattern.lean
+++ b/src/Iris/ProofMode/Patterns/SpecPattern.lean
@@ -3,6 +3,10 @@ Copyright (c) 2025 Oliver Soeser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Soeser
 -/
+module
+
+@[expose] public section
+
 namespace Iris.ProofMode
 open Lean
 
diff --git a/src/Iris/ProofMode/ProofModeM.lean b/src/Iris/ProofMode/ProofModeM.lean
index da3c746c0..399f1dffb 100644
--- a/src/Iris/ProofMode/ProofModeM.lean
+++ b/src/Iris/ProofMode/ProofModeM.lean
@@ -3,8 +3,12 @@ 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
 -/
-import Iris.ProofMode.Expr
-import Iris.ProofMode.Classes
+module
+
+public meta import Iris.ProofMode.Expr
+public import Iris.ProofMode.Classes
+
+public meta section
 
 namespace Iris.ProofMode
 open Lean Elab Tactic Meta Qq BI Std
diff --git a/src/Iris/ProofMode/SynthInstance.lean b/src/Iris/ProofMode/SynthInstance.lean
index dad465b5e..11f7bbccd 100644
--- a/src/Iris/ProofMode/SynthInstance.lean
+++ b/src/Iris/ProofMode/SynthInstance.lean
@@ -3,8 +3,12 @@ Copyright (c) 2025 Michael Sammler. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michael Sammler
 -/
-import Qq
-import Iris.BI
+module
+
+public import Qq
+public import Iris.BI
+
+public meta section
 
 /-
 This file implements a custom typeclass synthesis algorithm that is used for the proof mode typeclasses.
@@ -70,7 +74,7 @@ initialize registerBuiltinAttribute {
 }
 
 
-private partial def synthInstanceMainCore (mvar : Expr) : MetaM (Option Unit) := do
+partial def synthInstanceMainCore (mvar : Expr) : MetaM (Option Unit) := do
   withIncRecDepth do
     let backtrackSet := ipmBacktrackExt.getState (← getEnv)
     let mvarType  ← inferType mvar
@@ -103,7 +107,7 @@ private partial def synthInstanceMainCore (mvar : Expr) : MetaM (Option Unit) :=
         return res
     return none
 
-private def synthInstanceMain (type : Expr) (_maxResultSize : Nat) : MetaM (Option Expr) :=
+def synthInstanceMain (type : Expr) (_maxResultSize : Nat) : MetaM (Option Expr) :=
   withCurrHeartbeats do
      let mvar ← mkFreshExprMVar type
      tryCatchRuntimeEx (do
@@ -115,7 +119,7 @@ private def synthInstanceMain (type : Expr) (_maxResultSize : Nat) : MetaM (Opti
          else
            throw ex
 
-private def synthInstanceCore? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (Option Expr) := do
+def synthInstanceCore? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (Option Expr) := do
   let opts ← getOptions
   let maxResultSize := maxResultSize?.getD (synthInstance.maxSize.get opts)
   withTraceNode `Meta.synthInstance
diff --git a/src/Iris/ProofMode/Tactics.lean b/src/Iris/ProofMode/Tactics.lean
index c5b37ed56..006c80d8e 100644
--- a/src/Iris/ProofMode/Tactics.lean
+++ b/src/Iris/ProofMode/Tactics.lean
@@ -1,18 +1,20 @@
 /- A description of the tactics can be found in `tactics.md`. -/
-import Iris.ProofMode.Tactics.Apply
-import Iris.ProofMode.Tactics.Assumption
-import Iris.ProofMode.Tactics.Basic
-import Iris.ProofMode.Tactics.Cases
-import Iris.ProofMode.Tactics.Clear
-import Iris.ProofMode.Tactics.Exact
-import Iris.ProofMode.Tactics.ExFalso
-import Iris.ProofMode.Tactics.Exists
-import Iris.ProofMode.Tactics.Have
-import Iris.ProofMode.Tactics.Intro
-import Iris.ProofMode.Tactics.LeftRight
-import Iris.ProofMode.Tactics.Mod
-import Iris.ProofMode.Tactics.ModIntro
-import Iris.ProofMode.Tactics.Pure
-import Iris.ProofMode.Tactics.Rename
-import Iris.ProofMode.Tactics.Specialize
-import Iris.ProofMode.Tactics.Split
+module
+
+public meta import Iris.ProofMode.Tactics.Apply
+public meta import Iris.ProofMode.Tactics.Assumption
+public meta import Iris.ProofMode.Tactics.Basic
+public meta import Iris.ProofMode.Tactics.Cases
+public meta import Iris.ProofMode.Tactics.Clear
+public meta import Iris.ProofMode.Tactics.Exact
+public meta import Iris.ProofMode.Tactics.ExFalso
+public meta import Iris.ProofMode.Tactics.Exists
+public meta import Iris.ProofMode.Tactics.Have
+public meta import Iris.ProofMode.Tactics.Intro
+public meta import Iris.ProofMode.Tactics.LeftRight
+public meta import Iris.ProofMode.Tactics.Mod
+public meta import Iris.ProofMode.Tactics.ModIntro
+public meta import Iris.ProofMode.Tactics.Pure
+public meta import Iris.ProofMode.Tactics.Rename
+public meta import Iris.ProofMode.Tactics.Specialize
+public meta import Iris.ProofMode.Tactics.Split
diff --git a/src/Iris/ProofMode/Tactics/Apply.lean b/src/Iris/ProofMode/Tactics/Apply.lean
index 9ea2c2702..bfda925bf 100644
--- a/src/Iris/ProofMode/Tactics/Apply.lean
+++ b/src/Iris/ProofMode/Tactics/Apply.lean
@@ -3,18 +3,27 @@ Copyright (c) 2025 Oliver Soeser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Soeser, Michael Sammler
 -/
-import Iris.ProofMode.Patterns.ProofModeTerm
-import Iris.ProofMode.Tactics.Assumption
-import Iris.ProofMode.Tactics.HaveCore
+module
+
+import Iris.BI
+import Iris.ProofMode.Classes
+meta import Iris.ProofMode.Patterns.ProofModeTerm
+meta import Iris.ProofMode.Tactics.Assumption
+public meta import Iris.ProofMode.Tactics.HaveCore
 
 namespace Iris.ProofMode
-open Lean Elab Tactic Meta Qq BI Std
 
-private theorem apply [BI PROP] {p} {P Q Q1 R : PROP}
+public section
+open BI
+
+theorem apply [BI PROP] {p} {P Q Q1 R : PROP}
     (h1 : P ⊢ Q1)
     [h2 : IntoWand p false Q .out Q1 .in R] : P ∗ □?p Q ⊢ R :=
       (Entails.trans (sep_mono_l h1) (wand_elim' h2.1))
 
+public meta section
+open Lean Elab Tactic Meta Qq Std
+
 /--
 Apply a hypothesis `A` to the `goal` by eliminating the wands recursively
 
@@ -25,7 +34,7 @@ Apply a hypothesis `A` to the `goal` by eliminating the wands recursively
 ## Returns
 The proof of `hyps ∗ □?p A ⊢ goal`
 -/
-partial def iApplyCore {prop : Q(Type u)} {bi : Q(BI $prop)} {e} (hyps : Hyps bi e) (p : Q(Bool)) (A : Q($prop)) (goal : Q($prop)) : ProofModeM Q($e ∗ □?$p $A ⊢ $goal) := do
+private partial def iApplyCore {prop : Q(Type u)} {bi : Q(BI $prop)} {e} (hyps : Hyps bi e) (p : Q(Bool)) (A : Q($prop)) (goal : Q($prop)) : ProofModeM Q($e ∗ □?$p $A ⊢ $goal) := do
   let B ← mkFreshExprMVarQ q($prop)
   -- if `A := ?B -∗ goal`, add `B` as a new subgoal and conclude `goal`
   if let some _ ← ProofModeM.trySynthInstanceQ q(IntoWand $p false $A .out $B .in $goal) then
diff --git a/src/Iris/ProofMode/Tactics/Assumption.lean b/src/Iris/ProofMode/Tactics/Assumption.lean
index a3d9076bd..55f52e51b 100644
--- a/src/Iris/ProofMode/Tactics/Assumption.lean
+++ b/src/Iris/ProofMode/Tactics/Assumption.lean
@@ -3,15 +3,23 @@ Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lars König, Mario Carneiro, Michael Sammler
 -/
-import Iris.ProofMode.Tactics.Basic
+module
+
+import Iris.BI
+import Iris.ProofMode.Classes
+public meta import Iris.ProofMode.Tactics.Basic
 
 namespace Iris.ProofMode
-open Lean Elab Tactic Meta Qq BI Std
+public section
+open BI Std
 
 theorem assumption [BI PROP] {p : Bool} {P P' A Q : PROP} [inst : FromAssumption p .in A Q]
   [TCOr (Affine P') (Absorbing Q)] (h : P ⊣⊢ P' ∗ □?p A) : P ⊢ Q :=
   h.1.trans <| (sep_mono_r inst.1).trans sep_elim_r
 
+public meta section
+open Lean Elab Tactic Meta Qq
+
 elab "iassumption" : tactic => do
   ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
 
diff --git a/src/Iris/ProofMode/Tactics/Basic.lean b/src/Iris/ProofMode/Tactics/Basic.lean
index d28b88c55..9c050f9a8 100644
--- a/src/Iris/ProofMode/Tactics/Basic.lean
+++ b/src/Iris/ProofMode/Tactics/Basic.lean
@@ -3,10 +3,14 @@ Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lars König, Mario Carneiro, Michael Sammler
 -/
-import Iris.ProofMode.Expr
+module
+
 import Iris.ProofMode.Classes
-import Iris.ProofMode.ProofModeM
-import Iris.ProofMode.SynthInstance
+meta import Iris.ProofMode.Expr
+meta import Iris.ProofMode.SynthInstance
+public meta import Iris.ProofMode.ProofModeM
+
+public meta section
 
 namespace Iris.ProofMode
 open Lean Elab.Tactic Meta Qq BI Std
diff --git a/src/Iris/ProofMode/Tactics/Cases.lean b/src/Iris/ProofMode/Tactics/Cases.lean
index 9dbedad83..723d81f7a 100644
--- a/src/Iris/ProofMode/Tactics/Cases.lean
+++ b/src/Iris/ProofMode/Tactics/Cases.lean
@@ -3,21 +3,66 @@ Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lars König, Mario Carneiro, Michael Sammler
 -/
-import Iris.ProofMode.Patterns.ProofModeTerm
-import Iris.ProofMode.Patterns.CasesPattern
-import Iris.ProofMode.Tactics.Basic
-import Iris.ProofMode.Tactics.Clear
-import Iris.ProofMode.Tactics.Pure
-import Iris.ProofMode.Tactics.HaveCore
-import Iris.ProofMode.Tactics.Mod
+module
+
+meta import Iris.ProofMode.Patterns.ProofModeTerm
+meta import Iris.ProofMode.Patterns.CasesPattern
+public meta import Iris.ProofMode.Tactics.Mod
+public meta import Iris.ProofMode.Tactics.Pure
+public meta import Iris.ProofMode.Tactics.Clear
+public meta import Iris.ProofMode.Tactics.Basic
+public meta import Iris.ProofMode.Tactics.HaveCore
 
 namespace Iris.ProofMode
-open Lean Elab Tactic Meta Qq BI Std
 
-private theorem false_elim' [BI PROP] {P Q : PROP} : P ∗ □?p False ⊢ Q :=
+public section
+open BI Std
+
+theorem false_elim' [BI PROP] {P Q : PROP} : P ∗ □?p False ⊢ Q :=
   wand_elim' <| intuitionisticallyIf_elim.trans false_elim
 
-def iCasesEmptyConj {prop : Q(Type u)} (bi : Q(BI $prop))
+theorem exists_elim' [BI PROP] {p} {P A Q : PROP} {Φ : α → PROP} [inst : IntoExists A Φ]
+    (h : ∀ a, P ∗ □?p Φ a ⊢ Q) : P ∗ □?p A ⊢ Q :=
+  (sep_mono_r <| (intuitionisticallyIf_mono inst.1).trans intuitionisticallyIf_exists.1).trans <| sep_exists_l.1.trans (exists_elim h)
+
+theorem sep_and_elim_l [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoAnd p A A1 A2]
+    (h : P ∗ □?p A1 ⊢ Q) : P ∗ □?p A ⊢ Q :=
+  (sep_mono_r <| inst.1.trans <| intuitionisticallyIf_mono and_elim_l).trans h
+
+theorem sep_and_elim_r [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoAnd p A A1 A2]
+    (h : P ∗ □?p A2 ⊢ Q) : P ∗ □?p A ⊢ Q :=
+  (sep_mono_r <| inst.1.trans <| intuitionisticallyIf_mono and_elim_r).trans h
+
+theorem sep_elim_spatial [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoSep A A1 A2]
+    (h : P ∗ A1 ⊢ A2 -∗ Q) : P ∗ A ⊢ Q :=
+  (sep_mono_r inst.1).trans <| sep_assoc.2.trans <| wand_elim h
+
+theorem and_elim_intuitionistic [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoAnd true A A1 A2]
+    (h : P ∗ □ A1 ⊢ □ A2 -∗ Q) : P ∗ □ A ⊢ Q :=
+  (sep_mono_r <| inst.1.trans intuitionistically_and_sep.1).trans <|
+  sep_assoc.2.trans <| wand_elim h
+
+theorem or_elim' [BI PROP] {p} {P A Q A1 A2 : PROP} [inst : IntoOr A A1 A2]
+    (h1 : P ∗ □?p A1 ⊢ Q) (h2 : P ∗ □?p A2 ⊢ Q) : P ∗ □?p A ⊢ Q :=
+  (sep_mono_r <| (intuitionisticallyIf_mono inst.1).trans (intuitionisticallyIf_or _).1).trans <| BI.sep_or_l.1.trans <| or_elim h1 h2
+
+theorem intuitionistic_elim_spatial [BI PROP] {A A' Q : PROP}
+    [IntoPersistently false A A'] [TCOr (Affine A) (Absorbing Q)]
+    (h : P ∗ □ A' ⊢ Q) : P ∗ A ⊢ Q := (replaces_r to_persistent_spatial).apply h
+
+theorem intuitionistic_elim_intuitionistic [BI PROP] {A A' Q : PROP} [IntoPersistently true A A']
+    (h : P ∗ □ A' ⊢ Q) : P ∗ □ A ⊢ Q := intuitionistic_elim_spatial h
+
+theorem spatial_elim [BI PROP] {p} {A A' Q : PROP} [FromAffinely A' A p]
+    (h : P ∗ A' ⊢ Q) : P ∗ □?p A ⊢ Q :=
+      (sep_mono_r <| (affinelyIf_of_intuitionisticallyIf).trans from_affinely).trans h
+
+theorem of_emp_sep [BI PROP] {A Q : PROP} (h : A ⊢ Q) : emp ∗ A ⊢ Q := emp_sep.1.trans h
+
+public meta section
+open Lean Elab Tactic Meta Qq Std
+
+private def iCasesEmptyConj {prop : Q(Type u)} (bi : Q(BI $prop))
     {P} (_hyps : Hyps bi P) (Q A' : Q($prop)) (p : Q(Bool))
     (_k : ∀ {P}, Hyps bi P → ProofModeM Q($P ⊢ $Q)) :
     ProofModeM (Q($P ∗ □?$p $A' ⊢ $Q)) := do
@@ -26,12 +71,7 @@ def iCasesEmptyConj {prop : Q(Type u)} (bi : Q(BI $prop))
   else
     throwError "icases: cannot destruct {A'} as an empty conjunct"
 
-
-private theorem exists_elim' [BI PROP] {p} {P A Q : PROP} {Φ : α → PROP} [inst : IntoExists A Φ]
-    (h : ∀ a, P ∗ □?p Φ a ⊢ Q) : P ∗ □?p A ⊢ Q :=
-  (sep_mono_r <| (intuitionisticallyIf_mono inst.1).trans intuitionisticallyIf_exists.1).trans <| sep_exists_l.1.trans (exists_elim h)
-
-def iCasesExists {prop : Q(Type u)} (bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q(Bool))
+private def iCasesExists {prop : Q(Type u)} (bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q(Bool))
     (name : TSyntax ``binderIdent)
     (k : (B B' : Q($prop)) → (_ : $B =Q iprop(□?$p $B')) → ProofModeM Q($P ∗ $B ⊢ $Q)) :
     ProofModeM (Q($P ∗ □?$p $A' ⊢ $Q)) := do
@@ -49,16 +89,7 @@ def iCasesExists {prop : Q(Type u)} (bi : Q(BI $prop)) (P Q A' : Q($prop)) (p :
     let pf : Q(∀ x, $P ∗ □?$p $Φ x ⊢ $Q) ← mkLambdaFVars #[x] <|← k B B' ⟨⟩
     return q(exists_elim' (A := $A') $pf)
 
-
-private theorem sep_and_elim_l [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoAnd p A A1 A2]
-    (h : P ∗ □?p A1 ⊢ Q) : P ∗ □?p A ⊢ Q :=
-  (sep_mono_r <| inst.1.trans <| intuitionisticallyIf_mono and_elim_l).trans h
-
-private theorem sep_and_elim_r [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoAnd p A A1 A2]
-    (h : P ∗ □?p A2 ⊢ Q) : P ∗ □?p A ⊢ Q :=
-  (sep_mono_r <| inst.1.trans <| intuitionisticallyIf_mono and_elim_r).trans h
-
-def iCasesAndLR {prop : Q(Type u)} (bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q(Bool)) (right : Bool)
+private def iCasesAndLR {prop : Q(Type u)} (bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q(Bool)) (right : Bool)
   (k : (B B' : Q($prop)) → (_ : $B =Q iprop(□?$p $B')) → ProofModeM Q($P ∗ $B ⊢ $Q)) :
     ProofModeM (Option Q($P ∗ □?$p $A' ⊢ $Q)) := do
   let A1 ← mkFreshExprMVarQ q($prop)
@@ -72,16 +103,7 @@ def iCasesAndLR {prop : Q(Type u)} (bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q
     have ⟨A1', _⟩ := mkIntuitionisticIf bi p A1
     return some q(sep_and_elim_l $(← k A1' A1 ⟨⟩))
 
-private theorem sep_elim_spatial [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoSep A A1 A2]
-    (h : P ∗ A1 ⊢ A2 -∗ Q) : P ∗ A ⊢ Q :=
-  (sep_mono_r inst.1).trans <| sep_assoc.2.trans <| wand_elim h
-
-private theorem and_elim_intuitionistic [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoAnd true A A1 A2]
-    (h : P ∗ □ A1 ⊢ □ A2 -∗ Q) : P ∗ □ A ⊢ Q :=
-  (sep_mono_r <| inst.1.trans intuitionistically_and_sep.1).trans <|
-  sep_assoc.2.trans <| wand_elim h
-
-def iCasesSep {prop : Q(Type u)} (bi : Q(BI $prop))
+private def iCasesSep {prop : Q(Type u)} (bi : Q(BI $prop))
     {P} (hyps : Hyps bi P) (Q A' : Q($prop)) (p : Q(Bool))
     (k : ∀ {P}, Hyps bi P → ProofModeM Q($P ⊢ $Q))
     (k1 k2 : ∀ {P}, Hyps bi P → (Q B B' : Q($prop)) → (_ : $B =Q iprop(□?$p $B')) →
@@ -107,11 +129,7 @@ def iCasesSep {prop : Q(Type u)} (bi : Q(BI $prop))
       return q(wand_intro $pf)
     return q(sep_elim_spatial (A := $A') $pf)
 
-private theorem or_elim' [BI PROP] {p} {P A Q A1 A2 : PROP} [inst : IntoOr A A1 A2]
-    (h1 : P ∗ □?p A1 ⊢ Q) (h2 : P ∗ □?p A2 ⊢ Q) : P ∗ □?p A ⊢ Q :=
-  (sep_mono_r <| (intuitionisticallyIf_mono inst.1).trans (intuitionisticallyIf_or _).1).trans <| BI.sep_or_l.1.trans <| or_elim h1 h2
-
-def iCasesOr {prop : Q(Type u)} (bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q(Bool))
+private def iCasesOr {prop : Q(Type u)} (bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q(Bool))
     (k1 k2 : (B B' : Q($prop)) → (_ : $B =Q iprop(□?$p $B')) → ProofModeM Q($P ∗ $B ⊢ $Q)) :
     ProofModeM (Q($P ∗ □?$p $A' ⊢ $Q)) := do
   let A1 ← mkFreshExprMVarQ q($prop)
@@ -124,14 +142,7 @@ def iCasesOr {prop : Q(Type u)} (bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q(Bo
   let pf2 ← k2 A2' A2 ⟨⟩
   return q(or_elim' (A := $A') $pf1 $pf2)
 
-private theorem intuitionistic_elim_spatial [BI PROP] {A A' Q : PROP}
-    [IntoPersistently false A A'] [TCOr (Affine A) (Absorbing Q)]
-    (h : P ∗ □ A' ⊢ Q) : P ∗ A ⊢ Q := (replaces_r to_persistent_spatial).apply h
-
-private theorem intuitionistic_elim_intuitionistic [BI PROP] {A A' Q : PROP} [IntoPersistently true A A']
-    (h : P ∗ □ A' ⊢ Q) : P ∗ □ A ⊢ Q := intuitionistic_elim_spatial h
-
-def iCasesIntuitionistic {prop : Q(Type u)} (_bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q(Bool))
+private def iCasesIntuitionistic {prop : Q(Type u)} (_bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q(Bool))
     (k : (B' : Q($prop)) → ProofModeM Q($P ∗ □ $B' ⊢ $Q)) :
     ProofModeM (Q($P ∗ □?$p $A' ⊢ $Q)) := do
   let B' ← mkFreshExprMVarQ q($prop)
@@ -145,11 +156,7 @@ def iCasesIntuitionistic {prop : Q(Type u)} (_bi : Q(BI $prop)) (P Q A' : Q($pro
       | throwError "icases: {A'} not affine and the goal not absorbing"
     return q(intuitionistic_elim_spatial (A := $A') $(← k B'))
 
-private theorem spatial_elim [BI PROP] {p} {A A' Q : PROP} [FromAffinely A' A p]
-    (h : P ∗ A' ⊢ Q) : P ∗ □?p A ⊢ Q :=
-      (sep_mono_r <| (affinelyIf_of_intuitionisticallyIf).trans from_affinely).trans h
-
-def iCasesSpatial {prop : Q(Type u)} (_bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q(Bool))
+private def iCasesSpatial {prop : Q(Type u)} (_bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q(Bool))
     (k : (B' : Q($prop)) → ProofModeM Q($P ∗ $B' ⊢ $Q)) :
     ProofModeM (Q($P ∗ □?$p $A' ⊢ $Q)) := do
   let B' ← mkFreshExprMVarQ q($prop)
@@ -157,8 +164,6 @@ def iCasesSpatial {prop : Q(Type u)} (_bi : Q(BI $prop)) (P Q A' : Q($prop)) (p
   let _ ← ProofModeM.synthInstanceQ q(FromAffinely $B' $A' $p)
   return q(spatial_elim (A := $A') $(← k B'))
 
-private theorem of_emp_sep [BI PROP] {A Q : PROP} (h : A ⊢ Q) : emp ∗ A ⊢ Q := emp_sep.1.trans h
-
 -- TODO: Why does this function require both A and A' instead of just A'?
 variable {u : Level} {prop : Q(Type u)} (bi : Q(BI $prop)) in
 partial def iCasesCore
diff --git a/src/Iris/ProofMode/Tactics/Clear.lean b/src/Iris/ProofMode/Tactics/Clear.lean
index 6b339533d..0afb4dd87 100644
--- a/src/Iris/ProofMode/Tactics/Clear.lean
+++ b/src/Iris/ProofMode/Tactics/Clear.lean
@@ -3,18 +3,27 @@ Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lars König, Mario Carneiro, Michael Sammler
 -/
-import Iris.ProofMode.Tactics.Basic
+module
+
+import Iris.BI
+import Iris.ProofMode.Classes
+public meta import Iris.ProofMode.Tactics.Basic
 
 namespace Iris.ProofMode
-open Lean Elab Tactic Meta Qq BI Std
 
-private theorem clear_spatial [BI PROP] {P P' A Q : PROP} [TCOr (Affine A) (Absorbing Q)]
+public section
+open BI Std
+
+theorem clear_spatial [BI PROP] {P P' A Q : PROP} [TCOr (Affine A) (Absorbing Q)]
     (h_rem : P ⊣⊢ P' ∗ A) (h : P' ⊢ Q) : P ⊢ Q :=
   h_rem.1.trans <| (sep_mono_l h).trans sep_elim_l
 
-private theorem clear_intuitionistic [BI PROP] {P P' A Q : PROP}
+theorem clear_intuitionistic [BI PROP] {P P' A Q : PROP}
     (h_rem : P ⊣⊢ P' ∗ □ A) (h : P' ⊢ Q) : P ⊢ Q := clear_spatial h_rem h
 
+public meta section
+open Lean Elab Tactic Meta Qq
+
 def iClearCore {prop : Q(Type u)} (_bi : Q(BI $prop)) (e e' : Q($prop))
     (p : Q(Bool)) (out goal : Q($prop))
     (pf : Q($e ⊣⊢ $e' ∗ □?$p $out)) : ProofModeM Q(($e' ⊢ $goal) → $e ⊢ $goal) := do
diff --git a/src/Iris/ProofMode/Tactics/ExFalso.lean b/src/Iris/ProofMode/Tactics/ExFalso.lean
index 3d0ab97d6..1b819e9b8 100644
--- a/src/Iris/ProofMode/Tactics/ExFalso.lean
+++ b/src/Iris/ProofMode/Tactics/ExFalso.lean
@@ -3,12 +3,20 @@ Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lars König, Mario Carneiro, Michael Sammler
 -/
-import Iris.ProofMode.Tactics.Basic
+module
+
+import Iris.BI
+public meta import Iris.ProofMode.Tactics.Basic
 
 namespace Iris.ProofMode
-open Lean Elab.Tactic Meta Qq BI
 
-private theorem exfalso [BI PROP] {P Q : PROP} (h : P ⊢ False) : P ⊢ Q := h.trans false_elim
+public section
+open BI
+
+theorem exfalso [BI PROP] {P Q : PROP} (h : P ⊢ False) : P ⊢ Q := h.trans false_elim
+
+public meta section
+open Lean Elab.Tactic Meta Qq
 
 elab "iexfalso" : tactic => do
   ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
diff --git a/src/Iris/ProofMode/Tactics/Exact.lean b/src/Iris/ProofMode/Tactics/Exact.lean
index 7cdc3d74f..01424f5ce 100644
--- a/src/Iris/ProofMode/Tactics/Exact.lean
+++ b/src/Iris/ProofMode/Tactics/Exact.lean
@@ -3,10 +3,13 @@ Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lars König, Mario Carneiro, Michael Sammler
 -/
-import Iris.ProofMode.Tactics.Basic
-import Iris.ProofMode.Tactics.Assumption
+module
+
+public meta import Iris.ProofMode.Tactics.Assumption
 
 namespace Iris.ProofMode
+
+public meta section
 open Lean Elab Tactic Meta Qq BI Std
 
 elab "iexact" colGt hyp:ident : tactic => do
diff --git a/src/Iris/ProofMode/Tactics/Exists.lean b/src/Iris/ProofMode/Tactics/Exists.lean
index 9c8a5594b..80512ad49 100644
--- a/src/Iris/ProofMode/Tactics/Exists.lean
+++ b/src/Iris/ProofMode/Tactics/Exists.lean
@@ -3,15 +3,24 @@ Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lars König, Mario Carneiro, Michael Sammler
 -/
-import Iris.ProofMode.Tactics.Basic
+module
+
+import Iris.BI
+import Iris.ProofMode.Classes
+public meta import Iris.ProofMode.Tactics.Basic
 
 namespace Iris.ProofMode
-open Lean Elab Tactic Meta Qq BI
 
-private theorem exists_intro' [BI PROP] {Φ : α → PROP} {P Q : PROP} [inst : FromExists P Φ]
+public section
+open BI
+
+theorem exists_intro' [BI PROP] {Φ : α → PROP} {P Q : PROP} [inst : FromExists P Φ]
     (a : α) (h : P ⊢ Q) : Φ a ⊢ Q :=
   ((exists_intro a).trans inst.1).trans h
 
+public meta section
+open Lean Elab Tactic Meta Qq
+
 elab "iexists" xs:term,+ : tactic => do
   -- resolve existential quantifier with the given argument
   ProofModeM.runTactic λ mvar { prop, e, hyps, goal, .. } => do
diff --git a/src/Iris/ProofMode/Tactics/Have.lean b/src/Iris/ProofMode/Tactics/Have.lean
index d3ec48236..ab32fdac7 100644
--- a/src/Iris/ProofMode/Tactics/Have.lean
+++ b/src/Iris/ProofMode/Tactics/Have.lean
@@ -3,20 +3,28 @@ Copyright (c) 2025 Michael Sammler. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michael Sammler
 -/
-import Iris.ProofMode.Patterns.CasesPattern
-import Iris.ProofMode.Tactics.HaveCore
-import Iris.ProofMode.Tactics.Cases
+module
+
+import Iris.BI
+public meta import Iris.ProofMode.Patterns.CasesPattern
+public meta import Iris.ProofMode.Tactics.HaveCore
+public meta import Iris.ProofMode.Tactics.Cases
 
 namespace Iris.ProofMode
-open Lean Elab Tactic Meta Qq BI Std
 
-macro "ihave" colGt pat:icasesPat " := " pmt:pmTerm : tactic => `(tactic | icases +keep $pmt with $pat)
+public section
+open BI
 
-private theorem ihave_assert [BI PROP] {A B C : PROP}
+theorem ihave_assert [BI PROP] {A B C : PROP}
   (h1 : A ∗ □ (B -∗ B) ⊢ C) : A ⊢ C :=
     (and_intro .rfl (persistently_emp_intro.trans (persistently_mono $ wand_intro emp_sep.1))).trans
       $ persistently_and_intuitionistically_sep_r.1.trans h1
 
+public meta section
+open Lean Elab Tactic Meta Qq
+
+macro "ihave" colGt pat:icasesPat " := " pmt:pmTerm : tactic => `(tactic | icases +keep $pmt with $pat)
+
 elab "ihave" colGt pat:icasesPat " : " P:term "$$" spat:specPat : tactic => do
   let spat ← liftMacroM <| SpecPat.parse spat
   let pat ← liftMacroM <| iCasesPat.parse pat
diff --git a/src/Iris/ProofMode/Tactics/HaveCore.lean b/src/Iris/ProofMode/Tactics/HaveCore.lean
index 32817481b..9527c9418 100644
--- a/src/Iris/ProofMode/Tactics/HaveCore.lean
+++ b/src/Iris/ProofMode/Tactics/HaveCore.lean
@@ -3,9 +3,13 @@ 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
 -/
-import Iris.ProofMode.Patterns.ProofModeTerm
-import Iris.ProofMode.Tactics.Basic
-import Iris.ProofMode.Tactics.Specialize
+module
+
+import Iris.BI
+import Iris.ProofMode.Classes
+public meta import Iris.ProofMode.Patterns.ProofModeTerm
+public meta import Iris.ProofMode.Tactics.Basic
+public meta import Iris.ProofMode.Tactics.Specialize
 
 /- This file contains the `iHave` function for asserting a ProofModeTerm.
    It is separate from the implementation of `ihave` in `Have.lean` since
@@ -13,13 +17,19 @@ import Iris.ProofMode.Tactics.Specialize
    depends on `iHave` in this file.
 -/
 
+
 namespace Iris.ProofMode
-open Lean Elab Tactic Meta Qq BI Std
 
-private theorem have_asEmpValid [BI PROP] {φ} {P Q : PROP}
+public section
+open BI
+
+theorem have_asEmpValid [BI PROP] {φ} {P Q : PROP}
     [h1 : AsEmpValid .into φ P] (h : φ) : Q ⊢ Q ∗ □ P :=
   sep_emp.2.trans (sep_mono_r $ intuitionistically_emp.2.trans (intuitionistically_mono (asEmpValid_1 _ h)))
 
+public meta section
+open Lean Elab Tactic Meta Qq Std
+
 /--
 Assert a hypothesis from either a hypothesis name or a Lean proof term `tm`.
 
diff --git a/src/Iris/ProofMode/Tactics/Intro.lean b/src/Iris/ProofMode/Tactics/Intro.lean
index 0419d8270..96afab0d4 100644
--- a/src/Iris/ProofMode/Tactics/Intro.lean
+++ b/src/Iris/ProofMode/Tactics/Intro.lean
@@ -3,26 +3,30 @@ Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lars König, Mario Carneiro, Michael Sammler
 -/
-import Iris.ProofMode.Patterns.IntroPattern
-import Iris.ProofMode.Tactics.Cases
-import Iris.ProofMode.Tactics.ModIntro
+module
+
+public meta import Iris.ProofMode.Patterns.IntroPattern
+public meta import Iris.ProofMode.Tactics.Cases
+public meta import Iris.ProofMode.Tactics.ModIntro
 
 namespace Iris.ProofMode
-open Lean Elab Tactic Meta Qq BI Std
 
-private theorem imp_intro_drop [BI PROP] {P Q A1 A2 : PROP} [inst : FromImp Q A1 A2] (h : P ⊢ A2) : P ⊢ Q :=
+public section
+open BI Std
+
+theorem imp_intro_drop [BI PROP] {P Q A1 A2 : PROP} [inst : FromImp Q A1 A2] (h : P ⊢ A2) : P ⊢ Q :=
   BI.imp_intro (and_elim_l' h) |>.trans inst.1
 
-private theorem from_forall_intro [BI PROP] {P Q : PROP} {Φ : α → PROP} [inst : FromForall Q Φ]
+theorem from_forall_intro [BI PROP] {P Q : PROP} {Φ : α → PROP} [inst : FromForall Q Φ]
     (h : ∀ a, P ⊢ Φ a) : P ⊢ Q :=
   (forall_intro h).trans inst.1
 
-private theorem imp_intro_intuitionistic [BI PROP] {P Q A1 A2 B : PROP}
+theorem imp_intro_intuitionistic [BI PROP] {P Q A1 A2 B : PROP}
     [FromImp Q A1 A2] [inst : IntoPersistently false A1 B] (h : P ∗ □ B ⊢ A2) : P ⊢ Q := by
   refine BI.imp_intro ?_ |>.trans from_imp
   exact (and_mono_r inst.1).trans <| persistently_and_intuitionistically_sep_r.1.trans h
 
-private theorem wand_intro_intuitionistic [BI PROP] {P Q A1 A2 B : PROP}
+theorem wand_intro_intuitionistic [BI PROP] {P Q A1 A2 B : PROP}
     [FromWand Q A1 A2] [inst : IntoPersistently false A1 B] [or : TCOr (Affine A1) (Absorbing A2)]
     (h : P ∗ □ B ⊢ A2) : P ⊢ Q := by
   refine (wand_intro ?_).trans from_wand
@@ -31,7 +35,7 @@ private theorem wand_intro_intuitionistic [BI PROP] {P Q A1 A2 B : PROP}
   | TCOr.r => (sep_mono_r <| inst.1.trans absorbingly_intuitionistically.2).trans <|
       absorbingly_sep_r.1.trans <| (absorbingly_mono h).trans absorbing
 
-private theorem imp_intro_spatial [BI PROP] {P Q A1 A2 B : PROP}
+theorem imp_intro_spatial [BI PROP] {P Q A1 A2 B : PROP}
     [FromImp Q A1 A2] [inst : FromAffinely B A1] [or : TCOr (Persistent A1) (Intuitionistic P)]
     (h : P ∗ B ⊢ A2) : P ⊢ Q := by
   refine (BI.imp_intro ?_).trans from_imp
@@ -42,10 +46,13 @@ private theorem imp_intro_spatial [BI PROP] {P Q A1 A2 B : PROP}
     (and_mono_l u.1).trans <| affinely_and_lr.1.trans <|
     persistently_and_intuitionistically_sep_l.1.trans <| sep_mono_l intuitionistically_elim
 
-private theorem wand_intro_spatial [BI PROP] {P Q A1 A2 : PROP}
+theorem wand_intro_spatial [BI PROP] {P Q A1 A2 : PROP}
     [FromWand Q A1 A2] (h : P ∗ A1 ⊢ A2) : P ⊢ Q := (wand_intro h).trans from_wand
 
-partial def iIntroCore {prop : Q(Type u)} {bi : Q(BI $prop)}
+public meta section
+open Lean Elab Tactic Meta Qq BI Std
+
+private partial def iIntroCore {prop : Q(Type u)} {bi : Q(BI $prop)}
     {P} (hyps : Hyps bi P) (Q : Q($prop)) (pats : List (Syntax × IntroPat)) :
     ProofModeM (Q($P ⊢ $Q)) := do
   match pats with
diff --git a/src/Iris/ProofMode/Tactics/LeftRight.lean b/src/Iris/ProofMode/Tactics/LeftRight.lean
index 49985aa1e..f20778975 100644
--- a/src/Iris/ProofMode/Tactics/LeftRight.lean
+++ b/src/Iris/ProofMode/Tactics/LeftRight.lean
@@ -3,15 +3,28 @@ Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lars König, Mario Carneiro, Michael Sammler
 -/
-import Iris.ProofMode.Tactics.Basic
+module
+
+import Iris.BI
+import Iris.ProofMode.Classes
+public meta import Iris.ProofMode.Tactics.Basic
 
 namespace Iris.ProofMode
-open Lean Elab.Tactic Meta Qq BI Std
 
-private theorem from_or_l [BI PROP] {P Q A1 A2 : PROP} [inst : FromOr Q A1 A2]
+public section
+open BI
+
+theorem from_or_l [BI PROP] {P Q A1 A2 : PROP} [inst : FromOr Q A1 A2]
     (h1 : P ⊢ A1) : P ⊢ Q :=
   (or_intro_l' h1).trans inst.1
 
+theorem from_or_r [BI PROP] {P Q A1 A2 : PROP} [inst : FromOr Q A1 A2]
+    (h1 : P ⊢ A2) : P ⊢ Q :=
+  (or_intro_r' h1).trans inst.1
+
+public meta section
+open Lean Elab.Tactic Meta Qq Std
+
 elab "ileft" : tactic => do
   ProofModeM.runTactic λ mvar { prop, e, hyps, goal, .. } => do
   -- choose left side of disjunction
@@ -23,10 +36,6 @@ elab "ileft" : tactic => do
   let m : Q($e ⊢ $A1) ← addBIGoal hyps A1
   mvar.assign q(from_or_l (Q := $goal) $m)
 
-private theorem from_or_r [BI PROP] {P Q A1 A2 : PROP} [inst : FromOr Q A1 A2]
-    (h1 : P ⊢ A2) : P ⊢ Q :=
-  (or_intro_r' h1).trans inst.1
-
 elab "iright" : tactic => do
   ProofModeM.runTactic λ mvar { prop, e, hyps, goal, .. } => do
   -- choose right side of disjunction
diff --git a/src/Iris/ProofMode/Tactics/Mod.lean b/src/Iris/ProofMode/Tactics/Mod.lean
index b70f9d649..a0083f025 100644
--- a/src/Iris/ProofMode/Tactics/Mod.lean
+++ b/src/Iris/ProofMode/Tactics/Mod.lean
@@ -3,15 +3,24 @@ Copyright (c) 2026 Michael Sammler. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michael Sammler
 -/
-import Iris.ProofMode.Tactics.Basic
+module
+
+import Iris.BI
+public import Iris.ProofMode.Classes
+public meta import Iris.ProofMode.Tactics.Basic
 
 namespace Iris.ProofMode
-open Lean Elab Tactic Meta Qq BI Std
 
-private theorem mod [BI PROP] {e} {Φ} {p p'} {A A' Q Q' : PROP} [he : ElimModal Φ p p' A A' Q Q']
+public section
+open BI
+
+theorem mod [BI PROP] {e} {Φ} {p p'} {A A' Q Q' : PROP} [he : ElimModal Φ p p' A A' Q Q']
   (h1 : e ∗ □?p' A' ⊢ Q') (hΦ : Φ) : e ∗ □?p A ⊢ Q :=
     (sep_comm.1.trans (sep_mono_r (wand_intro h1))).trans (he.1 hΦ)
 
+public meta section
+open Lean Elab Tactic Meta Qq Std
+
 /--
 Eliminate a modality from `A` by transforming the goal from `P ∗ □?p A ⊢ Q` to `P ∗ □?p' A' ⊢ Q'`,
 where `p'`, `A'`, and `Q'` are determined by `ElimModal`.
diff --git a/src/Iris/ProofMode/Tactics/ModIntro.lean b/src/Iris/ProofMode/Tactics/ModIntro.lean
index e5b3c43a5..efb633874 100644
--- a/src/Iris/ProofMode/Tactics/ModIntro.lean
+++ b/src/Iris/ProofMode/Tactics/ModIntro.lean
@@ -3,44 +3,37 @@ Copyright (c) 2026 Michael Sammler. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michael Sammler
 -/
-import Iris.ProofMode.Tactics.Basic
+module
+
 import Iris.ProofMode.Modalities
+public meta import Iris.ProofMode.Tactics.Basic
 
 namespace Iris.ProofMode
-open Lean Elab Tactic Meta Qq BI Std
+
+public section
+open Qq BI Std
 
 /-- Reified version of ModalityAction -/
-private inductive ModalityActionQ (PROP1 : Q(Type u)) (PROP2 : Q(Type u)) : Type where
+inductive ModalityActionQ (PROP1 : Q(Type u)) (PROP2 : Q(Type u)) : Type where
 | isEmpty
 | forall (C : Q($PROP1 → Prop))
 | transform (C : Q($PROP2 → $PROP1 → Prop))
 | clear
 | id
 
-private def ModalityActionQ.parse {prop1 prop2 : Q(Type u)} (act : Q(ModalityAction $prop1 $prop2)) :
-  ProofModeM (ModalityActionQ prop1 prop2) := do
-  let act ← whnf q($act)
-  match_expr act with
-  | ModalityAction.isEmpty _ _ => return .isEmpty
-  | ModalityAction.forall _ C => return .forall C
-  | ModalityAction.transform _ _ C => return .transform C
-  | ModalityAction.clear _ _ => return .clear
-  | ModalityAction.id _ => return .id
-  | _ => throwError "imodintro: unknown modality action {act}"
-
-private theorem modaction_forall [BI PROP] {p P} (M : Modality PROP PROP) {C} (h : M.action p = .forall C) (hC : C P)
+theorem modaction_forall [BI PROP] {p P} (M : Modality PROP PROP) {C} (h : M.action p = .forall C) (hC : C P)
   : □?p P ⊢ M.M iprop(□?p P) := by
     have hs := M.spec p
     rw [h] at hs
     apply (hs _ hC)
 
-private theorem modaction_transform [BI PROP1] [BI PROP2] {p P Q} (M : Modality PROP1 PROP2) {C} (h : M.action p = .transform C) (hC : C P Q)
+theorem modaction_transform [BI PROP1] [BI PROP2] {p P Q} (M : Modality PROP1 PROP2) {C} (h : M.action p = .transform C) (hC : C P Q)
   : □?p P ⊢ M.M iprop(□?p Q) := by
     have hs := M.spec p
     rw [h] at hs
     apply (hs _ _ hC)
 
-private theorem modaction_clear [BI PROP1] [BI PROP2] {p P} (M : Modality PROP1 PROP2) (h : M.action p = .clear)
+theorem modaction_clear [BI PROP1] [BI PROP2] {p P} (M : Modality PROP1 PROP2) (h : M.action p = .clear)
   : □?p P ⊢ M.M emp :=
   match p, h  with
   | true, _ => affine.trans M.emp
@@ -49,22 +42,38 @@ private theorem modaction_clear [BI PROP1] [BI PROP2] {p P} (M : Modality PROP1
     simp [h] at hs
     apply Entails.trans (sep_emp.2.trans (sep_mono true_intro M.emp)) absorbing
 
-private theorem modaction_id [BI PROP] {p P} (M : Modality PROP PROP) (h : M.action p = .id)
+theorem modaction_id [BI PROP] {p P} (M : Modality PROP PROP) (h : M.action p = .id)
   : □?p P ⊢ M.M iprop(□?p P) := by
     have hs := M.spec p
     rw [h] at hs
     apply hs
 
-
-private theorem modaction_sep_emp_l [BI PROP1] [bi2: BI PROP2] {elhs erhs erhs'} {M : Modality PROP1 PROP2}
+theorem modaction_sep_emp_l [BI PROP1] [bi2: BI PROP2] {elhs erhs erhs'} {M : Modality PROP1 PROP2}
   (h1 : elhs ⊢ M.M emp) (h2 : erhs ⊢ M.M erhs') : elhs ∗ erhs ⊢ M.M iprop(erhs') := (sep_mono h1 h2).trans $ M.sep.trans (M.mono emp_sep.1)
 
-private theorem modaction_sep_emp_r [BI PROP1] [bi2: BI PROP2] {elhs elhs' erhs} {M : Modality PROP1 PROP2}
+theorem modaction_sep_emp_r [BI PROP1] [bi2: BI PROP2] {elhs elhs' erhs} {M : Modality PROP1 PROP2}
   (h1 : elhs ⊢ M.M elhs') (h2 : erhs ⊢ M.M emp) : elhs ∗ erhs ⊢ M.M iprop(elhs') := (sep_mono h1 h2).trans $ M.sep.trans (M.mono sep_emp.1)
 
-private theorem modaction_sep [BI PROP1] [bi2: BI PROP2] {elhs erhs elhs' erhs'} {M : Modality PROP1 PROP2}
+theorem modaction_sep [BI PROP1] [bi2: BI PROP2] {elhs erhs elhs' erhs'} {M : Modality PROP1 PROP2}
   (h1 : elhs ⊢ M.M elhs') (h2 : erhs ⊢ M.M erhs') : elhs ∗ erhs ⊢ M.M iprop(elhs' ∗ erhs') := (sep_mono h1 h2).trans M.sep
 
+theorem modintro [BI PROP1] [BI PROP2] {e e'} {Φ M sel} {P : PROP2} {Q : PROP1} [FromModal Φ M sel P Q]
+  (h1 : e ⊢ M.M e') (h2 : e' ⊢ Q) (hΦ : Φ) : e ⊢ P :=
+    (h1.trans (M.mono h2)).trans (from_modal sel hΦ)
+
+public meta section
+open Lean Elab Tactic Meta
+
+private def parseModalityActionQ {prop1 prop2 : Q(Type u)} (act : Q(ModalityAction $prop1 $prop2)) :
+  ProofModeM (ModalityActionQ prop1 prop2) := do
+  let act ← whnf q($act)
+  match_expr act with
+  | ModalityAction.isEmpty _ _ => return .isEmpty
+  | ModalityAction.forall _ C => return .forall C
+  | ModalityAction.transform _ _ C => return .transform C
+  | ModalityAction.clear _ _ => return .clear
+  | ModalityAction.id _ => return .id
+  | _ => throwError "imodintro: unknown modality action {act}"
 
 /--
 Applies modality actions to transform proof mode context.
@@ -125,10 +134,6 @@ private def iModAction {prop1 : Q(Type u)} {bi1 : Q(BI $prop1)} {bi2} {e}
       return ⟨_, lhs', q(modaction_sep_emp_r $pflhs $pfrhs)⟩
     return ⟨_, .mkSep lhs' rhs', q(modaction_sep $pflhs $pfrhs)⟩
 
-private theorem modintro [BI PROP1] [BI PROP2] {e e'} {Φ M sel} {P : PROP2} {Q : PROP1} [FromModal Φ M sel P Q]
-  (h1 : e ⊢ M.M e') (h2 : e' ⊢ Q) (hΦ : Φ) : e ⊢ P :=
-    (h1.trans (M.mono h2)).trans (from_modal sel hΦ)
-
 /-- Introduce a modality by applying modality actions to transform hypotheses.
 
 # Parameters
@@ -157,8 +162,8 @@ def iModIntroCore {e} (hyps : @Hyps u prop bi e) (goal : Q($prop)) (sel : TSynta
     let hΦ ← mkFreshExprMVarQ q($Φ)
     iSolveSideconditionAt hΦ.mvarId!
     -- pre-compute the actions
-    let iact ← ModalityActionQ.parse q($(M).action true)
-    let sact ← ModalityActionQ.parse q($(M).action false)
+    let iact ← parseModalityActionQ q($(M).action true)
+    let sact ← parseModalityActionQ q($(M).action false)
     -- perform modality actions, get transformed context `hyps'` and `pf : hyps ⊢ M hyps'`
     let ⟨_, hyps', pf⟩ ← iModAction hyps M (λ p => if p then iact else sact)
     -- get proof `hyps' ⊢ Q`
diff --git a/src/Iris/ProofMode/Tactics/Pure.lean b/src/Iris/ProofMode/Tactics/Pure.lean
index 34c9e165e..4756b76f7 100644
--- a/src/Iris/ProofMode/Tactics/Pure.lean
+++ b/src/Iris/ProofMode/Tactics/Pure.lean
@@ -3,13 +3,17 @@ Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lars König, Mario Carneiro, Michael Sammler
 -/
-import Iris.ProofMode.Instances
-import Iris.ProofMode.Tactics.Basic
+module
+
+public import Iris.ProofMode.Instances
+public meta import Iris.ProofMode.Tactics.Basic
 
 namespace Iris.ProofMode
-open Lean Elab Tactic Meta Qq BI Std
 
-private theorem pure_elim_spatial [BI PROP] {P P' A Q : PROP} {φ : Prop}
+public section
+open BI Std
+
+theorem pure_elim_spatial [BI PROP] {P P' A Q : PROP} {φ : Prop}
     [hA : IntoPure A φ] [or : TCOr (Affine A) (Absorbing Q)]
     (h : P ⊣⊢ P' ∗ A) (h_entails : φ → P' ⊢ Q) : P ⊢ Q :=
   h.1.trans <| match or with
@@ -21,10 +25,13 @@ private theorem pure_elim_spatial [BI PROP] {P P' A Q : PROP} {φ : Prop}
     absorbingly_sep_lr.2.trans <| persistent_and_affinely_sep_r.2.trans <|
     pure_elim_r fun hφ => (absorbingly_mono <| h_entails hφ).trans absorbing
 
-private theorem pure_elim_intuitionistic [BI PROP] {P P' A Q : PROP} {φ : Prop}
+theorem pure_elim_intuitionistic [BI PROP] {P P' A Q : PROP} {φ : Prop}
     [IntoPure A φ] (h : P ⊣⊢ P' ∗ □ A) (h' : φ → P' ⊢ Q) : P ⊢ Q :=
   pure_elim_spatial h h'
 
+public meta section
+open Lean Elab Tactic Meta Qq
+
 def iPureCore {prop : Q(Type u)} (_bi : Q(BI $prop))
     (P P' : Q($prop)) (p : Q(Bool)) (A Q : Q($prop)) (name : TSyntax ``binderIdent) (pf : Q($P ⊣⊢ $P' ∗ □?$p $A))
     (k : (φ : Q(Prop)) → Q($φ) → ProofModeM (Q($P' ⊢ $Q))) : ProofModeM (Q($P ⊢ $Q)) := do
@@ -64,11 +71,11 @@ elab "iemp_intro" : tactic => do
     | throwError "iemp_intro: context is not affine"
   mvar.assign q(affine (P := $e))
 
-private theorem pure_intro_affine [BI PROP] {Q : PROP} {φ : Prop}
+theorem pure_intro_affine [BI PROP] {Q : PROP} {φ : Prop}
     [h : FromPure true Q φ] [Affine P] (hφ : φ) : P ⊢ Q :=
   (affine.trans (eq_true hφ ▸ affinely_true.2)).trans h.1
 
-private theorem pure_intro_spatial [BI PROP] {Q : PROP} {φ : Prop}
+theorem pure_intro_spatial [BI PROP] {Q : PROP} {φ : Prop}
     [h : FromPure false Q φ] (hφ : φ) : P ⊢ Q :=
   (pure_intro hφ).trans h.1
 
diff --git a/src/Iris/ProofMode/Tactics/Rename.lean b/src/Iris/ProofMode/Tactics/Rename.lean
index c29bf7cc0..ddb601ab4 100644
--- a/src/Iris/ProofMode/Tactics/Rename.lean
+++ b/src/Iris/ProofMode/Tactics/Rename.lean
@@ -3,9 +3,13 @@ Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lars König, Mario Carneiro, Michael Sammler
 -/
-import Iris.ProofMode.Tactics.Basic
+module
+
+public meta import Iris.ProofMode.Tactics.Basic
 
 namespace Iris.ProofMode
+
+public meta section
 open Lean Elab Tactic Qq
 
 elab "irename" colGt nameFrom:ident " => " colGt nameTo:ident : tactic => do
diff --git a/src/Iris/ProofMode/Tactics/Specialize.lean b/src/Iris/ProofMode/Tactics/Specialize.lean
index 862bdb229..6c20199d4 100644
--- a/src/Iris/ProofMode/Tactics/Specialize.lean
+++ b/src/Iris/ProofMode/Tactics/Specialize.lean
@@ -3,18 +3,18 @@ Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lars König, Mario Carneiro, Michael Sammler
 -/
-import Iris.ProofMode.Patterns.ProofModeTerm
-import Iris.ProofMode.Patterns.CasesPattern
-import Iris.ProofMode.Tactics.Basic
+module
+
+public meta import Iris.ProofMode.Patterns.ProofModeTerm
+public meta import Iris.ProofMode.Patterns.CasesPattern
+public meta import Iris.ProofMode.Tactics.Basic
 
 namespace Iris.ProofMode
-open Lean Elab Tactic Meta Qq BI Std
 
-private structure SpecializeState {prop : Q(Type u)} (bi : Q(BI $prop)) (orig : Q($prop)) where
-  (e : Q($prop)) (hyps : Hyps bi e) (p : Q(Bool)) (out : Q($prop))
-  pf : Q($orig ⊢ $e ∗ □?$p $out)
+public section
+open BI
 
-private theorem specialize_wand [BI PROP] {q p : Bool} {A1 A2 A3 Q P1 P2 : PROP}
+theorem specialize_wand [BI PROP] {q p : Bool} {A1 A2 A3 Q P1 P2 : PROP}
     (h1 : A1 ⊢ A2 ∗ □?q Q) (h2 : A2 ⊣⊢ A3 ∗ □?p P1)
     [h3 : IntoWand q p Q .in P1 .out P2] :
     A1 ⊢ A3 ∗ □?(p && q) P2 := by
@@ -27,17 +27,34 @@ private theorem specialize_wand [BI PROP] {q p : Bool} {A1 A2 A3 Q P1 P2 : PROP}
 
 -- TODO: if q is true and A1 is persistent, this proof can guarantee □ P2 instead of P2
 -- see https://gitlab.mpi-sws.org/iris/iris/-/blob/846ed45bed6951035c6204fef365d9a344022ae6/iris/proofmode/coq_tactics.v#L336
-private theorem specialize_wand_subgoal [BI PROP] {q : Bool} {A1 A2 A3 A4 Q P1 : PROP} P2
+theorem specialize_wand_subgoal [BI PROP] {q : Bool} {A1 A2 A3 A4 Q P1 : PROP} P2
     (h1 : A1 ⊢ A2 ∗ □?q Q) (h2 : A2 ⊣⊢ A3 ∗ A4) (h3 : A4 ⊢ P1)
     [inst : IntoWand q false Q .out P1 .out P2] : A1 ⊢ A3 ∗ P2 := by
   refine h1.trans <| (sep_mono_l h2.1).trans <| sep_assoc.1.trans (sep_mono_r ((sep_mono_l h3).trans ?_))
   exact (sep_mono_r inst.1).trans wand_elim_r
 
-private theorem specialize_forall [BI PROP] {p : Bool} {A1 A2 P : PROP} {α : Sort _} {Φ : α → PROP}
+theorem specialize_forall [BI PROP] {p : Bool} {A1 A2 P : PROP} {α : Sort _} {Φ : α → PROP}
     [inst : IntoForall P Φ] (h : A1 ⊢ A2 ∗ □?p P) (a : α) : A1 ⊢ A2 ∗ □?p (Φ a) := by
   refine h.trans <| sep_mono_r <| intuitionisticallyIf_mono <| inst.1.trans (forall_elim a)
 
-private def SpecializeState.process_wand :
+theorem specialize_dup_context [BI PROP] {P : PROP} {pa A P' pb B}
+  (h : P ∗ □?pa A ⊢ P' ∗ □?pb B)
+  (h2 : pa = true ∨ Affine A)
+  [IntoPersistently pb B B']
+  : P ∗ □?pa A ⊢ P ∗ □ B' := by
+    apply Entails.trans _ persistently_and_intuitionistically_sep_r.1
+    apply and_intro
+    · cases h2 <;> subst_eqs <;> apply sep_elim_l
+    · apply h.trans $ (sep_mono_r (persistentlyIf_of_intuitionisticallyIf.trans into_persistently)).trans sep_elim_r
+
+public meta section
+open Lean Elab Tactic Meta Qq Std
+
+structure SpecializeState {prop : Q(Type u)} (bi : Q(BI $prop)) (orig : Q($prop)) where
+  (e : Q($prop)) (hyps : Hyps bi e) (p : Q(Bool)) (out : Q($prop))
+  pf : Q($orig ⊢ $e ∗ □?$p $out)
+
+private def processWand :
     @SpecializeState u prop bi orig → SpecPat → ProofModeM (SpecializeState bi orig)
   | { hyps, p, out, pf, .. }, .ident i => do
     let uniq ← hyps.findWithInfo i
@@ -87,16 +104,6 @@ def iCasesPat.should_try_dup_context (pat : iCasesPat) : Bool :=
   | .pure _ => true
   | _ => false
 
-private theorem specialize_dup_context [BI PROP] {P : PROP} {pa A P' pb B}
-  (h : P ∗ □?pa A ⊢ P' ∗ □?pb B)
-  (h2 : pa = true ∨ Affine A)
-  [IntoPersistently pb B B']
-  : P ∗ □?pa A ⊢ P ∗ □ B' := by
-    apply Entails.trans _ persistently_and_intuitionistically_sep_r.1
-    apply and_intro
-    · cases h2 <;> subst_eqs <;> apply sep_elim_l
-    · apply h.trans $ (sep_mono_r (persistentlyIf_of_intuitionisticallyIf.trans into_persistently)).trans sep_elim_r
-
 /-- Specialize a proposition `A` by applying a sequence of specialization patterns.
 
 ## Parameters
@@ -116,7 +123,7 @@ A tuple containing:
 def iSpecializeCore {e} (hyps : @Hyps u prop bi e) (pa : Q(Bool)) (A : Q($prop)) (spats : List SpecPat) (try_dup_context : Bool := false) :
   ProofModeM ((e' : _) × Hyps bi e' × (pb : Q(Bool)) × (B : Q($prop)) × Q($e ∗ □?$pa $A ⊢ $e' ∗ □?$pb $B)) := do
   let state := { hyps, out := A, p := pa, pf := q(.rfl), .. }
-  let ⟨_, hyps', pb, B, pf⟩ ← spats.foldlM SpecializeState.process_wand state
+  let ⟨_, hyps', pb, B, pf⟩ ← spats.foldlM processWand state
   if try_dup_context then
     -- context duplication succeeds if `B` is persistent, and `A` is persistent or affine
     let B' : Q($prop) ← mkFreshExprMVarQ q($prop)
diff --git a/src/Iris/ProofMode/Tactics/Split.lean b/src/Iris/ProofMode/Tactics/Split.lean
index 3fcb23eaf..c7fdbf113 100644
--- a/src/Iris/ProofMode/Tactics/Split.lean
+++ b/src/Iris/ProofMode/Tactics/Split.lean
@@ -3,15 +3,28 @@ Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lars König, Mario Carneiro, Michael Sammler
 -/
-import Iris.ProofMode.Tactics.Basic
+module
+
+import Iris.BI
+import Iris.ProofMode.Classes
+public meta import Iris.ProofMode.Tactics.Basic
 
 namespace Iris.ProofMode
-open Lean Elab Tactic Meta Qq BI
 
-private theorem from_and_intro [BI PROP] {P Q A1 A2 : PROP} [inst : FromAnd Q A1 A2]
+public section
+open BI
+
+theorem from_and_intro [BI PROP] {P Q A1 A2 : PROP} [inst : FromAnd Q A1 A2]
     (h1 : P ⊢ A1) (h2 : P ⊢ A2) : P ⊢ Q :=
   (and_intro h1 h2).trans inst.1
 
+theorem sep_split [BI PROP] {P P1 P2 Q Q1 Q2 : PROP} [inst : FromSep Q Q1 Q2]
+    (h : P ⊣⊢ P1 ∗ P2) (h1 : P1 ⊢ Q1) (h2 : P2 ⊢ Q2) : P ⊢ Q :=
+  h.1.trans <| (sep_mono h1 h2).trans inst.1
+
+public meta section
+open Lean Elab Tactic Meta Qq
+
 elab "isplit" : tactic => do
   ProofModeM.runTactic λ mvar { prop, hyps, goal, .. } => do
 
@@ -22,14 +35,10 @@ elab "isplit" : tactic => do
   let m2 ← addBIGoal hyps A2
   mvar.assign q(from_and_intro (Q := $goal) $m1 $m2)
 
-private theorem sep_split [BI PROP] {P P1 P2 Q Q1 Q2 : PROP} [inst : FromSep Q Q1 Q2]
-    (h : P ⊣⊢ P1 ∗ P2) (h1 : P1 ⊢ Q1) (h2 : P2 ⊢ Q2) : P ⊢ Q :=
-  h.1.trans <| (sep_mono h1 h2).trans inst.1
-
 inductive splitSide where
 | splitLeft | splitRight
 
-def isplitCore (side : splitSide) (names : Array (TSyntax `ident)) : TacticM Unit := do
+private def isplitCore (side : splitSide) (names : Array (TSyntax `ident)) : TacticM Unit := do
   let splitRight := match side with
     | .splitLeft => false
     | .splitRight => true
diff --git a/src/Iris/ProofMode/UnifHints.lean b/src/Iris/ProofMode/UnifHints.lean
index 58cf0ef0b..f3a5fa1b7 100644
--- a/src/Iris/ProofMode/UnifHints.lean
+++ b/src/Iris/ProofMode/UnifHints.lean
@@ -3,7 +3,11 @@ 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
 -/
-import Iris.BI
+module
+
+public import Iris.BI
+
+@[expose] public section
 
 namespace Iris.ProofMode
 open Iris.BI
diff --git a/src/Iris/Std.lean b/src/Iris/Std.lean
index 13967d062..6539947bf 100644
--- a/src/Iris/Std.lean
+++ b/src/Iris/Std.lean
@@ -1,11 +1,13 @@
-import Iris.Std.Classes
-import Iris.Std.Expr
-import Iris.Std.HeapInstances
-import Iris.Std.Infinite
-import Iris.Std.Nat
-import Iris.Std.Prod
-import Iris.Std.Qq
-import Iris.Std.Rewrite
-import Iris.Std.Tactic
-import Iris.Std.TC
-import Iris.Std.Try
+module
+
+public import Iris.Std.Classes
+public import Iris.Std.Expr
+public import Iris.Std.HeapInstances
+public import Iris.Std.Infinite
+public import Iris.Std.Nat
+public import Iris.Std.Prod
+public import Iris.Std.Qq
+public import Iris.Std.Rewrite
+public import Iris.Std.Tactic
+public import Iris.Std.TC
+public import Iris.Std.Try
diff --git a/src/Iris/Std/BigOp.lean b/src/Iris/Std/BigOp.lean
index d28518cf3..17eea983f 100644
--- a/src/Iris/Std/BigOp.lean
+++ b/src/Iris/Std/BigOp.lean
@@ -3,6 +3,9 @@ Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lars König, Mario Carneiro
 -/
+module
+
+@[expose] public section
 
 namespace Iris.Std
 
diff --git a/src/Iris/Std/Classes.lean b/src/Iris/Std/Classes.lean
index a2e88a817..e91c724cb 100644
--- a/src/Iris/Std/Classes.lean
+++ b/src/Iris/Std/Classes.lean
@@ -3,6 +3,10 @@ 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
 -/
+module
+
+@[expose] public section
+
 namespace Iris.Std
 
 /-- Represents a binary relation with two arguments of the same type `α`. -/
diff --git a/src/Iris/Std/DelabRule.lean b/src/Iris/Std/DelabRule.lean
index aef1a2056..f27dbe9bb 100644
--- a/src/Iris/Std/DelabRule.lean
+++ b/src/Iris/Std/DelabRule.lean
@@ -3,14 +3,19 @@ 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
 -/
-import Lean.PrettyPrinter.Delaborator
+module
+
+public meta import Lean.PrettyPrinter.Delaborator
+public meta import Lean.Parser.Term
+
+public meta section
 
 namespace Iris.Std
 open Lean Lean.Macro
 
 -- macro for adding unexpanders for function applications
 open Lean.Parser.Term in
-private def matchAlts' := leading_parser matchAlts
+def matchAlts' := leading_parser matchAlts
 
 syntax "delab_rule" ident matchAlts' : command
 macro_rules
@@ -24,10 +29,10 @@ macro_rules
 
     if p.any fun t : TSyntax _ ↦ t matches `(`($$_)) then
       `(@[app_unexpander $(mkIdent f)]
-        def unexpand : Lean.PrettyPrinter.Unexpander
+        meta def unexpand : Lean.PrettyPrinter.Unexpander
           $[| $p => $s]*)
     else
       `(@[app_unexpander $(mkIdent f)]
-        def unexpand : Lean.PrettyPrinter.Unexpander
+        meta def unexpand : Lean.PrettyPrinter.Unexpander
           $[| $p => $s]*
           | _ => throw ())
diff --git a/src/Iris/Std/Equivalence.lean b/src/Iris/Std/Equivalence.lean
index c993fdf49..878b8b8ea 100644
--- a/src/Iris/Std/Equivalence.lean
+++ b/src/Iris/Std/Equivalence.lean
@@ -3,5 +3,8 @@ Copyright (c) 2023 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
+module
+
+@[expose] public section
 
 theorem equivalence_eq : Equivalence (@Eq α) := ⟨.refl, .symm, .trans⟩
diff --git a/src/Iris/Std/Expr.lean b/src/Iris/Std/Expr.lean
index 52757c398..defa01aa1 100644
--- a/src/Iris/Std/Expr.lean
+++ b/src/Iris/Std/Expr.lean
@@ -3,8 +3,12 @@ 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
 -/
-import Lean.Expr
-import Lean.Meta
+module
+
+public import Lean.Expr
+public import Lean.Meta
+
+@[expose] public section
 
 namespace Lean.Expr
 open Lean.Meta
diff --git a/src/Iris/Std/FromMathlib.lean b/src/Iris/Std/FromMathlib.lean
index acda13174..71d5f7724 100644
--- a/src/Iris/Std/FromMathlib.lean
+++ b/src/Iris/Std/FromMathlib.lean
@@ -2,6 +2,9 @@
 Copyright (c) 2026 Zongyuan Liu, Markus de Medeiros. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
+module
+
+@[expose] public section
 
 namespace FromMathlib
 
diff --git a/src/Iris/Std/HeapInstances.lean b/src/Iris/Std/HeapInstances.lean
index ee725af14..54e9db292 100644
--- a/src/Iris/Std/HeapInstances.lean
+++ b/src/Iris/Std/HeapInstances.lean
@@ -3,11 +3,12 @@ Copyright (c) 2025 Alok Singh. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alok Singh, Markus de Medeiros
 -/
+module
 
-import Iris.Std.PartialMap
-import Iris.Std.Infinite
-import Std.Data.TreeMap
-import Std.Data.ExtTreeMap
+public import Iris.Std.PartialMap
+public import Iris.Std.Infinite
+public import Std.Data.TreeMap
+public import Std.Data.ExtTreeMap
 
 /-!
 # Heap Instances for Standard Types
@@ -24,6 +25,8 @@ instances for types from the Lean standard library.
 - `ExtTreeMap`: `PartialMap`
 -/
 
+@[expose] public section
+
 namespace Iris.Std
 
 /-! ## Function PartialMap Instance -/
diff --git a/src/Iris/Std/Infinite.lean b/src/Iris/Std/Infinite.lean
index f41dc0e68..4897b434b 100644
--- a/src/Iris/Std/Infinite.lean
+++ b/src/Iris/Std/Infinite.lean
@@ -3,6 +3,9 @@ Copyright (c) 2023 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus de Medeiros
 -/
+module
+
+@[expose] public section
 
 /-- A set S is infinite if there exists an injection from Nat into the set of elements
   such that S holds. -/
diff --git a/src/Iris/Std/Nat.lean b/src/Iris/Std/Nat.lean
index 8a7302f4c..4ea7f7a41 100644
--- a/src/Iris/Std/Nat.lean
+++ b/src/Iris/Std/Nat.lean
@@ -3,6 +3,10 @@ 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
 -/
+module
+
+@[expose] public section
+
 namespace Nat
 
 theorem eq_of_not_lt_not_lt {a b : Nat} : ¬(a < b) → ¬(b < a) → a = b := by
diff --git a/src/Iris/Std/PartialMap.lean b/src/Iris/Std/PartialMap.lean
index bb52582b3..4b7fe0630 100644
--- a/src/Iris/Std/PartialMap.lean
+++ b/src/Iris/Std/PartialMap.lean
@@ -1,11 +1,12 @@
-import Batteries.Data.List.Perm
-import Iris.Std.FromMathlib
-
 /-
 Copyright (c) 2026 Zongyuan Liu, Markus de Medeiros. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Zongyuan Liu, Markus de Medeiros
 -/
+module
+
+import Iris.Std.FromMathlib
+import Batteries.Data.List.Perm
 
 /-! ## Partial Maps
 
@@ -28,6 +29,7 @@ be unique, ie. all constructions reason extensionally about the get? function ra
 than intensionally about map equalities. PartialMaps are free to be non-uniquely
 represented.
 -/
+@[expose] public section
 namespace Iris.Std
 
 /-- Base typeclass for partial maps: maps from keys `K` to optional values `V`. -/
@@ -1043,5 +1045,4 @@ theorem toList_zip {m₁ : M V} {m₂ : M V'} :
 
 end LawfulFiniteMap
 
-
 end Iris.Std
diff --git a/src/Iris/Std/Prod.lean b/src/Iris/Std/Prod.lean
index 6a0df6fb8..5a9729e01 100644
--- a/src/Iris/Std/Prod.lean
+++ b/src/Iris/Std/Prod.lean
@@ -3,6 +3,10 @@ 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
 -/
+module
+
+@[expose] public section
+
 namespace Prod
 
 /-- Apply `f` to all elements of a tuple. All elements of the tuple must have the same type `α`. -/
diff --git a/src/Iris/Std/Qq.lean b/src/Iris/Std/Qq.lean
index c16e896da..41b962dbd 100644
--- a/src/Iris/Std/Qq.lean
+++ b/src/Iris/Std/Qq.lean
@@ -3,7 +3,11 @@ Copyright (c) 2023 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import Qq
+module
+
+public import Qq
+
+@[expose] public section
 open Qq
 
 instance : Inhabited (QuotedDefEq a b) := ⟨⟨⟩⟩
diff --git a/src/Iris/Std/Rewrite.lean b/src/Iris/Std/Rewrite.lean
index 5fa2410f3..25d2794a2 100644
--- a/src/Iris/Std/Rewrite.lean
+++ b/src/Iris/Std/Rewrite.lean
@@ -3,10 +3,14 @@ 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
 -/
-import Iris.Std.Classes
-import Iris.Std.Tactic
+module
 
-import Lean.Elab.Tactic
+public import Iris.Std.Classes
+public meta import Iris.Std.Tactic
+
+public meta import Lean.Elab.Tactic
+
+public meta section
 
 namespace Iris.Std
 open Lean Lean.Elab Lean.Elab.Tactic Lean.Meta Lean.Parser.Tactic
diff --git a/src/Iris/Std/Set.lean b/src/Iris/Std/Set.lean
index 6ec6222ef..c4f1818b8 100644
--- a/src/Iris/Std/Set.lean
+++ b/src/Iris/Std/Set.lean
@@ -3,7 +3,9 @@ Copyright (c) 2023 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus de Medeiros
 -/
+module
 
+@[expose] public section
 
 namespace Set
 
diff --git a/src/Iris/Std/TC.lean b/src/Iris/Std/TC.lean
index f55d0f416..6ce7579b1 100644
--- a/src/Iris/Std/TC.lean
+++ b/src/Iris/Std/TC.lean
@@ -3,6 +3,10 @@ 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
 -/
+module
+
+@[expose] public section
+
 namespace Iris.Std
 
 set_option checkBinderAnnotations false
diff --git a/src/Iris/Std/Tactic.lean b/src/Iris/Std/Tactic.lean
index 416e06a7e..ac69f46e8 100644
--- a/src/Iris/Std/Tactic.lean
+++ b/src/Iris/Std/Tactic.lean
@@ -3,8 +3,12 @@ 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
 -/
-import Lean.Elab.Tactic
-import Lean.Meta.Tactic.Util
+module
+
+public meta import Lean.Elab.Tactic
+public meta import Lean.Meta.Tactic.Util
+
+public meta section
 
 namespace Iris.Std
 open Lean Lean.Elab.Tactic Lean.Meta
diff --git a/src/Iris/Std/Try.lean b/src/Iris/Std/Try.lean
index 40a9494c6..5466baffd 100644
--- a/src/Iris/Std/Try.lean
+++ b/src/Iris/Std/Try.lean
@@ -3,6 +3,9 @@ Copyright (c) 2023 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
+module
+
+@[expose] public section
 
 namespace Iris.ProofMode
 
diff --git a/src/Iris/Tests.lean b/src/Iris/Tests.lean
index a5dd1ca4f..8ea520df2 100644
--- a/src/Iris/Tests.lean
+++ b/src/Iris/Tests.lean
@@ -1,3 +1,5 @@
-import Iris.Tests.Instances
-import Iris.Tests.Notation
-import Iris.Tests.Tactics
+module
+
+public import Iris.Tests.Instances
+public import Iris.Tests.Notation
+public import Iris.Tests.Tactics
diff --git a/src/Iris/Tests/Instances.lean b/src/Iris/Tests/Instances.lean
index 78dac4c0b..a23f0d491 100644
--- a/src/Iris/Tests/Instances.lean
+++ b/src/Iris/Tests/Instances.lean
@@ -3,8 +3,12 @@ Copyright (c) 2025 Michael Sammler. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michael Sammler
 -/
-import Iris.BI
-import Iris.ProofMode
+module
+
+public import Iris.BI
+public import Iris.ProofMode
+
+@[expose] public section
 
 namespace Iris.Tests
 open BI ProofMode
diff --git a/src/Iris/Tests/Notation.lean b/src/Iris/Tests/Notation.lean
index a60467191..3eb1eec2d 100644
--- a/src/Iris/Tests/Notation.lean
+++ b/src/Iris/Tests/Notation.lean
@@ -3,7 +3,11 @@ 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
 -/
-import Iris.BI.BIBase
+module
+
+public import Iris.BI.BIBase
+
+@[expose] public section
 
 namespace Iris.Tests
 open Iris.BI
diff --git a/src/Iris/Tests/Tactics.lean b/src/Iris/Tests/Tactics.lean
index ed8c26046..7ed08f415 100644
--- a/src/Iris/Tests/Tactics.lean
+++ b/src/Iris/Tests/Tactics.lean
@@ -3,8 +3,12 @@ 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, Oliver Soeser, Michael Sammler
 -/
-import Iris.BI
-import Iris.ProofMode
+module
+
+public import Iris.BI
+public import Iris.ProofMode
+
+@[expose] public section
 
 namespace Iris.Tests
 open Iris.BI