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 :
  ∀ (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 ∂μ
pos₈ : ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) (t ∩ s)) • c = ∫ (x : Ω) in s ∩ t, c ∂μ
⊢ 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 = μ.real (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]
-- 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 ∂μ
pos₈ : ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) (t ∩ s)) • c = ∫ (x : Ω) in s ∩ t, c ∂μ
pos₉ : ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) (t ∩ s)) • c = μ.real (s ∩ t) • c
⊢ 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 ∩ t)) • c = μ.real (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]
-- 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 ∂μ
pos₈ : ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) (t ∩ s)) • c = ∫ (x : Ω) in s ∩ t, c ∂μ
pos₉ : ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) (t ∩ s)) • c = μ.real (s ∩ t) • c
pos₁₀ : ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t)) • c = μ.real (s ∩ t) • c
⊢ 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 ∩ t)) • c = ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) (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]
-- Lean 4 proof step from Mathlib.Probability.ConditionalExpectation (hypothesis)
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∞)
u v : Ω → E
h : Disjoint (Function.support u) (Function.support v)
huint : MemLp u 1 μ
hvint : MemLp v 1 μ
hu : StronglyMeasurable u
hv : StronglyMeasurable v
hu_eq : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), u x ∂μ) = ∫ (x : Ω) in s, u x ∂μ
hv_eq : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), v x ∂μ) = ∫ (x : Ω) in s, v x ∂μ
⊢ HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), (u + v) x ∂μ) = ∫ (x : Ω) in s, (u + v) x ∂μ
have huint₁ : Integrable u μ
Tactic: rw [memLp_one_iff_integrable] at huint hvint
Cleared hypotheses: huint, hvint, hu, hv, hu_eq, hv_eq
-- Lean 4 proof step from Mathlib.Probability.ConditionalExpectation (hypothesis)
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∞)
u v : Ω → E
h : Disjoint (Function.support u) (Function.support v)
huint : MemLp u 1 μ
hvint : MemLp v 1 μ
hu : StronglyMeasurable u
hv : StronglyMeasurable v
hu_eq : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), u x ∂μ) = ∫ (x : Ω) in s, u x ∂μ
hv_eq : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), v x ∂μ) = ∫ (x : Ω) in s, v x ∂μ
huint₁ : Integrable u μ
⊢ HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), (u + v) x ∂μ) = ∫ (x : Ω) in s, (u + v) x ∂μ
have hvint₁ : Integrable v μ
Tactic: rw [memLp_one_iff_integrable] at huint hvint
Cleared hypotheses: huint, hvint, hu, hv, hu_eq, hv_eq
-- 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∞)
u v : Ω → E
h : Disjoint (Function.support u) (Function.support v)
huint : Integrable u μ
hvint : Integrable v μ
hu : StronglyMeasurable u
hv : StronglyMeasurable v
hu_eq : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), u x ∂μ) = ∫ (x : Ω) in s, u x ∂μ
hv_eq : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), v x ∂μ) = ∫ (x : Ω) in s, v x ∂μ
⊢ HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), (u + v) x ∂μ) = ∫ (x : Ω) in s, (u + v) x ∂μ
have pos : μ.real s • HAdd.hAdd (α := E) (∫ (a : Ω), u a ∂μ) (∫ (a : Ω), v a ∂μ) = ∫ (x : Ω) in s, (u + v) x ∂μ
Tactic: rw [integral_add' huint hvint, smul_add, hu_eq, hv_eq,
      integral_add' huint.integrableOn hvint.integrableOn]
-- 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∞)
u v : Ω → E
h : Disjoint (Function.support u) (Function.support v)
huint : Integrable u μ
hvint : Integrable v μ
hu : StronglyMeasurable u
hv : StronglyMeasurable v
hu_eq : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), u x ∂μ) = ∫ (x : Ω) in s, u x ∂μ
hv_eq : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), v x ∂μ) = ∫ (x : Ω) in s, v x ∂μ
pos : μ.real s • HAdd.hAdd (α := E) (∫ (a : Ω), u a ∂μ) (∫ (a : Ω), v a ∂μ) = ∫ (x : Ω) in s, (u + v) x ∂μ
⊢ HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), (u + v) x ∂μ) = ∫ (x : Ω) in s, (u + v) x ∂μ
have pos₁ : HSMul.hSMul (β := E) (μ.real s) (∫ (a : Ω), u a ∂μ) + HSMul.hSMul (β := E) (μ.real s) (∫ (a : Ω), v a ∂μ) =
  ∫ (x : Ω) in s, (u + v) x ∂μ
Tactic: rw [integral_add' huint hvint, smul_add, hu_eq, hv_eq,
      integral_add' huint.integrableOn hvint.integrableOn]
-- 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∞)
u v : Ω → E
h : Disjoint (Function.support u) (Function.support v)
huint : Integrable u μ
hvint : Integrable v μ
hu : StronglyMeasurable u
hv : StronglyMeasurable v
hu_eq : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), u x ∂μ) = ∫ (x : Ω) in s, u x ∂μ
hv_eq : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), v x ∂μ) = ∫ (x : Ω) in s, v x ∂μ
pos : μ.real s • HAdd.hAdd (α := E) (∫ (a : Ω), u a ∂μ) (∫ (a : Ω), v a ∂μ) = ∫ (x : Ω) in s, (u + v) x ∂μ
pos₁ :
  HSMul.hSMul (β := E) (μ.real s) (∫ (a : Ω), u a ∂μ) + HSMul.hSMul (β := E) (μ.real s) (∫ (a : Ω), v a ∂μ) =
    ∫ (x : Ω) in s, (u + v) x ∂μ
⊢ HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), (u + v) x ∂μ) = ∫ (x : Ω) in s, (u + v) x ∂μ
have pos₂ : ∫ (x : Ω) in s, u x ∂μ + HSMul.hSMul (β := E) (μ.real s) (∫ (a : Ω), v a ∂μ) = ∫ (x : Ω) in s, (u + v) x ∂μ
Tactic: rw [integral_add' huint hvint, smul_add, hu_eq, hv_eq,
      integral_add' huint.integrableOn hvint.integrableOn]
-- 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∞)
u v : Ω → E
h : Disjoint (Function.support u) (Function.support v)
huint : Integrable u μ
hvint : Integrable v μ
hu : StronglyMeasurable u
hv : StronglyMeasurable v
hu_eq : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), u x ∂μ) = ∫ (x : Ω) in s, u x ∂μ
hv_eq : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), v x ∂μ) = ∫ (x : Ω) in s, v x ∂μ
pos : μ.real s • HAdd.hAdd (α := E) (∫ (a : Ω), u a ∂μ) (∫ (a : Ω), v a ∂μ) = ∫ (x : Ω) in s, (u + v) x ∂μ
pos₁ :
  HSMul.hSMul (β := E) (μ.real s) (∫ (a : Ω), u a ∂μ) + HSMul.hSMul (β := E) (μ.real s) (∫ (a : Ω), v a ∂μ) =
    ∫ (x : Ω) in s, (u + v) x ∂μ
pos₂ : ∫ (x : Ω) in s, u x ∂μ + HSMul.hSMul (β := E) (μ.real s) (∫ (a : Ω), v a ∂μ) = ∫ (x : Ω) in s, (u + v) x ∂μ
⊢ HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), (u + v) x ∂μ) = ∫ (x : Ω) in s, (u + v) x ∂μ
have pos₃ : HAdd.hAdd (α := E) (∫ (x : Ω) in s, u x ∂μ) (∫ (x : Ω) in s, v x ∂μ) = ∫ (x : Ω) in s, (u + v) x ∂μ
Tactic: rw [integral_add' huint hvint, smul_add, hu_eq, hv_eq,
      integral_add' huint.integrableOn hvint.integrableOn]
-- 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∞)
u v : Ω → E
h : Disjoint (Function.support u) (Function.support v)
huint : Integrable u μ
hvint : Integrable v μ
hu : StronglyMeasurable u
hv : StronglyMeasurable v
hu_eq : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), u x ∂μ) = ∫ (x : Ω) in s, u x ∂μ
hv_eq : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), v x ∂μ) = ∫ (x : Ω) in s, v x ∂μ
pos : μ.real s • HAdd.hAdd (α := E) (∫ (a : Ω), u a ∂μ) (∫ (a : Ω), v a ∂μ) = ∫ (x : Ω) in s, (u + v) x ∂μ
pos₁ :
  HSMul.hSMul (β := E) (μ.real s) (∫ (a : Ω), u a ∂μ) + HSMul.hSMul (β := E) (μ.real s) (∫ (a : Ω), v a ∂μ) =
    ∫ (x : Ω) in s, (u + v) x ∂μ
pos₂ : ∫ (x : Ω) in s, u x ∂μ + HSMul.hSMul (β := E) (μ.real s) (∫ (a : Ω), v a ∂μ) = ∫ (x : Ω) in s, (u + v) x ∂μ
pos₃ : HAdd.hAdd (α := E) (∫ (x : Ω) in s, u x ∂μ) (∫ (x : Ω) in s, v x ∂μ) = ∫ (x : Ω) in s, (u + v) x ∂μ
⊢ HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), (u + v) x ∂μ) = ∫ (x : Ω) in s, (u + v) x ∂μ
have pos₄ : HAdd.hAdd (α := E) (∫ (x : Ω) in s, u x ∂μ) (∫ (x : Ω) in s, v x ∂μ) =
  HAdd.hAdd (α := E) (∫ (a : Ω) in s, u a ∂μ) (∫ (a : Ω) in s, v a ∂μ)
Tactic: rw [integral_add' huint hvint, smul_add, hu_eq, hv_eq,
      integral_add' huint.integrableOn hvint.integrableOn]
-- Lean 4 proof step from Mathlib.Probability.ConditionalExpectation (hypothesis)
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∞)
⊢ 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 ∂μ}
have h_integral : Continuous (Y := E) fun (f : ↥(lpMeas E ℝ m₁ 1 μ)) ↦ ∫ (x : Ω), (↑(↑(↑f : ↥(Lp E 1 μ)) : Ω →ₘ[μ] E) : Ω → E) x ∂μ
Tactic: have h_integral : Continuous fun f : lpMeas E ℝ m₁ 1 μ => ∫ x, (f : Ω → E) x ∂μ := by
      simpa using continuous_integral.comp (ContinuousLinearMap.continuous (Submodule.subtypeL _))
-- Lean 4 proof step from Mathlib.Probability.ConditionalExpectation (hypothesis)
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∞)
h_integral :
  Continuous (Y := E) fun (f : ↥(lpMeas E ℝ m₁ 1 μ)) ↦ ∫ (x : Ω), (↑(↑(↑f : ↥(Lp E 1 μ)) : Ω →ₘ[μ] E) : Ω → E) x ∂μ
⊢ 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 ∂μ}
have h_setIntegral : Continuous (Y := E) fun (f : ↥(lpMeas E ℝ m₁ 1 μ)) ↦ ∫ (x : Ω) in s, (↑(↑(↑f : ↥(Lp E 1 μ)) : Ω →ₘ[μ] E) : Ω → E) x ∂μ
Tactic: have h_setIntegral : Continuous fun f : lpMeas E ℝ m₁ 1 μ => ∫ x in s, (f : Ω → E) x ∂μ := by
      simpa using (continuous_setIntegral s).comp
        (ContinuousLinearMap.continuous (Submodule.subtypeL _))
-- 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∞)
u v : Ω → E
huv : u =ᶠ[ae μ] v
h : MemLp u 1 μ
hueq : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), u x ∂μ) = ∫ (x : Ω) in s, u x ∂μ
⊢ HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), v x ∂μ) = ∫ (x : Ω) in s, v x ∂μ
have rwa : ∀ᵐ (x : Ω) ∂μ, x ∈ s → u x = v x
Tactic: rwa [← integral_congr_ae huv, ←
      (setIntegral_congr_ae (hle₂ _ hms) _ : ∫ x in s, u x ∂μ = ∫ x in s, v x ∂μ)]
-- 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∞)
u v : Ω → E
huv : u =ᶠ[ae μ] v
h : MemLp u 1 μ
hueq : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), u x ∂μ) = ∫ (x : Ω) in s, u x ∂μ
⊢ ∀ᵐ (x : Ω) ∂μ, x ∈ s → u x = v x
have h : ∀ (a : Ω),
  Membership.mem (γ := Set Ω)
    {x : Ω |
      Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ u x = v x) x} x →
        Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ x ∈ s → u x = v x) x} x}
    a
Tactic: filter_upwards [huv] with x hx _ using hx
-- 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∞)
u v : Ω → E
huv : u =ᶠ[ae μ] v
h_1 : MemLp u 1 μ
hueq : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), u x ∂μ) = ∫ (x : Ω) in s, u x ∂μ
h :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ u x = v x) x} x →
          Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ x ∈ s → u x = v x) x} x}
      a
⊢ ∀ᵐ (x : Ω) ∂μ, x ∈ s → u x = v x
have h₁ : ∀ (a : Ω), u a = v a → a ∈ s → u a = v a
Tactic: filter_upwards [huv] with x hx _ using hx
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hcs : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
    (1 : ℝ≥0∞)
have simp : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 1
Tactic: simp only [Measure.coe_smul, Pi.smul_apply, MeasurableSet.univ, Measure.restrict_apply,
      Set.univ_inter, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
α : Type u_3
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s t : Set Ω
⊢ IsZeroOrProbabilityMeasure μ[|s]
have measure_univ : Eq (α := ℝ≥0∞) (μ[univ | s] : ℝ≥0∞) (0 : ℝ≥0∞) ∨ Eq (α := ℝ≥0∞) (μ[univ | s] : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
α : Type u_3
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s t : Set Ω
⊢ Eq (α := ℝ≥0∞) (μ[univ | s] : ℝ≥0∞) (0 : ℝ≥0∞) ∨ Eq (α := ℝ≥0∞) (μ[univ | s] : ℝ≥0∞) (1 : ℝ≥0∞)
have measure_univ : HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 0 ∨
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 1
Tactic: simp only [cond, Measure.coe_smul, Pi.smul_apply, MeasurableSet.univ, Measure.restrict_apply,
    univ_inter, smul_eq_mul, ← ENNReal.div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Probability.ConditionalProbability (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
α : Type u_3
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s t : Set Ω
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 0 ∨
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 1
have measure_univ : ∀ (h : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 0 ∨
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 1
Tactic: rcases eq_or_ne (μ s) 0 with h | h