case a
α : Type u_1
β : Type ?u.600866
γ : Type ?u.600869
δ : Type ?u.600872
ι : Type ?u.600875
R : Type ?u.600878
R' : Type ?u.600881
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
⊢ s ∈ ae (dirac a) ↔ s ∈ pure a
α : Type u_1
β : Type ?u.600866
γ : Type ?u.600869
δ : Type ?u.600872
ι : Type ?u.600875
R : Type ?u.600878
R' : Type ?u.600881
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
⊢ ae (dirac a) = pure a
ext s
no goals
case a
α : Type u_1
β : Type ?u.600866
γ : Type ?u.600869
δ : Type ?u.600872
ι : Type ?u.600875
R : Type ?u.600878
R' : Type ?u.600881
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
⊢ s ∈ ae (dirac a) ↔ s ∈ pure a
simp [mem_ae_iff, imp_false]