import Mathlib.MeasureTheory.Order.Lattice
import Mathlib.Combinatorics.Quiver.ReflQuiver
import Mathlib.Probability.Kernel.Category.SFinKer
import Mathlib.Probability.Kernel.Composition.CompProd
import Mathlib.MeasureTheory.MeasurableSpace.Embedding
import Mathlib.Probability.Kernel.Deterministic
import Mathlib.MeasureTheory.Integral.Lebesgue.Countable

/-! # Standalone extraction for `MeasurableCoherence.inst`
Definitions are copied verbatim; theorem proofs are replaced by `sorry`.
Auto-generated by Referee. -/

set_option quotPrecheck false

-- Namespace stubs (so later `open`s resolve).
namespace Finset
end Finset
namespace MeasureTheory
end MeasureTheory
namespace ProbabilityTheory
end ProbabilityTheory
namespace MeasurableEquiv
end MeasurableEquiv
namespace MeasurableCoherence
end MeasurableCoherence

-- ═══ ForMathlib.MeasureTheory.Order.Lattice ═══
section
open Finset
variable {α δ : Type*} [MeasurableSpace δ] [SemilatticeInf α] {m : MeasurableSpace α} [MeasurableInf₂ α]
attribute [to_dual existing] MeasurableInf₂
end

-- ═══ Tactic.KernelHom.Kernel.MonoidalComp ═══
section
open CategoryTheory MeasureTheory ProbabilityTheory MeasurableEquiv
open scoped MonoidalCategory SFinKer

/-- A class witnessing the existence of a measurable equivalence between two measurable spaces. -/
class MeasurableCoherence (X Y : Type*) [MeasurableSpace X] [MeasurableSpace Y] where
  /-- A measurable equivalence between `X` and `Y`. -/
  miso : X ≃ᵐ Y

namespace MeasurableCoherence
variable {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y] [mXY : MeasurableCoherence X Y]

instance : MeasurableCoherence X X where
  miso := MeasurableEquiv.refl X

end MeasurableCoherence
end