-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToSimpleFunc_smul_left' (T T' : Set α → E →L[ℝ] F') (c : ℝ)
    (h_smul : ∀ s, MeasurableSet s → μ s < ∞ → T' s = c • T s) {f : α →ₛ E} (hf : Integrable f μ) :
    setToSimpleFunc T' f = c • setToSimpleFunc T f

Proof state:
α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
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 ∈ filter (fun x => x ≠ 0) f.range, T' (⇑f ⁻¹' {x}) = c • T (⇑f ⁻¹' {x})
⊢ ∑ x ∈ filter (fun x => x ≠ 0) f.range, (T' (⇑f ⁻¹' {x})) x =
    c • ∑ x ∈ filter (fun x => x ≠ 0) f.range, (T (⇑f ⁻¹' {x})) x

Tactic:
rw [smul_sum]

Result:
α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
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 ∈ filter (fun x => x ≠ 0) f.range, T' (⇑f ⁻¹' {x}) = c • T (⇑f ⁻¹' {x})
⊢ ∑ x ∈ filter (fun x => x ≠ 0) f.range, (T' (⇑f ⁻¹' {x})) x =
    ∑ x ∈ filter (fun x => x ≠ 0) f.range, c • (T (⇑f ⁻¹' {x})) x

Proof state:
α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
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

Tactic:
simp_rw [setToSimpleFunc_eq_sum_filter]

Result:
α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
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 ∈ filter (fun x => x ≠ 0) f.range, (T' (⇑f ⁻¹' {x})) x =
    c • ∑ x ∈ filter (fun x => x ≠ 0) f.range, (T (⇑f ⁻¹' {x})) x

Proof state:
α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
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 ∈ filter (fun x => x ≠ 0) f.range, T' (⇑f ⁻¹' {x}) = c • T (⇑f ⁻¹' {x})
x : E
hx : x ∈ filter (fun x => x ≠ 0) f.range
⊢ (T' (⇑f ⁻¹' {x})) x = c • (T (⇑f ⁻¹' {x})) x

Tactic:
rw [this x hx]

Result:
α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
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 ∈ filter (fun x => x ≠ 0) f.range, T' (⇑f ⁻¹' {x}) = c • T (⇑f ⁻¹' {x})
x : E
hx : x ∈ filter (fun x => x ≠ 0) f.range
⊢ (c • T (⇑f ⁻¹' {x})) x = c • (T (⇑f ⁻¹' {x})) x

Proof state:
α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
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 ∈ filter (fun x => x ≠ 0) f.range, T' (⇑f ⁻¹' {x}) = c • T (⇑f ⁻¹' {x})
x : E
hx : x ∈ filter (fun x => x ≠ 0) f.range
⊢ (c • T (⇑f ⁻¹' {x})) x = c • (T (⇑f ⁻¹' {x})) x

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
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

Tactic:
classical
simp_rw [setToSimpleFunc_eq_sum_filter]
suffices ∀ x ∈ {x ∈ f.range | x ≠ 0}, T' (f ⁻¹' {x}) = c • T (f ⁻¹' {x}) by
  rw [smul_sum]
  refine Finset.sum_congr rfl fun x hx => ?_
  rw [this x hx]
  rfl
intro x hx
refine
  h_smul (f ⁻¹' {x}) (measurableSet_preimage _ _) (measure_preimage_lt_top_of_integrable _ hf ?_)
rw [mem_filter] at hx
exact hx.2

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
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 ∈ filter (fun x => x ≠ 0) f.range, (T' (⇑f ⁻¹' {x})) x =
    c • ∑ x ∈ filter (fun x => x ≠ 0) f.range, (T (⇑f ⁻¹' {x})) x

Tactic:
suffices ∀ x ∈ {x ∈ f.range | x ≠ 0}, T' (f ⁻¹' {x}) = c • T (f ⁻¹' {x}) by
  rw [smul_sum]
  refine Finset.sum_congr rfl fun x hx => ?_
  rw [this x hx]
  rfl

Result:
α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
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 ∈ filter (fun x => x ≠ 0) f.range, T' (⇑f ⁻¹' {x}) = c • T (⇑f ⁻¹' {x})

Proof state:
α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
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 ∈ f.range ∧ x ≠ 0
⊢ x ≠ 0

Tactic:
exact hx.2

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
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 ∈ filter (fun x => x ≠ 0) f.range, T' (⇑f ⁻¹' {x}) = c • T (⇑f ⁻¹' {x})

Tactic:
intro x hx

Result:
α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
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) f.range
⊢ T' (⇑f ⁻¹' {x}) = c • T (⇑f ⁻¹' {x})