α : Type u_1
β : Type ?u.31363
γ : Type ?u.31366
δ : Type ?u.31369
ι : Type ?u.31372
R : Type ?u.31375
R' : Type ?u.31378
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h₁ : s ≤ᵐ[μ] t
h₂ : ↑↑μ t ≤ ↑↑μ s
hsm : MeasurableSet s
ht : ↑↑μ t ≠ ⊤
⊢ ↑↑μ (t \ s) = 0
α : Type u_1
β : Type ?u.31363
γ : Type ?u.31366
δ : Type ?u.31369
ι : Type ?u.31372
R : Type ?u.31375
R' : Type ?u.31378
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h₁ : s ≤ᵐ[μ] t
h₂ : ↑↑μ t ≤ ↑↑μ s
hsm : MeasurableSet s
ht : ↑↑μ t ≠ ⊤
⊢ s =ᵐ[μ] t
refine' eventuallyLE_antisymm_iff.mpr ⟨h₁, ae_le_set.mpr _⟩
case h₂
α : Type u_1
β : Type ?u.31363
γ : Type ?u.31366
δ : Type ?u.31369
ι : Type ?u.31372
R : Type ?u.31375
R' : Type ?u.31378
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h₁ : s ≤ᵐ[μ] t
h₂ : ↑↑μ t ≤ ↑↑μ s
hsm : MeasurableSet s
ht : ↑↑μ t ≠ ⊤
⊢ ↑↑μ t = ↑↑μ s

α : Type u_1
β : Type ?u.31363
γ : Type ?u.31366
δ : Type ?u.31369
ι : Type ?u.31372
R : Type ?u.31375
R' : Type ?u.31378
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h₁ : s ≤ᵐ[μ] t
hsm : MeasurableSet s
ht : ↑↑μ t ≠ ⊤
h₂ : ↑↑μ t = ↑↑μ s
⊢ ↑↑μ (t \ s) = 0
α : Type u_1
β : Type ?u.31363
γ : Type ?u.31366
δ : Type ?u.31369
ι : Type ?u.31372
R : Type ?u.31375
R' : Type ?u.31378
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h₁ : s ≤ᵐ[μ] t
h₂ : ↑↑μ t ≤ ↑↑μ s
hsm : MeasurableSet s
ht : ↑↑μ t ≠ ⊤
⊢ ↑↑μ (t \ s) = 0
replace h₂ : μ t = μ s
α : Type u_1
β : Type ?u.31363
γ : Type ?u.31366
δ : Type ?u.31369
ι : Type ?u.31372
R : Type ?u.31375
R' : Type ?u.31378
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h₁ : s ≤ᵐ[μ] t
hsm : MeasurableSet s
ht : ↑↑μ t ≠ ⊤
h₂ : ↑↑μ t = ↑↑μ s
⊢ ↑↑μ (t \ s) = 0
case h₂
α : Type u_1
β : Type ?u.31363
γ : Type ?u.31366
δ : Type ?u.31369
ι : Type ?u.31372
R : Type ?u.31375
R' : Type ?u.31378
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h₁ : s ≤ᵐ[μ] t
h₂ : ↑↑μ t ≤ ↑↑μ s
hsm : MeasurableSet s
ht : ↑↑μ t ≠ ⊤
⊢ ↑↑μ t = ↑↑μ s

α : Type u_1
β : Type ?u.31363
γ : Type ?u.31366
δ : Type ?u.31369
ι : Type ?u.31372
R : Type ?u.31375
R' : Type ?u.31378
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h₁ : s ≤ᵐ[μ] t
hsm : MeasurableSet s
ht : ↑↑μ t ≠ ⊤
h₂ : ↑↑μ t = ↑↑μ s
⊢ ↑↑μ (t \ s) = 0
exact h₂.antisymm (measure_mono_ae h₁)
case ht
α : Type u_1
β : Type ?u.31363
γ : Type ?u.31366
δ : Type ?u.31369
ι : Type ?u.31372
R : Type ?u.31375
R' : Type ?u.31378
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h₁ : s ≤ᵐ[μ] t
hsm : MeasurableSet s
ht : ↑↑μ t ≠ ⊤
h₂ : ↑↑μ t = ↑↑μ s
⊢ ↑↑μ s ≠ ⊤

α : Type u_1
β : Type ?u.31363
γ : Type ?u.31366
δ : Type ?u.31369
ι : Type ?u.31372
R : Type ?u.31375
R' : Type ?u.31378
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h₁ : s ≤ᵐ[μ] t
hsm : MeasurableSet s
h₂ : ↑↑μ t = ↑↑μ s
ht : ↑↑μ s ≠ ⊤
⊢ ↑↑μ (t \ s) = 0
α : Type u_1
β : Type ?u.31363
γ : Type ?u.31366
δ : Type ?u.31369
ι : Type ?u.31372
R : Type ?u.31375
R' : Type ?u.31378
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h₁ : s ≤ᵐ[μ] t
hsm : MeasurableSet s
ht : ↑↑μ t ≠ ⊤
h₂ : ↑↑μ t = ↑↑μ s
⊢ ↑↑μ (t \ s) = 0
replace ht : μ s ≠ ∞
α : Type u_1
β : Type ?u.31363
γ : Type ?u.31366
δ : Type ?u.31369
ι : Type ?u.31372
R : Type ?u.31375
R' : Type ?u.31378
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h₁ : s ≤ᵐ[μ] t
hsm : MeasurableSet s
h₂ : ↑↑μ t = ↑↑μ s
ht : ↑↑μ s ≠ ⊤
⊢ ↑↑μ (t \ s) = 0
case ht
α : Type u_1
β : Type ?u.31363
γ : Type ?u.31366
δ : Type ?u.31369
ι : Type ?u.31372
R : Type ?u.31375
R' : Type ?u.31378
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h₁ : s ≤ᵐ[μ] t
hsm : MeasurableSet s
ht : ↑↑μ t ≠ ⊤
h₂ : ↑↑μ t = ↑↑μ s
⊢ ↑↑μ s ≠ ⊤

α : Type u_1
β : Type ?u.31363
γ : Type ?u.31366
δ : Type ?u.31369
ι : Type ?u.31372
R : Type ?u.31375
R' : Type ?u.31378
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h₁ : s ≤ᵐ[μ] t
hsm : MeasurableSet s
h₂ : ↑↑μ t = ↑↑μ s
ht : ↑↑μ s ≠ ⊤
⊢ ↑↑μ (t \ s) = 0
exact h₂ ▸ ht
no goals
α : Type u_1
β : Type ?u.31363
γ : Type ?u.31366
δ : Type ?u.31369
ι : Type ?u.31372
R : Type ?u.31375
R' : Type ?u.31378
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h₁ : s ≤ᵐ[μ] t
hsm : MeasurableSet s
h₂ : ↑↑μ t = ↑↑μ s
ht : ↑↑μ s ≠ ⊤
⊢ ↑↑μ (t \ s) = 0
rw [measure_diff' t hsm ht, measure_congr (union_ae_eq_left_iff_ae_subset.mpr h₁), h₂, tsub_self]