α : Type u_1
β : Type ?u.588993
γ : Type ?u.588996
δ : Type ?u.588999
ι : Type ?u.589002
R : Type ?u.589005
R' : Type ?u.589008
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t s : Set α
hs : MeasurableSet s
⊢ ∃ t₁, t₁ ∈ ae μ ∧ ∃ t₂, s ⊆ t₂ ∧ s = t₁ ∩ t₂
α : Type u_1
β : Type ?u.588993
γ : Type ?u.588996
δ : Type ?u.588999
ι : Type ?u.589002
R : Type ?u.589005
R' : Type ?u.589008
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t s : Set α
hs : MeasurableSet s
⊢ s ∈ ae (Measure.restrict μ s)
simp only [ae_restrict_eq hs, exists_prop, mem_principal, mem_inf_iff]
no goals
α : Type u_1
β : Type ?u.588993
γ : Type ?u.588996
δ : Type ?u.588999
ι : Type ?u.589002
R : Type ?u.589005
R' : Type ?u.589008
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t s : Set α
hs : MeasurableSet s
⊢ ∃ t₁, t₁ ∈ ae μ ∧ ∃ t₂, s ⊆ t₂ ∧ s = t₁ ∩ t₂
exact ⟨_, univ_mem, s, Subset.rfl, (univ_inter s).symm⟩