case h.e'_5
α : Type u_1
β : Type ?u.115131
γ : Type ?u.115134
δ : Type ?u.115137
ι : Type ?u.115140
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h : t =ᵐ[μ] univ
⊢ univ = s ∪ univ
α : Type u_1
β : Type ?u.115131
γ : Type ?u.115134
δ : Type ?u.115137
ι : Type ?u.115140
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h : t =ᵐ[μ] univ
⊢ s ∪ t =ᵐ[μ] univ
convert ae_eq_set_union (ae_eq_refl s) h
no goals
case h.e'_5
α : Type u_1
β : Type ?u.115131
γ : Type ?u.115134
δ : Type ?u.115137
ι : Type ?u.115140
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h : t =ᵐ[μ] univ
⊢ univ = s ∪ univ
rw [union_univ]