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