awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.ConditionalExpectation (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
pos : AEStronglyMeasurable f μ
⊢ HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), f x ∂μ) = ∫ (x : Ω) in s, f x ∂μ
have pos₁ : ∀ (c : E) ⦃s_1 : Set Ω⦄,
  MeasurableSet s_1 →
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
      HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), s_1.indicator (fun (x : Ω) ↦ c) x ∂μ) =
        ∫ (x : Ω) in s, s_1.indicator (fun (x : Ω) ↦ c) x ∂μ
Tactic: refine MemLp.induction_stronglyMeasurable hle₁ ENNReal.one_ne_top _ ?_ ?_ ?_ ?_ hfint ?_
-- Lean 4 proof step from Mathlib.Probability.ConditionalExpectation (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
pos : AEStronglyMeasurable f μ
pos₁ :
  ∀ (c : E) ⦃s_1 : Set Ω⦄,
    MeasurableSet s_1 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
        HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), s_1.indicator (fun (x : Ω) ↦ c) x ∂μ) =
          ∫ (x : Ω) in s, s_1.indicator (fun (x : Ω) ↦ c) x ∂μ
⊢ HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), f x ∂μ) = ∫ (x : Ω) in s, f x ∂μ
have pos₂ : ∀ ⦃f g : Ω → E⦄,
  Disjoint (Function.support f) (Function.support g) →
    MemLp f 1 μ →
      MemLp g 1 μ →
        StronglyMeasurable f →
          StronglyMeasurable g →
            HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), f x ∂μ) = ∫ (x : Ω) in s, f x ∂μ →
              HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), g x ∂μ) = ∫ (x : Ω) in s, g x ∂μ →
                HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), (f + g) x ∂μ) = ∫ (x : Ω) in s, (f + g) x ∂μ
Tactic: refine MemLp.induction_stronglyMeasurable hle₁ ENNReal.one_ne_top _ ?_ ?_ ?_ ?_ hfint ?_
-- Lean 4 proof step from Mathlib.Probability.ConditionalExpectation (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
pos : AEStronglyMeasurable f μ
pos₁ :
  ∀ (c : E) ⦃s_1 : Set Ω⦄,
    MeasurableSet s_1 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
        HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), s_1.indicator (fun (x : Ω) ↦ c) x ∂μ) =
          ∫ (x : Ω) in s, s_1.indicator (fun (x : Ω) ↦ c) x ∂μ
pos₂ :
  ∀ ⦃f g : Ω → E⦄,
    Disjoint (Function.support f) (Function.support g) →
      MemLp f 1 μ →
        MemLp g 1 μ →
          StronglyMeasurable f →
            StronglyMeasurable g →
              HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), f x ∂μ) = ∫ (x : Ω) in s, f x ∂μ →
                HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), g x ∂μ) = ∫ (x : Ω) in s, g x ∂μ →
                  HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), (f + g) x ∂μ) = ∫ (x : Ω) in s, (f + g) x ∂μ
⊢ HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), f x ∂μ) = ∫ (x : Ω) in s, f x ∂μ
have pos₃ : IsClosed (X := ↥(lpMeas E ℝ m₁ 1 μ))
  {f : ↥(lpMeas E ℝ m₁ 1 μ) |
    HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), (↑(↑(↑f : ↥(Lp E 1 μ)) : Ω →ₘ[μ] E) : Ω → E) x ∂μ) =
      ∫ (x : Ω) in s, (↑(↑(↑f : ↥(Lp E 1 μ)) : Ω →ₘ[μ] E) : Ω → E) x ∂μ}
Tactic: refine MemLp.induction_stronglyMeasurable hle₁ ENNReal.one_ne_top _ ?_ ?_ ?_ ?_ hfint ?_
-- Lean 4 proof step from Mathlib.Probability.ConditionalExpectation (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
pos : AEStronglyMeasurable f μ
pos₁ :
  ∀ (c : E) ⦃s_1 : Set Ω⦄,
    MeasurableSet s_1 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
        HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), s_1.indicator (fun (x : Ω) ↦ c) x ∂μ) =
          ∫ (x : Ω) in s, s_1.indicator (fun (x : Ω) ↦ c) x ∂μ
pos₂ :
  ∀ ⦃f g : Ω → E⦄,
    Disjoint (Function.support f) (Function.support g) →
      MemLp f 1 μ →
        MemLp g 1 μ →
          StronglyMeasurable f →
            StronglyMeasurable g →
              HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), f x ∂μ) = ∫ (x : Ω) in s, f x ∂μ →
                HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), g x ∂μ) = ∫ (x : Ω) in s, g x ∂μ →
                  HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), (f + g) x ∂μ) = ∫ (x : Ω) in s, (f + g) x ∂μ
pos₃ :
  IsClosed (X := ↥(lpMeas E ℝ m₁ 1 μ))
    {f : ↥(lpMeas E ℝ m₁ 1 μ) |
      HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), (↑(↑(↑f : ↥(Lp E 1 μ)) : Ω →ₘ[μ] E) : Ω → E) x ∂μ) =
        ∫ (x : Ω) in s, (↑(↑(↑f : ↥(Lp E 1 μ)) : Ω →ₘ[μ] E) : Ω → E) x ∂μ}
⊢ HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), f x ∂μ) = ∫ (x : Ω) in s, f x ∂μ
have pos₄ : ∀ ⦃f g : Ω → E⦄,
  f =ᶠ[ae μ] g →
    MemLp f 1 μ →
      HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), f x ∂μ) = ∫ (x : Ω) in s, f x ∂μ →
        HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), g x ∂μ) = ∫ (x : Ω) in s, g x ∂μ
Tactic: refine MemLp.induction_stronglyMeasurable hle₁ ENNReal.one_ne_top _ ?_ ?_ ?_ ?_ hfint ?_
-- Lean 4 proof step from Mathlib.Probability.ConditionalExpectation (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
t : Set Ω
hmt : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), t.indicator (fun (x : Ω) ↦ c) x ∂μ) =
    ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
have pos : ∀
  (hindp :
    ∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          (μ : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
            HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞))
  (hfint : MemLp f 1 μ) (s : Set Ω) (hms : MeasurableSet s)
  (hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)) (c : E) ⦃t : Set Ω⦄ (hmt : MeasurableSet t),
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) →
    HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), t.indicator (fun (x : Ω) ↦ c) x ∂μ) =
      ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
Tactic: rw [Indep_iff] at hindp
Cleared hypotheses: hindp, hfint, s, hms, hs, c, t, hmt, h
-- Lean 4 proof step from Mathlib.Probability.ConditionalExpectation (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp :
  ∀ (t1 t2 : Set Ω),
    MeasurableSet t1 →
      MeasurableSet t2 →
        (μ : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
t : Set Ω
hmt : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), t.indicator (fun (x : Ω) ↦ c) x ∂μ) =
    ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
have pos : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω) in t, c ∂μ) = ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
Tactic: rw [integral_indicator (hle₁ _ hmt), setIntegral_const, smul_smul, measureReal_def,
      measureReal_def, ← ENNReal.toReal_mul,
      mul_comm, ← hindp _ _ hmt hms, setIntegral_indicator (hle₁ _ hmt), setIntegral_const,
      Set.inter_comm, measureReal_def]
-- Lean 4 proof step from Mathlib.Probability.ConditionalExpectation (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp :
  ∀ (t1 t2 : Set Ω),
    MeasurableSet t1 →
      MeasurableSet t2 →
        (μ : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
t : Set Ω
hmt : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
pos : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω) in t, c ∂μ) = ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
⊢ HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), t.indicator (fun (x : Ω) ↦ c) x ∂μ) =
    ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
have pos₁ : μ.real s • μ.real t • c = ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
Tactic: rw [integral_indicator (hle₁ _ hmt), setIntegral_const, smul_smul, measureReal_def,
      measureReal_def, ← ENNReal.toReal_mul,
      mul_comm, ← hindp _ _ hmt hms, setIntegral_indicator (hle₁ _ hmt), setIntegral_const,
      Set.inter_comm, measureReal_def]
-- Lean 4 proof step from Mathlib.Probability.ConditionalExpectation (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp :
  ∀ (t1 t2 : Set Ω),
    MeasurableSet t1 →
      MeasurableSet t2 →
        (μ : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
t : Set Ω
hmt : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
pos : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω) in t, c ∂μ) = ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
pos₁ : μ.real s • μ.real t • c = ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
⊢ HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), t.indicator (fun (x : Ω) ↦ c) x ∂μ) =
    ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
have pos₂ : (μ.real s * μ.real t) • c = ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
Tactic: rw [integral_indicator (hle₁ _ hmt), setIntegral_const, smul_smul, measureReal_def,
      measureReal_def, ← ENNReal.toReal_mul,
      mul_comm, ← hindp _ _ hmt hms, setIntegral_indicator (hle₁ _ hmt), setIntegral_const,
      Set.inter_comm, measureReal_def]
-- Lean 4 proof step from Mathlib.Probability.ConditionalExpectation (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp :
  ∀ (t1 t2 : Set Ω),
    MeasurableSet t1 →
      MeasurableSet t2 →
        (μ : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
t : Set Ω
hmt : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
pos : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω) in t, c ∂μ) = ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
pos₁ : μ.real s • μ.real t • c = ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
pos₂ : (μ.real s * μ.real t) • c = ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
⊢ HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), t.indicator (fun (x : Ω) ↦ c) x ∂μ) =
    ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
have pos₃ : (ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) s) * μ.real t) • c = ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
Tactic: rw [integral_indicator (hle₁ _ hmt), setIntegral_const, smul_smul, measureReal_def,
      measureReal_def, ← ENNReal.toReal_mul,
      mul_comm, ← hindp _ _ hmt hms, setIntegral_indicator (hle₁ _ hmt), setIntegral_const,
      Set.inter_comm, measureReal_def]
-- Lean 4 proof step from Mathlib.Probability.ConditionalExpectation (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp :
  ∀ (t1 t2 : Set Ω),
    MeasurableSet t1 →
      MeasurableSet t2 →
        (μ : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
t : Set Ω
hmt : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
pos : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω) in t, c ∂μ) = ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
pos₁ : μ.real s • μ.real t • c = ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
pos₂ : (μ.real s * μ.real t) • c = ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
pos₃ : (ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) s) * μ.real t) • c = ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
⊢ HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), t.indicator (fun (x : Ω) ↦ c) x ∂μ) =
    ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
have pos₄ : (ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) s) * ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) t)) • c =
  ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
Tactic: rw [integral_indicator (hle₁ _ hmt), setIntegral_const, smul_smul, measureReal_def,
      measureReal_def, ← ENNReal.toReal_mul,
      mul_comm, ← hindp _ _ hmt hms, setIntegral_indicator (hle₁ _ hmt), setIntegral_const,
      Set.inter_comm, measureReal_def]
-- Lean 4 proof step from Mathlib.Probability.ConditionalExpectation (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp :
  ∀ (t1 t2 : Set Ω),
    MeasurableSet t1 →
      MeasurableSet t2 →
        (μ : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
t : Set Ω
hmt : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
pos : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω) in t, c ∂μ) = ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
pos₁ : μ.real s • μ.real t • c = ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
pos₂ : (μ.real s * μ.real t) • c = ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
pos₃ : (ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) s) * μ.real t) • c = ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
pos₄ :
  (ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) s) * ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) t)) • c =
    ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
⊢ HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), t.indicator (fun (x : Ω) ↦ c) x ∂μ) =
    ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
have pos₅ : (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)).toReal • c =
  ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
Tactic: rw [integral_indicator (hle₁ _ hmt), setIntegral_const, smul_smul, measureReal_def,
      measureReal_def, ← ENNReal.toReal_mul,
      mul_comm, ← hindp _ _ hmt hms, setIntegral_indicator (hle₁ _ hmt), setIntegral_const,
      Set.inter_comm, measureReal_def]
-- Lean 4 proof step from Mathlib.Probability.ConditionalExpectation (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp :
  ∀ (t1 t2 : Set Ω),
    MeasurableSet t1 →
      MeasurableSet t2 →
        (μ : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
t : Set Ω
hmt : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
pos : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω) in t, c ∂μ) = ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
pos₁ : μ.real s • μ.real t • c = ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
pos₂ : (μ.real s * μ.real t) • c = ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
pos₃ : (ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) s) * μ.real t) • c = ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
pos₄ :
  (ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) s) * ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) t)) • c =
    ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
pos₅ :
  (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)).toReal •
      c =
    ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
⊢ HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), t.indicator (fun (x : Ω) ↦ c) x ∂μ) =
    ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
have pos₆ : (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)).toReal • c =
  ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
Tactic: rw [integral_indicator (hle₁ _ hmt), setIntegral_const, smul_smul, measureReal_def,
      measureReal_def, ← ENNReal.toReal_mul,
      mul_comm, ← hindp _ _ hmt hms, setIntegral_indicator (hle₁ _ hmt), setIntegral_const,
      Set.inter_comm, measureReal_def]
-- Lean 4 proof step from Mathlib.Probability.ConditionalExpectation (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp :
  ∀ (t1 t2 : Set Ω),
    MeasurableSet t1 →
      MeasurableSet t2 →
        (μ : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
t : Set Ω
hmt : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
pos : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω) in t, c ∂μ) = ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
pos₁ : μ.real s • μ.real t • c = ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
pos₂ : (μ.real s * μ.real t) • c = ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
pos₃ : (ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) s) * μ.real t) • c = ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
pos₄ :
  (ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) s) * ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) t)) • c =
    ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
pos₅ :
  (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)).toReal •
      c =
    ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
pos₆ :
  (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)).toReal •
      c =
    ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
⊢ HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), t.indicator (fun (x : Ω) ↦ c) x ∂μ) =
    ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
have pos₇ : ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) (t ∩ s)) • c = ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
Tactic: rw [integral_indicator (hle₁ _ hmt), setIntegral_const, smul_smul, measureReal_def,
      measureReal_def, ← ENNReal.toReal_mul,
      mul_comm, ← hindp _ _ hmt hms, setIntegral_indicator (hle₁ _ hmt), setIntegral_const,
      Set.inter_comm, measureReal_def]
-- Lean 4 proof step from Mathlib.Probability.ConditionalExpectation (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp :
  ∀ (t1 t2 : Set Ω),
    MeasurableSet t1 →
      MeasurableSet t2 →
        (μ : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
t : Set Ω
hmt : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
pos : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω) in t, c ∂μ) = ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
pos₁ : μ.real s • μ.real t • c = ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
pos₂ : (μ.real s * μ.real t) • c = ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
pos₃ : (ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) s) * μ.real t) • c = ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
pos₄ :
  (ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) s) * ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) t)) • c =
    ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
pos₅ :
  (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)).toReal •
      c =
    ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
pos₆ :
  (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)).toReal •
      c =
    ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
pos₇ : ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) (t ∩ s)) • c = ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
⊢ HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), t.indicator (fun (x : Ω) ↦ c) x ∂μ) =
    ∫ (x : Ω) in s, t.indicator (fun (x : Ω) ↦ c) x ∂μ
have pos₈ : ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) (t ∩ s)) • c = ∫ (x : Ω) in s ∩ t, c ∂μ
Tactic: rw [integral_indicator (hle₁ _ hmt), setIntegral_const, smul_smul, measureReal_def,
      measureReal_def, ← ENNReal.toReal_mul,
      mul_comm, ← hindp _ _ hmt hms, setIntegral_indicator (hle₁ _ hmt), setIntegral_const,
      Set.inter_comm, measureReal_def]