From 52afa1b0c47432755d697a7ce358380b6ca71c39 Mon Sep 17 00:00:00 2001
From: David Ledvinka <dledvinka.ledvinka@mail.utoronto.ca>
Date: Fri, 13 Nov 2026 22:34:27 +0000
Subject: [PATCH 1/3] Add measurable monad lifting

---
 RandomDo.lean                           |   1 +
 RandomDo/MeasurableSpaceMonad/Defs.lean |  14 ++
 RandomDo/MeasurableSpaceMonad/Lift.lean | 168 ++++++++++++++++++++++++
 RandomDo/Monad/Instances.lean           |  10 --
 Test.lean                               |   1 +
 Test/MeasurableSpaceMonad/Lift.lean     |  76 +++++++++++
 6 files changed, 260 insertions(+), 10 deletions(-)
 create mode 100644 RandomDo/MeasurableSpaceMonad/Lift.lean
 create mode 100644 Test/MeasurableSpaceMonad/Lift.lean

diff --git a/RandomDo.lean b/RandomDo.lean
index 4c24e0c..327f697 100644
--- a/RandomDo.lean
+++ b/RandomDo.lean
@@ -4,6 +4,7 @@ public import RandomDo.ForMathlib.MeasureTheory.MeasurableSpace.Embedding
 public import RandomDo.Measurable
 public import RandomDo.MeasurableSpaceMonad.Defs
 public import RandomDo.MeasurableSpaceMonad.ForIn
+public import RandomDo.MeasurableSpaceMonad.Lift
 public import RandomDo.Monad.ForInInstances
 public import RandomDo.Monad.Instances
 public import RandomDo.Monad.Notation
diff --git a/RandomDo/MeasurableSpaceMonad/Defs.lean b/RandomDo/MeasurableSpaceMonad/Defs.lean
index 74d5fc8..c02616f 100644
--- a/RandomDo/MeasurableSpaceMonad/Defs.lean
+++ b/RandomDo/MeasurableSpaceMonad/Defs.lean
@@ -26,6 +26,8 @@ instance.
 `MeasurableSpaceFunctor` satisfies the laws of a functor on measurable spaces.
 * `LawfulMeasurableSpaceMonad`: A `Prop`-valued typeclass which states that a given
 `MeasurableSpaceMonad` satisfies the laws of a monad on measurable spaces.
+* `Monad.toMeasurableSpaceMonad`: Adapts a core monad to accept a measurable space argument.
+The resulting instance need not be lawful as a measurable space monad.
 
 ## Notation
 
@@ -269,3 +271,15 @@ theorem mBind_mPure_unit {x : m PUnit} : (x >>=ₘ fun _ => mPure ⟨⟩) = x :=
 end Lawful
 
 end MeasureTheory
+
+universe u v
+
+/-- A (core) monad automatically defines a (not necessarily lawful) measurable space monad by
+forgetting the measurable space argument. -/
+def Monad.toMeasurableSpaceMonad (m : Type u → Type v) (α : Type u) [_mα : MeasurableSpace α] :
+    Type v := m α
+
+instance {m : Type u → Type v} [Monad m] :
+    MeasureTheory.MeasurableSpaceMonad (Monad.toMeasurableSpaceMonad m) where
+  mPure := pure
+  mBind := bind
diff --git a/RandomDo/MeasurableSpaceMonad/Lift.lean b/RandomDo/MeasurableSpaceMonad/Lift.lean
new file mode 100644
index 0000000..b36b4c2
--- /dev/null
+++ b/RandomDo/MeasurableSpaceMonad/Lift.lean
@@ -0,0 +1,168 @@
+/-
+Copyright (c) 2026 David Ledvinka. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Ledvinka
+-/
+module
+
+public import RandomDo.MeasurableSpaceMonad.Defs
+
+/-!
+# Lifting between measurable space monads
+
+This file defines classes `MeasurableSpaceMonadLift` and `MeasurableSpaceMonadLiftT` for lifting
+computations from one measurable space monad to another. They play the role of Lean core's
+`MonadLift` and `MonadLiftT`.
+
+## Main definitions
+
+* `MeasurableSpaceMonadLift`: a lifting operation between two measurable space monads.
+* `MeasurableSpaceMonadLiftT`: the reflexive, transitive lifting interface.
+* `LawfulMeasurableSpaceMonadLift`: A `Prop`-valued typeclass which asserts that the `mMonadLift`
+of a `MeasurableSpaceMonadLift` is measurable and preserves the monad operations.
+* `LawfulMeasurableSpaceMonadLiftT`: A `Prop`-valued typeclass which asserts that the `mMonadLift`
+of a `MeasurableSpaceMonadLiftT` is measurable and preserves the monad operations.
+-/
+
+@[expose] public section
+
+namespace MeasureTheory
+
+universe u v w
+
+/-- Computations in the measurable space monad `m` can be run in the measurable space monad `n`. -/
+class MeasurableSpaceMonadLift
+    (m : semiOutParam ((α : Type u) → [MeasurableSpace α] → Type v))
+    (n : (α : Type u) → [MeasurableSpace α] → Type w) where
+  /-- Translates an action from `m` into `n`. -/
+  mMonadLift {α : Type u} [MeasurableSpace α] : m α → n α
+
+/-- Computations in the measurable space monad `m` can be run in the measurable monad `n`.
+Unlike `do` notation, `rdo` notation can't currently automatically insert these translations.
+
+This is the reflexive, transitive closure of `MeasurableSpaceMonadLift`. Clients that require one
+measurable space monad to be liftable into another should request an instance of
+`MeasurableSpaceMonadLiftT`. New instances should instead be defined for `MeasurableSpaceMonadLift`
+itself. -/
+class MeasurableSpaceMonadLiftT
+    (m : (α : Type u) → [MeasurableSpace α] → Type v)
+    (n : (α : Type u) → [MeasurableSpace α] → Type w) where
+  /-- Translates an action from `m` into `n`. -/
+  mMonadLift {α : Type u} [MeasurableSpace α] : m α → n α
+
+export MeasurableSpaceMonadLiftT (mMonadLift)
+
+@[inherit_doc mMonadLift]
+abbrev mLiftM := @mMonadLift
+
+@[always_inline]
+instance (m n o) [MeasurableSpaceMonadLift n o] [MeasurableSpaceMonadLiftT m n] :
+    MeasurableSpaceMonadLiftT m o where
+  mMonadLift x := MeasurableSpaceMonadLift.mMonadLift (m := n) (mMonadLift x)
+
+@[always_inline]
+instance (m) : MeasurableSpaceMonadLiftT m m where
+  mMonadLift x := x
+
+-- This instance is set to low priority so that the composition and identity instances
+-- are preferred.
+instance (priority := low) {m : Type u → Type v} {n : Type u → Type w} [MonadLiftT m n] :
+    MeasurableSpaceMonadLiftT (Monad.toMeasurableSpaceMonad m)
+      (Monad.toMeasurableSpaceMonad n) where
+  mMonadLift := monadLift
+
+instance {m : (α : Type u) → [MeasurableSpace α] → Type v} [MeasurableSpacePure m] :
+    MeasurableSpaceMonadLiftT (Monad.toMeasurableSpaceMonad Id) m where
+  mMonadLift x := MeasurableSpacePure.mPure x.run
+
+section Lawful
+
+/-- Asserts that the `mMonadLift` of a `MeasurableSpaceMonadLift` is measurable and preserves
+`mPure` and `mBind` of measurable functions. -/
+class LawfulMeasurableSpaceMonadLift
+    (m : semiOutParam ((α : Type u) → [MeasurableSpace α] → Type v))
+    (n : (α : Type u) → [MeasurableSpace α] → Type w)
+    [MeasurableSpaceMonad m] [MeasurableSpaceMonad n]
+    [∀ α, [MeasurableSpace α] → MeasurableSpace (m α)]
+    [∀ α, [MeasurableSpace α] → MeasurableSpace (n α)]
+    [inst : MeasurableSpaceMonadLift m n] : Prop where
+  /-- `mMonadLift` is a measurable function. -/
+  measurable_mMonadLift {α : Type u} [MeasurableSpace α] :
+    Measurable (inst.mMonadLift : m α → n α)
+  /-- Lifting preserves `mPure`. -/
+  mMonadLift_mPure {α : Type u} [MeasurableSpace α] (a : α) :
+    inst.mMonadLift (mPure a) = mPure a
+  /-- Lifting preserves `mBind` of measurable functions. -/
+  mMonadLift_mBind {α β : Type u} [MeasurableSpace α] [MeasurableSpace β]
+      (ma : m α) (f : α → m β) (hf : Measurable f) :
+    inst.mMonadLift (ma >>=ₘ f) = inst.mMonadLift ma >>=ₘ (fun a => inst.mMonadLift (f a))
+
+/-- Asserts that the `mMonadLift` of a `MeasurableSpaceMonadLiftT` is measurable and preserves
+`mPure` and `mBind` of measurable functions. -/
+class LawfulMeasurableSpaceMonadLiftT
+    (m : (α : Type u) → [MeasurableSpace α] → Type v)
+    (n : (α : Type u) → [MeasurableSpace α] → Type w)
+    [MeasurableSpaceMonad m] [MeasurableSpaceMonad n]
+    [∀ α, [MeasurableSpace α] → MeasurableSpace (m α)]
+    [∀ α, [MeasurableSpace α] → MeasurableSpace (n α)]
+    [inst : MeasurableSpaceMonadLiftT m n] : Prop where
+  /-- Lifting is a measurable function. -/
+  measurable_mMonadLift {α : Type u} [MeasurableSpace α] :
+    Measurable (mMonadLift : m α → n α)
+  /-- Lifting preserves `mPure`. -/
+  mMonadLift_mPure {α : Type u} [MeasurableSpace α] (a : α) :
+    inst.mMonadLift (mPure a) = mPure a
+  /-- Lifting preserves `mBind` of measurable functions. -/
+  mMonadLift_mBind {α β : Type u} [MeasurableSpace α] [MeasurableSpace β]
+      (ma : m α) (f : α → m β) (hf : Measurable f) :
+    inst.mMonadLift (ma >>=ₘ f) = mMonadLift ma >>=ₘ (fun a => mMonadLift (f a))
+
+export LawfulMeasurableSpaceMonadLiftT (measurable_mMonadLift mMonadLift_mPure mMonadLift_mBind)
+
+attribute [fun_prop] LawfulMeasurableSpaceMonadLift.measurable_mMonadLift measurable_mMonadLift
+
+section
+
+variable {m : (α : Type u) → [MeasurableSpace α] → Type v}
+  {n : (α : Type u) → [MeasurableSpace α] → Type w}
+  [MeasurableSpaceMonad m] [MeasurableSpaceMonad n]
+  [∀ α, [MeasurableSpace α] → MeasurableSpace (m α)]
+  [∀ α, [MeasurableSpace α] → MeasurableSpace (n α)]
+  [MeasurableSpaceMonadLiftT m n] [LawfulMeasurableSpaceMonadLiftT m n]
+  {α β : Type u} [MeasurableSpace α] [MeasurableSpace β]
+
+-- As in core, duplicate the laws for the alias so that `rw` matches either spelling.
+@[simp] theorem mLiftM_mPure (a : α) : mLiftM (mPure a : m α) = mPure (f := n) a :=
+  mMonadLift_mPure _
+
+@[simp] theorem mLiftM_mBind (ma : m α) (f : α → m β) (hf : Measurable f) :
+    mLiftM (n := n) (ma >>=ₘ f) = mLiftM ma >>=ₘ fun a => mLiftM (f a) :=
+  mMonadLift_mBind _ _ hf
+
+end
+
+instance (m n o) [MeasurableSpaceMonad m] [MeasurableSpaceMonad n] [MeasurableSpaceMonad o]
+    [∀ α, [MeasurableSpace α] → MeasurableSpace (m α)]
+    [∀ α, [MeasurableSpace α] → MeasurableSpace (n α)]
+    [∀ α, [MeasurableSpace α] → MeasurableSpace (o α)]
+    [MeasurableSpaceMonadLift n o] [MeasurableSpaceMonadLiftT m n]
+    [LawfulMeasurableSpaceMonadLift n o] [LawfulMeasurableSpaceMonadLiftT m n] :
+    LawfulMeasurableSpaceMonadLiftT m o where
+  measurable_mMonadLift {_} _ :=
+    LawfulMeasurableSpaceMonadLift.measurable_mMonadLift.comp measurable_mMonadLift
+  mMonadLift_mPure a := by
+    simp [mMonadLift, LawfulMeasurableSpaceMonadLift.mMonadLift_mPure]
+  mMonadLift_mBind ma f hf := by
+    simp only [mMonadLift, mLiftM_mBind ma f hf]
+    exact LawfulMeasurableSpaceMonadLift.mMonadLift_mBind _ _ (by fun_prop)
+
+instance (m) [MeasurableSpaceMonad m]
+    [∀ α, [MeasurableSpace α] → MeasurableSpace (m α)] :
+    LawfulMeasurableSpaceMonadLiftT m m where
+  measurable_mMonadLift {_} _ := measurable_id
+  mMonadLift_mPure _ := rfl
+  mMonadLift_mBind _ _ _ := rfl
+
+end Lawful
+
+end MeasureTheory
diff --git a/RandomDo/Monad/Instances.lean b/RandomDo/Monad/Instances.lean
index 04bf7c3..b92e24c 100644
--- a/RandomDo/Monad/Instances.lean
+++ b/RandomDo/Monad/Instances.lean
@@ -23,16 +23,6 @@ open MeasureTheory
 
 universe u v w
 
-/-- A (core) monad automatically defines a (not necessarily lawful) measurable space monad by
-forgetting the measurable space argument. -/
-def Monad.toMeasurableSpaceMonad (m : Type u → Type v) (α : Type u) [_mα : MeasurableSpace α] :
-    Type v := m α
-
-instance {m : Type u → Type v} [Monad m] :
-    MeasurableSpaceMonad (Monad.toMeasurableSpaceMonad m) where
-  mPure := pure
-  mBind := bind
-
 /-- A measurable space monad for pseudo random number generation. -/
 abbrev PseudoRandomM := Monad.toMeasurableSpaceMonad Rand
 
diff --git a/Test.lean b/Test.lean
index bba557b..2a0294c 100644
--- a/Test.lean
+++ b/Test.lean
@@ -8,6 +8,7 @@ public import Test.Gaps
 public import Test.Instances
 public import Test.IsMarkov
 public import Test.Loops
+public import Test.MeasurableSpaceMonad.Lift
 public import Test.MonadLaws
 public import Test.Polymorphic
 public import Test.Sample
diff --git a/Test/MeasurableSpaceMonad/Lift.lean b/Test/MeasurableSpaceMonad/Lift.lean
new file mode 100644
index 0000000..0c526a6
--- /dev/null
+++ b/Test/MeasurableSpaceMonad/Lift.lean
@@ -0,0 +1,76 @@
+/-
+Copyright (c) 2026 David Ledvinka. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Ledvinka
+-/
+module
+
+import RandomDo.MeasurableSpaceMonad.Lift
+
+/-!
+# Regression tests for measurable monad lifting
+
+These tests check direct-lift measurability, inference through composed lifts, and the precedence
+of native measurable lifts over the fallback to core's `MonadLiftT`.
+-/
+
+set_option linter.privateModule false
+
+open MeasureTheory
+
+namespace Test.MeasurableSpaceMonad.Lift
+
+universe u v w z
+
+section Measurability
+
+variable {m : (α : Type u) → [MeasurableSpace α] → Type v}
+  {n : (α : Type u) → [MeasurableSpace α] → Type w}
+  [MeasurableSpaceMonad m] [MeasurableSpaceMonad n]
+  [∀ α, [MeasurableSpace α] → MeasurableSpace (m α)]
+  [∀ α, [MeasurableSpace α] → MeasurableSpace (n α)]
+  [direct : MeasurableSpaceMonadLift m n] [LawfulMeasurableSpaceMonadLift m n]
+  {α β : Type u} [MeasurableSpace α] [MeasurableSpace β]
+
+-- Regression: stating the direct measurability law using the transitive projection made
+-- `fun_prop` unable to find a theorem for the direct projection.
+example (f : α → m β) (hf : Measurable f) :
+    Measurable (fun a => direct.mMonadLift (f a)) := by
+  fun_prop
+
+variable {o : (α : Type u) → [MeasurableSpace α] → Type z}
+  [MeasurableSpaceMonad o] [∀ α, [MeasurableSpace α] → MeasurableSpace (o α)]
+  [MeasurableSpaceMonadLift n o] [LawfulMeasurableSpaceMonadLift n o]
+
+-- Infer the intermediate monad and the lawful composite from direct instances; `fun_prop`
+-- must also recognize the public `mLiftM` alias.
+example (f : α → m β) (hf : Measurable f) :
+    Measurable (fun a => mLiftM (n := o) (f a)) := by
+  fun_prop
+
+end Measurability
+
+section CoreBridge
+
+variable {m : Type u → Type v} {n : Type u → Type w}
+  {α : Type u} [MeasurableSpace α]
+
+-- A supplied core self-lift need not be identity. Measurable self-lifting must still use
+-- the native identity instance, so these are not two definitionally identical candidates.
+example [MonadLiftT m m] (x : Monad.toMeasurableSpaceMonad m α) :
+    mMonadLift (n := Monad.toMeasurableSpaceMonad m) x = x := rfl
+
+-- Native composition must also win when a core lift is available for the same endpoints.
+example [MonadLiftT m n]
+    [native : MeasurableSpaceMonadLift (Monad.toMeasurableSpaceMonad m)
+      (Monad.toMeasurableSpaceMonad n)]
+    (x : Monad.toMeasurableSpaceMonad m α) :
+    mMonadLift (n := Monad.toMeasurableSpaceMonad n) x = native.mMonadLift x := rfl
+
+-- If there is no native route, the bridge must use the supplied core lift.
+example [MonadLiftT m n] (x : Monad.toMeasurableSpaceMonad m α) :
+    mMonadLift (n := Monad.toMeasurableSpaceMonad n) x = monadLift (n := n) x := rfl
+
+end CoreBridge
+
+end Test.MeasurableSpaceMonad.Lift

From 8bf49de04d06ac68c2a355560bc62742f3bfaddb Mon Sep 17 00:00:00 2001
From: David Ledvinka <dledvinka.ledvinka@mail.utoronto.ca>
Date: Fri, 13 Nov 2026 22:49:12 +0000
Subject: [PATCH 2/3] Match scaffold adapter placement and retain tests in
 scaffold

---
 RandomDo/MeasurableSpaceMonad/Defs.lean | 26 ++++-----
 Test.lean                               |  1 -
 Test/MeasurableSpaceMonad/Lift.lean     | 76 -------------------------
 3 files changed, 12 insertions(+), 91 deletions(-)
 delete mode 100644 Test/MeasurableSpaceMonad/Lift.lean

diff --git a/RandomDo/MeasurableSpaceMonad/Defs.lean b/RandomDo/MeasurableSpaceMonad/Defs.lean
index c02616f..a703ead 100644
--- a/RandomDo/MeasurableSpaceMonad/Defs.lean
+++ b/RandomDo/MeasurableSpaceMonad/Defs.lean
@@ -26,8 +26,8 @@ instance.
 `MeasurableSpaceFunctor` satisfies the laws of a functor on measurable spaces.
 * `LawfulMeasurableSpaceMonad`: A `Prop`-valued typeclass which states that a given
 `MeasurableSpaceMonad` satisfies the laws of a monad on measurable spaces.
-* `Monad.toMeasurableSpaceMonad`: Adapts a core monad to accept a measurable space argument.
-The resulting instance need not be lawful as a measurable space monad.
+* `Monad.toMeasurableSpaceMonad`: transforms a core monad into a measurable space monad by
+forgetting the measurable space argument.
 
 ## Notation
 
@@ -151,6 +151,16 @@ class MeasurableSpaceMonad (m : (α : Type u) → [MeasurableSpace α] → Type
     extends MeasurableSpaceFunctor m, MeasurableSpacePure m, MeasurableSpaceBind m where
   mMap f μ := mBind μ (Function.comp mPure f)
 
+/-- A (core) monad automatically defines a (not necessarily lawful) measurable space monad by
+forgetting the measurable space argument. -/
+def Monad.toMeasurableSpaceMonad (m : Type u → Type v) (α : Type u)
+    [_mα : MeasurableSpace α] : Type v := m α
+
+instance {m : Type u → Type v} [Monad m] :
+    MeasurableSpaceMonad (Monad.toMeasurableSpaceMonad m) where
+  mPure := pure
+  mBind := bind
+
 variable {m : (α : Type u) → [MeasurableSpace α] → Type v} {α β : Type u}
   [MeasurableSpace α] [MeasurableSpace β]
 
@@ -271,15 +281,3 @@ theorem mBind_mPure_unit {x : m PUnit} : (x >>=ₘ fun _ => mPure ⟨⟩) = x :=
 end Lawful
 
 end MeasureTheory
-
-universe u v
-
-/-- A (core) monad automatically defines a (not necessarily lawful) measurable space monad by
-forgetting the measurable space argument. -/
-def Monad.toMeasurableSpaceMonad (m : Type u → Type v) (α : Type u) [_mα : MeasurableSpace α] :
-    Type v := m α
-
-instance {m : Type u → Type v} [Monad m] :
-    MeasureTheory.MeasurableSpaceMonad (Monad.toMeasurableSpaceMonad m) where
-  mPure := pure
-  mBind := bind
diff --git a/Test.lean b/Test.lean
index 2a0294c..bba557b 100644
--- a/Test.lean
+++ b/Test.lean
@@ -8,7 +8,6 @@ public import Test.Gaps
 public import Test.Instances
 public import Test.IsMarkov
 public import Test.Loops
-public import Test.MeasurableSpaceMonad.Lift
 public import Test.MonadLaws
 public import Test.Polymorphic
 public import Test.Sample
diff --git a/Test/MeasurableSpaceMonad/Lift.lean b/Test/MeasurableSpaceMonad/Lift.lean
deleted file mode 100644
index 0c526a6..0000000
--- a/Test/MeasurableSpaceMonad/Lift.lean
+++ /dev/null
@@ -1,76 +0,0 @@
-/-
-Copyright (c) 2026 David Ledvinka. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: David Ledvinka
--/
-module
-
-import RandomDo.MeasurableSpaceMonad.Lift
-
-/-!
-# Regression tests for measurable monad lifting
-
-These tests check direct-lift measurability, inference through composed lifts, and the precedence
-of native measurable lifts over the fallback to core's `MonadLiftT`.
--/
-
-set_option linter.privateModule false
-
-open MeasureTheory
-
-namespace Test.MeasurableSpaceMonad.Lift
-
-universe u v w z
-
-section Measurability
-
-variable {m : (α : Type u) → [MeasurableSpace α] → Type v}
-  {n : (α : Type u) → [MeasurableSpace α] → Type w}
-  [MeasurableSpaceMonad m] [MeasurableSpaceMonad n]
-  [∀ α, [MeasurableSpace α] → MeasurableSpace (m α)]
-  [∀ α, [MeasurableSpace α] → MeasurableSpace (n α)]
-  [direct : MeasurableSpaceMonadLift m n] [LawfulMeasurableSpaceMonadLift m n]
-  {α β : Type u} [MeasurableSpace α] [MeasurableSpace β]
-
--- Regression: stating the direct measurability law using the transitive projection made
--- `fun_prop` unable to find a theorem for the direct projection.
-example (f : α → m β) (hf : Measurable f) :
-    Measurable (fun a => direct.mMonadLift (f a)) := by
-  fun_prop
-
-variable {o : (α : Type u) → [MeasurableSpace α] → Type z}
-  [MeasurableSpaceMonad o] [∀ α, [MeasurableSpace α] → MeasurableSpace (o α)]
-  [MeasurableSpaceMonadLift n o] [LawfulMeasurableSpaceMonadLift n o]
-
--- Infer the intermediate monad and the lawful composite from direct instances; `fun_prop`
--- must also recognize the public `mLiftM` alias.
-example (f : α → m β) (hf : Measurable f) :
-    Measurable (fun a => mLiftM (n := o) (f a)) := by
-  fun_prop
-
-end Measurability
-
-section CoreBridge
-
-variable {m : Type u → Type v} {n : Type u → Type w}
-  {α : Type u} [MeasurableSpace α]
-
--- A supplied core self-lift need not be identity. Measurable self-lifting must still use
--- the native identity instance, so these are not two definitionally identical candidates.
-example [MonadLiftT m m] (x : Monad.toMeasurableSpaceMonad m α) :
-    mMonadLift (n := Monad.toMeasurableSpaceMonad m) x = x := rfl
-
--- Native composition must also win when a core lift is available for the same endpoints.
-example [MonadLiftT m n]
-    [native : MeasurableSpaceMonadLift (Monad.toMeasurableSpaceMonad m)
-      (Monad.toMeasurableSpaceMonad n)]
-    (x : Monad.toMeasurableSpaceMonad m α) :
-    mMonadLift (n := Monad.toMeasurableSpaceMonad n) x = native.mMonadLift x := rfl
-
--- If there is no native route, the bridge must use the supplied core lift.
-example [MonadLiftT m n] (x : Monad.toMeasurableSpaceMonad m α) :
-    mMonadLift (n := Monad.toMeasurableSpaceMonad n) x = monadLift (n := n) x := rfl
-
-end CoreBridge
-
-end Test.MeasurableSpaceMonad.Lift

From 5dfcb8c4937fb49be8524eacc772d91eb6c5c3bc Mon Sep 17 00:00:00 2001
From: David Ledvinka <dledvinka.ledvinka@mail.utoronto.ca>
Date: Fri, 13 Nov 2026 22:58:10 +0000
Subject: [PATCH 3/3] Preserve root namespace for the monad adapter

---
 RandomDo/MeasurableSpaceMonad/Defs.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/RandomDo/MeasurableSpaceMonad/Defs.lean b/RandomDo/MeasurableSpaceMonad/Defs.lean
index a703ead..481dca0 100644
--- a/RandomDo/MeasurableSpaceMonad/Defs.lean
+++ b/RandomDo/MeasurableSpaceMonad/Defs.lean
@@ -153,7 +153,7 @@ class MeasurableSpaceMonad (m : (α : Type u) → [MeasurableSpace α] → Type
 
 /-- A (core) monad automatically defines a (not necessarily lawful) measurable space monad by
 forgetting the measurable space argument. -/
-def Monad.toMeasurableSpaceMonad (m : Type u → Type v) (α : Type u)
+def _root_.Monad.toMeasurableSpaceMonad (m : Type u → Type v) (α : Type u)
     [_mα : MeasurableSpace α] : Type v := m α
 
 instance {m : Type u → Type v} [Monad m] :