case h.e'_5
α : Type u_1
β : Type ?u.130171
γ : Type ?u.130174
δ : Type ?u.130177
ι : Type ?u.130180
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h : t =ᵐ[μ] ∅
⊢ ∅ = s ∩ ∅
α : Type u_1
β : Type ?u.130171
γ : Type ?u.130174
δ : Type ?u.130177
ι : Type ?u.130180
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h : t =ᵐ[μ] ∅
⊢ s ∩ t =ᵐ[μ] ∅
convert ae_eq_set_inter (ae_eq_refl s) h
no goals
case h.e'_5
α : Type u_1
β : Type ?u.130171
γ : Type ?u.130174
δ : Type ?u.130177
ι : Type ?u.130180
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h : t =ᵐ[μ] ∅
⊢ ∅ = s ∩ ∅
rw [inter_empty]