α : Type u_1
E : Type u_2
F : Type ?u.251923
F' : Type u_3
G : Type ?u.251929
𝕜 : Type ?u.251932
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 α
T T' : Set α → E →L[ℝ] F'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T' s = c • T s
f : α →ₛ E
hf : Integrable ↑f
⊢ ∑ x in filter (fun x => x ≠ 0) (SimpleFunc.range f), ↑(T' (↑f ⁻¹' {x})) x =
    c • ∑ x in filter (fun x => x ≠ 0) (SimpleFunc.range f), ↑(T (↑f ⁻¹' {x})) x
α : Type u_1
E : Type u_2
F : Type ?u.251923
F' : Type u_3
G : Type ?u.251929
𝕜 : Type ?u.251932
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 α
T T' : Set α → E →L[ℝ] F'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T' s = c • T s
f : α →ₛ E
hf : Integrable ↑f
⊢ setToSimpleFunc T' f = c • setToSimpleFunc T f
simp_rw [setToSimpleFunc_eq_sum_filter]
α : Type u_1
E : Type u_2
F : Type ?u.251923
F' : Type u_3
G : Type ?u.251929
𝕜 : Type ?u.251932
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 α
T T' : Set α → E →L[ℝ] F'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T' s = c • T s
f : α →ₛ E
hf : Integrable ↑f
⊢ ∀ (x : E), x ∈ filter (fun x => x ≠ 0) (SimpleFunc.range f) → T' (↑f ⁻¹' {x}) = c • T (↑f ⁻¹' {x})
α : Type u_1
E : Type u_2
F : Type ?u.251923
F' : Type u_3
G : Type ?u.251929
𝕜 : Type ?u.251932
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 α
T T' : Set α → E →L[ℝ] F'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T' s = c • T s
f : α →ₛ E
hf : Integrable ↑f
⊢ ∑ x in filter (fun x => x ≠ 0) (SimpleFunc.range f), ↑(T' (↑f ⁻¹' {x})) x =
    c • ∑ x in filter (fun x => x ≠ 0) (SimpleFunc.range f), ↑(T (↑f ⁻¹' {x})) x
suffices ∀ x ∈ filter (fun x : E => x ≠ 0) f.range, T' (f ⁻¹' {x}) = c • T (f ⁻¹' {x}) by
  rw [smul_sum]
  refine' Finset.sum_congr rfl fun x hx => _
  rw [this x hx]
  rfl
α : Type u_1
E : Type u_2
F : Type ?u.251923
F' : Type u_3
G : Type ?u.251929
𝕜 : Type ?u.251932
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 α
T T' : Set α → E →L[ℝ] F'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T' s = c • T s
f : α →ₛ E
hf : Integrable ↑f
x : E
hx : x ∈ filter (fun x => x ≠ 0) (SimpleFunc.range f)
⊢ T' (↑f ⁻¹' {x}) = c • T (↑f ⁻¹' {x})
α : Type u_1
E : Type u_2
F : Type ?u.251923
F' : Type u_3
G : Type ?u.251929
𝕜 : Type ?u.251932
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 α
T T' : Set α → E →L[ℝ] F'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T' s = c • T s
f : α →ₛ E
hf : Integrable ↑f
⊢ ∀ (x : E), x ∈ filter (fun x => x ≠ 0) (SimpleFunc.range f) → T' (↑f ⁻¹' {x}) = c • T (↑f ⁻¹' {x})
intro x hx
α : Type u_1
E : Type u_2
F : Type ?u.251923
F' : Type u_3
G : Type ?u.251929
𝕜 : Type ?u.251932
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 α
T T' : Set α → E →L[ℝ] F'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T' s = c • T s
f : α →ₛ E
hf : Integrable ↑f
x : E
hx : x ∈ filter (fun x => x ≠ 0) (SimpleFunc.range f)
⊢ x ≠ 0
α : Type u_1
E : Type u_2
F : Type ?u.251923
F' : Type u_3
G : Type ?u.251929
𝕜 : Type ?u.251932
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 α
T T' : Set α → E →L[ℝ] F'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T' s = c • T s
f : α →ₛ E
hf : Integrable ↑f
x : E
hx : x ∈ filter (fun x => x ≠ 0) (SimpleFunc.range f)
⊢ T' (↑f ⁻¹' {x}) = c • T (↑f ⁻¹' {x})
refine'
  h_smul (f ⁻¹' {x}) (measurableSet_preimage _ _) (measure_preimage_lt_top_of_integrable _ hf _)
α : Type u_1
E : Type u_2
F : Type ?u.251923
F' : Type u_3
G : Type ?u.251929
𝕜 : Type ?u.251932
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 α
T T' : Set α → E →L[ℝ] F'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T' s = c • T s
f : α →ₛ E
hf : Integrable ↑f
x : E
hx : x ∈ SimpleFunc.range f ∧ x ≠ 0
⊢ x ≠ 0
α : Type u_1
E : Type u_2
F : Type ?u.251923
F' : Type u_3
G : Type ?u.251929
𝕜 : Type ?u.251932
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 α
T T' : Set α → E →L[ℝ] F'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T' s = c • T s
f : α →ₛ E
hf : Integrable ↑f
x : E
hx : x ∈ filter (fun x => x ≠ 0) (SimpleFunc.range f)
⊢ x ≠ 0
rw [mem_filter] at hx
no goals
α : Type u_1
E : Type u_2
F : Type ?u.251923
F' : Type u_3
G : Type ?u.251929
𝕜 : Type ?u.251932
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 α
T T' : Set α → E →L[ℝ] F'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T' s = c • T s
f : α →ₛ E
hf : Integrable ↑f
x : E
hx : x ∈ SimpleFunc.range f ∧ x ≠ 0
⊢ x ≠ 0
exact hx.2
α : Type u_1
E : Type u_2
F : Type ?u.251923
F' : Type u_3
G : Type ?u.251929
𝕜 : Type ?u.251932
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 α
T T' : Set α → E →L[ℝ] F'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T' s = c • T s
f : α →ₛ E
hf : Integrable ↑f
this : ∀ (x : E), x ∈ filter (fun x => x ≠ 0) (SimpleFunc.range f) → T' (↑f ⁻¹' {x}) = c • T (↑f ⁻¹' {x})
⊢ ∑ x in filter (fun x => x ≠ 0) (SimpleFunc.range f), ↑(T' (↑f ⁻¹' {x})) x =
    ∑ x in filter (fun x => x ≠ 0) (SimpleFunc.range f), c • ↑(T (↑f ⁻¹' {x})) x
α : Type u_1
E : Type u_2
F : Type ?u.251923
F' : Type u_3
G : Type ?u.251929
𝕜 : Type ?u.251932
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 α
T T' : Set α → E →L[ℝ] F'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T' s = c • T s
f : α →ₛ E
hf : Integrable ↑f
this : ∀ (x : E), x ∈ filter (fun x => x ≠ 0) (SimpleFunc.range f) → T' (↑f ⁻¹' {x}) = c • T (↑f ⁻¹' {x})
⊢ ∑ x in filter (fun x => x ≠ 0) (SimpleFunc.range f), ↑(T' (↑f ⁻¹' {x})) x =
    c • ∑ x in filter (fun x => x ≠ 0) (SimpleFunc.range f), ↑(T (↑f ⁻¹' {x})) x
rw [smul_sum]
α : Type u_1
E : Type u_2
F : Type ?u.251923
F' : Type u_3
G : Type ?u.251929
𝕜 : Type ?u.251932
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 α
T T' : Set α → E →L[ℝ] F'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T' s = c • T s
f : α →ₛ E
hf : Integrable ↑f
this : ∀ (x : E), x ∈ filter (fun x => x ≠ 0) (SimpleFunc.range f) → T' (↑f ⁻¹' {x}) = c • T (↑f ⁻¹' {x})
x : E
hx : x ∈ filter (fun x => x ≠ 0) (SimpleFunc.range f)
⊢ ↑(T' (↑f ⁻¹' {x})) x = c • ↑(T (↑f ⁻¹' {x})) x
α : Type u_1
E : Type u_2
F : Type ?u.251923
F' : Type u_3
G : Type ?u.251929
𝕜 : Type ?u.251932
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 α
T T' : Set α → E →L[ℝ] F'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T' s = c • T s
f : α →ₛ E
hf : Integrable ↑f
this : ∀ (x : E), x ∈ filter (fun x => x ≠ 0) (SimpleFunc.range f) → T' (↑f ⁻¹' {x}) = c • T (↑f ⁻¹' {x})
⊢ ∑ x in filter (fun x => x ≠ 0) (SimpleFunc.range f), ↑(T' (↑f ⁻¹' {x})) x =
    ∑ x in filter (fun x => x ≠ 0) (SimpleFunc.range f), c • ↑(T (↑f ⁻¹' {x})) x
refine' Finset.sum_congr rfl fun x hx => _
α : Type u_1
E : Type u_2
F : Type ?u.251923
F' : Type u_3
G : Type ?u.251929
𝕜 : Type ?u.251932
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 α
T T' : Set α → E →L[ℝ] F'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T' s = c • T s
f : α →ₛ E
hf : Integrable ↑f
this : ∀ (x : E), x ∈ filter (fun x => x ≠ 0) (SimpleFunc.range f) → T' (↑f ⁻¹' {x}) = c • T (↑f ⁻¹' {x})
x : E
hx : x ∈ filter (fun x => x ≠ 0) (SimpleFunc.range f)
⊢ ↑(c • T (↑f ⁻¹' {x})) x = c • ↑(T (↑f ⁻¹' {x})) x
α : Type u_1
E : Type u_2
F : Type ?u.251923
F' : Type u_3
G : Type ?u.251929
𝕜 : Type ?u.251932
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 α
T T' : Set α → E →L[ℝ] F'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T' s = c • T s
f : α →ₛ E
hf : Integrable ↑f
this : ∀ (x : E), x ∈ filter (fun x => x ≠ 0) (SimpleFunc.range f) → T' (↑f ⁻¹' {x}) = c • T (↑f ⁻¹' {x})
x : E
hx : x ∈ filter (fun x => x ≠ 0) (SimpleFunc.range f)
⊢ ↑(T' (↑f ⁻¹' {x})) x = c • ↑(T (↑f ⁻¹' {x})) x
rw [this x hx]
no goals
α : Type u_1
E : Type u_2
F : Type ?u.251923
F' : Type u_3
G : Type ?u.251929
𝕜 : Type ?u.251932
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 α
T T' : Set α → E →L[ℝ] F'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → T' s = c • T s
f : α →ₛ E
hf : Integrable ↑f
this : ∀ (x : E), x ∈ filter (fun x => x ≠ 0) (SimpleFunc.range f) → T' (↑f ⁻¹' {x}) = c • T (↑f ⁻¹' {x})
x : E
hx : x ∈ filter (fun x => x ≠ 0) (SimpleFunc.range f)
⊢ ↑(c • T (↑f ⁻¹' {x})) x = c • ↑(T (↑f ⁻¹' {x})) x
rfl