diff --git a/RandomDo/MeasurableSpaceMonad/Defs.lean b/RandomDo/MeasurableSpaceMonad/Defs.lean
index 940bce5..74d5fc8 100644
--- a/RandomDo/MeasurableSpaceMonad/Defs.lean
+++ b/RandomDo/MeasurableSpaceMonad/Defs.lean
@@ -95,6 +95,8 @@ class MeasurableSpaceFunctor (f : (α : Type u) → [MeasurableSpace α] → Typ
   mMapConst {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] : α → f β → f α :=
     mMap ∘ (const _)
 
+export MeasurableSpaceFunctor (mMap mMapConst)
+
 @[inherit_doc] scoped infixr:100 " <$>ₘ " => MeasurableSpaceFunctor.mMap
 
 /--
@@ -107,6 +109,8 @@ class MeasurableSpacePure (f : (α : Type u) → [MeasurableSpace α] → Type v
   action that does nothing and returns `a`. -/
   mPure {α : Type u} [MeasurableSpace α] : α → f α
 
+export MeasurableSpacePure (mPure)
+
 /--
 The `>>=ₘ` operator is overloaded via instances of `MeasurableSpaceBind`.
 
@@ -121,6 +125,8 @@ class MeasurableSpaceBind (m : (α : Type u) → [MeasurableSpace α] → Type v
   -/
   mBind {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] : m α → (α → m β) → m β
 
+export MeasurableSpaceBind (mBind)
+
 @[inherit_doc] scoped infixl:55  " >>=ₘ " => MeasurableSpaceBind.mBind
 
 /--
@@ -158,8 +164,6 @@ end MeasurableSpaceMonad
 
 section Lawful
 
-open MeasurableSpaceFunctor
-
 /-- A `MeasurableSpaceFunctor` satisfies the measurable space functor laws. -/
 class LawfulMeasurableSpaceFunctor
     (f : (α : Type u) → [MeasurableSpace α] → Type v) [MeasurableSpaceFunctor f]
@@ -177,7 +181,7 @@ class LawfulMeasurableSpaceFunctor
     {g₀ : α → β} {g₁ : β → γ} (x : f α) (hg₀ : Measurable g₀) (hg₁ : Measurable g₁) :
     (g₁ ∘ g₀) <$>ₘ x = g₁ <$>ₘ g₀ <$>ₘ x
 
-open LawfulMeasurableSpaceFunctor
+export LawfulMeasurableSpaceFunctor (measurable_mMap mMap_const id_mMap comp_mMap)
 
 attribute [fun_prop] measurable_mMap
 attribute [simp] id_mMap
@@ -193,8 +197,6 @@ variable {f : (α : Type u) → [MeasurableSpace α] → Type v} [MeasurableSpac
     g₁ <$>ₘ g₀ <$>ₘ x = (fun a => g₁ (g₀ a)) <$>ₘ x :=
   (comp_mMap x hg₀ hg₁).symm
 
-open MeasurableSpaceBind MeasurableSpacePure MeasurableSpaceFunctor
-
 /-- A `MeasurableSpaceMonad` satisfies the measurable space monad laws. -/
 class LawfulMeasurableSpaceMonad
     (m : (α : Type u) → [MeasurableSpace α] → Type v) [MeasurableSpaceMonad m]
@@ -227,7 +229,8 @@ class LawfulMeasurableSpaceMonad
     congr with _
     exact (mPure_mBind _ (measurable_mPure.comp h_meas)).symm)
 
-open LawfulMeasurableSpaceMonad
+export LawfulMeasurableSpaceMonad
+  (measurable_mPure measurable_mBind mBind_mPure_comp mPure_mBind mBind_assoc)
 
 attribute [fun_prop] measurable_mPure measurable_mBind
 attribute [simp] mPure_mBind mBind_assoc mBind_mPure_comp
diff --git a/RandomDo/Monad/ForInInstances.lean b/RandomDo/Monad/ForInInstances.lean
index fde7c94..9a0cfc7 100644
--- a/RandomDo/Monad/ForInInstances.lean
+++ b/RandomDo/Monad/ForInInstances.lean
@@ -48,7 +48,7 @@ end MeasurableSpace
 
 universe u v
 
-open MeasureTheory MeasurableSpacePure
+open MeasureTheory
 
 variable {α : Type u} [mα : MeasurableSpace α] {m : (α : Type u) → [MeasurableSpace α] → Type v}
 
diff --git a/RandomDo/Monad/Instances.lean b/RandomDo/Monad/Instances.lean
index e716032..04bf7c3 100644
--- a/RandomDo/Monad/Instances.lean
+++ b/RandomDo/Monad/Instances.lean
@@ -36,8 +36,6 @@ instance {m : Type u → Type v} [Monad m] :
 /-- A measurable space monad for pseudo random number generation. -/
 abbrev PseudoRandomM := Monad.toMeasurableSpaceMonad Rand
 
-open MeasurableSpacePure MeasurableSpaceBind MeasurableSpaceFunctor MeasurableSpaceMonad
-
 @[simps]
 noncomputable instance : MeasurableSpaceMonad Measure where
   mPure := Measure.dirac
diff --git a/RandomDo/Monad/Notation.lean b/RandomDo/Monad/Notation.lean
index 9b1d5f9..672bc78 100644
--- a/RandomDo/Monad/Notation.lean
+++ b/RandomDo/Monad/Notation.lean
@@ -19,7 +19,7 @@ public meta import Lean.Meta.ProdN
 
 open Lean Lean.Parser Lean.Parser.Term Lean.Meta Lean.Elab Lean.Elab.Do Lean.Elab.Term Std Meta
 
-open MeasureTheory MeasurableSpacePure MeasurableSpaceBind
+open MeasureTheory
 
 public meta section
 
diff --git a/RandomDo/Tactic/IsMarkov/Lemmas.lean b/RandomDo/Tactic/IsMarkov/Lemmas.lean
index 38cc0d0..7a496a7 100644
--- a/RandomDo/Tactic/IsMarkov/Lemmas.lean
+++ b/RandomDo/Tactic/IsMarkov/Lemmas.lean
@@ -54,7 +54,6 @@ complex program to the Markov property/measurability of its underlying mathemati
 @[expose] public section
 
 open MeasureTheory ProbabilityTheory Function
-open MeasurableSpacePure
 open scoped ENNReal
 
 namespace IsMarkov
diff --git a/Test/MonadLaws.lean b/Test/MonadLaws.lean
index 7787395..fa84ce8 100644
--- a/Test/MonadLaws.lean
+++ b/Test/MonadLaws.lean
@@ -12,8 +12,7 @@ guarded by measurability hypotheses, which is what makes the Giry monad fit the
 these tests also record the exact shape each law is stated in.
 -/
 
-open MeasureTheory ProbabilityTheory MeasurableSpacePure MeasurableSpaceBind
-  MeasurableSpaceFunctor
+open MeasureTheory ProbabilityTheory
 
 @[expose] public section