case pos
α : Type u_1
a : α
s : Set α
x✝ : MeasurableSet s
t : Set α
ht : a ∈ t
⊢ ↑(dirac a) t = ↑(dirac a) (t ∩ s) + ↑(dirac a) (t \ s)

case neg
α : Type u_1
a : α
s : Set α
x✝ : MeasurableSet s
t : Set α
ht : ¬a ∈ t
⊢ ↑(dirac a) t = ↑(dirac a) (t ∩ s) + ↑(dirac a) (t \ s)
α : Type u_1
a : α
s : Set α
x✝ : MeasurableSet s
t : Set α
⊢ ↑(dirac a) t = ↑(dirac a) (t ∩ s) + ↑(dirac a) (t \ s)
by_cases ht : a ∈ t
case neg
α : Type u_1
a : α
s : Set α
x✝ : MeasurableSet s
t : Set α
ht : ¬a ∈ t
⊢ ↑(dirac a) t = ↑(dirac a) (t ∩ s) + ↑(dirac a) (t \ s)

case pos
α : Type u_1
a : α
s : Set α
x✝ : MeasurableSet s
t : Set α
ht : a ∈ t
⊢ ↑(dirac a) t = ↑(dirac a) (t ∩ s) + ↑(dirac a) (t \ s)
case pos
α : Type u_1
a : α
s : Set α
x✝ : MeasurableSet s
t : Set α
ht : a ∈ t
⊢ ↑(dirac a) t = ↑(dirac a) (t ∩ s) + ↑(dirac a) (t \ s)

case neg
α : Type u_1
a : α
s : Set α
x✝ : MeasurableSet s
t : Set α
ht : ¬a ∈ t
⊢ ↑(dirac a) t = ↑(dirac a) (t ∩ s) + ↑(dirac a) (t \ s)
swap
no goals
case pos
α : Type u_1
a : α
s : Set α
x✝ : MeasurableSet s
t : Set α
ht : a ∈ t
⊢ ↑(dirac a) t = ↑(dirac a) (t ∩ s) + ↑(dirac a) (t \ s)
by_cases hs : a ∈ s <;> simp [*]
no goals
case neg
α : Type u_1
a : α
s : Set α
x✝ : MeasurableSet s
t : Set α
ht : ¬a ∈ t
⊢ ↑(dirac a) t = ↑(dirac a) (t ∩ s) + ↑(dirac a) (t \ s)
simp [ht]