Theorem: MeasureTheory.measureReal_univ_pos (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✝¹ : IsFiniteMeasure μ
inst✝ : NeZero μ
⊢ 0 < μ.real univ
Tactic:
rw [measureReal_def]
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
inst✝¹ : IsFiniteMeasure μ
inst✝ : NeZero μ
⊢ 0 < (μ univ).toReal

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
inst✝¹ : IsFiniteMeasure μ
inst✝ : NeZero μ
⊢ 0 < (μ univ).toReal
Tactic:
apply ENNReal.toReal_pos
State after:
case ha₀
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
inst✝¹ : IsFiniteMeasure μ
inst✝ : NeZero μ
⊢ μ univ ≠ 0

case ha_top
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
inst✝¹ : IsFiniteMeasure μ
inst✝ : NeZero μ
⊢ μ univ ≠ ⊤

State before:
case ha₀
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
inst✝¹ : IsFiniteMeasure μ
inst✝ : NeZero μ
⊢ μ univ ≠ 0

case ha_top
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
inst✝¹ : IsFiniteMeasure μ
inst✝ : NeZero μ
⊢ μ univ ≠ ⊤
Tactic:
exact NeZero.ne (μ Set.univ)
State after:
case ha_top
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
inst✝¹ : IsFiniteMeasure μ
inst✝ : NeZero μ
⊢ μ univ ≠ ⊤

State before:
case ha_top
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
inst✝¹ : IsFiniteMeasure μ
inst✝ : NeZero μ
⊢ μ univ ≠ ⊤
Tactic:
finiteness
State after:
no goals