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

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

Tactic:
simp_rw [setToFun_undef _ hf]

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

Proof state:
case pos
α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
G'' : Type u_8
inst✝² : NormedLatticeAddCommGroup G''
inst✝¹ : NormedSpace ℝ G''
inst✝ : CompleteSpace G''
T T' : Set α → E →L[ℝ] G''
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x
f : α → E
hf : Integrable f μ
⊢ setToFun μ T hT f ≤ setToFun μ T' hT' f

Tactic:
simp_rw [setToFun_eq _ hf]

Result:
case pos
α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
G'' : Type u_8
inst✝² : NormedLatticeAddCommGroup G''
inst✝¹ : NormedSpace ℝ G''
inst✝ : CompleteSpace G''
T T' : Set α → E →L[ℝ] G''
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x
f : α → E
hf : Integrable f μ
⊢ (L1.setToL1 hT) (Integrable.toL1 f hf) ≤ (L1.setToL1 hT') (Integrable.toL1 f hf)

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

Tactic:
by_cases hf : Integrable f μ

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

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

Proof state:
case pos
α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
G'' : Type u_8
inst✝² : NormedLatticeAddCommGroup G''
inst✝¹ : NormedSpace ℝ G''
inst✝ : CompleteSpace G''
T T' : Set α → E →L[ℝ] G''
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x
f : α → E
hf : Integrable f μ
⊢ (L1.setToL1 hT) (Integrable.toL1 f hf) ≤ (L1.setToL1 hT') (Integrable.toL1 f hf)

Tactic:
exact L1.setToL1_mono_left' hT hT' hTT' _

Result:
no goals

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

Tactic:
rfl

Result:
no goals