case h
α : Type u_1
β : Type ?u.331505
γ : Type ?u.331508
δ : Type ?u.331511
ι : Type ?u.331514
R : Type ?u.331517
R' : Type ?u.331520
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : MeasurableSpace α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
⊢ ↑↑(restrict μ {a}) s = ↑↑(↑↑μ {a} • dirac a) s
α : Type u_1
β : Type ?u.331505
γ : Type ?u.331508
δ : Type ?u.331511
ι : Type ?u.331514
R : Type ?u.331517
R' : Type ?u.331520
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : MeasurableSpace α
μ : Measure α
a : α
⊢ restrict μ {a} = ↑↑μ {a} • dirac a
ext1 s hs
case pos
α : Type u_1
β : Type ?u.331505
γ : Type ?u.331508
δ : Type ?u.331511
ι : Type ?u.331514
R : Type ?u.331517
R' : Type ?u.331520
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : MeasurableSpace α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : a ∈ s
⊢ ↑↑(restrict μ {a}) s = ↑↑(↑↑μ {a} • dirac a) s

case neg
α : Type u_1
β : Type ?u.331505
γ : Type ?u.331508
δ : Type ?u.331511
ι : Type ?u.331514
R : Type ?u.331517
R' : Type ?u.331520
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : MeasurableSpace α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : ¬a ∈ s
⊢ ↑↑(restrict μ {a}) s = ↑↑(↑↑μ {a} • dirac a) s
case h
α : Type u_1
β : Type ?u.331505
γ : Type ?u.331508
δ : Type ?u.331511
ι : Type ?u.331514
R : Type ?u.331517
R' : Type ?u.331520
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : MeasurableSpace α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
⊢ ↑↑(restrict μ {a}) s = ↑↑(↑↑μ {a} • dirac a) s
by_cases ha : a ∈ s
case pos
α : Type u_1
β : Type ?u.331505
γ : Type ?u.331508
δ : Type ?u.331511
ι : Type ?u.331514
R : Type ?u.331517
R' : Type ?u.331520
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : MeasurableSpace α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : a ∈ s
this : s ∩ {a} = {a}
⊢ ↑↑(restrict μ {a}) s = ↑↑(↑↑μ {a} • dirac a) s
case pos
α : Type u_1
β : Type ?u.331505
γ : Type ?u.331508
δ : Type ?u.331511
ι : Type ?u.331514
R : Type ?u.331517
R' : Type ?u.331520
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : MeasurableSpace α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : a ∈ s
⊢ ↑↑(restrict μ {a}) s = ↑↑(↑↑μ {a} • dirac a) s
have : s ∩ {a} = {a} := by simpa
no goals
case pos
α : Type u_1
β : Type ?u.331505
γ : Type ?u.331508
δ : Type ?u.331511
ι : Type ?u.331514
R : Type ?u.331517
R' : Type ?u.331520
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : MeasurableSpace α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : a ∈ s
this : s ∩ {a} = {a}
⊢ ↑↑(restrict μ {a}) s = ↑↑(↑↑μ {a} • dirac a) s
simp [*]
no goals
α : Type u_1
β : Type ?u.331505
γ : Type ?u.331508
δ : Type ?u.331511
ι : Type ?u.331514
R : Type ?u.331517
R' : Type ?u.331520
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : MeasurableSpace α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : a ∈ s
⊢ s ∩ {a} = {a}
simpa
case neg
α : Type u_1
β : Type ?u.331505
γ : Type ?u.331508
δ : Type ?u.331511
ι : Type ?u.331514
R : Type ?u.331517
R' : Type ?u.331520
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : MeasurableSpace α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : ¬a ∈ s
this : s ∩ {a} = ∅
⊢ ↑↑(restrict μ {a}) s = ↑↑(↑↑μ {a} • dirac a) s
case neg
α : Type u_1
β : Type ?u.331505
γ : Type ?u.331508
δ : Type ?u.331511
ι : Type ?u.331514
R : Type ?u.331517
R' : Type ?u.331520
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : MeasurableSpace α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : ¬a ∈ s
⊢ ↑↑(restrict μ {a}) s = ↑↑(↑↑μ {a} • dirac a) s
have : s ∩ {a} = ∅ := inter_singleton_eq_empty.2 ha
no goals
case neg
α : Type u_1
β : Type ?u.331505
γ : Type ?u.331508
δ : Type ?u.331511
ι : Type ?u.331514
R : Type ?u.331517
R' : Type ?u.331520
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : MeasurableSpace α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : ¬a ∈ s
this : s ∩ {a} = ∅
⊢ ↑↑(restrict μ {a}) s = ↑↑(↑↑μ {a} • dirac a) s
simp [*]