-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem Integrable.simpleFunc_mul (g : SimpleFunc X ℝ) (hf : Integrable f μ) :
    Integrable (⇑g * f) μ

Proof state:
X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
c : ℝ
s : Set X
hs : MeasurableSet s
⊢ s.indicator (const X c) * f = s.indicator (c • f)

Tactic:
ext1 x

Result:
case h
X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
c : ℝ
s : Set X
hs : MeasurableSet s
x : X
⊢ (s.indicator (const X c) * f) x = s.indicator (c • f) x

Proof state:
case h
X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
c : ℝ
s : Set X
hs : MeasurableSet s
x : X
⊢ (s.indicator (const X c) * f) x = s.indicator (c • f) x

Tactic:
by_cases hx : x ∈ s

Result:
case pos
X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
c : ℝ
s : Set X
hs : MeasurableSet s
x : X
hx : x ∈ s
⊢ (s.indicator (const X c) * f) x = s.indicator (c • f) x

case neg
X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
c : ℝ
s : Set X
hs : MeasurableSet s
x : X
hx : x ∉ s
⊢ (s.indicator (const X c) * f) x = s.indicator (c • f) x

Proof state:
X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
c : ℝ
s : Set X
hs : MeasurableSet s
⊢ Integrable (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const X c) (SimpleFunc.const X 0)) * f) μ

Tactic:
simp only [SimpleFunc.const_zero, SimpleFunc.coe_piecewise, SimpleFunc.coe_const,
  SimpleFunc.coe_zero, Set.piecewise_eq_indicator]

Result:
X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
c : ℝ
s : Set X
hs : MeasurableSet s
⊢ Integrable (s.indicator (const X c) * f) μ

Proof state:
X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
g₁ g₂ : SimpleFunc X ℝ
x✝ : Disjoint (support ⇑g₁) (support ⇑g₂)
h_int₁ : Integrable (⇑g₁ * f) μ
h_int₂ : Integrable (⇑g₂ * f) μ
⊢ ⇑g₁ * f + ⇑g₂ * f =ᶠ[ae μ] ⇑(g₁ + g₂) * f

Tactic:
rw [SimpleFunc.coe_add, add_mul]

Result:
no goals

Proof state:
X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
c : ℝ
s : Set X
hs : MeasurableSet s
this : s.indicator (const X c) * f = s.indicator (c • f)
⊢ IntegrableOn (c • f) s μ

Tactic:
exact (hf.smul c).integrableOn

Result:
no goals

Proof state:
case pos
X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
c : ℝ
s : Set X
hs : MeasurableSet s
x : X
hx : x ∈ s
⊢ (s.indicator (const X c) * f) x = s.indicator (c • f) x

Tactic:
simp only [hx, Pi.mul_apply, Set.indicator_of_mem, Pi.smul_apply, Algebra.id.smul_eq_mul,
  ← Function.const_def]

Result:
no goals

Proof state:
X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
c : ℝ
s : Set X
hs : MeasurableSet s
this : s.indicator (const X c) * f = s.indicator (c • f)
⊢ Integrable (s.indicator (const X c) * f) μ

Tactic:
rw [this, integrable_indicator_iff hs]

Result:
X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
c : ℝ
s : Set X
hs : MeasurableSet s
this : s.indicator (const X c) * f = s.indicator (c • f)
⊢ IntegrableOn (c • f) s μ

Proof state:
X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
⊢ Integrable (⇑g * f) μ

Tactic:
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

Result:
X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
c : ℝ
s : Set X
hs : MeasurableSet s
⊢ Integrable (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const X c) (SimpleFunc.const X 0)) * f) μ

Proof state:
case neg
X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
c : ℝ
s : Set X
hs : MeasurableSet s
x : X
hx : x ∉ s
⊢ (s.indicator (const X c) * f) x = s.indicator (c • f) x

Tactic:
simp only [hx, Pi.mul_apply, Set.indicator_of_not_mem, not_false_iff, zero_mul]

Result:
no goals