case a
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ ν : ProbabilityMeasure Ω
h : ∀ (s : Set Ω), MeasurableSet s → ↑↑↑μ s = ↑↑↑ν s
⊢ ↑μ = ↑ν
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ ν : ProbabilityMeasure Ω
h : ∀ (s : Set Ω), MeasurableSet s → ↑↑↑μ s = ↑↑↑ν s
⊢ μ = ν
apply toMeasure_injective
case a.h
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ ν : ProbabilityMeasure Ω
h : ∀ (s : Set Ω), MeasurableSet s → ↑↑↑μ s = ↑↑↑ν s
s : Set Ω
s_mble : MeasurableSet s
⊢ ↑↑↑μ s = ↑↑↑ν s
case a
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ ν : ProbabilityMeasure Ω
h : ∀ (s : Set Ω), MeasurableSet s → ↑↑↑μ s = ↑↑↑ν s
⊢ ↑μ = ↑ν
ext1 s s_mble
no goals
case a.h
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ ν : ProbabilityMeasure Ω
h : ∀ (s : Set Ω), MeasurableSet s → ↑↑↑μ s = ↑↑↑ν s
s : Set Ω
s_mble : MeasurableSet s
⊢ ↑↑↑μ s = ↑↑↑ν s
exact h s s_mble