ι : Type ?u.9675
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t u v : Set α
h : AEDisjoint μ s t
x : α
hx : x ∈ s \ toMeasurable μ (s ∩ t)
⊢ x ∈ ?m.10357 h ∧ ¬x ∈ t
ι : Type ?u.9675
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t u v : Set α
h : AEDisjoint μ s t
x : α
hx : x ∈ s \ toMeasurable μ (s ∩ t)
⊢ x ∈ ?m.10357 h \ t
simp
no goals
ι : Type ?u.9675
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t u v : Set α
h : AEDisjoint μ s t
x : α
hx : x ∈ s \ toMeasurable μ (s ∩ t)
⊢ x ∈ ?m.10357 h ∧ ¬x ∈ t
exact ⟨hx.1, fun hxt => hx.2 <| subset_toMeasurable _ _ ⟨hx.1, hxt⟩⟩