α : Type u_1
β : Type ?u.948903
γ : Type ?u.948906
δ : Type ?u.948909
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ (⨆ (x : { i // ↑i ≤ fun a => indicator s f a }), SimpleFunc.lintegral (↑x) μ) =
    ⨆ (x : { i // ↑i ≤ fun a => f a }), SimpleFunc.lintegral (restrict (↑x) s) μ
α : Type u_1
β : Type ?u.948903
γ : Type ?u.948906
δ : Type ?u.948909
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ (∫⁻ (a : α), indicator s f a ∂μ) = ∫⁻ (a : α) in s, f a ∂μ
simp only [lintegral, ← restrict_lintegral_eq_lintegral_restrict _ hs, iSup_subtype']
case a
α : Type u_1
β : Type ?u.948903
γ : Type ?u.948906
δ : Type ?u.948909
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
φ : α →ₛ ℝ≥0∞
hφ : ↑φ ≤ fun a => indicator s f a
⊢ ∃ i', SimpleFunc.lintegral (↑{ val := φ, property := hφ }) μ ≤ SimpleFunc.lintegral (restrict (↑i') s) μ

case a
α : Type u_1
β : Type ?u.948903
γ : Type ?u.948906
δ : Type ?u.948909
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
φ : α →ₛ ℝ≥0∞
hφ : ↑φ ≤ fun a => f a
⊢ ∃ i', SimpleFunc.lintegral (restrict (↑{ val := φ, property := hφ }) s) μ ≤ SimpleFunc.lintegral (↑i') μ
α : Type u_1
β : Type ?u.948903
γ : Type ?u.948906
δ : Type ?u.948909
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ (⨆ (x : { i // ↑i ≤ fun a => indicator s f a }), SimpleFunc.lintegral (↑x) μ) =
    ⨆ (x : { i // ↑i ≤ fun a => f a }), SimpleFunc.lintegral (restrict (↑x) s) μ
apply le_antisymm <;> refine' iSup_mono' (Subtype.forall.2 fun φ hφ => _)
case a
α : Type u_1
β : Type ?u.948903
γ : Type ?u.948906
δ : Type ?u.948909
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
φ : α →ₛ ℝ≥0∞
hφ : ↑φ ≤ fun a => indicator s f a
⊢ SimpleFunc.lintegral (↑{ val := φ, property := hφ }) μ ≤
    SimpleFunc.lintegral (restrict (↑{ val := φ, property := (_ : ↑φ ≤ fun a => f a) }) s) μ
case a
α : Type u_1
β : Type ?u.948903
γ : Type ?u.948906
δ : Type ?u.948909
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
φ : α →ₛ ℝ≥0∞
hφ : ↑φ ≤ fun a => indicator s f a
⊢ ∃ i', SimpleFunc.lintegral (↑{ val := φ, property := hφ }) μ ≤ SimpleFunc.lintegral (restrict (↑i') s) μ
refine' ⟨⟨φ, le_trans hφ (indicator_le_self _ _)⟩, _⟩
case a
α : Type u_1
β : Type ?u.948903
γ : Type ?u.948906
δ : Type ?u.948909
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
φ : α →ₛ ℝ≥0∞
hφ : ↑φ ≤ fun a => indicator s f a
x : α
⊢ ↑↑{ val := φ, property := hφ } x ≤ ↑(restrict (↑{ val := φ, property := (_ : ↑φ ≤ fun a => f a) }) s) x
case a
α : Type u_1
β : Type ?u.948903
γ : Type ?u.948906
δ : Type ?u.948909
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
φ : α →ₛ ℝ≥0∞
hφ : ↑φ ≤ fun a => indicator s f a
⊢ SimpleFunc.lintegral (↑{ val := φ, property := hφ }) μ ≤
    SimpleFunc.lintegral (restrict (↑{ val := φ, property := (_ : ↑φ ≤ fun a => f a) }) s) μ
refine' SimpleFunc.lintegral_mono (fun x => _) le_rfl
case pos
α : Type u_1
β : Type ?u.948903
γ : Type ?u.948906
δ : Type ?u.948909
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
φ : α →ₛ ℝ≥0∞
hφ : ↑φ ≤ fun a => indicator s f a
x : α
hx : x ∈ s
⊢ ↑↑{ val := φ, property := hφ } x ≤ ↑(restrict (↑{ val := φ, property := (_ : ↑φ ≤ fun a => f a) }) s) x

case neg
α : Type u_1
β : Type ?u.948903
γ : Type ?u.948906
δ : Type ?u.948909
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
φ : α →ₛ ℝ≥0∞
hφ : ↑φ ≤ fun a => indicator s f a
x : α
hx : ¬x ∈ s
⊢ ↑↑{ val := φ, property := hφ } x ≤ ↑(restrict (↑{ val := φ, property := (_ : ↑φ ≤ fun a => f a) }) s) x
case a
α : Type u_1
β : Type ?u.948903
γ : Type ?u.948906
δ : Type ?u.948909
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
φ : α →ₛ ℝ≥0∞
hφ : ↑φ ≤ fun a => indicator s f a
x : α
⊢ ↑↑{ val := φ, property := hφ } x ≤ ↑(restrict (↑{ val := φ, property := (_ : ↑φ ≤ fun a => f a) }) s) x
by_cases hx : x ∈ s
no goals
case pos
α : Type u_1
β : Type ?u.948903
γ : Type ?u.948906
δ : Type ?u.948909
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
φ : α →ₛ ℝ≥0∞
hφ : ↑φ ≤ fun a => indicator s f a
x : α
hx : x ∈ s
⊢ ↑↑{ val := φ, property := hφ } x ≤ ↑(restrict (↑{ val := φ, property := (_ : ↑φ ≤ fun a => f a) }) s) x
simp [hx, hs, le_refl]
case neg
α : Type u_1
β : Type ?u.948903
γ : Type ?u.948906
δ : Type ?u.948909
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
φ : α →ₛ ℝ≥0∞
hφ : ↑φ ≤ fun a => indicator s f a
x : α
hx : ¬x ∈ s
⊢ (fun a => indicator s f a) x ≤ ↑(restrict (↑{ val := φ, property := (_ : ↑φ ≤ fun a => f a) }) s) x
case neg
α : Type u_1
β : Type ?u.948903
γ : Type ?u.948906
δ : Type ?u.948909
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
φ : α →ₛ ℝ≥0∞
hφ : ↑φ ≤ fun a => indicator s f a
x : α
hx : ¬x ∈ s
⊢ ↑↑{ val := φ, property := hφ } x ≤ ↑(restrict (↑{ val := φ, property := (_ : ↑φ ≤ fun a => f a) }) s) x
apply le_trans (hφ x)
no goals
case neg
α : Type u_1
β : Type ?u.948903
γ : Type ?u.948906
δ : Type ?u.948909
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
φ : α →ₛ ℝ≥0∞
hφ : ↑φ ≤ fun a => indicator s f a
x : α
hx : ¬x ∈ s
⊢ (fun a => indicator s f a) x ≤ ↑(restrict (↑{ val := φ, property := (_ : ↑φ ≤ fun a => f a) }) s) x
simp [hx, hs, le_refl]
case a
α : Type u_1
β : Type ?u.948903
γ : Type ?u.948906
δ : Type ?u.948909
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
φ : α →ₛ ℝ≥0∞
hφ : ↑φ ≤ fun a => f a
x : α
⊢ ↑(restrict φ s) x ≤ (fun a => indicator s f a) x
case a
α : Type u_1
β : Type ?u.948903
γ : Type ?u.948906
δ : Type ?u.948909
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
φ : α →ₛ ℝ≥0∞
hφ : ↑φ ≤ fun a => f a
⊢ ∃ i', SimpleFunc.lintegral (restrict (↑{ val := φ, property := hφ }) s) μ ≤ SimpleFunc.lintegral (↑i') μ
refine' ⟨⟨φ.restrict s, fun x => _⟩, le_rfl⟩
no goals
case a
α : Type u_1
β : Type ?u.948903
γ : Type ?u.948906
δ : Type ?u.948909
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
φ : α →ₛ ℝ≥0∞
hφ : ↑φ ≤ fun a => f a
x : α
⊢ ↑(restrict φ s) x ≤ (fun a => indicator s f a) x
simp [hφ x, hs, indicator_le_indicator]