α : Type u_1
β : Type ?u.397362
γ : Type ?u.397365
δ : Type ?u.397368
ι : Type ?u.397371
R : Type ?u.397374
R' : Type ?u.397377
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
h : ∀ ⦃s : Set α⦄, MeasurableSet s → ↑↑ν s = 0 → ↑↑μ s = 0
s : Set α
hs : ↑↑ν s = 0
⊢ ↑↑μ s = 0
α : Type u_1
β : Type ?u.397362
γ : Type ?u.397365
δ : Type ?u.397368
ι : Type ?u.397371
R : Type ?u.397374
R' : Type ?u.397377
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
h : ∀ ⦃s : Set α⦄, MeasurableSet s → ↑↑ν s = 0 → ↑↑μ s = 0
⊢ μ ≪ ν
intro s hs
case intro.intro.intro
α : Type u_1
β : Type ?u.397362
γ : Type ?u.397365
δ : Type ?u.397368
ι : Type ?u.397371
R : Type ?u.397374
R' : Type ?u.397377
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
h : ∀ ⦃s : Set α⦄, MeasurableSet s → ↑↑ν s = 0 → ↑↑μ s = 0
s : Set α
hs : ↑↑ν s = 0
t : Set α
h1t : s ⊆ t
h2t : MeasurableSet t
h3t : ↑↑ν t = 0
⊢ ↑↑μ s = 0
α : Type u_1
β : Type ?u.397362
γ : Type ?u.397365
δ : Type ?u.397368
ι : Type ?u.397371
R : Type ?u.397374
R' : Type ?u.397377
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
h : ∀ ⦃s : Set α⦄, MeasurableSet s → ↑↑ν s = 0 → ↑↑μ s = 0
s : Set α
hs : ↑↑ν s = 0
⊢ ↑↑μ s = 0
rcases exists_measurable_superset_of_null hs with ⟨t, h1t, h2t, h3t⟩
no goals
case intro.intro.intro
α : Type u_1
β : Type ?u.397362
γ : Type ?u.397365
δ : Type ?u.397368
ι : Type ?u.397371
R : Type ?u.397374
R' : Type ?u.397377
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
h : ∀ ⦃s : Set α⦄, MeasurableSet s → ↑↑ν s = 0 → ↑↑μ s = 0
s : Set α
hs : ↑↑ν s = 0
t : Set α
h1t : s ⊆ t
h2t : MeasurableSet t
h3t : ↑↑ν t = 0
⊢ ↑↑μ s = 0
exact measure_mono_null h1t (h h2t h3t)