awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind :
  ∀ (t1 t2 : Set Ω),
    Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t1 →
      Membership.mem (γ := Set (Set Ω)) {T} t2 →
        (μ : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
h_mul_indicator :
  ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable (β := ℝ≥0∞) fun (a : Ω) ↦ g a * T.indicator (fun (x : Ω) ↦ c) a
c' : ℝ≥0∞
s' : Set Ω
h_meas_s' : MeasurableSet s'
indicator :
  HMul.hMul (β := ℝ≥0∞) (c' * c) ((μ : (a : Set Ω) → ℝ≥0∞) (s' ∩ T) : ℝ≥0∞) =
    c' * c * HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s' : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) T : ℝ≥0∞)
indicator₁ indicator₂ :
  c' * c * HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s' : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) T : ℝ≥0∞) =
    c' * c * HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s' : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) T : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) (c' * c) ((μ : (a : Set Ω) → ℝ≥0∞) (s' ∩ T) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) c' ((μ : (a : Set Ω) → ℝ≥0∞) s' : ℝ≥0∞) *
      HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set Ω) → ℝ≥0∞) T : ℝ≥0∞)

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

Premises used: Set.mem_singleton, mul_mul_mul_comm
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s : Set Ω | MeasurableSet s} {T} μ
h_mul_indicator :
  ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable (β := ℝ≥0∞) fun (a : Ω) ↦ g a * T.indicator (fun (x : Ω) ↦ c) a
f' g : Ω → ℝ≥0∞
add :
  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) ω ∂μ
⊢ 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:
_
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s : Set Ω | MeasurableSet s} {T} μ
h_mul_indicator :
  ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable (β := ℝ≥0∞) fun (a : Ω) ↦ g a * T.indicator (fun (x : Ω) ↦ c) a
f' g : Ω → ℝ≥0∞
h : Disjoint (Function.support f') (Function.support g)
h_meas_f' : Measurable f'
add :
  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) ω ∂μ
⊢ 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:
_
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s : Set Ω | MeasurableSet s} {T} μ
h_mul_indicator :
  ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable (β := ℝ≥0∞) fun (a : Ω) ↦ g a * T.indicator (fun (x : Ω) ↦ c) a
f' g : Ω → ℝ≥0∞
h : Disjoint (Function.support f') (Function.support g)
h_meas_f' : Measurable f'
h_1 : 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) ω ∂μ
⊢ Measurable f'

Tactic:
have h_measM_f' : Measurable f' := h_meas_f'.mono hMf le_rfl
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s : Set Ω | MeasurableSet s} {T} μ
h_mul_indicator :
  ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable (β := ℝ≥0∞) fun (a : Ω) ↦ g a * T.indicator (fun (x : Ω) ↦ c) a
f' g : Ω → ℝ≥0∞
h : Disjoint (Function.support f') (Function.support g)
h_meas_f' : Measurable f'
h_1 : 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'
add :
  ∫⁻ (ω : Ω), f' ω * 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) ω ∂μ =
    (∫⁻ (ω : Ω), (f' + g) ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ

Tactic:
simp_rw [Pi.add_apply, right_distrib]

Premises used: Pi.add_apply, right_distrib
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s : Set Ω | MeasurableSet s} {T} μ
h_mul_indicator :
  ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable (β := ℝ≥0∞) fun (a : Ω) ↦ g a * T.indicator (fun (x : Ω) ↦ c) a
f' g : Ω → ℝ≥0∞
h : Disjoint (Function.support f') (Function.support g)
h_meas_f' : Measurable f'
h_1 : 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'
add :
  ∫⁻ (a : Ω), f' a * T.indicator (fun (x : Ω) ↦ c) a ∂μ + ∫⁻ (a : Ω), g a * T.indicator (fun (x : Ω) ↦ c) a ∂μ =
    (∫⁻ (ω : Ω), f' ω + g ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ
add₁ :
  ∫⁻ (a : Ω), f' a * T.indicator (fun (x : Ω) ↦ c) a ∂μ + ∫⁻ (a : Ω), g a * T.indicator (fun (x : Ω) ↦ c) a ∂μ =
    (∫⁻ (a : Ω), f' a ∂μ + ∫⁻ (a : Ω), g a ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ
add₂ :
  ∫⁻ (a : Ω), f' a * T.indicator (fun (x : Ω) ↦ c) a ∂μ + ∫⁻ (a : Ω), g a * T.indicator (fun (x : Ω) ↦ c) a ∂μ =
    (∫⁻ (a : Ω), f' a ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ +
      (∫⁻ (a : Ω), g a ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ
add₃ :
  (∫⁻ (ω : Ω), f' ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ +
      ∫⁻ (a : Ω), g a * T.indicator (fun (x : Ω) ↦ c) a ∂μ =
    (∫⁻ (a : Ω), f' a ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ +
      (∫⁻ (a : Ω), g a ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ
add₄ add₅ :
  (∫⁻ (ω : Ω), f' ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ +
      (∫⁻ (ω : Ω), g ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ =
    (∫⁻ (a : Ω), f' a ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ +
      (∫⁻ (a : Ω), g a ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ
⊢ ∫⁻ (ω : Ω), 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]

Premises used: MeasureTheory.lintegral_add_left, right_distrib
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s : Set Ω | MeasurableSet s} {T} μ
h_mul_indicator :
  ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable (β := ℝ≥0∞) 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) ω ∂μ
⊢ ∀ (n : ℕ), Measurable (f n)

Tactic:
have h_measM_f : ∀ n, Measurable (f n) := fun n => (h_meas_f n).mono hMf le_rfl
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s : Set Ω | MeasurableSet s} {T} μ
h_mul_indicator :
  ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable (β := ℝ≥0∞) 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)
iSup :
  ∫⁻ (ω : Ω), ⨆ (i : ℕ), f i ω * T.indicator (fun (x : Ω) ↦ c) ω ∂μ =
    (∫⁻ (ω : Ω), ⨆ (n : ℕ), f n ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ
⊢ ∫⁻ (ω : Ω), HMul.hMul (α := ℝ≥0∞) ((fun (x : Ω) ↦ (⨆ (n : ℕ), f n x : ℝ≥0∞)) ω) (T.indicator (fun (x : Ω) ↦ c) ω) ∂μ =
    (∫⁻ (ω : Ω), (fun (x : Ω) ↦ (⨆ (n : ℕ), f n x : ℝ≥0∞)) ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ

Tactic:
simp_rw [iSup_mul]

Premises used: ENNReal.iSup_mul
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s : Set Ω | MeasurableSet s} {T} μ
h_mul_indicator :
  ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable (β := ℝ≥0∞) 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)
iSup :
  Eq (α := ℝ≥0∞) (⨆ (n : ℕ), ∫⁻ (a : Ω), f n a * T.indicator (fun (x : Ω) ↦ c) a ∂μ)
    (⨆ (i : ℕ), (∫⁻ (a : Ω), f i a ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ)
iSup₁ : ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (ω : Ω) ↦ f n ω * T.indicator (fun (x : Ω) ↦ c) ω
iSup₂ : Monotone.{0, u_1} (β := Ω → ℝ≥0∞) fun (i : ℕ) (ω : Ω) ↦ f i ω * T.indicator (fun (x : Ω) ↦ c) ω
⊢ ∫⁻ (ω : Ω), ⨆ (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, iSup_mul]

Premises used: MeasureTheory.lintegral_iSup, ENNReal.iSup_mul
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s : Set Ω | MeasurableSet s} {T} μ
h_mul_indicator :
  ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable (β := ℝ≥0∞) 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)
⊢ Eq (α := ℝ≥0∞) (⨆ (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]
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s : Set Ω | MeasurableSet s} {T} μ
h_mul_indicator :
  ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable (β := ℝ≥0∞) 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 (β := ℝ≥0∞) fun (ω : Ω) ↦ f n ω * T.indicator (fun (x : Ω) ↦ c) ω

Tactic:
fun n => h_mul_indicator _ (h_measM_f n)
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s : Set Ω | MeasurableSet s} {T} μ
h_mul_indicator :
  ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable (β := ℝ≥0∞) 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 (β := ℝ≥0∞) fun (ω : Ω) ↦ f n ω * T.indicator (fun (x : Ω) ↦ c) ω

Tactic:
exact fun n => h_mul_indicator _ (h_measM_f n)
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s : Set Ω | MeasurableSet s} {T} μ
h_mul_indicator :
  ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable (β := ℝ≥0∞) 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.{0, u_1} (β := Ω → ℝ≥0∞) fun (i : ℕ) (ω : Ω) ↦ f i ω * T.indicator (fun (x : Ω) ↦ c) ω

Tactic:
fun m n h_le a => mul_le_mul_left (h_mono_f h_le a) _

Premises used: Set.indicator, Monotone, mul_le_mul_left
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s : Set Ω | MeasurableSet s} {T} μ
h_mul_indicator :
  ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable (β := ℝ≥0∞) 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.{0, u_1} (β := Ω → ℝ≥0∞) fun (i : ℕ) (ω : Ω) ↦ f i ω * T.indicator (fun (x : Ω) ↦ c) ω

Tactic:
exact fun m n h_le a => mul_le_mul_left (h_mono_f h_le a) _

Premises used: mul_le_mul_left
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
f g : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_meas_g : Measurable g
revert :
  ∀ {g : Ω → ℝ≥0∞} (h_meas_g : Measurable g), ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
⊢ ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ

Tactic:
revert g
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
⊢ Measurable f

Tactic:
have h_measM_f : Measurable f := h_meas_f.mono hMf le_rfl
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
indicator :
  ∀ (c : ℝ≥0∞) ⦃s : Set Ω⦄,
    MeasurableSet s →
      ∫⁻ (ω : Ω), f ω * s.indicator (fun (x : Ω) ↦ c) ω ∂μ =
        (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), s.indicator (fun (x : Ω) ↦ c) ω ∂μ
add :
  ∀ ⦃f_1 g : Ω → ℝ≥0∞⦄,
    Disjoint (Function.support f_1) (Function.support g) →
      Measurable f_1 →
        Measurable g →
          ∫⁻ (ω : Ω), f ω * f_1 ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f_1 ω ∂μ →
            ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ →
              ∫⁻ (ω : Ω), f ω * (f_1 + g) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), (f_1 + g) ω ∂μ
iSup :
  ∀ ⦃f_1 : ℕ → Ω → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f_1 n)) →
      Monotone f_1 →
        (∀ (n : ℕ), ∫⁻ (ω : Ω), f ω * f_1 n ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f_1 n ω ∂μ) →
          ∫⁻ (ω : Ω), f ω * (fun (x : Ω) ↦ (⨆ (n : ℕ), f_1 n x : ℝ≥0∞)) ω ∂μ =
            (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), (fun (x : Ω) ↦ (⨆ (n : ℕ), f_1 n x : ℝ≥0∞)) ω ∂μ
⊢ ∀ {g : Ω → ℝ≥0∞} (h_meas_g : Measurable g), ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ

Tactic:
apply @Measurable.ennreal_induction _ Mg

Premises used: Measurable.ennreal_induction
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
c : ℝ≥0∞
s : Set Ω
h_s : MeasurableSet s
apply : IndepSets {s : Set Ω | MeasurableSet s} {s} μ
⊢ ∫⁻ (ω : Ω), f ω * s.indicator (fun (x : Ω) ↦ c) ω ∂μ =
    (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), s.indicator (fun (x : Ω) ↦ c) ω ∂μ

Tactic:
apply lintegral_mul_indicator_eq_lintegral_mul_lintegral_indicator hMf _ (hMg _ h_s) _ h_meas_f

Premises used: ProbabilityTheory.lintegral_mul_indicator_eq_lintegral_mul_lintegral_indicator
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
c : ℝ≥0∞
s : Set Ω
h_s : MeasurableSet s
apply : Subset (α := Set (Set Ω)) {s} {s : Set Ω | MeasurableSet s}
⊢ IndepSets {s : Set Ω | MeasurableSet s} {s} μ

Tactic:
apply indepSets_of_indepSets_of_le_right h_ind

Premises used: ProbabilityTheory.indepSets_of_indepSets_of_le_right
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
c : ℝ≥0∞
s : Set Ω
h_s : MeasurableSet s
rwa rwa₁ rwa₂ rwa₃ : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} s
⊢ Subset (α := Set (Set Ω)) {s} {s : Set Ω | MeasurableSet s}

Tactic:
rwa [singleton_subset_iff]

Premises used: Set.singleton_subset_iff
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
f' g : Ω → ℝ≥0∞
add :
  Disjoint (Function.support f') (Function.support g) →
    Measurable f' →
      Measurable g →
        ∫⁻ (ω : Ω), f ω * f' ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' ω ∂μ →
          ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ →
            ∫⁻ (ω : Ω), f ω * (f' + g) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), (f' + g) ω ∂μ
⊢ Disjoint (Function.support f') (Function.support g) →
    Measurable f' →
      Measurable g →
        ∫⁻ (ω : Ω), f ω * f' ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' ω ∂μ →
          ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ →
            ∫⁻ (ω : Ω), f ω * (f' + g) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), (f' + g) ω ∂μ

Tactic:
_
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
f' g : Ω → ℝ≥0∞
h : Disjoint (Function.support f') (Function.support g)
h_measMg_f' : Measurable f'
add :
  Measurable g →
    ∫⁻ (ω : Ω), f ω * f' ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' ω ∂μ →
      ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ →
        ∫⁻ (ω : Ω), f ω * (f' + g) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), (f' + g) ω ∂μ
⊢ Measurable g →
    ∫⁻ (ω : Ω), f ω * f' ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' ω ∂μ →
      ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ →
        ∫⁻ (ω : Ω), f ω * (f' + g) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), (f' + g) ω ∂μ

Tactic:
_
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
f' g : Ω → ℝ≥0∞
h : Disjoint (Function.support f') (Function.support g)
h_measMg_f' : Measurable f'
h_1 : Measurable g
h_ind_f' : ∫⁻ (ω : Ω), f ω * f' ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' ω ∂μ
h_ind_g' : ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
⊢ Measurable f'

Tactic:
have h_measM_f' : Measurable f' := h_measMg_f'.mono hMg le_rfl
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
f' g : Ω → ℝ≥0∞
h : Disjoint (Function.support f') (Function.support g)
h_measMg_f' : Measurable f'
h_1 : Measurable g
h_ind_f' : ∫⁻ (ω : Ω), f ω * f' ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' ω ∂μ
h_ind_g' : ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
h_measM_f' : Measurable f'
add : ∫⁻ (ω : Ω), f ω * f' ω + f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' ω + g ω ∂μ
⊢ ∫⁻ (ω : Ω), f ω * (f' + g) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), (f' + g) ω ∂μ

Tactic:
simp_rw [Pi.add_apply, left_distrib]

Premises used: Pi.add_apply, left_distrib