-- Mathlib/Probability/Integration.lean
theorem lintegral_mul_indicator_eq_lintegral_mul_lintegral_indicator {Mf mΩ : MeasurableSpace Ω}
    {μ : Measure Ω} (hMf : Mf ≤ mΩ) (c : ℝ≥0∞) {T : Set Ω} (h_meas_T : MeasurableSet T)
    (h_ind : IndepSets {s | MeasurableSet[Mf] s} {T} μ) (h_meas_f : Measurable[Mf] f) :
    (∫⁻ ω, f ω * T.indicator (fun _ => c) ω ∂μ) =
      (∫⁻ ω, f ω ∂μ) * ∫⁻ ω, T.indicator (fun _ => c) ω ∂μ

Proof state:
case h_add
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T} μ
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a => g a * T.indicator (fun x => c) a
⊢ ∀ ⦃f g : Ω → ℝ≥0∞⦄,
    Disjoint (Function.support f) (Function.support g) →
      Measurable f →
        Measurable g →
          ∫⁻ (ω : Ω), f ω * T.indicator (fun x => c) ω ∂μ =
              (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x => c) ω ∂μ →
            ∫⁻ (ω : Ω), g ω * T.indicator (fun x => c) ω ∂μ =
                (∫⁻ (ω : Ω), g ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x => c) ω ∂μ →
              ∫⁻ (ω : Ω), (f + g) ω * T.indicator (fun x => c) ω ∂μ =
                (∫⁻ (ω : Ω), (f + g) ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x => c) ω ∂μ

Tactic:
intro f' g _ h_meas_f' _ h_ind_f' h_ind_g

Result:
case h_add
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T} μ
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a => g a * T.indicator (fun x => c) a
f' g : Ω → ℝ≥0∞
a✝¹ : Disjoint (Function.support f') (Function.support g)
h_meas_f' : Measurable f'
a✝ : Measurable g
h_ind_f' :
  ∫⁻ (ω : Ω), f' ω * T.indicator (fun x => c) ω ∂μ = (∫⁻ (ω : Ω), f' ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x => c) ω ∂μ
h_ind_g :
  ∫⁻ (ω : Ω), g ω * T.indicator (fun x => c) ω ∂μ = (∫⁻ (ω : Ω), g ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x => c) ω ∂μ
⊢ ∫⁻ (ω : Ω), (f' + g) ω * T.indicator (fun x => c) ω ∂μ =
    (∫⁻ (ω : Ω), (f' + g) ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x => c) ω ∂μ

Proof state:
case h_ind
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : ∀ (t1 t2 : Set Ω), t1 ∈ {s | MeasurableSet s} → t2 ∈ {T} → μ (t1 ∩ t2) = μ t1 * μ t2
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a => g a * T.indicator (fun x => c) a
c' : ℝ≥0∞
s' : Set Ω
h_meas_s' : MeasurableSet s'
⊢ c' * c * μ (s' ∩ T) = c' * μ s' * (c * μ T)

Tactic:
rw [mul_mul_mul_comm, h_ind s' T h_meas_s' (Set.mem_singleton _)]

Result:
no goals

Proof state:
case h_add
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T} μ
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a => g a * T.indicator (fun x => c) a
f' g : Ω → ℝ≥0∞
a✝¹ : Disjoint (Function.support f') (Function.support g)
h_meas_f' : Measurable f'
a✝ : Measurable g
h_ind_f' :
  ∫⁻ (ω : Ω), f' ω * T.indicator (fun x => c) ω ∂μ = (∫⁻ (ω : Ω), f' ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x => c) ω ∂μ
h_ind_g :
  ∫⁻ (ω : Ω), g ω * T.indicator (fun x => c) ω ∂μ = (∫⁻ (ω : Ω), g ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x => c) ω ∂μ
h_measM_f' : Measurable f'
⊢ ∫⁻ (ω : Ω), f' ω * T.indicator (fun x => c) ω + g ω * T.indicator (fun x => c) ω ∂μ =
    (∫⁻ (ω : Ω), f' ω + g ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x => c) ω ∂μ

Tactic:
rw [lintegral_add_left (h_mul_indicator _ h_measM_f'), lintegral_add_left h_measM_f',
  right_distrib, h_ind_f', h_ind_g]

Result:
no goals

Proof state:
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T} μ
h_meas_f : Measurable f
⊢ ∫⁻ (ω : Ω), f ω * T.indicator (fun x => c) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x => c) ω ∂μ

Tactic:
revert f

Result:
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T} μ
⊢ ∀ {f : Ω → ℝ≥0∞},
    Measurable f →
      ∫⁻ (ω : Ω), f ω * T.indicator (fun x => c) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x => c) ω ∂μ

Proof state:
case h_add
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T} μ
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a => g a * T.indicator (fun x => c) a
f' g : Ω → ℝ≥0∞
a✝¹ : Disjoint (Function.support f') (Function.support g)
h_meas_f' : Measurable f'
a✝ : Measurable g
h_ind_f' :
  ∫⁻ (ω : Ω), f' ω * T.indicator (fun x => c) ω ∂μ = (∫⁻ (ω : Ω), f' ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x => c) ω ∂μ
h_ind_g :
  ∫⁻ (ω : Ω), g ω * T.indicator (fun x => c) ω ∂μ = (∫⁻ (ω : Ω), g ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x => c) ω ∂μ
h_measM_f' : Measurable f'
⊢ ∫⁻ (ω : Ω), (f' + g) ω * T.indicator (fun x => c) ω ∂μ =
    (∫⁻ (ω : Ω), (f' + g) ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x => c) ω ∂μ

Tactic:
simp_rw [Pi.add_apply, right_distrib]

Result:
case h_add
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T} μ
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a => g a * T.indicator (fun x => c) a
f' g : Ω → ℝ≥0∞
a✝¹ : Disjoint (Function.support f') (Function.support g)
h_meas_f' : Measurable f'
a✝ : Measurable g
h_ind_f' :
  ∫⁻ (ω : Ω), f' ω * T.indicator (fun x => c) ω ∂μ = (∫⁻ (ω : Ω), f' ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x => c) ω ∂μ
h_ind_g :
  ∫⁻ (ω : Ω), g ω * T.indicator (fun x => c) ω ∂μ = (∫⁻ (ω : Ω), g ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x => c) ω ∂μ
h_measM_f' : Measurable f'
⊢ ∫⁻ (ω : Ω), f' ω * T.indicator (fun x => c) ω + g ω * T.indicator (fun x => c) ω ∂μ =
    (∫⁻ (ω : Ω), f' ω + g ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x => c) ω ∂μ

Proof state:
case h_iSup
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T} μ
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a => g a * T.indicator (fun x => c) a
f : ℕ → Ω → ℝ≥0∞
h_meas_f : ∀ (n : ℕ), Measurable (f n)
h_mono_f : Monotone f
h_ind_f :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), f n ω * T.indicator (fun x => c) ω ∂μ =
      (∫⁻ (ω : Ω), f n ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x => c) ω ∂μ
h_measM_f : ∀ (n : ℕ), Measurable (f n)
⊢ ⨆ n, ∫⁻ (a : Ω), f n a * T.indicator (fun x => c) a ∂μ =
    ⨆ i, (∫⁻ (a : Ω), f i a ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x => c) ω ∂μ

Tactic:
simp_rw [← h_ind_f]

Result:
no goals