-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToFun_nonneg {T : Set α → G' →L[ℝ] G''} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C)
    (hT_nonneg : ∀ s, MeasurableSet s → μ s < ∞ → ∀ x, 0 ≤ x → 0 ≤ T s x) {f : α → G'}
    (hf : 0 ≤ᵐ[μ] f) : 0 ≤ setToFun μ T hT f

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst✝⁴ : NormedLatticeAddCommGroup G''
inst✝³ : NormedSpace ℝ G''
inst✝² : CompleteSpace G''
inst✝¹ : NormedLatticeAddCommGroup G'
inst✝ : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
C : ℝ
hT : DominatedFinMeasAdditive μ T C
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f : α → G'
hf : 0 ≤ᶠ[ae μ] f
hfi : Integrable f μ
h0 : ↑↑0 =ᶠ[ae μ] 0
h : ↑↑(Integrable.toL1 f hfi) =ᶠ[ae μ] f
a✝ : α
h0a : ↑↑0 a✝ = 0 a✝
ha : ↑↑(Integrable.toL1 f hfi) a✝ = f a✝
hfa : 0 a✝ ≤ f a✝
⊢ ↑↑0 a✝ ≤ ↑↑(Integrable.toL1 f hfi) a✝

Tactic:
rw [h0a, ha]

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst✝⁴ : NormedLatticeAddCommGroup G''
inst✝³ : NormedSpace ℝ G''
inst✝² : CompleteSpace G''
inst✝¹ : NormedLatticeAddCommGroup G'
inst✝ : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
C : ℝ
hT : DominatedFinMeasAdditive μ T C
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f : α → G'
hf : 0 ≤ᶠ[ae μ] f
hfi : Integrable f μ
h0 : ↑↑0 =ᶠ[ae μ] 0
h : ↑↑(Integrable.toL1 f hfi) =ᶠ[ae μ] f
a✝ : α
h0a : ↑↑0 a✝ = 0 a✝
ha : ↑↑(Integrable.toL1 f hfi) a✝ = f a✝
hfa : 0 a✝ ≤ f a✝
⊢ 0 a✝ ≤ f a✝

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst✝⁴ : NormedLatticeAddCommGroup G''
inst✝³ : NormedSpace ℝ G''
inst✝² : CompleteSpace G''
inst✝¹ : NormedLatticeAddCommGroup G'
inst✝ : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
C : ℝ
hT : DominatedFinMeasAdditive μ T C
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f : α → G'
hf : 0 ≤ᶠ[ae μ] f
hfi : Integrable f μ
⊢ ↑↑0 ≤ᶠ[ae μ] ↑↑(Integrable.toL1 f hfi)

Tactic:
have h0 := Lp.coeFn_zero G' 1 μ

Result:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst✝⁴ : NormedLatticeAddCommGroup G''
inst✝³ : NormedSpace ℝ G''
inst✝² : CompleteSpace G''
inst✝¹ : NormedLatticeAddCommGroup G'
inst✝ : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
C : ℝ
hT : DominatedFinMeasAdditive μ T C
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f : α → G'
hf : 0 ≤ᶠ[ae μ] f
hfi : Integrable f μ
h0 : ↑↑0 =ᶠ[ae μ] 0
⊢ ↑↑0 ≤ᶠ[ae μ] ↑↑(Integrable.toL1 f hfi)

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst✝⁴ : NormedLatticeAddCommGroup G''
inst✝³ : NormedSpace ℝ G''
inst✝² : CompleteSpace G''
inst✝¹ : NormedLatticeAddCommGroup G'
inst✝ : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
C : ℝ
hT : DominatedFinMeasAdditive μ T C
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f : α → G'
hf : 0 ≤ᶠ[ae μ] f
hfi : Integrable f μ
h0 : ↑↑0 =ᶠ[ae μ] 0
h : ↑↑(Integrable.toL1 f hfi) =ᶠ[ae μ] f
a✝ : α
h0a : ↑↑0 a✝ = 0 a✝
ha : ↑↑(Integrable.toL1 f hfi) a✝ = f a✝
hfa : 0 a✝ ≤ f a✝
⊢ 0 a✝ ≤ f a✝

Tactic:
exact hfa

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst✝⁴ : NormedLatticeAddCommGroup G''
inst✝³ : NormedSpace ℝ G''
inst✝² : CompleteSpace G''
inst✝¹ : NormedLatticeAddCommGroup G'
inst✝ : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
C : ℝ
hT : DominatedFinMeasAdditive μ T C
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f : α → G'
hf : 0 ≤ᶠ[ae μ] f
⊢ 0 ≤ setToFun μ T hT f

Tactic:
by_cases hfi : Integrable f μ

Result:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst✝⁴ : NormedLatticeAddCommGroup G''
inst✝³ : NormedSpace ℝ G''
inst✝² : CompleteSpace G''
inst✝¹ : NormedLatticeAddCommGroup G'
inst✝ : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
C : ℝ
hT : DominatedFinMeasAdditive μ T C
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f : α → G'
hf : 0 ≤ᶠ[ae μ] f
hfi : Integrable f μ
⊢ 0 ≤ setToFun μ T hT f

case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst✝⁴ : NormedLatticeAddCommGroup G''
inst✝³ : NormedSpace ℝ G''
inst✝² : CompleteSpace G''
inst✝¹ : NormedLatticeAddCommGroup G'
inst✝ : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
C : ℝ
hT : DominatedFinMeasAdditive μ T C
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f : α → G'
hf : 0 ≤ᶠ[ae μ] f
hfi : ¬Integrable f μ
⊢ 0 ≤ setToFun μ T hT f