α : Type ?u.5134274
β : Type u_1
E : Type ?u.5134280
F : Type ?u.5134283
inst✝¹ : MeasurableSpace α
ι : Type ?u.5134289
inst✝ : NormedAddCommGroup E
f : β → ℝ
m m0 : MeasurableSpace β
μ : Measure β
g : SimpleFunc β ℝ
hf : Integrable f
c : ℝ
s : Set β
hs : MeasurableSet s
⊢ Integrable (↑(SimpleFunc.piecewise s hs (SimpleFunc.const β c) (SimpleFunc.const β 0)) * f)
α : Type ?u.5134274
β : Type u_1
E : Type ?u.5134280
F : Type ?u.5134283
inst✝¹ : MeasurableSpace α
ι : Type ?u.5134289
inst✝ : NormedAddCommGroup E
f : β → ℝ
m m0 : MeasurableSpace β
μ : Measure β
g : SimpleFunc β ℝ
hf : Integrable f
⊢ Integrable (↑g * f)
refine'
  SimpleFunc.induction (fun c s hs => _)
    (fun g₁ g₂ _ h_int₁ h_int₂ =>
      (h_int₁.add h_int₂).congr (by rw [SimpleFunc.coe_add, add_mul]))
    g
α : Type ?u.5134274
β : Type u_1
E : Type ?u.5134280
F : Type ?u.5134283
inst✝¹ : MeasurableSpace α
ι : Type ?u.5134289
inst✝ : NormedAddCommGroup E
f : β → ℝ
m m0 : MeasurableSpace β
μ : Measure β
g : SimpleFunc β ℝ
hf : Integrable f
c : ℝ
s : Set β
hs : MeasurableSet s
⊢ Integrable (Set.indicator s (const β c) * f)
α : Type ?u.5134274
β : Type u_1
E : Type ?u.5134280
F : Type ?u.5134283
inst✝¹ : MeasurableSpace α
ι : Type ?u.5134289
inst✝ : NormedAddCommGroup E
f : β → ℝ
m m0 : MeasurableSpace β
μ : Measure β
g : SimpleFunc β ℝ
hf : Integrable f
c : ℝ
s : Set β
hs : MeasurableSet s
⊢ Integrable (↑(SimpleFunc.piecewise s hs (SimpleFunc.const β c) (SimpleFunc.const β 0)) * f)
simp only [SimpleFunc.const_zero, SimpleFunc.coe_piecewise, SimpleFunc.coe_const,
  SimpleFunc.coe_zero, Set.piecewise_eq_indicator]
α : Type ?u.5134274
β : Type u_1
E : Type ?u.5134280
F : Type ?u.5134283
inst✝¹ : MeasurableSpace α
ι : Type ?u.5134289
inst✝ : NormedAddCommGroup E
f : β → ℝ
m m0 : MeasurableSpace β
μ : Measure β
g : SimpleFunc β ℝ
hf : Integrable f
c : ℝ
s : Set β
hs : MeasurableSet s
this : Set.indicator s (const β c) * f = Set.indicator s (c • f)
⊢ IntegrableOn (c • f) s
α : Type ?u.5134274
β : Type u_1
E : Type ?u.5134280
F : Type ?u.5134283
inst✝¹ : MeasurableSpace α
ι : Type ?u.5134289
inst✝ : NormedAddCommGroup E
f : β → ℝ
m m0 : MeasurableSpace β
μ : Measure β
g : SimpleFunc β ℝ
hf : Integrable f
c : ℝ
s : Set β
hs : MeasurableSet s
this : Set.indicator s (const β c) * f = Set.indicator s (c • f)
⊢ Integrable (Set.indicator s (const β c) * f)
rw [this, integrable_indicator_iff hs]
no goals
α : Type ?u.5134274
β : Type u_1
E : Type ?u.5134280
F : Type ?u.5134283
inst✝¹ : MeasurableSpace α
ι : Type ?u.5134289
inst✝ : NormedAddCommGroup E
f : β → ℝ
m m0 : MeasurableSpace β
μ : Measure β
g : SimpleFunc β ℝ
hf : Integrable f
c : ℝ
s : Set β
hs : MeasurableSet s
this : Set.indicator s (const β c) * f = Set.indicator s (c • f)
⊢ IntegrableOn (c • f) s
exact (hf.smul c).integrableOn
no goals
α : Type ?u.5134274
β : Type u_1
E : Type ?u.5134280
F : Type ?u.5134283
inst✝¹ : MeasurableSpace α
ι : Type ?u.5134289
inst✝ : NormedAddCommGroup E
f : β → ℝ
m m0 : MeasurableSpace β
μ : Measure β
g : SimpleFunc β ℝ
hf : Integrable f
g₁ g₂ : SimpleFunc β ℝ
x✝ : Disjoint (support ↑g₁) (support ↑g₂)
h_int₁ : Integrable (↑g₁ * f)
h_int₂ : Integrable (↑g₂ * f)
⊢ ↑g₁ * f + ↑g₂ * f =ᵐ[μ] ↑(g₁ + g₂) * f
rw [SimpleFunc.coe_add, add_mul]
case h
α : Type ?u.5134274
β : Type u_1
E : Type ?u.5134280
F : Type ?u.5134283
inst✝¹ : MeasurableSpace α
ι : Type ?u.5134289
inst✝ : NormedAddCommGroup E
f : β → ℝ
m m0 : MeasurableSpace β
μ : Measure β
g : SimpleFunc β ℝ
hf : Integrable f
c : ℝ
s : Set β
hs : MeasurableSet s
x : β
⊢ (Set.indicator s (const β c) * f) x = Set.indicator s (c • f) x
α : Type ?u.5134274
β : Type u_1
E : Type ?u.5134280
F : Type ?u.5134283
inst✝¹ : MeasurableSpace α
ι : Type ?u.5134289
inst✝ : NormedAddCommGroup E
f : β → ℝ
m m0 : MeasurableSpace β
μ : Measure β
g : SimpleFunc β ℝ
hf : Integrable f
c : ℝ
s : Set β
hs : MeasurableSet s
⊢ Set.indicator s (const β c) * f = Set.indicator s (c • f)
ext1 x
case pos
α : Type ?u.5134274
β : Type u_1
E : Type ?u.5134280
F : Type ?u.5134283
inst✝¹ : MeasurableSpace α
ι : Type ?u.5134289
inst✝ : NormedAddCommGroup E
f : β → ℝ
m m0 : MeasurableSpace β
μ : Measure β
g : SimpleFunc β ℝ
hf : Integrable f
c : ℝ
s : Set β
hs : MeasurableSet s
x : β
hx : x ∈ s
⊢ (Set.indicator s (const β c) * f) x = Set.indicator s (c • f) x

case neg
α : Type ?u.5134274
β : Type u_1
E : Type ?u.5134280
F : Type ?u.5134283
inst✝¹ : MeasurableSpace α
ι : Type ?u.5134289
inst✝ : NormedAddCommGroup E
f : β → ℝ
m m0 : MeasurableSpace β
μ : Measure β
g : SimpleFunc β ℝ
hf : Integrable f
c : ℝ
s : Set β
hs : MeasurableSet s
x : β
hx : ¬x ∈ s
⊢ (Set.indicator s (const β c) * f) x = Set.indicator s (c • f) x
case h
α : Type ?u.5134274
β : Type u_1
E : Type ?u.5134280
F : Type ?u.5134283
inst✝¹ : MeasurableSpace α
ι : Type ?u.5134289
inst✝ : NormedAddCommGroup E
f : β → ℝ
m m0 : MeasurableSpace β
μ : Measure β
g : SimpleFunc β ℝ
hf : Integrable f
c : ℝ
s : Set β
hs : MeasurableSet s
x : β
⊢ (Set.indicator s (const β c) * f) x = Set.indicator s (c • f) x
by_cases hx : x ∈ s
no goals
case pos
α : Type ?u.5134274
β : Type u_1
E : Type ?u.5134280
F : Type ?u.5134283
inst✝¹ : MeasurableSpace α
ι : Type ?u.5134289
inst✝ : NormedAddCommGroup E
f : β → ℝ
m m0 : MeasurableSpace β
μ : Measure β
g : SimpleFunc β ℝ
hf : Integrable f
c : ℝ
s : Set β
hs : MeasurableSet s
x : β
hx : x ∈ s
⊢ (Set.indicator s (const β c) * f) x = Set.indicator s (c • f) x
simp only [hx, Pi.mul_apply, Set.indicator_of_mem, Pi.smul_apply, Algebra.id.smul_eq_mul,
  ← Function.const_def]
no goals
case neg
α : Type ?u.5134274
β : Type u_1
E : Type ?u.5134280
F : Type ?u.5134283
inst✝¹ : MeasurableSpace α
ι : Type ?u.5134289
inst✝ : NormedAddCommGroup E
f : β → ℝ
m m0 : MeasurableSpace β
μ : Measure β
g : SimpleFunc β ℝ
hf : Integrable f
c : ℝ
s : Set β
hs : MeasurableSet s
x : β
hx : ¬x ∈ s
⊢ (Set.indicator s (const β c) * f) x = Set.indicator s (c • f) x
simp only [hx, Pi.mul_apply, Set.indicator_of_not_mem, not_false_iff, MulZeroClass.zero_mul]