-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToSimpleFunc_mono_left' (T T' : Set α → E →L[ℝ] G'')
    (hTT' : ∀ s, MeasurableSet s → μ s < ∞ → ∀ x, T s x ≤ T' s x) (f : α →ₛ E)
    (hf : Integrable f μ) : setToSimpleFunc T f ≤ setToSimpleFunc T' f

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''
T T' : Set α → E →L[ℝ] G''
hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ setToSimpleFunc T f ≤ setToSimpleFunc T' f

Tactic:
refine sum_le_sum fun i _ => ?_

Result:
α : 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''
T T' : Set α → E →L[ℝ] G''
hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x
f : α →ₛ E
hf : Integrable (⇑f) μ
i : E
x✝ : i ∈ f.range
⊢ (T (⇑f ⁻¹' {i})) i ≤ (T' (⇑f ⁻¹' {i})) i

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''
T T' : Set α → E →L[ℝ] G''
hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x
f : α →ₛ E
hf : Integrable (⇑f) μ
i : E
x✝ : i ∈ f.range
h0 : ¬i = 0
⊢ (T (⇑f ⁻¹' {i})) i ≤ (T' (⇑f ⁻¹' {i})) i

Tactic:
exact hTT' _ (measurableSet_fiber _ _) (measure_preimage_lt_top_of_integrable _ hf h0) i

Result:
no goals

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''
T T' : Set α → E →L[ℝ] G''
hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x
f : α →ₛ E
hf : Integrable (⇑f) μ
i : E
x✝ : i ∈ f.range
h0 : i = 0
⊢ (T (⇑f ⁻¹' {i})) i ≤ (T' (⇑f ⁻¹' {i})) i

Tactic:
simp [h0]

Result:
no goals

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''
T T' : Set α → E →L[ℝ] G''
hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x
f : α →ₛ E
hf : Integrable (⇑f) μ
i : E
x✝ : i ∈ f.range
⊢ (T (⇑f ⁻¹' {i})) i ≤ (T' (⇑f ⁻¹' {i})) i

Tactic:
by_cases h0 : i = 0

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''
T T' : Set α → E →L[ℝ] G''
hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x
f : α →ₛ E
hf : Integrable (⇑f) μ
i : E
x✝ : i ∈ f.range
h0 : i = 0
⊢ (T (⇑f ⁻¹' {i})) i ≤ (T' (⇑f ⁻¹' {i})) i

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''
T T' : Set α → E →L[ℝ] G''
hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x
f : α →ₛ E
hf : Integrable (⇑f) μ
i : E
x✝ : i ∈ f.range
h0 : ¬i = 0
⊢ (T (⇑f ⁻¹' {i})) i ≤ (T' (⇑f ⁻¹' {i})) i