α : Type u_1
E : Type ?u.465938
F : Type ?u.465941
F' : Type ?u.465944
G : Type u_2
𝕜 : Type ?u.465950
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 α
f : { x // x ∈ simpleFunc G 1 μ }
⊢ ENNReal.toReal (∫⁻ (x : α), ↑‖↑(toSimpleFunc f) x‖₊ ∂μ) =
    ∑ x in SimpleFunc.range (toSimpleFunc f), ENNReal.toReal (↑↑μ (↑(toSimpleFunc f) ⁻¹' {x})) * ‖x‖
α : Type u_1
E : Type ?u.465938
F : Type ?u.465941
F' : Type ?u.465944
G : Type u_2
𝕜 : Type ?u.465950
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 α
f : { x // x ∈ simpleFunc G 1 μ }
⊢ ‖f‖ = ∑ x in SimpleFunc.range (toSimpleFunc f), ENNReal.toReal (↑↑μ (↑(toSimpleFunc f) ⁻¹' {x})) * ‖x‖
rw [norm_toSimpleFunc, snorm_one_eq_lintegral_nnnorm]
α : Type u_1
E : Type ?u.465938
F : Type ?u.465941
F' : Type ?u.465944
G : Type u_2
𝕜 : Type ?u.465950
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 α
f : { x // x ∈ simpleFunc G 1 μ }
h_eq : ∀ (a : α), ↑(SimpleFunc.map (fun x => ↑‖x‖₊) (toSimpleFunc f)) a = ↑‖↑(toSimpleFunc f) a‖₊
⊢ ENNReal.toReal (∫⁻ (x : α), ↑‖↑(toSimpleFunc f) x‖₊ ∂μ) =
    ∑ x in SimpleFunc.range (toSimpleFunc f), ENNReal.toReal (↑↑μ (↑(toSimpleFunc f) ⁻¹' {x})) * ‖x‖
α : Type u_1
E : Type ?u.465938
F : Type ?u.465941
F' : Type ?u.465944
G : Type u_2
𝕜 : Type ?u.465950
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 α
f : { x // x ∈ simpleFunc G 1 μ }
⊢ ENNReal.toReal (∫⁻ (x : α), ↑‖↑(toSimpleFunc f) x‖₊ ∂μ) =
    ∑ x in SimpleFunc.range (toSimpleFunc f), ENNReal.toReal (↑↑μ (↑(toSimpleFunc f) ⁻¹' {x})) * ‖x‖
have h_eq := SimpleFunc.map_apply (fun x => (‖x‖₊ : ℝ≥0∞)) (toSimpleFunc f)
α : Type u_1
E : Type ?u.465938
F : Type ?u.465941
F' : Type ?u.465944
G : Type u_2
𝕜 : Type ?u.465950
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 α
f : { x // x ∈ simpleFunc G 1 μ }
h_eq : ∀ (a : α), ↑(SimpleFunc.map (fun x => ↑‖x‖₊) (toSimpleFunc f)) a = ↑‖↑(toSimpleFunc f) a‖₊
⊢ ENNReal.toReal (∫⁻ (x : α), ↑‖↑(toSimpleFunc f) x‖₊ ∂μ) =
    ∑ x in SimpleFunc.range (toSimpleFunc f), ENNReal.toReal (↑↑μ (↑(toSimpleFunc f) ⁻¹' {x})) * ‖x‖
α : Type u_1
E : Type ?u.465938
F : Type ?u.465941
F' : Type ?u.465944
G : Type u_2
𝕜 : Type ?u.465950
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 α
f : { x // x ∈ simpleFunc G 1 μ }
h_eq : ∀ (a : α), ↑(SimpleFunc.map (fun x => ↑‖x‖₊) (toSimpleFunc f)) a = ↑‖↑(toSimpleFunc f) a‖₊
⊢ ENNReal.toReal (∫⁻ (x : α), ↑‖↑(toSimpleFunc f) x‖₊ ∂μ) =
    ∑ x in SimpleFunc.range (toSimpleFunc f), ENNReal.toReal (↑↑μ (↑(toSimpleFunc f) ⁻¹' {x})) * ‖x‖
dsimp only at h_eq
α : Type u_1
E : Type ?u.465938
F : Type ?u.465941
F' : Type ?u.465944
G : Type u_2
𝕜 : Type ?u.465950
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 α
f : { x // x ∈ simpleFunc G 1 μ }
h_eq : ∀ (a : α), ↑(SimpleFunc.map (fun x => ↑‖x‖₊) (toSimpleFunc f)) a = ↑‖↑(toSimpleFunc f) a‖₊
⊢ ENNReal.toReal (∫⁻ (x : α), ↑(SimpleFunc.map (fun x => ↑‖x‖₊) (toSimpleFunc f)) x ∂μ) =
    ∑ x in SimpleFunc.range (toSimpleFunc f), ENNReal.toReal (↑↑μ (↑(toSimpleFunc f) ⁻¹' {x})) * ‖x‖
α : Type u_1
E : Type ?u.465938
F : Type ?u.465941
F' : Type ?u.465944
G : Type u_2
𝕜 : Type ?u.465950
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 α
f : { x // x ∈ simpleFunc G 1 μ }
h_eq : ∀ (a : α), ↑(SimpleFunc.map (fun x => ↑‖x‖₊) (toSimpleFunc f)) a = ↑‖↑(toSimpleFunc f) a‖₊
⊢ ENNReal.toReal (∫⁻ (x : α), ↑‖↑(toSimpleFunc f) x‖₊ ∂μ) =
    ∑ x in SimpleFunc.range (toSimpleFunc f), ENNReal.toReal (↑↑μ (↑(toSimpleFunc f) ⁻¹' {x})) * ‖x‖
simp_rw [← h_eq]
α : Type u_1
E : Type ?u.465938
F : Type ?u.465941
F' : Type ?u.465944
G : Type u_2
𝕜 : Type ?u.465950
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 α
f : { x // x ∈ simpleFunc G 1 μ }
h_eq : ∀ (a : α), ↑(SimpleFunc.map (fun x => ↑‖x‖₊) (toSimpleFunc f)) a = ↑‖↑(toSimpleFunc f) a‖₊
⊢ ∑ a in SimpleFunc.range (toSimpleFunc f), ENNReal.toReal (↑‖a‖₊ * ↑↑μ (↑(toSimpleFunc f) ⁻¹' {a})) =
    ∑ x in SimpleFunc.range (toSimpleFunc f), ENNReal.toReal (↑↑μ (↑(toSimpleFunc f) ⁻¹' {x})) * ‖x‖

α : Type u_1
E : Type ?u.465938
F : Type ?u.465941
F' : Type ?u.465944
G : Type u_2
𝕜 : Type ?u.465950
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 α
f : { x // x ∈ simpleFunc G 1 μ }
h_eq : ∀ (a : α), ↑(SimpleFunc.map (fun x => ↑‖x‖₊) (toSimpleFunc f)) a = ↑‖↑(toSimpleFunc f) a‖₊
⊢ ∀ (a : G), a ∈ SimpleFunc.range (toSimpleFunc f) → ↑‖a‖₊ * ↑↑μ (↑(toSimpleFunc f) ⁻¹' {a}) ≠ ⊤
α : Type u_1
E : Type ?u.465938
F : Type ?u.465941
F' : Type ?u.465944
G : Type u_2
𝕜 : Type ?u.465950
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 α
f : { x // x ∈ simpleFunc G 1 μ }
h_eq : ∀ (a : α), ↑(SimpleFunc.map (fun x => ↑‖x‖₊) (toSimpleFunc f)) a = ↑‖↑(toSimpleFunc f) a‖₊
⊢ ENNReal.toReal (∫⁻ (x : α), ↑(SimpleFunc.map (fun x => ↑‖x‖₊) (toSimpleFunc f)) x ∂μ) =
    ∑ x in SimpleFunc.range (toSimpleFunc f), ENNReal.toReal (↑↑μ (↑(toSimpleFunc f) ⁻¹' {x})) * ‖x‖
rw [SimpleFunc.lintegral_eq_lintegral, SimpleFunc.map_lintegral, ENNReal.toReal_sum]
case e_f
α : Type u_1
E : Type ?u.465938
F : Type ?u.465941
F' : Type ?u.465944
G : Type u_2
𝕜 : Type ?u.465950
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 α
f : { x // x ∈ simpleFunc G 1 μ }
h_eq : ∀ (a : α), ↑(SimpleFunc.map (fun x => ↑‖x‖₊) (toSimpleFunc f)) a = ↑‖↑(toSimpleFunc f) a‖₊
⊢ (fun a => ENNReal.toReal (↑‖a‖₊ * ↑↑μ (↑(toSimpleFunc f) ⁻¹' {a}))) = fun x =>
    ENNReal.toReal (↑↑μ (↑(toSimpleFunc f) ⁻¹' {x})) * ‖x‖
α : Type u_1
E : Type ?u.465938
F : Type ?u.465941
F' : Type ?u.465944
G : Type u_2
𝕜 : Type ?u.465950
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 α
f : { x // x ∈ simpleFunc G 1 μ }
h_eq : ∀ (a : α), ↑(SimpleFunc.map (fun x => ↑‖x‖₊) (toSimpleFunc f)) a = ↑‖↑(toSimpleFunc f) a‖₊
⊢ ∑ a in SimpleFunc.range (toSimpleFunc f), ENNReal.toReal (↑‖a‖₊ * ↑↑μ (↑(toSimpleFunc f) ⁻¹' {a})) =
    ∑ x in SimpleFunc.range (toSimpleFunc f), ENNReal.toReal (↑↑μ (↑(toSimpleFunc f) ⁻¹' {x})) * ‖x‖
congr
case e_f.h
α : Type u_1
E : Type ?u.465938
F : Type ?u.465941
F' : Type ?u.465944
G : Type u_2
𝕜 : Type ?u.465950
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 α
f : { x // x ∈ simpleFunc G 1 μ }
h_eq : ∀ (a : α), ↑(SimpleFunc.map (fun x => ↑‖x‖₊) (toSimpleFunc f)) a = ↑‖↑(toSimpleFunc f) a‖₊
x : G
⊢ ENNReal.toReal (↑‖x‖₊ * ↑↑μ (↑(toSimpleFunc f) ⁻¹' {x})) = ENNReal.toReal (↑↑μ (↑(toSimpleFunc f) ⁻¹' {x})) * ‖x‖
case e_f
α : Type u_1
E : Type ?u.465938
F : Type ?u.465941
F' : Type ?u.465944
G : Type u_2
𝕜 : Type ?u.465950
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 α
f : { x // x ∈ simpleFunc G 1 μ }
h_eq : ∀ (a : α), ↑(SimpleFunc.map (fun x => ↑‖x‖₊) (toSimpleFunc f)) a = ↑‖↑(toSimpleFunc f) a‖₊
⊢ (fun a => ENNReal.toReal (↑‖a‖₊ * ↑↑μ (↑(toSimpleFunc f) ⁻¹' {a}))) = fun x =>
    ENNReal.toReal (↑↑μ (↑(toSimpleFunc f) ⁻¹' {x})) * ‖x‖
ext1 x
no goals
case e_f.h
α : Type u_1
E : Type ?u.465938
F : Type ?u.465941
F' : Type ?u.465944
G : Type u_2
𝕜 : Type ?u.465950
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 α
f : { x // x ∈ simpleFunc G 1 μ }
h_eq : ∀ (a : α), ↑(SimpleFunc.map (fun x => ↑‖x‖₊) (toSimpleFunc f)) a = ↑‖↑(toSimpleFunc f) a‖₊
x : G
⊢ ENNReal.toReal (↑‖x‖₊ * ↑↑μ (↑(toSimpleFunc f) ⁻¹' {x})) = ENNReal.toReal (↑↑μ (↑(toSimpleFunc f) ⁻¹' {x})) * ‖x‖
rw [ENNReal.toReal_mul, mul_comm, ← ofReal_norm_eq_coe_nnnorm,
  ENNReal.toReal_ofReal (norm_nonneg _)]
α : Type u_1
E : Type ?u.465938
F : Type ?u.465941
F' : Type ?u.465944
G : Type u_2
𝕜 : Type ?u.465950
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 α
f : { x // x ∈ simpleFunc G 1 μ }
h_eq : ∀ (a : α), ↑(SimpleFunc.map (fun x => ↑‖x‖₊) (toSimpleFunc f)) a = ↑‖↑(toSimpleFunc f) a‖₊
x : G
a✝ : x ∈ SimpleFunc.range (toSimpleFunc f)
⊢ ↑‖x‖₊ * ↑↑μ (↑(toSimpleFunc f) ⁻¹' {x}) ≠ ⊤
α : Type u_1
E : Type ?u.465938
F : Type ?u.465941
F' : Type ?u.465944
G : Type u_2
𝕜 : Type ?u.465950
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 α
f : { x // x ∈ simpleFunc G 1 μ }
h_eq : ∀ (a : α), ↑(SimpleFunc.map (fun x => ↑‖x‖₊) (toSimpleFunc f)) a = ↑‖↑(toSimpleFunc f) a‖₊
⊢ ∀ (a : G), a ∈ SimpleFunc.range (toSimpleFunc f) → ↑‖a‖₊ * ↑↑μ (↑(toSimpleFunc f) ⁻¹' {a}) ≠ ⊤
intro x _
case pos
α : Type u_1
E : Type ?u.465938
F : Type ?u.465941
F' : Type ?u.465944
G : Type u_2
𝕜 : Type ?u.465950
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 α
f : { x // x ∈ simpleFunc G 1 μ }
h_eq : ∀ (a : α), ↑(SimpleFunc.map (fun x => ↑‖x‖₊) (toSimpleFunc f)) a = ↑‖↑(toSimpleFunc f) a‖₊
x : G
a✝ : x ∈ SimpleFunc.range (toSimpleFunc f)
hx0 : x = 0
⊢ ↑‖x‖₊ * ↑↑μ (↑(toSimpleFunc f) ⁻¹' {x}) ≠ ⊤

case neg
α : Type u_1
E : Type ?u.465938
F : Type ?u.465941
F' : Type ?u.465944
G : Type u_2
𝕜 : Type ?u.465950
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 α
f : { x // x ∈ simpleFunc G 1 μ }
h_eq : ∀ (a : α), ↑(SimpleFunc.map (fun x => ↑‖x‖₊) (toSimpleFunc f)) a = ↑‖↑(toSimpleFunc f) a‖₊
x : G
a✝ : x ∈ SimpleFunc.range (toSimpleFunc f)
hx0 : ¬x = 0
⊢ ↑‖x‖₊ * ↑↑μ (↑(toSimpleFunc f) ⁻¹' {x}) ≠ ⊤
α : Type u_1
E : Type ?u.465938
F : Type ?u.465941
F' : Type ?u.465944
G : Type u_2
𝕜 : Type ?u.465950
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 α
f : { x // x ∈ simpleFunc G 1 μ }
h_eq : ∀ (a : α), ↑(SimpleFunc.map (fun x => ↑‖x‖₊) (toSimpleFunc f)) a = ↑‖↑(toSimpleFunc f) a‖₊
x : G
a✝ : x ∈ SimpleFunc.range (toSimpleFunc f)
⊢ ↑‖x‖₊ * ↑↑μ (↑(toSimpleFunc f) ⁻¹' {x}) ≠ ⊤
by_cases hx0 : x = 0
case pos
α : Type u_1
E : Type ?u.465938
F : Type ?u.465941
F' : Type ?u.465944
G : Type u_2
𝕜 : Type ?u.465950
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 α
f : { x // x ∈ simpleFunc G 1 μ }
h_eq : ∀ (a : α), ↑(SimpleFunc.map (fun x => ↑‖x‖₊) (toSimpleFunc f)) a = ↑‖↑(toSimpleFunc f) a‖₊
x : G
a✝ : x ∈ SimpleFunc.range (toSimpleFunc f)
hx0 : x = 0
⊢ ↑‖0‖₊ * ↑↑μ (↑(toSimpleFunc f) ⁻¹' {0}) ≠ ⊤
case pos
α : Type u_1
E : Type ?u.465938
F : Type ?u.465941
F' : Type ?u.465944
G : Type u_2
𝕜 : Type ?u.465950
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 α
f : { x // x ∈ simpleFunc G 1 μ }
h_eq : ∀ (a : α), ↑(SimpleFunc.map (fun x => ↑‖x‖₊) (toSimpleFunc f)) a = ↑‖↑(toSimpleFunc f) a‖₊
x : G
a✝ : x ∈ SimpleFunc.range (toSimpleFunc f)
hx0 : x = 0
⊢ ↑‖x‖₊ * ↑↑μ (↑(toSimpleFunc f) ⁻¹' {x}) ≠ ⊤
rw [hx0]
no goals
case pos
α : Type u_1
E : Type ?u.465938
F : Type ?u.465941
F' : Type ?u.465944
G : Type u_2
𝕜 : Type ?u.465950
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 α
f : { x // x ∈ simpleFunc G 1 μ }
h_eq : ∀ (a : α), ↑(SimpleFunc.map (fun x => ↑‖x‖₊) (toSimpleFunc f)) a = ↑‖↑(toSimpleFunc f) a‖₊
x : G
a✝ : x ∈ SimpleFunc.range (toSimpleFunc f)
hx0 : x = 0
⊢ ↑‖0‖₊ * ↑↑μ (↑(toSimpleFunc f) ⁻¹' {0}) ≠ ⊤
simp
no goals
case neg
α : Type u_1
E : Type ?u.465938
F : Type ?u.465941
F' : Type ?u.465944
G : Type u_2
𝕜 : Type ?u.465950
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 α
f : { x // x ∈ simpleFunc G 1 μ }
h_eq : ∀ (a : α), ↑(SimpleFunc.map (fun x => ↑‖x‖₊) (toSimpleFunc f)) a = ↑‖↑(toSimpleFunc f) a‖₊
x : G
a✝ : x ∈ SimpleFunc.range (toSimpleFunc f)
hx0 : ¬x = 0
⊢ ↑‖x‖₊ * ↑↑μ (↑(toSimpleFunc f) ⁻¹' {x}) ≠ ⊤
exact
  ENNReal.mul_ne_top ENNReal.coe_ne_top
    (SimpleFunc.measure_preimage_lt_top_of_integrable _ (SimpleFunc.integrable f) hx0).ne