case h
α : Type u_1
mα : MeasurableSpace α
a : α
s : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
t : Set α
ht : MeasurableSet t
⊢ ↑↑(Measure.restrict (Measure.dirac a) s) t = ↑↑(if a ∈ s then Measure.dirac a else 0) t
α : Type u_1
mα : MeasurableSpace α
a : α
s : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
⊢ Measure.restrict (Measure.dirac a) s = if a ∈ s then Measure.dirac a else 0
ext1 t ht
case h
α : Type u_1
mα : MeasurableSpace α
a : α
s : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
t : Set α
ht : MeasurableSet t
⊢ (if a ∈ t ∧ a ∈ s then 1 else 0) = ↑↑(if a ∈ s then Measure.dirac a else 0) t
case h
α : Type u_1
mα : MeasurableSpace α
a : α
s : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
t : Set α
ht : MeasurableSet t
⊢ ↑↑(Measure.restrict (Measure.dirac a) s) t = ↑↑(if a ∈ s then Measure.dirac a else 0) t
simp only [Measure.restrict_apply ht, Measure.dirac_apply a, Set.indicator_apply,
  Set.mem_inter_iff, Pi.one_apply]
case pos
α : Type u_1
mα : MeasurableSpace α
a : α
s : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
t : Set α
ht : MeasurableSet t
has : a ∈ s
⊢ (if a ∈ t ∧ a ∈ s then 1 else 0) = ↑↑(if a ∈ s then Measure.dirac a else 0) t

case neg
α : Type u_1
mα : MeasurableSpace α
a : α
s : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
t : Set α
ht : MeasurableSet t
has : ¬a ∈ s
⊢ (if a ∈ t ∧ a ∈ s then 1 else 0) = ↑↑(if a ∈ s then Measure.dirac a else 0) t
case h
α : Type u_1
mα : MeasurableSpace α
a : α
s : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
t : Set α
ht : MeasurableSet t
⊢ (if a ∈ t ∧ a ∈ s then 1 else 0) = ↑↑(if a ∈ s then Measure.dirac a else 0) t
by_cases has : a ∈ s
case pos
α : Type u_1
mα : MeasurableSpace α
a : α
s : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
t : Set α
ht : MeasurableSet t
has : a ∈ s
⊢ (if a ∈ t then 1 else 0) = ↑↑(Measure.dirac a) t
case pos
α : Type u_1
mα : MeasurableSpace α
a : α
s : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
t : Set α
ht : MeasurableSet t
has : a ∈ s
⊢ (if a ∈ t ∧ a ∈ s then 1 else 0) = ↑↑(if a ∈ s then Measure.dirac a else 0) t
simp only [has, and_true_iff, if_true]
case pos.inl
α : Type u_1
mα : MeasurableSpace α
a : α
s : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
t : Set α
ht : MeasurableSet t
has : a ∈ s
hat : a ∈ t
⊢ 1 = ↑↑(Measure.dirac a) t

case pos.inr
α : Type u_1
mα : MeasurableSpace α
a : α
s : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
t : Set α
ht : MeasurableSet t
has : a ∈ s
hat : ¬a ∈ t
⊢ 0 = ↑↑(Measure.dirac a) t
case pos
α : Type u_1
mα : MeasurableSpace α
a : α
s : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
t : Set α
ht : MeasurableSet t
has : a ∈ s
⊢ (if a ∈ t then 1 else 0) = ↑↑(Measure.dirac a) t
split_ifs with hat
no goals
case pos.inl
α : Type u_1
mα : MeasurableSpace α
a : α
s : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
t : Set α
ht : MeasurableSet t
has : a ∈ s
hat : a ∈ t
⊢ 1 = ↑↑(Measure.dirac a) t
rw [Measure.dirac_apply_of_mem hat]
no goals
case pos.inr
α : Type u_1
mα : MeasurableSpace α
a : α
s : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
t : Set α
ht : MeasurableSet t
has : a ∈ s
hat : ¬a ∈ t
⊢ 0 = ↑↑(Measure.dirac a) t
simp only [Measure.dirac_apply' _ ht, Set.indicator_apply, hat, if_false]
no goals
case neg
α : Type u_1
mα : MeasurableSpace α
a : α
s : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
t : Set α
ht : MeasurableSet t
has : ¬a ∈ s
⊢ (if a ∈ t ∧ a ∈ s then 1 else 0) = ↑↑(if a ∈ s then Measure.dirac a else 0) t
simp only [has, and_false_iff, if_false, Measure.coe_zero, Pi.zero_apply]