case h.e'_4.h.e'_4.h
α : Type u_1
β : Type ?u.5010653
E✝ : Type ?u.5010656
F : Type ?u.5010659
inst✝² : MeasurableSpace α
ι : Type ?u.5010665
inst✝¹ : NormedAddCommGroup E✝
inst✝ : PseudoEMetricSpace α
μ : MeasureTheory.Measure α
E : Set α
E_mble : MeasurableSet E
δ : ℝ
δ_pos : 0 < δ
x✝ : α
⊢ ↑(↑(thickenedIndicator δ_pos E) x✝) = thickenedIndicatorAux δ E x✝
α : Type u_1
β : Type ?u.5010653
E✝ : Type ?u.5010656
F : Type ?u.5010659
inst✝² : MeasurableSpace α
ι : Type ?u.5010665
inst✝¹ : NormedAddCommGroup E✝
inst✝ : PseudoEMetricSpace α
μ : MeasureTheory.Measure α
E : Set α
E_mble : MeasurableSet E
δ : ℝ
δ_pos : 0 < δ
⊢ ↑↑μ E ≤ ∫⁻ (a : α), ↑(↑(thickenedIndicator δ_pos E) a) ∂μ
convert measure_le_lintegral_thickenedIndicatorAux μ E_mble δ
case h.e'_4.h.e'_4.h
α : Type u_1
β : Type ?u.5010653
E✝ : Type ?u.5010656
F : Type ?u.5010659
inst✝² : MeasurableSpace α
ι : Type ?u.5010665
inst✝¹ : NormedAddCommGroup E✝
inst✝ : PseudoEMetricSpace α
μ : MeasureTheory.Measure α
E : Set α
E_mble : MeasurableSet E
δ : ℝ
δ_pos : 0 < δ
x✝ : α
⊢ ↑(ENNReal.toNNReal (thickenedIndicatorAux δ E x✝)) = thickenedIndicatorAux δ E x✝
case h.e'_4.h.e'_4.h
α : Type u_1
β : Type ?u.5010653
E✝ : Type ?u.5010656
F : Type ?u.5010659
inst✝² : MeasurableSpace α
ι : Type ?u.5010665
inst✝¹ : NormedAddCommGroup E✝
inst✝ : PseudoEMetricSpace α
μ : MeasureTheory.Measure α
E : Set α
E_mble : MeasurableSet E
δ : ℝ
δ_pos : 0 < δ
x✝ : α
⊢ ↑(↑(thickenedIndicator δ_pos E) x✝) = thickenedIndicatorAux δ E x✝
dsimp
no goals
case h.e'_4.h.e'_4.h
α : Type u_1
β : Type ?u.5010653
E✝ : Type ?u.5010656
F : Type ?u.5010659
inst✝² : MeasurableSpace α
ι : Type ?u.5010665
inst✝¹ : NormedAddCommGroup E✝
inst✝ : PseudoEMetricSpace α
μ : MeasureTheory.Measure α
E : Set α
E_mble : MeasurableSet E
δ : ℝ
δ_pos : 0 < δ
x✝ : α
⊢ ↑(ENNReal.toNNReal (thickenedIndicatorAux δ E x✝)) = thickenedIndicatorAux δ E x✝
simp only [thickenedIndicatorAux_lt_top.ne, ENNReal.coe_toNNReal, Ne.def, not_false_iff]