case pos
α : Type u_1
β : Type ?u.327267
γ : Type ?u.327270
δ : Type ?u.327273
ι : Type ?u.327276
R : Type ?u.327279
R' : Type ?u.327282
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : a ∈ s
⊢ ↑↑(dirac a) s = indicator s 1 a

case neg
α : Type u_1
β : Type ?u.327267
γ : Type ?u.327270
δ : Type ?u.327273
ι : Type ?u.327276
R : Type ?u.327279
R' : Type ?u.327282
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : ¬a ∈ s
⊢ ↑↑(dirac a) s = indicator s 1 a
α : Type u_1
β : Type ?u.327267
γ : Type ?u.327270
δ : Type ?u.327273
ι : Type ?u.327276
R : Type ?u.327279
R' : Type ?u.327282
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
⊢ ↑↑(dirac a) s = indicator s 1 a
by_cases h : a ∈ s
case neg
α : Type u_1
β : Type ?u.327267
γ : Type ?u.327270
δ : Type ?u.327273
ι : Type ?u.327276
R : Type ?u.327279
R' : Type ?u.327282
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : ¬a ∈ s
⊢ ↑↑(dirac a) s ≤ 0
case neg
α : Type u_1
β : Type ?u.327267
γ : Type ?u.327270
δ : Type ?u.327273
ι : Type ?u.327276
R : Type ?u.327279
R' : Type ?u.327282
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : ¬a ∈ s
⊢ ↑↑(dirac a) s = indicator s 1 a
rw [indicator_of_not_mem h, ← nonpos_iff_eq_zero]
no goals
case neg
α : Type u_1
β : Type ?u.327267
γ : Type ?u.327270
δ : Type ?u.327273
ι : Type ?u.327276
R : Type ?u.327279
R' : Type ?u.327282
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : ¬a ∈ s
⊢ ↑↑(dirac a) s ≤ 0
calc
  dirac a s ≤ dirac a ({a}ᶜ) := measure_mono (subset_compl_comm.1 <| singleton_subset_iff.2 h)
  _ = 0 := by simp [dirac_apply' _ (measurableSet_singleton _).compl]
no goals
case pos
α : Type u_1
β : Type ?u.327267
γ : Type ?u.327270
δ : Type ?u.327273
ι : Type ?u.327276
R : Type ?u.327279
R' : Type ?u.327282
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : a ∈ s
⊢ ↑↑(dirac a) s = indicator s 1 a
rw [dirac_apply_of_mem h, indicator_of_mem h, Pi.one_apply]
no goals
α : Type u_1
β : Type ?u.327267
γ : Type ?u.327270
δ : Type ?u.327273
ι : Type ?u.327276
R : Type ?u.327279
R' : Type ?u.327282
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : ¬a ∈ s
⊢ ↑↑(dirac a) ({a}ᶜ) = 0
simp [dirac_apply' _ (measurableSet_singleton _).compl]