case h.e'_5
α : Type u_1
β : Type ?u.122594
γ : Type ?u.122597
δ : Type ?u.122600
ι : Type ?u.122603
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h : s =ᵐ[μ] univ
⊢ t = univ ∩ t
α : Type u_1
β : Type ?u.122594
γ : Type ?u.122597
δ : Type ?u.122600
ι : Type ?u.122603
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h : s =ᵐ[μ] univ
⊢ s ∩ t =ᵐ[μ] t
convert ae_eq_set_inter h (ae_eq_refl t)
no goals
case h.e'_5
α : Type u_1
β : Type ?u.122594
γ : Type ?u.122597
δ : Type ?u.122600
ι : Type ?u.122603
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h : s =ᵐ[μ] univ
⊢ t = univ ∩ t
rw [univ_inter]