-- 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 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 ≤ 0

Tactic:
rfl

Result:
no goals

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 ≤ Integrable.toL1 f hfi

Tactic:
rw [← Lp.coeFn_le]

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 ≤ᶠ[ae μ] ↑↑(Integrable.toL1 f hfi)

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 μ
h0 : ↑↑0 =ᶠ[ae μ] 0
⊢ ↑↑0 ≤ᶠ[ae μ] ↑↑(Integrable.toL1 f hfi)

Tactic:
have h := Integrable.coeFn_toL1 hfi

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
h : ↑↑(Integrable.toL1 f hfi) =ᶠ[ae μ] f
⊢ ↑↑0 ≤ᶠ[ae μ] ↑↑(Integrable.toL1 f hfi)

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 ≤ setToFun μ T hT f

Tactic:
simp_rw [setToFun_eq _ hfi]

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 ≤ (L1.setToL1 hT) (Integrable.toL1 f hfi)

Proof state:
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

Tactic:
simp_rw [setToFun_undef _ hfi]

Result:
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 ≤ 0

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 μ
h0 : ↑↑0 =ᶠ[ae μ] 0
h : ↑↑(Integrable.toL1 f hfi) =ᶠ[ae μ] f
⊢ ↑↑0 ≤ᶠ[ae μ] ↑↑(Integrable.toL1 f hfi)

Tactic:
filter_upwards [h0, h, hf] with _ h0a ha hfa

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✝ ≤ ↑↑(Integrable.toL1 f hfi) 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 ≤ (L1.setToL1 hT) (Integrable.toL1 f hfi)

Tactic:
refine L1.setToL1_nonneg hT hT_nonneg ?_

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 ≤ Integrable.toL1 f hfi