-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem norm_eq_sum_mul (f : α →₁ₛ[μ] G) :
    ‖f‖ = ∑ x ∈ (toSimpleFunc f).range, (μ (toSimpleFunc f ⁻¹' {x})).toReal * ‖x‖

Proof state:
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc G 1 μ)
h_eq : ∀ (a : α), (SimpleFunc.map (fun x => ‖x‖ₑ) (toSimpleFunc f)) a = ‖(toSimpleFunc f) a‖ₑ
⊢ (∫⁻ (x : α), ‖(toSimpleFunc f) x‖ₑ ∂μ).toReal =
    ∑ x ∈ (toSimpleFunc f).range, (μ (⇑(toSimpleFunc f) ⁻¹' {x})).toReal * ‖x‖

Tactic:
simp_rw [← h_eq]

Result:
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc G 1 μ)
h_eq : ∀ (a : α), (SimpleFunc.map (fun x => ‖x‖ₑ) (toSimpleFunc f)) a = ‖(toSimpleFunc f) a‖ₑ
⊢ (∫⁻ (x : α), (SimpleFunc.map (fun x => ‖x‖ₑ) (toSimpleFunc f)) x ∂μ).toReal =
    ∑ x ∈ (toSimpleFunc f).range, (μ (⇑(toSimpleFunc f) ⁻¹' {x})).toReal * ‖x‖

Proof state:
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc G 1 μ)
h_eq : ∀ (a : α), (SimpleFunc.map (fun x => ‖x‖ₑ) (toSimpleFunc f)) a = ‖(toSimpleFunc f) a‖ₑ
⊢ (∫⁻ (x : α), (SimpleFunc.map (fun x => ‖x‖ₑ) (toSimpleFunc f)) x ∂μ).toReal =
    ∑ x ∈ (toSimpleFunc f).range, (μ (⇑(toSimpleFunc f) ⁻¹' {x})).toReal * ‖x‖

Tactic:
rw [SimpleFunc.lintegral_eq_lintegral, SimpleFunc.map_lintegral, ENNReal.toReal_sum]

Result:
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc G 1 μ)
h_eq : ∀ (a : α), (SimpleFunc.map (fun x => ‖x‖ₑ) (toSimpleFunc f)) a = ‖(toSimpleFunc f) a‖ₑ
⊢ ∑ a ∈ (toSimpleFunc f).range, (‖a‖ₑ * μ (⇑(toSimpleFunc f) ⁻¹' {a})).toReal =
    ∑ x ∈ (toSimpleFunc f).range, (μ (⇑(toSimpleFunc f) ⁻¹' {x})).toReal * ‖x‖

α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc G 1 μ)
h_eq : ∀ (a : α), (SimpleFunc.map (fun x => ‖x‖ₑ) (toSimpleFunc f)) a = ‖(toSimpleFunc f) a‖ₑ
⊢ ∀ a ∈ (toSimpleFunc f).range, ‖a‖ₑ * μ (⇑(toSimpleFunc f) ⁻¹' {a}) ≠ ⊤

Proof state:
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc G 1 μ)
h_eq : ∀ (a : α), (SimpleFunc.map (fun x => ‖x‖ₑ) (toSimpleFunc f)) a = ‖(toSimpleFunc f) a‖ₑ
⊢ ∀ a ∈ (toSimpleFunc f).range, ‖a‖ₑ * μ (⇑(toSimpleFunc f) ⁻¹' {a}) ≠ ⊤

Tactic:
intro x _

Result:
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc G 1 μ)
h_eq : ∀ (a : α), (SimpleFunc.map (fun x => ‖x‖ₑ) (toSimpleFunc f)) a = ‖(toSimpleFunc f) a‖ₑ
x : G
a✝ : x ∈ (toSimpleFunc f).range
⊢ ‖x‖ₑ * μ (⇑(toSimpleFunc f) ⁻¹' {x}) ≠ ⊤

Proof state:
case pos
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc G 1 μ)
h_eq : ∀ (a : α), (SimpleFunc.map (fun x => ‖x‖ₑ) (toSimpleFunc f)) a = ‖(toSimpleFunc f) a‖ₑ
x : G
a✝ : x ∈ (toSimpleFunc f).range
hx0 : x = 0
⊢ ‖0‖ₑ * μ (⇑(toSimpleFunc f) ⁻¹' {0}) ≠ ⊤

Tactic:
simp

Result:
no goals

Proof state:
case neg
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc G 1 μ)
h_eq : ∀ (a : α), (SimpleFunc.map (fun x => ‖x‖ₑ) (toSimpleFunc f)) a = ‖(toSimpleFunc f) a‖ₑ
x : G
a✝ : x ∈ (toSimpleFunc f).range
hx0 : ¬x = 0
⊢ ‖x‖ₑ * μ (⇑(toSimpleFunc f) ⁻¹' {x}) ≠ ⊤

Tactic:
exact
  ENNReal.mul_ne_top ENNReal.coe_ne_top
    (SimpleFunc.measure_preimage_lt_top_of_integrable _ (SimpleFunc.integrable f) hx0).ne

Result:
no goals

Proof state:
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc G 1 μ)
h_eq : ∀ (a : α), (SimpleFunc.map (fun x => ‖x‖ₑ) (toSimpleFunc f)) a = ‖(toSimpleFunc f) a‖ₑ
x : G
a✝ : x ∈ (toSimpleFunc f).range
⊢ ‖x‖ₑ * μ (⇑(toSimpleFunc f) ⁻¹' {x}) ≠ ⊤

Tactic:
by_cases hx0 : x = 0

Result:
case pos
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc G 1 μ)
h_eq : ∀ (a : α), (SimpleFunc.map (fun x => ‖x‖ₑ) (toSimpleFunc f)) a = ‖(toSimpleFunc f) a‖ₑ
x : G
a✝ : x ∈ (toSimpleFunc f).range
hx0 : x = 0
⊢ ‖x‖ₑ * μ (⇑(toSimpleFunc f) ⁻¹' {x}) ≠ ⊤

case neg
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc G 1 μ)
h_eq : ∀ (a : α), (SimpleFunc.map (fun x => ‖x‖ₑ) (toSimpleFunc f)) a = ‖(toSimpleFunc f) a‖ₑ
x : G
a✝ : x ∈ (toSimpleFunc f).range
hx0 : ¬x = 0
⊢ ‖x‖ₑ * μ (⇑(toSimpleFunc f) ⁻¹' {x}) ≠ ⊤

Proof state:
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc G 1 μ)
h_eq : ∀ (a : α), (SimpleFunc.map (fun x => ‖x‖ₑ) (toSimpleFunc f)) a = ‖(toSimpleFunc f) a‖ₑ
⊢ ∑ a ∈ (toSimpleFunc f).range, (‖a‖ₑ * μ (⇑(toSimpleFunc f) ⁻¹' {a})).toReal =
    ∑ x ∈ (toSimpleFunc f).range, (μ (⇑(toSimpleFunc f) ⁻¹' {x})).toReal * ‖x‖

Tactic:
congr

Result:
case e_f
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc G 1 μ)
h_eq : ∀ (a : α), (SimpleFunc.map (fun x => ‖x‖ₑ) (toSimpleFunc f)) a = ‖(toSimpleFunc f) a‖ₑ
⊢ (fun a => (‖a‖ₑ * μ (⇑(toSimpleFunc f) ⁻¹' {a})).toReal) = fun x => (μ (⇑(toSimpleFunc f) ⁻¹' {x})).toReal * ‖x‖

Proof state:
case e_f
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc G 1 μ)
h_eq : ∀ (a : α), (SimpleFunc.map (fun x => ‖x‖ₑ) (toSimpleFunc f)) a = ‖(toSimpleFunc f) a‖ₑ
⊢ (fun a => (‖a‖ₑ * μ (⇑(toSimpleFunc f) ⁻¹' {a})).toReal) = fun x => (μ (⇑(toSimpleFunc f) ⁻¹' {x})).toReal * ‖x‖

Tactic:
ext1 x

Result:
case e_f.h
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc G 1 μ)
h_eq : ∀ (a : α), (SimpleFunc.map (fun x => ‖x‖ₑ) (toSimpleFunc f)) a = ‖(toSimpleFunc f) a‖ₑ
x : G
⊢ (‖x‖ₑ * μ (⇑(toSimpleFunc f) ⁻¹' {x})).toReal = (μ (⇑(toSimpleFunc f) ⁻¹' {x})).toReal * ‖x‖

Proof state:
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc G 1 μ)
⊢ ‖f‖ = ∑ x ∈ (toSimpleFunc f).range, (μ (⇑(toSimpleFunc f) ⁻¹' {x})).toReal * ‖x‖

Tactic:
rw [norm_toSimpleFunc, eLpNorm_one_eq_lintegral_enorm]

Result:
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc G 1 μ)
⊢ (∫⁻ (x : α), ‖(toSimpleFunc f) x‖ₑ ∂μ).toReal =
    ∑ x ∈ (toSimpleFunc f).range, (μ (⇑(toSimpleFunc f) ⁻¹' {x})).toReal * ‖x‖

Proof state:
case e_f.h
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc G 1 μ)
h_eq : ∀ (a : α), (SimpleFunc.map (fun x => ‖x‖ₑ) (toSimpleFunc f)) a = ‖(toSimpleFunc f) a‖ₑ
x : G
⊢ (‖x‖ₑ * μ (⇑(toSimpleFunc f) ⁻¹' {x})).toReal = (μ (⇑(toSimpleFunc f) ⁻¹' {x})).toReal * ‖x‖

Tactic:
rw [ENNReal.toReal_mul, mul_comm, ← ofReal_norm_eq_enorm,
  ENNReal.toReal_ofReal (norm_nonneg _)]

Result:
no goals

Proof state:
case pos
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc G 1 μ)
h_eq : ∀ (a : α), (SimpleFunc.map (fun x => ‖x‖ₑ) (toSimpleFunc f)) a = ‖(toSimpleFunc f) a‖ₑ
x : G
a✝ : x ∈ (toSimpleFunc f).range
hx0 : x = 0
⊢ ‖x‖ₑ * μ (⇑(toSimpleFunc f) ⁻¹' {x}) ≠ ⊤

Tactic:
rw [hx0]

Result:
case pos
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc G 1 μ)
h_eq : ∀ (a : α), (SimpleFunc.map (fun x => ‖x‖ₑ) (toSimpleFunc f)) a = ‖(toSimpleFunc f) a‖ₑ
x : G
a✝ : x ∈ (toSimpleFunc f).range
hx0 : x = 0
⊢ ‖0‖ₑ * μ (⇑(toSimpleFunc f) ⁻¹' {0}) ≠ ⊤