α : Type u_1
β : Type ?u.644466
γ : Type ?u.644469
δ : Type ?u.644472
ι : Type ?u.644475
R : Type ?u.644478
R' : Type ?u.644481
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : IsFiniteMeasure μ
hμ : measureUnivNNReal μ ≤ 0
⊢ μ = 0
α : Type u_1
β : Type ?u.644466
γ : Type ?u.644469
δ : Type ?u.644472
ι : Type ?u.644475
R : Type ?u.644478
R' : Type ?u.644481
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
⊢ 0 < measureUnivNNReal μ
contrapose! hμ
no goals
α : Type u_1
β : Type ?u.644466
γ : Type ?u.644469
δ : Type ?u.644472
ι : Type ?u.644475
R : Type ?u.644478
R' : Type ?u.644481
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : IsFiniteMeasure μ
hμ : measureUnivNNReal μ ≤ 0
⊢ μ = 0
simpa [measureUnivNNReal_eq_zero, le_zero_iff] using hμ