import Mathlib.MeasureTheory.Order.Lattice
import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
import Mathlib.Probability.Independence.Basic
import Mathlib.Probability.Independence.Conditional
import Mathlib.MeasureTheory.Measure.SubFinite
import Mathlib.Probability.Kernel.RadonNikodym

/-! # Standalone extraction for `ProbabilityTheory.ProbabilityMeasure.ext_iff_coe`
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 ENNReal
end ENNReal

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

-- ═══ ForMathlib.Probability.Independence.CondDistrib ═══
section
open MeasureTheory ProbabilityTheory Finset
open scoped ENNReal NNReal
variable {α β γ δ Ω Ω' : Type*} {m mα : MeasurableSpace α} {μ : Measure α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [mΩ' : MeasurableSpace Ω'] [StandardBorelSpace Ω'] [Nonempty Ω'] {X : α → β} {Y : α → Ω} {Z : α → Ω'} {T : α → γ}
namespace ProbabilityTheory
section CondDistrib
variable [IsFiniteMeasure μ]

lemma ProbabilityMeasure.ext_iff_coe {α : Type*} {mα : MeasurableSpace α}
    {μ ν : ProbabilityMeasure α} :
    μ = ν ↔ (μ : Measure α) = ν := sorry

end CondDistrib
end ProbabilityTheory
end