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