-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_indicator_le (f : α → ℝ≥0∞) (s : Set α) :
    ∫⁻ a, s.indicator f a ∂μ ≤ ∫⁻ a in s, f a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : ⇑g ≤ fun a => s.indicator f a
this : ⇑g ≤ f
⊢ g.lintegral μ = g.lintegral (μ.restrict s)

Tactic:
rw [lintegral_restrict, SimpleFunc.lintegral]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : ⇑g ≤ fun a => s.indicator f a
this : ⇑g ≤ f
⊢ ∑ x ∈ g.range, x * μ (⇑g ⁻¹' {x}) = ∑ y ∈ g.range, y * μ (⇑g ⁻¹' {y} ∩ s)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : ⇑g ≤ fun a => s.indicator f a
⊢ g.lintegral μ ≤ ⨆ g, ⨆ (_ : ⇑g ≤ fun a => f a), g.lintegral (μ.restrict s)

Tactic:
have : g ≤ f := hg.trans (indicator_le_self s f)

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : ⇑g ≤ fun a => s.indicator f a
this : ⇑g ≤ f
⊢ g.lintegral μ ≤ ⨆ g, ⨆ (_ : ⇑g ≤ fun a => f a), g.lintegral (μ.restrict s)

Proof state:
case neg.e_a.h.e_6.h.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : ⇑g ≤ fun a => s.indicator f a
this : ⇑g ≤ f
x : α
H : x ∉ s
⊢ g x = 0

Tactic:
simpa [H] using hg x

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : ⇑g ≤ fun a => s.indicator f a
this : ⇑g ≤ f
⊢ ∑ x ∈ g.range, x * μ (⇑g ⁻¹' {x}) = ∑ y ∈ g.range, y * μ (⇑g ⁻¹' {y} ∩ s)

Tactic:
congr with t

Result:
case e_f.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : ⇑g ≤ fun a => s.indicator f a
this : ⇑g ≤ f
t : ℝ≥0∞
⊢ t * μ (⇑g ⁻¹' {t}) = t * μ (⇑g ⁻¹' {t} ∩ s)

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : ⇑g ≤ fun a => s.indicator f a
this : ⇑g ≤ f
t : ℝ≥0∞
H : t = 0
⊢ t * μ (⇑g ⁻¹' {t}) = t * μ (⇑g ⁻¹' {t} ∩ s)

Tactic:
simp [H]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
⊢ ∫⁻ (a : α), s.indicator f a ∂μ ≤ ∫⁻ (a : α) in s, f a ∂μ

Tactic:
simp only [lintegral]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
⊢ ⨆ g, ⨆ (_ : ⇑g ≤ fun a => s.indicator f a), g.lintegral μ ≤ ⨆ g, ⨆ (_ : ⇑g ≤ fun a => f a), g.lintegral (μ.restrict s)

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : ⇑g ≤ fun a => s.indicator f a
this : ⇑g ≤ f
t : ℝ≥0∞
H : ¬t = 0
⊢ t * μ (⇑g ⁻¹' {t}) = t * μ (⇑g ⁻¹' {t} ∩ s)

Tactic:
congr with x

Result:
case neg.e_a.h.e_6.h.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : ⇑g ≤ fun a => s.indicator f a
this : ⇑g ≤ f
t : ℝ≥0∞
H : ¬t = 0
x : α
⊢ x ∈ ⇑g ⁻¹' {t} ↔ x ∈ ⇑g ⁻¹' {t} ∩ s

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : ⇑g ≤ fun a => s.indicator f a
this : ⇑g ≤ f
⊢ g.lintegral μ ≤ ⨆ g, ⨆ (_ : ⇑g ≤ fun a => f a), g.lintegral (μ.restrict s)

Tactic:
refine le_iSup_of_le g (le_iSup_of_le this (le_of_eq ?_))

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : ⇑g ≤ fun a => s.indicator f a
this : ⇑g ≤ f
⊢ g.lintegral μ = g.lintegral (μ.restrict s)

Proof state:
case e_f.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : ⇑g ≤ fun a => s.indicator f a
this : ⇑g ≤ f
t : ℝ≥0∞
⊢ t * μ (⇑g ⁻¹' {t}) = t * μ (⇑g ⁻¹' {t} ∩ s)

Tactic:
by_cases H : t = 0

Result:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : ⇑g ≤ fun a => s.indicator f a
this : ⇑g ≤ f
t : ℝ≥0∞
H : t = 0
⊢ t * μ (⇑g ⁻¹' {t}) = t * μ (⇑g ⁻¹' {t} ∩ s)

case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : ⇑g ≤ fun a => s.indicator f a
this : ⇑g ≤ f
t : ℝ≥0∞
H : ¬t = 0
⊢ t * μ (⇑g ⁻¹' {t}) = t * μ (⇑g ⁻¹' {t} ∩ s)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
⊢ ⨆ g, ⨆ (_ : ⇑g ≤ fun a => s.indicator f a), g.lintegral μ ≤ ⨆ g, ⨆ (_ : ⇑g ≤ fun a => f a), g.lintegral (μ.restrict s)

Tactic:
apply iSup_le (fun g ↦ (iSup_le (fun hg ↦ ?_)))

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : ⇑g ≤ fun a => s.indicator f a
⊢ g.lintegral μ ≤ ⨆ g, ⨆ (_ : ⇑g ≤ fun a => f a), g.lintegral (μ.restrict s)

Proof state:
case neg.e_a.h.e_6.h.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : ⇑g ≤ fun a => s.indicator f a
this : ⇑g ≤ f
t : ℝ≥0∞
H : ¬t = 0
x : α
⊢ g x = t → x ∈ s

Tactic:
rintro rfl

Result:
case neg.e_a.h.e_6.h.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : ⇑g ≤ fun a => s.indicator f a
this : ⇑g ≤ f
x : α
H : ¬g x = 0
⊢ x ∈ s

Proof state:
case neg.e_a.h.e_6.h.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : ⇑g ≤ fun a => s.indicator f a
this : ⇑g ≤ f
x : α
H : ¬g x = 0
⊢ x ∈ s

Tactic:
contrapose! H

Result:
case neg.e_a.h.e_6.h.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : ⇑g ≤ fun a => s.indicator f a
this : ⇑g ≤ f
x : α
H : x ∉ s
⊢ g x = 0

Proof state:
case neg.e_a.h.e_6.h.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : ⇑g ≤ fun a => s.indicator f a
this : ⇑g ≤ f
t : ℝ≥0∞
H : ¬t = 0
x : α
⊢ x ∈ ⇑g ⁻¹' {t} ↔ x ∈ ⇑g ⁻¹' {t} ∩ s

Tactic:
simp only [mem_preimage, mem_singleton_iff, mem_inter_iff, iff_self_and]

Result:
case neg.e_a.h.e_6.h.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : ⇑g ≤ fun a => s.indicator f a
this : ⇑g ≤ f
t : ℝ≥0∞
H : ¬t = 0
x : α
⊢ g x = t → x ∈ s