awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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 : Measurable f),
    ∫⁻ (ω : Ω), f ω * T.indicator (fun (x : Ω) ↦ c) ω ∂μ =
      (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ
have indicator : ∀ (c_1 : ℝ≥0∞) ⦃s : Set Ω⦄,
  MeasurableSet s →
    ∫⁻ (ω : Ω), HMul.hMul (α := ℝ≥0∞) (s.indicator (fun (x : Ω) ↦ c_1) ω) (T.indicator (fun (x : Ω) ↦ c) ω) ∂μ =
      (∫⁻ (ω : Ω), s.indicator (fun (x : Ω) ↦ c_1) ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ
Tactic: apply @Measurable.ennreal_induction _ Mf
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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
indicator :
  ∀ (c_1 : ℝ≥0∞) ⦃s : Set Ω⦄,
    MeasurableSet s →
      ∫⁻ (ω : Ω), HMul.hMul (α := ℝ≥0∞) (s.indicator (fun (x : Ω) ↦ c_1) ω) (T.indicator (fun (x : Ω) ↦ c) ω) ∂μ =
        (∫⁻ (ω : Ω), s.indicator (fun (x : Ω) ↦ c_1) ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ
⊢ ∀ {f : Ω → ℝ≥0∞} (h_meas_f : Measurable f),
    ∫⁻ (ω : Ω), f ω * T.indicator (fun (x : Ω) ↦ c) ω ∂μ =
      (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ
have add : ∀ ⦃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: apply @Measurable.ennreal_induction _ Mf
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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
indicator :
  ∀ (c_1 : ℝ≥0∞) ⦃s : Set Ω⦄,
    MeasurableSet s →
      ∫⁻ (ω : Ω), HMul.hMul (α := ℝ≥0∞) (s.indicator (fun (x : Ω) ↦ c_1) ω) (T.indicator (fun (x : Ω) ↦ c) ω) ∂μ =
        (∫⁻ (ω : Ω), s.indicator (fun (x : Ω) ↦ c_1) ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ
add :
  ∀ ⦃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) ω ∂μ
⊢ ∀ {f : Ω → ℝ≥0∞} (h_meas_f : Measurable f),
    ∫⁻ (ω : Ω), f ω * T.indicator (fun (x : Ω) ↦ c) ω ∂μ =
      (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ
have iSup : ∀ ⦃f : ℕ → Ω → ℝ≥0∞⦄,
  (∀ (n : ℕ), Measurable (f n)) →
    Monotone f →
      (∀ (n : ℕ),
          ∫⁻ (ω : Ω), f n ω * T.indicator (fun (x : Ω) ↦ c) ω ∂μ =
            (∫⁻ (ω : Ω), 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: apply @Measurable.ennreal_induction _ Mf
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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
c' : ℝ≥0∞
s' : Set Ω
h_meas_s' : MeasurableSet s'
⊢ ∫⁻ (ω : Ω), HMul.hMul (α := ℝ≥0∞) (s'.indicator (fun (x : Ω) ↦ c') ω) (T.indicator (fun (x : Ω) ↦ c) ω) ∂μ =
    (∫⁻ (ω : Ω), s'.indicator (fun (x : Ω) ↦ c') ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ
have indicator : ∫⁻ (ω : Ω), (s' ∩ T).indicator (fun (j : Ω) ↦ c' * c) ω ∂μ =
  (∫⁻ (ω : Ω), s'.indicator (fun (x : Ω) ↦ c') ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ
Tactic: simp_rw [← inter_indicator_mul]
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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
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) ω ∂μ
have indicator : ∫⁻ (a : Ω) in s' ∩ T, c' * c ∂μ = (∫⁻ (a : Ω) in s', c' ∂μ) * ∫⁻ (a : Ω) in T, c ∂μ
Tactic: rw [lintegral_indicator (MeasurableSet.inter (hMf _ h_meas_s') h_meas_T),
      lintegral_indicator (hMf _ h_meas_s'), lintegral_indicator h_meas_T]
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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
c' : ℝ≥0∞
s' : Set Ω
h_meas_s' : MeasurableSet s'
⊢ ∫⁻ (a : Ω) in s' ∩ T, c' * c ∂μ = (∫⁻ (a : Ω) in s', c' ∂μ) * ∫⁻ (a : Ω) in T, c ∂μ
have indicator : 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: simp only [lintegral_const, univ_inter,
      MeasurableSet.univ, Measure.restrict_apply]
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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
c' : ℝ≥0∞
s' : Set Ω
h_meas_s' : MeasurableSet s'
⊢ 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∞)
have indicator : ∀
  (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'),
  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 [IndepSets_iff] at h_ind
Cleared hypotheses: h_ind, h_mul_indicator, c', s', h_meas_s'
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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'
⊢ 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∞)
have 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∞)
Tactic: rw [mul_mul_mul_comm, h_ind s' T h_meas_s' (Set.mem_singleton _)]
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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∞)
⊢ 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∞)
have 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∞)
Tactic: rw [mul_mul_mul_comm, h_ind s' T h_meas_s' (Set.mem_singleton _)]
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (hypothesis)
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) ω ∂μ
⊢ ∫⁻ (ω : Ω), (f' + g) ω * T.indicator (fun (x : Ω) ↦ c) ω ∂μ =
    (∫⁻ (ω : Ω), (f' + g) ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ
have h_measM_f' : Measurable f'
Tactic: have h_measM_f' : Measurable f' := h_meas_f'.mono hMf le_rfl
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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'
⊢ ∫⁻ (ω : Ω), (f' + g) ω * T.indicator (fun (x : Ω) ↦ c) ω ∂μ =
    (∫⁻ (ω : Ω), (f' + g) ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ
have add : ∫⁻ (ω : Ω), f' ω * T.indicator (fun (x : Ω) ↦ c) ω + g ω * T.indicator (fun (x : Ω) ↦ c) ω ∂μ =
  (∫⁻ (ω : Ω), f' ω + g ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ
Tactic: simp_rw [Pi.add_apply, right_distrib]
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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'
⊢ ∫⁻ (ω : Ω), f' ω * T.indicator (fun (x : Ω) ↦ c) ω + g ω * T.indicator (fun (x : Ω) ↦ c) ω ∂μ =
    (∫⁻ (ω : Ω), f' ω + g ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ
have 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) ω ∂μ
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]
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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) ω ∂μ
⊢ ∫⁻ (ω : Ω), f' ω * T.indicator (fun (x : Ω) ↦ c) ω + g ω * T.indicator (fun (x : Ω) ↦ c) ω ∂μ =
    (∫⁻ (ω : Ω), f' ω + g ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ
have 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) ω ∂μ
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]
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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) ω ∂μ
⊢ ∫⁻ (ω : Ω), f' ω * T.indicator (fun (x : Ω) ↦ c) ω + g ω * T.indicator (fun (x : Ω) ↦ c) ω ∂μ =
    (∫⁻ (ω : Ω), f' ω + g ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ
have 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) ω ∂μ
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]
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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) ω ∂μ
⊢ ∫⁻ (ω : Ω), f' ω * T.indicator (fun (x : Ω) ↦ c) ω + g ω * T.indicator (fun (x : Ω) ↦ c) ω ∂μ =
    (∫⁻ (ω : Ω), f' ω + g ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ
have 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) ω ∂μ
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]
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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) ω ∂μ
⊢ ∫⁻ (ω : Ω), f' ω * T.indicator (fun (x : Ω) ↦ c) ω + g ω * T.indicator (fun (x : Ω) ↦ c) ω ∂μ =
    (∫⁻ (ω : Ω), f' ω + g ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ
have 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) ω ∂μ
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]
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (hypothesis)
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) ω ∂μ
⊢ ∫⁻ (ω : Ω), 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) ω ∂μ
have h_measM_f : ∀ (n : ℕ), Measurable (f n)
Tactic: have h_measM_f : ∀ n, Measurable (f n) := fun n => (h_meas_f n).mono hMf le_rfl