α : Type u_1
E : Type ?u.361138
F : Type ?u.361141
F' : Type ?u.361144
G : Type ?u.361147
𝕜 : Type ?u.361150
p : ℝ≥0∞
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup F'
inst✝⁵ : NormedSpace ℝ F'
inst✝⁴ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
G' : Type u_2
G'' : Type u_3
inst✝³ : NormedLatticeAddCommGroup G''
inst✝² : NormedSpace ℝ G''
inst✝¹ : NormedLatticeAddCommGroup G'
inst✝ : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
hT_nonneg : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ ↑(T s) x
f : α →ₛ G'
hf : 0 ≤ f
hfi : Integrable ↑f
i : G'
hi : i ∈ SimpleFunc.range f
⊢ 0 ≤ ↑(T (↑f ⁻¹' {i})) i
α : Type u_1
E : Type ?u.361138
F : Type ?u.361141
F' : Type ?u.361144
G : Type ?u.361147
𝕜 : Type ?u.361150
p : ℝ≥0∞
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup F'
inst✝⁵ : NormedSpace ℝ F'
inst✝⁴ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
G' : Type u_2
G'' : Type u_3
inst✝³ : NormedLatticeAddCommGroup G''
inst✝² : NormedSpace ℝ G''
inst✝¹ : NormedLatticeAddCommGroup G'
inst✝ : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
hT_nonneg : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ ↑(T s) x
f : α →ₛ G'
hf : 0 ≤ f
hfi : Integrable ↑f
⊢ 0 ≤ setToSimpleFunc T f
refine' sum_nonneg fun i hi => _
case pos
α : Type u_1
E : Type ?u.361138
F : Type ?u.361141
F' : Type ?u.361144
G : Type ?u.361147
𝕜 : Type ?u.361150
p : ℝ≥0∞
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup F'
inst✝⁵ : NormedSpace ℝ F'
inst✝⁴ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
G' : Type u_2
G'' : Type u_3
inst✝³ : NormedLatticeAddCommGroup G''
inst✝² : NormedSpace ℝ G''
inst✝¹ : NormedLatticeAddCommGroup G'
inst✝ : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
hT_nonneg : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ ↑(T s) x
f : α →ₛ G'
hf : 0 ≤ f
hfi : Integrable ↑f
i : G'
hi : i ∈ SimpleFunc.range f
h0 : i = 0
⊢ 0 ≤ ↑(T (↑f ⁻¹' {i})) i

case neg
α : Type u_1
E : Type ?u.361138
F : Type ?u.361141
F' : Type ?u.361144
G : Type ?u.361147
𝕜 : Type ?u.361150
p : ℝ≥0∞
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup F'
inst✝⁵ : NormedSpace ℝ F'
inst✝⁴ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
G' : Type u_2
G'' : Type u_3
inst✝³ : NormedLatticeAddCommGroup G''
inst✝² : NormedSpace ℝ G''
inst✝¹ : NormedLatticeAddCommGroup G'
inst✝ : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
hT_nonneg : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ ↑(T s) x
f : α →ₛ G'
hf : 0 ≤ f
hfi : Integrable ↑f
i : G'
hi : i ∈ SimpleFunc.range f
h0 : ¬i = 0
⊢ 0 ≤ ↑(T (↑f ⁻¹' {i})) i
α : Type u_1
E : Type ?u.361138
F : Type ?u.361141
F' : Type ?u.361144
G : Type ?u.361147
𝕜 : Type ?u.361150
p : ℝ≥0∞
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup F'
inst✝⁵ : NormedSpace ℝ F'
inst✝⁴ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
G' : Type u_2
G'' : Type u_3
inst✝³ : NormedLatticeAddCommGroup G''
inst✝² : NormedSpace ℝ G''
inst✝¹ : NormedLatticeAddCommGroup G'
inst✝ : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
hT_nonneg : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ ↑(T s) x
f : α →ₛ G'
hf : 0 ≤ f
hfi : Integrable ↑f
i : G'
hi : i ∈ SimpleFunc.range f
⊢ 0 ≤ ↑(T (↑f ⁻¹' {i})) i
by_cases h0 : i = 0
case neg
α : Type u_1
E : Type ?u.361138
F : Type ?u.361141
F' : Type ?u.361144
G : Type ?u.361147
𝕜 : Type ?u.361150
p : ℝ≥0∞
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup F'
inst✝⁵ : NormedSpace ℝ F'
inst✝⁴ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
G' : Type u_2
G'' : Type u_3
inst✝³ : NormedLatticeAddCommGroup G''
inst✝² : NormedSpace ℝ G''
inst✝¹ : NormedLatticeAddCommGroup G'
inst✝ : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
hT_nonneg : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ ↑(T s) x
f : α →ₛ G'
hf : 0 ≤ f
hfi : Integrable ↑f
i : G'
hi : i ∈ SimpleFunc.range f
h0 : ¬i = 0
⊢ 0 ≤ i
case neg
α : Type u_1
E : Type ?u.361138
F : Type ?u.361141
F' : Type ?u.361144
G : Type ?u.361147
𝕜 : Type ?u.361150
p : ℝ≥0∞
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup F'
inst✝⁵ : NormedSpace ℝ F'
inst✝⁴ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
G' : Type u_2
G'' : Type u_3
inst✝³ : NormedLatticeAddCommGroup G''
inst✝² : NormedSpace ℝ G''
inst✝¹ : NormedLatticeAddCommGroup G'
inst✝ : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
hT_nonneg : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ ↑(T s) x
f : α →ₛ G'
hf : 0 ≤ f
hfi : Integrable ↑f
i : G'
hi : i ∈ SimpleFunc.range f
h0 : ¬i = 0
⊢ 0 ≤ ↑(T (↑f ⁻¹' {i})) i
refine'
  hT_nonneg _ (measurableSet_fiber _ _) (measure_preimage_lt_top_of_integrable _ hfi h0) i _
case neg
α : Type u_1
E : Type ?u.361138
F : Type ?u.361141
F' : Type ?u.361144
G : Type ?u.361147
𝕜 : Type ?u.361150
p : ℝ≥0∞
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup F'
inst✝⁵ : NormedSpace ℝ F'
inst✝⁴ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
G' : Type u_2
G'' : Type u_3
inst✝³ : NormedLatticeAddCommGroup G''
inst✝² : NormedSpace ℝ G''
inst✝¹ : NormedLatticeAddCommGroup G'
inst✝ : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
hT_nonneg : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ ↑(T s) x
f : α →ₛ G'
hf : 0 ≤ f
hfi : Integrable ↑f
i : G'
hi : i ∈ Set.range ↑f
h0 : ¬i = 0
⊢ 0 ≤ i
case neg
α : Type u_1
E : Type ?u.361138
F : Type ?u.361141
F' : Type ?u.361144
G : Type ?u.361147
𝕜 : Type ?u.361150
p : ℝ≥0∞
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup F'
inst✝⁵ : NormedSpace ℝ F'
inst✝⁴ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
G' : Type u_2
G'' : Type u_3
inst✝³ : NormedLatticeAddCommGroup G''
inst✝² : NormedSpace ℝ G''
inst✝¹ : NormedLatticeAddCommGroup G'
inst✝ : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
hT_nonneg : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ ↑(T s) x
f : α →ₛ G'
hf : 0 ≤ f
hfi : Integrable ↑f
i : G'
hi : i ∈ SimpleFunc.range f
h0 : ¬i = 0
⊢ 0 ≤ i
rw [mem_range] at hi
case neg.intro
α : Type u_1
E : Type ?u.361138
F : Type ?u.361141
F' : Type ?u.361144
G : Type ?u.361147
𝕜 : Type ?u.361150
p : ℝ≥0∞
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup F'
inst✝⁵ : NormedSpace ℝ F'
inst✝⁴ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
G' : Type u_2
G'' : Type u_3
inst✝³ : NormedLatticeAddCommGroup G''
inst✝² : NormedSpace ℝ G''
inst✝¹ : NormedLatticeAddCommGroup G'
inst✝ : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
hT_nonneg : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ ↑(T s) x
f : α →ₛ G'
hf : 0 ≤ f
hfi : Integrable ↑f
i : G'
hi : i ∈ Set.range ↑f
h0 : ¬i = 0
y : α
hy : ↑f y = i
⊢ 0 ≤ i
case neg
α : Type u_1
E : Type ?u.361138
F : Type ?u.361141
F' : Type ?u.361144
G : Type ?u.361147
𝕜 : Type ?u.361150
p : ℝ≥0∞
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup F'
inst✝⁵ : NormedSpace ℝ F'
inst✝⁴ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
G' : Type u_2
G'' : Type u_3
inst✝³ : NormedLatticeAddCommGroup G''
inst✝² : NormedSpace ℝ G''
inst✝¹ : NormedLatticeAddCommGroup G'
inst✝ : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
hT_nonneg : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ ↑(T s) x
f : α →ₛ G'
hf : 0 ≤ f
hfi : Integrable ↑f
i : G'
hi : i ∈ Set.range ↑f
h0 : ¬i = 0
⊢ 0 ≤ i
obtain ⟨y, hy⟩ := Set.mem_range.mp hi
case neg.intro
α : Type u_1
E : Type ?u.361138
F : Type ?u.361141
F' : Type ?u.361144
G : Type ?u.361147
𝕜 : Type ?u.361150
p : ℝ≥0∞
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup F'
inst✝⁵ : NormedSpace ℝ F'
inst✝⁴ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
G' : Type u_2
G'' : Type u_3
inst✝³ : NormedLatticeAddCommGroup G''
inst✝² : NormedSpace ℝ G''
inst✝¹ : NormedLatticeAddCommGroup G'
inst✝ : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
hT_nonneg : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ ↑(T s) x
f : α →ₛ G'
hf : 0 ≤ f
hfi : Integrable ↑f
i : G'
hi : i ∈ Set.range ↑f
h0 : ¬i = 0
y : α
hy : ↑f y = i
⊢ 0 ≤ ↑f y
case neg.intro
α : Type u_1
E : Type ?u.361138
F : Type ?u.361141
F' : Type ?u.361144
G : Type ?u.361147
𝕜 : Type ?u.361150
p : ℝ≥0∞
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup F'
inst✝⁵ : NormedSpace ℝ F'
inst✝⁴ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
G' : Type u_2
G'' : Type u_3
inst✝³ : NormedLatticeAddCommGroup G''
inst✝² : NormedSpace ℝ G''
inst✝¹ : NormedLatticeAddCommGroup G'
inst✝ : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
hT_nonneg : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ ↑(T s) x
f : α →ₛ G'
hf : 0 ≤ f
hfi : Integrable ↑f
i : G'
hi : i ∈ Set.range ↑f
h0 : ¬i = 0
y : α
hy : ↑f y = i
⊢ 0 ≤ i
rw [← hy]
no goals
case neg.intro
α : Type u_1
E : Type ?u.361138
F : Type ?u.361141
F' : Type ?u.361144
G : Type ?u.361147
𝕜 : Type ?u.361150
p : ℝ≥0∞
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup F'
inst✝⁵ : NormedSpace ℝ F'
inst✝⁴ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
G' : Type u_2
G'' : Type u_3
inst✝³ : NormedLatticeAddCommGroup G''
inst✝² : NormedSpace ℝ G''
inst✝¹ : NormedLatticeAddCommGroup G'
inst✝ : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
hT_nonneg : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ ↑(T s) x
f : α →ₛ G'
hf : 0 ≤ f
hfi : Integrable ↑f
i : G'
hi : i ∈ Set.range ↑f
h0 : ¬i = 0
y : α
hy : ↑f y = i
⊢ 0 ≤ ↑f y
convert hf y
no goals
case pos
α : Type u_1
E : Type ?u.361138
F : Type ?u.361141
F' : Type ?u.361144
G : Type ?u.361147
𝕜 : Type ?u.361150
p : ℝ≥0∞
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup F'
inst✝⁵ : NormedSpace ℝ F'
inst✝⁴ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
G' : Type u_2
G'' : Type u_3
inst✝³ : NormedLatticeAddCommGroup G''
inst✝² : NormedSpace ℝ G''
inst✝¹ : NormedLatticeAddCommGroup G'
inst✝ : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
hT_nonneg : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ ↑(T s) x
f : α →ₛ G'
hf : 0 ≤ f
hfi : Integrable ↑f
i : G'
hi : i ∈ SimpleFunc.range f
h0 : i = 0
⊢ 0 ≤ ↑(T (↑f ⁻¹' {i})) i
simp [h0]