Theorem: MeasureTheory.IsProbabilityMeasure.measureReal_univ (Carleson/ToMathlib/MeasureReal.lean)

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
inst✝ : IsProbabilityMeasure μ
⊢ μ.real univ = 1
Tactic:
simp [Measure.real]
State after:
no goals