-- 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_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)
⊢ ∫⁻ (ω : Ω), ⨆ i, f i ω * T.indicator (fun x => c) ω ∂μ =
    (∫⁻ (ω : Ω), ⨆ n, f n ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x => c) ω ∂μ

Tactic:
rw [lintegral_iSup h_measM_f h_mono_f, lintegral_iSup, ENNReal.iSup_mul]

Result:
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) ω ∂μ

case h_iSup.hf
Ω : 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 : ℕ), Measurable fun ω => f n ω * T.indicator (fun x => c) ω

case h_iSup.h_mono
Ω : 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)
⊢ Monotone fun i ω => f i ω * 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 : IndepSets {s | MeasurableSet s} {T} μ
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 [IndepSets_iff] at h_ind

Result:
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)

Proof state:
Ω : 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) ω ∂μ

Tactic:
have h_mul_indicator : ∀ g, Measurable g → Measurable fun a => g a * T.indicator (fun _ => c) a :=
  fun g h_mg => h_mg.mul (measurable_const.indicator h_meas_T)

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} μ
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a => g a * T.indicator (fun x => c) a
⊢ ∀ {f : Ω → ℝ≥0∞},
    Measurable f →
      ∫⁻ (ω : Ω), f ω * T.indicator (fun x => c) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x => c) ω ∂μ

Proof state:
case h_iSup.hf
Ω : 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 : ℕ), Measurable fun ω => f n ω * T.indicator (fun x => c) ω

Tactic:
exact fun n => h_mul_indicator _ (h_measM_f n)

Result:
no goals

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 : IndepSets {s | MeasurableSet s} {T} μ
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'
⊢ ∫⁻ (ω : Ω), s'.indicator (fun x => c') ω * T.indicator (fun x => c) ω ∂μ =
    (∫⁻ (ω : Ω), s'.indicator (fun x => c') ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x => c) ω ∂μ

Tactic:
simp_rw [← inter_indicator_mul]

Result:
case h_ind
Ω : 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
c' : ℝ≥0∞
s' : Set Ω
h_meas_s' : MeasurableSet s'
⊢ ∫⁻ (ω : Ω), (s' ∩ T).indicator (fun j => c' * c) ω ∂μ =
    (∫⁻ (ω : Ω), s'.indicator (fun x => c') ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x => c) ω ∂μ